:: PRVECT_1 semantic presentation

deffunc H₁( 1-sorted ) -> set = the carrier of $1;

deffunc H₂( LoopStr ) -> M6([:the carrier of $1,the carrier of $1:],the carrier of $1) = the add of $1;

deffunc H₃( non empty LoopStr ) -> M6(the carrier of $1,the carrier of $1) = comp $1;

deffunc H₄( LoopStr ) -> Element of the carrier of $1 = the Zero of $1;

theorem :: PRVECT_1:1

canceled;

theorem :: PRVECT_1:2

canceled;

theorem Th3: :: PRVECT_1:3

for G being non empty Abelian add-associative right_zeroed right_complementable LoopStr holds the Zero of G is_a_unity_wrt the add of G

proof end;

theorem Th4: :: PRVECT_1:4

for G being AbGroup holds comp G is_an_inverseOp_wrt the add of G

proof end;

Lm1: for G being non empty Abelian add-associative right_zeroed right_complementable LoopStr holds comp G is_an_inverseOp_wrt the add of G

proof end;

theorem :: PRVECT_1:5

for GS being non empty LoopStr st the add of GS is commutative & the add of GS is associative & the Zero of GS is_a_unity_wrt the add of GS & comp GS is_an_inverseOp_wrt the add of GS holds
GS is AbGroup

proof end;

Lm2: for GS being non empty LoopStr st the add of GS is commutative & the add of GS is associative holds
( GS is Abelian & GS is add-associative )

proof end;

Lm3: for GS being non empty LoopStr st the Zero of GS is_a_unity_wrt the add of GS holds
GS is right_zeroed

proof end;

Lm4: for F being Field holds the mult of F is associative

proof end;

theorem :: PRVECT_1:6

canceled;

theorem :: PRVECT_1:7

canceled;

theorem :: PRVECT_1:8

canceled;

theorem :: PRVECT_1:9

canceled;

theorem :: PRVECT_1:10

for F being Field holds the Zero of F is_a_unity_wrt the add of F

proof end;

theorem Th11: :: PRVECT_1:11

for F being Field holds 1. F is_a_unity_wrt the mult of F

proof end;

Lm5: for F being Field holds the mult of F is_distributive_wrt the add of F

proof end;

definition

let D be non empty set ;
let n be Nat;
let F be BinOp of D;
let x, y be Element of n -tuples_on D;
:: original: .:
redefine func F .: x,y -> Element of n -tuples_on D;
coherence by FINSEQ_2:140;

end;

definition

let D be non empty set ;
let F be BinOp of D;
let n be Nat;
func product F,n -> BinOp of n -tuples_on D means :Def1: :: PRVECT_1:def 1
for x, y being Element of n -tuples_on D holds it . x,y = F .: x,y;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines product PRVECT_1:def 1 :

definition

let D be non empty set ;
let F be UnOp of D;
let n be Nat;
func product F,n -> UnOp of n -tuples_on D means :Def2: :: PRVECT_1:def 2
for x being Element of n -tuples_on D holds it . x = F * x;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines product PRVECT_1:def 2 :

notation

let D be non empty set ;
let n be Nat;
let x be Element of D;
synonym n .--> x for D |-> n;

end;

definition

let D be non empty set ;
let n be Nat;
let x be Element of D;
:: original: .-->
redefine func n .--> x -> Element of n -tuples_on D;
correctness by FINSEQ_2:132;

end;

theorem :: PRVECT_1:12

canceled;

theorem :: PRVECT_1:13

canceled;

theorem Th14: :: PRVECT_1:14

for n being Nat
for D being non empty set
for B being BinOp of D st B is commutative holds
product B,n is commutative

proof end;

theorem Th15: :: PRVECT_1:15

for n being Nat
for D being non empty set
for B being BinOp of D st B is associative holds
product B,n is associative

proof end;

theorem Th16: :: PRVECT_1:16

for n being Nat
for D being non empty set
for d being Element of D
for B being BinOp of D st d is_a_unity_wrt B holds
n .--> d is_a_unity_wrt product B,n

proof end;

theorem Th17: :: PRVECT_1:17

for n being Nat
for D being non empty set
for B being BinOp of D
for C being UnOp of D st B has_a_unity & B is associative & C is_an_inverseOp_wrt B holds
product C,n is_an_inverseOp_wrt product B,n

proof end;

definition

let F be non empty LoopStr ;
let n be Nat;
assume A1: ( F is Abelian & F is add-associative & F is right_zeroed & F is right_complementable ) ;
func n -Group_over F -> strict AbGroup equals :Def3: :: PRVECT_1:def 3
LoopStr(# (n -tuples_on the carrier of F),(product the add of F,n),(n .--> the Zero of F) #);
coherence

proof end;

end;

:: deftheorem Def3 defines -Group_over PRVECT_1:def 3 :

registration

let F be AbGroup;
let n be Nat;
cluster n -Group_over F -> strict ;
coherence ;

end;

definition

let F be Field;
let n be Nat;
func n -Mult_over F -> Function of [:the carrier of F,(n -tuples_on the carrier of F):],n -tuples_on the carrier of F means :Def4: :: PRVECT_1:def 4
for x being Element of F
for v being Element of n -tuples_on the carrier of F holds it . x,v = the mult of F [;] x,v;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines -Mult_over PRVECT_1:def 4 :

definition

let F be Field;
let n be Nat;
func n -VectSp_over F -> strict VectSpStr of F means :Def5: :: PRVECT_1:def 5
( LoopStr(# the carrier of it,the add of it,the Zero of it #) = n -Group_over F & the lmult of it = n -Mult_over F );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def5 defines -VectSp_over PRVECT_1:def 5 :

registration

let F be Field;
let n be Nat;
cluster n -VectSp_over F -> non empty strict ;
coherence

proof end;

end;

theorem Th18: :: PRVECT_1:18

for n being Nat
for D being non empty set
for H, G being BinOp of D
for d being Element of D
for t1, t2 being Element of n -tuples_on D st H is_distributive_wrt G holds
H [;] d,(G .: t1,t2) = G .: (H [;] d,t1),(H [;] d,t2)

proof end;

definition

let D be non empty set ;
let n be Nat;
let F be BinOp of D;
let x be Element of D;
let v be Element of n -tuples_on D;
:: original: [;]
redefine func F [;] x,v -> Element of n -tuples_on D;
coherence by FINSEQ_2:141;

end;

registration

let F be Field;
let n be Nat;
cluster n -VectSp_over F -> non empty strict VectSp-like ;
coherence

proof end;

end;

registration

cluster non-empty non empty set ;
existence

proof end;

end;

definition

mode Domain-Sequence is non-empty non empty FinSequence;

end;

registration

let a be non empty Function;
cluster dom a -> non empty ;
coherence

proof end;

end;

scheme :: PRVECT_1:sch 1
NEFinSeqLambda{ F₁() -> non empty FinSequence, F₂( set ) -> set } :

ex p being non empty FinSequence st
( len p = len F₁() & ( for i being Element of dom F₁() holds p . i = F₂(i) ) )

proof end;

registration

let a be non-empty non empty Function;
let i be Element of dom a;
cluster a . i -> non empty ;
coherence

proof end;

end;

definition

let a be non-empty non empty Function;
let f be Element of product a;
let i be Element of dom a;
:: original: .
redefine func f . i -> Element of a . i;
coherence by CARD_3:18;

end;

definition

let a be non-empty non empty Function;
canceled;
canceled;
mode BinOps of a -> Function means :Def8: :: PRVECT_1:def 8
( dom it = dom a & ( for i being Element of dom a holds it . i is BinOp of a . i ) );
existence

proof end;

mode UnOps of a -> Function means :Def9: :: PRVECT_1:def 9
( dom it = dom a & ( for i being Element of dom a holds it . i is UnOp of a . i ) );
existence

proof end;

end;

:: deftheorem PRVECT_1:def 6 :

:: deftheorem PRVECT_1:def 7 :

:: deftheorem Def8 defines BinOps PRVECT_1:def 8 :

:: deftheorem Def9 defines UnOps PRVECT_1:def 9 :

registration

let a be Domain-Sequence;
cluster -> FinSequence-like BinOps of a;
coherence

proof end;

cluster -> FinSequence-like UnOps of a;
coherence

proof end;

end;

theorem Th19: :: PRVECT_1:19

for a being Domain-Sequence
for p being FinSequence holds
( p is BinOps of a iff ( len p = len a & ( for i being Element of dom a holds p . i is BinOp of a . i ) ) )

proof end;

theorem Th20: :: PRVECT_1:20

for a being Domain-Sequence
for p being FinSequence holds
( p is UnOps of a iff ( len p = len a & ( for i being Element of dom a holds p . i is UnOp of a . i ) ) )

proof end;

definition

let a be Domain-Sequence;
let b be BinOps of a;
let i be Element of dom a;
:: original: .
redefine func b . i -> BinOp of a . i;
coherence by Th19;

end;

definition

let a be Domain-Sequence;
let u be UnOps of a;
let i be Element of dom a;
:: original: .
redefine func u . i -> UnOp of a . i;
coherence by Th20;

end;

definition

let F be non empty functional set ;
let u be UnOp of F;
let f be Element of F;
:: original: .
redefine func u . f -> Element of F;
coherence

proof end;

end;

theorem :: PRVECT_1:21

for a being Domain-Sequence
for d, d' being UnOp of product a st ( for f being Element of product a
for i being Element of dom a holds (d . f) . i = (d' . f) . i ) holds
d = d'

proof end;

theorem Th22: :: PRVECT_1:22

for a being Domain-Sequence
for u being UnOps of a holds
( doms u = a & product (rngs u) c= product a )

proof end;

definition

let a be Domain-Sequence;
let u be UnOps of a;
:: original: Frege
redefine func Frege u -> UnOp of product a;
coherence

proof end;

end;

theorem Th23: :: PRVECT_1:23

for a being Domain-Sequence
for u being UnOps of a
for f being Element of product a
for i being Element of dom a holds ((Frege u) . f) . i = (u . i) . (f . i)

proof end;

definition

let F be non empty functional set ;
let b be BinOp of F;
let f, g be Element of F;
:: original: .
redefine func b . f,g -> Element of F;
coherence

proof end;

end;

theorem Th24: :: PRVECT_1:24

for a being Domain-Sequence
for d, d' being BinOp of product a st ( for f, g being Element of product a
for i being Element of dom a holds (d . f,g) . i = (d' . f,g) . i ) holds
d = d'

proof end;

definition

let a be Domain-Sequence;
let b be BinOps of a;
func [:b:] -> BinOp of product a means :Def10: :: PRVECT_1:def 10
for f, g being Element of product a
for i being Element of dom a holds (it . f,g) . i = (b . i) . (f . i),(g . i);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines [: PRVECT_1:def 10 :

theorem Th25: :: PRVECT_1:25

for a being Domain-Sequence
for b being BinOps of a st ( for i being Element of dom a holds b . i is commutative ) holds
[:b:] is commutative

proof end;

theorem Th26: :: PRVECT_1:26

for a being Domain-Sequence
for b being BinOps of a st ( for i being Element of dom a holds b . i is associative ) holds
[:b:] is associative

proof end;

theorem Th27: :: PRVECT_1:27

for a being Domain-Sequence
for b being BinOps of a
for f being Element of product a st ( for i being Element of dom a holds f . i is_a_unity_wrt b . i ) holds
f is_a_unity_wrt [:b:]

proof end;

theorem Th28: :: PRVECT_1:28

for a being Domain-Sequence
for b being BinOps of a
for u being UnOps of a st ( for i being Element of dom a holds
( u . i is_an_inverseOp_wrt b . i & b . i has_a_unity ) ) holds
Frege u is_an_inverseOp_wrt [:b:]

proof end;

definition

let F be Relation;
attr F is AbGroup-yielding means :Def11: :: PRVECT_1:def 11
for x being set st x in rng F holds
x is AbGroup;

end;

:: deftheorem Def11 defines AbGroup-yielding PRVECT_1:def 11 :

registration

cluster non empty AbGroup-yielding set ;
existence

proof end;

end;

definition

mode Group-Sequence is non empty AbGroup-yielding FinSequence;

end;

definition

let g be Group-Sequence;
let i be Element of dom g;
:: original: .
redefine func g . i -> AbGroup;
coherence

proof end;

end;

definition

let g be Group-Sequence;
func carr g -> Domain-Sequence means :Def12: :: PRVECT_1:def 12
( len it = len g & ( for j being Element of dom g holds it . j = the carrier of (g . j) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines carr PRVECT_1:def 12 :

definition

let g be Group-Sequence;
let i be Element of dom (carr g);
:: original: .
redefine func g . i -> AbGroup;
coherence

proof end;

end;

definition

let g be Group-Sequence;
func addop g -> BinOps of carr g means :Def13: :: PRVECT_1:def 13
( len it = len (carr g) & ( for i being Element of dom (carr g) holds it . i = the add of (g . i) ) );
existence

proof end;

uniqueness

proof end;

func complop g -> UnOps of carr g means :Def14: :: PRVECT_1:def 14
( len it = len (carr g) & ( for i being Element of dom (carr g) holds it . i = comp (g . i) ) );
existence

proof end;

uniqueness

proof end;

func zeros g -> Element of product (carr g) means :Def15: :: PRVECT_1:def 15
for i being Element of dom (carr g) holds it . i = the Zero of (g . i);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines addop PRVECT_1:def 13 :

:: deftheorem Def14 defines complop PRVECT_1:def 14 :

:: deftheorem Def15 defines zeros PRVECT_1:def 15 :

definition

let G be Group-Sequence;
func product G -> strict AbGroup equals :: PRVECT_1:def 16
LoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);
coherence

proof end;

end;

:: deftheorem defines product PRVECT_1:def 16 :