:: PRVECT_1 semantic presentation
begin
deffunc H1( 1-sorted ) -> set = the carrier of $1;
deffunc H2( addLoopStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the addF of $1;
deffunc H3( non empty addLoopStr ) -> Element of bool [: the carrier of $1, the carrier of $1:] = comp $1;
deffunc H4( addLoopStr ) -> Element of the carrier of $1 = 0. $1;
theorem Th1: :: PRVECT_1:1
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds 0. G is_a_unity_wrt the addF of G
proof
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: 0. G is_a_unity_wrt the addF of G
now__::_thesis:_for_x_being_Element_of_G_holds_
(_the_addF_of_G_._((0._G),x)_=_x_&_the_addF_of_G_._(x,(0._G))_=_x_)
let x be Element of G; ::_thesis: ( the addF of G . ((0. G),x) = x & the addF of G . (x,(0. G)) = x )
thus the addF of G . ((0. G),x) = (0. G) + x
.= x by RLVECT_1:4 ; ::_thesis: the addF of G . (x,(0. G)) = x
thus the addF of G . (x,(0. G)) = x + (0. G)
.= x by RLVECT_1:4 ; ::_thesis: verum
end;
hence 0. G is_a_unity_wrt the addF of G by BINOP_1:3; ::_thesis: verum
end;
theorem Th2: :: PRVECT_1:2
for G being AbGroup holds comp G is_an_inverseOp_wrt the addF of G
proof
let G be AbGroup; ::_thesis: comp G is_an_inverseOp_wrt the addF of G
A1: 0. G is_a_unity_wrt the addF of G by Th1;
now__::_thesis:_for_x_being_Element_of_G_holds_
(_the_addF_of_G_._(x,((comp_G)_._x))_=_the_unity_wrt_the_addF_of_G_&_the_addF_of_G_._(((comp_G)_._x),x)_=_the_unity_wrt_the_addF_of_G_)
let x be Element of G; ::_thesis: ( the addF of G . (x,((comp G) . x)) = the_unity_wrt the addF of G & the addF of G . (((comp G) . x),x) = the_unity_wrt the addF of G )
thus the addF of G . (x,((comp G) . x)) = x + (- x) by VECTSP_1:def_13
.= 0. G by RLVECT_1:5
.= the_unity_wrt the addF of G by A1, BINOP_1:def_8 ; ::_thesis: the addF of G . (((comp G) . x),x) = the_unity_wrt the addF of G
thus the addF of G . (((comp G) . x),x) = ((comp G) . x) + x
.= x + (- x) by VECTSP_1:def_13
.= 0. G by RLVECT_1:5
.= the_unity_wrt the addF of G by A1, BINOP_1:def_8 ; ::_thesis: verum
end;
hence comp G is_an_inverseOp_wrt the addF of G by FINSEQOP:def_1; ::_thesis: verum
end;
Lm1: for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds comp G is_an_inverseOp_wrt the addF of G
proof
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: comp G is_an_inverseOp_wrt the addF of G
A1: 0. G is_a_unity_wrt the addF of G by Th1;
now__::_thesis:_for_x_being_Element_of_G_holds_
(_the_addF_of_G_._(x,((comp_G)_._x))_=_the_unity_wrt_the_addF_of_G_&_the_addF_of_G_._(((comp_G)_._x),x)_=_the_unity_wrt_the_addF_of_G_)
let x be Element of G; ::_thesis: ( the addF of G . (x,((comp G) . x)) = the_unity_wrt the addF of G & the addF of G . (((comp G) . x),x) = the_unity_wrt the addF of G )
thus the addF of G . (x,((comp G) . x)) = x + (- x) by VECTSP_1:def_13
.= 0. G by RLVECT_1:5
.= the_unity_wrt the addF of G by A1, BINOP_1:def_8 ; ::_thesis: the addF of G . (((comp G) . x),x) = the_unity_wrt the addF of G
thus the addF of G . (((comp G) . x),x) = ((comp G) . x) + x
.= x + (- x) by VECTSP_1:def_13
.= 0. G by RLVECT_1:5
.= the_unity_wrt the addF of G by A1, BINOP_1:def_8 ; ::_thesis: verum
end;
hence comp G is_an_inverseOp_wrt the addF of G by FINSEQOP:def_1; ::_thesis: verum
end;
theorem :: PRVECT_1:3
for GS being non empty addLoopStr st the addF of GS is commutative & the addF of GS is associative & 0. GS is_a_unity_wrt the addF of GS & comp GS is_an_inverseOp_wrt the addF of GS holds
GS is AbGroup
proof
let GS be non empty addLoopStr ; ::_thesis: ( the addF of GS is commutative & the addF of GS is associative & 0. GS is_a_unity_wrt the addF of GS & comp GS is_an_inverseOp_wrt the addF of GS implies GS is AbGroup )
assume that
A1: ( the addF of GS is commutative & the addF of GS is associative ) and
A2: 0. GS is_a_unity_wrt the addF of GS and
A3: comp GS is_an_inverseOp_wrt the addF of GS ; ::_thesis: GS is AbGroup
A4: GS is right_complementable
proof
let x be Element of GS; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider b = (comp GS) . x as Element of GS ;
take b ; :: according to ALGSTR_0:def_11 ::_thesis: x + b = 0. GS
thus x + b = the_unity_wrt the addF of GS by A3, FINSEQOP:def_1
.= 0. GS by A2, BINOP_1:def_8 ; ::_thesis: verum
end;
for x, y, z being Element of GS holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. GS) = x ) by A1, A2, BINOP_1:3, BINOP_1:def_2, BINOP_1:def_3;
hence GS is AbGroup by A4, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4; ::_thesis: verum
end;
Lm2: for GS being non empty addLoopStr st the addF of GS is commutative & the addF of GS is associative holds
( GS is Abelian & GS is add-associative )
proof
let GS be non empty addLoopStr ; ::_thesis: ( the addF of GS is commutative & the addF of GS is associative implies ( GS is Abelian & GS is add-associative ) )
assume that
A1: the addF of GS is commutative and
A2: the addF of GS is associative ; ::_thesis: ( GS is Abelian & GS is add-associative )
thus GS is Abelian ::_thesis: GS is add-associative
proof
let x, y be Element of GS; :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
thus x + y = y + x by A1, BINOP_1:def_2; ::_thesis: verum
end;
let x, y, z be Element of GS; :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
thus (x + y) + z = x + (y + z) by A2, BINOP_1:def_3; ::_thesis: verum
end;
Lm3: for GS being non empty addLoopStr st 0. GS is_a_unity_wrt the addF of GS holds
GS is right_zeroed
proof
let GS be non empty addLoopStr ; ::_thesis: ( 0. GS is_a_unity_wrt the addF of GS implies GS is right_zeroed )
assume A1: 0. GS is_a_unity_wrt the addF of GS ; ::_thesis: GS is right_zeroed
let x be Element of GS; :: according to RLVECT_1:def_4 ::_thesis: x + (0. GS) = x
thus x + (0. GS) = x by A1, BINOP_1:3; ::_thesis: verum
end;
Lm4: for F being Field holds the multF of F is associative
proof
let F be Field; ::_thesis: the multF of F is associative
let x, y, z be Element of F; :: according to BINOP_1:def_3 ::_thesis: the multF of F . (x,( the multF of F . (y,z))) = the multF of F . (( the multF of F . (x,y)),z)
thus the multF of F . (x,( the multF of F . (y,z))) = x * (y * z)
.= (x * y) * z by GROUP_1:def_3
.= the multF of F . (( the multF of F . (x,y)),z) ; ::_thesis: verum
end;
theorem :: PRVECT_1:4
for F being Field holds 0. F is_a_unity_wrt the addF of F
proof
let F be Field; ::_thesis: 0. F is_a_unity_wrt the addF of F
now__::_thesis:_for_x_being_Element_of_F_holds_
(_the_addF_of_F_._((0._F),x)_=_x_&_the_addF_of_F_._(x,(0._F))_=_x_)
let x be Element of F; ::_thesis: ( the addF of F . ((0. F),x) = x & the addF of F . (x,(0. F)) = x )
thus the addF of F . ((0. F),x) = x + (0. F) by RLVECT_1:2
.= x by RLVECT_1:4 ; ::_thesis: the addF of F . (x,(0. F)) = x
thus the addF of F . (x,(0. F)) = x + (0. F)
.= x by RLVECT_1:4 ; ::_thesis: verum
end;
hence 0. F is_a_unity_wrt the addF of F by BINOP_1:3; ::_thesis: verum
end;
theorem Th5: :: PRVECT_1:5
for F being Field holds 1_ F is_a_unity_wrt the multF of F
proof
let F be Field; ::_thesis: 1_ F is_a_unity_wrt the multF of F
now__::_thesis:_for_x_being_Element_of_F_holds_
(_the_multF_of_F_._((1__F),x)_=_x_&_the_multF_of_F_._(x,(1__F))_=_x_)
let x be Element of F; ::_thesis: ( the multF of F . ((1_ F),x) = x & the multF of F . (x,(1_ F)) = x )
thus the multF of F . ((1_ F),x) = (1_ F) * x
.= x by VECTSP_1:def_8 ; ::_thesis: the multF of F . (x,(1_ F)) = x
thus the multF of F . (x,(1_ F)) = x * (1_ F)
.= x by VECTSP_1:def_8 ; ::_thesis: verum
end;
hence 1_ F is_a_unity_wrt the multF of F by BINOP_1:3; ::_thesis: verum
end;
Lm5: for F being Field holds the multF of F is_distributive_wrt the addF of F
proof
let F be Field; ::_thesis: the multF of F is_distributive_wrt the addF of F
now__::_thesis:_for_x,_y,_z_being_Element_of_F_holds_
(_the_multF_of_F_._(x,(_the_addF_of_F_._(y,z)))_=_the_addF_of_F_._((_the_multF_of_F_._(x,y)),(_the_multF_of_F_._(x,z)))_&_the_multF_of_F_._((_the_addF_of_F_._(x,y)),z)_=_the_addF_of_F_._((_the_multF_of_F_._(x,z)),(_the_multF_of_F_._(y,z)))_)
let x, y, z be Element of F; ::_thesis: ( the multF of F . (x,( the addF of F . (y,z))) = the addF of F . (( the multF of F . (x,y)),( the multF of F . (x,z))) & the multF of F . (( the addF of F . (x,y)),z) = the addF of F . (( the multF of F . (x,z)),( the multF of F . (y,z))) )
thus the multF of F . (x,( the addF of F . (y,z))) = x * (y + z)
.= (x * y) + (x * z) by VECTSP_1:def_7
.= the addF of F . (( the multF of F . (x,y)),( the multF of F . (x,z))) ; ::_thesis: the multF of F . (( the addF of F . (x,y)),z) = the addF of F . (( the multF of F . (x,z)),( the multF of F . (y,z)))
thus the multF of F . (( the addF of F . (x,y)),z) = (x + y) * z
.= (x * z) + (y * z) by VECTSP_1:def_7
.= the addF of F . (( the multF of F . (x,z)),( the multF of F . (y,z))) ; ::_thesis: verum
end;
hence the multF of F is_distributive_wrt the addF of F by BINOP_1:11; ::_thesis: verum
end;
begin
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 funcF .: (x,y) -> Element of n -tuples_on D;
coherence
F .: (x,y) is Element of n -tuples_on D by FINSEQ_2:120;
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
ex b1 being BinOp of (n -tuples_on D) st
for x, y being Element of n -tuples_on D holds b1 . (x,y) = F .: (x,y)
proof
defpred S1[ set , set , set ] means ex x9, y9 being Element of n -tuples_on D st
( $1 = x9 & $2 = y9 & $3 = F .: (x9,y9) );
A1: for x, y being Element of n -tuples_on D ex z being Element of n -tuples_on D st S1[x,y,z]
proof
let x, y be Element of n -tuples_on D; ::_thesis: ex z being Element of n -tuples_on D st S1[x,y,z]
reconsider x9 = x, y9 = y as Element of n -tuples_on D ;
reconsider z = F .: (x9,y9) as Element of n -tuples_on D ;
take z ; ::_thesis: S1[x,y,z]
take x9 ; ::_thesis: ex y9 being Element of n -tuples_on D st
( x = x9 & y = y9 & z = F .: (x9,y9) )
take y9 ; ::_thesis: ( x = x9 & y = y9 & z = F .: (x9,y9) )
thus ( x = x9 & y = y9 & z = F .: (x9,y9) ) ; ::_thesis: verum
end;
consider G being BinOp of (n -tuples_on D) such that
A2: for x, y being Element of n -tuples_on D holds S1[x,y,G . (x,y)] from BINOP_1:sch_3(A1);
take G ; ::_thesis: for x, y being Element of n -tuples_on D holds G . (x,y) = F .: (x,y)
let p1, p2 be Element of n -tuples_on D; ::_thesis: G . (p1,p2) = F .: (p1,p2)
reconsider x = p1, y = p2 as Element of n -tuples_on D ;
ex x9, y9 being Element of n -tuples_on D st
( x = x9 & y = y9 & G . (x,y) = F .: (x9,y9) ) by A2;
hence G . (p1,p2) = F .: (p1,p2) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (n -tuples_on D) st ( for x, y being Element of n -tuples_on D holds b1 . (x,y) = F .: (x,y) ) & ( for x, y being Element of n -tuples_on D holds b2 . (x,y) = F .: (x,y) ) holds
b1 = b2
proof
let G, H be BinOp of (n -tuples_on D); ::_thesis: ( ( for x, y being Element of n -tuples_on D holds G . (x,y) = F .: (x,y) ) & ( for x, y being Element of n -tuples_on D holds H . (x,y) = F .: (x,y) ) implies G = H )
assume that
A3: for x, y being Element of n -tuples_on D holds G . (x,y) = F .: (x,y) and
A4: for x, y being Element of n -tuples_on D holds H . (x,y) = F .: (x,y) ; ::_thesis: G = H
now__::_thesis:_for_x,_y_being_Element_of_n_-tuples_on_D_holds_G_._(x,y)_=_H_._(x,y)
let x, y be Element of n -tuples_on D; ::_thesis: G . (x,y) = H . (x,y)
G . (x,y) = F .: (x,y) by A3;
hence G . (x,y) = H . (x,y) by A4; ::_thesis: verum
end;
hence G = H by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines product PRVECT_1:def_1_:_
for D being non empty set
for F being BinOp of D
for n being Nat
for b4 being BinOp of (n -tuples_on D) holds
( b4 = product (F,n) iff for x, y being Element of n -tuples_on D holds b4 . (x,y) = F .: (x,y) );
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
ex b1 being UnOp of (n -tuples_on D) st
for x being Element of n -tuples_on D holds b1 . x = F * x
proof
defpred S1[ set , set ] means ex x9 being Element of n -tuples_on D st
( x9 = $1 & $2 = F * x9 );
A1: for x being Element of n -tuples_on D ex y being Element of n -tuples_on D st S1[x,y]
proof
let x be Element of n -tuples_on D; ::_thesis: ex y being Element of n -tuples_on D st S1[x,y]
reconsider x9 = x as Element of n -tuples_on D ;
reconsider y = F * x9 as Element of n -tuples_on D by FINSEQ_2:113;
take y ; ::_thesis: S1[x,y]
take x9 ; ::_thesis: ( x9 = x & y = F * x9 )
thus ( x9 = x & y = F * x9 ) ; ::_thesis: verum
end;
consider G being UnOp of (n -tuples_on D) such that
A2: for x being Element of n -tuples_on D holds S1[x,G . x] from FUNCT_2:sch_3(A1);
take G ; ::_thesis: for x being Element of n -tuples_on D holds G . x = F * x
let p1 be Element of n -tuples_on D; ::_thesis: G . p1 = F * p1
reconsider x = p1 as Element of n -tuples_on D ;
ex x9 being Element of n -tuples_on D st
( x9 = x & G . x = F * x9 ) by A2;
hence G . p1 = F * p1 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being UnOp of (n -tuples_on D) st ( for x being Element of n -tuples_on D holds b1 . x = F * x ) & ( for x being Element of n -tuples_on D holds b2 . x = F * x ) holds
b1 = b2
proof
let G, H be UnOp of (n -tuples_on D); ::_thesis: ( ( for x being Element of n -tuples_on D holds G . x = F * x ) & ( for x being Element of n -tuples_on D holds H . x = F * x ) implies G = H )
assume that
A3: for x being Element of n -tuples_on D holds G . x = F * x and
A4: for x being Element of n -tuples_on D holds H . x = F * x ; ::_thesis: G = H
now__::_thesis:_for_x_being_Element_of_n_-tuples_on_D_holds_G_._x_=_H_._x
let x be Element of n -tuples_on D; ::_thesis: G . x = H . x
G . x = F * x by A3;
hence G . x = H . x by A4; ::_thesis: verum
end;
hence G = H by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines product PRVECT_1:def_2_:_
for D being non empty set
for F being UnOp of D
for n being Nat
for b4 being UnOp of (n -tuples_on D) holds
( b4 = product (F,n) iff for x being Element of n -tuples_on D holds b4 . x = F * x );
theorem Th6: :: PRVECT_1:6
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
let n be Nat; ::_thesis: for D being non empty set
for B being BinOp of D st B is commutative holds
product (B,n) is commutative
let D be non empty set ; ::_thesis: for B being BinOp of D st B is commutative holds
product (B,n) is commutative
let B be BinOp of D; ::_thesis: ( B is commutative implies product (B,n) is commutative )
assume A1: B is commutative ; ::_thesis: product (B,n) is commutative
now__::_thesis:_for_x,_y_being_Element_of_n_-tuples_on_D_holds_(product_(B,n))_._(x,y)_=_(product_(B,n))_._(y,x)
let x, y be Element of n -tuples_on D; ::_thesis: (product (B,n)) . (x,y) = (product (B,n)) . (y,x)
thus (product (B,n)) . (x,y) = B .: (x,y) by Def1
.= B .: (y,x) by A1, FINSEQOP:33
.= (product (B,n)) . (y,x) by Def1 ; ::_thesis: verum
end;
hence product (B,n) is commutative by BINOP_1:def_2; ::_thesis: verum
end;
theorem Th7: :: PRVECT_1:7
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
let n be Nat; ::_thesis: for D being non empty set
for B being BinOp of D st B is associative holds
product (B,n) is associative
let D be non empty set ; ::_thesis: for B being BinOp of D st B is associative holds
product (B,n) is associative
let B be BinOp of D; ::_thesis: ( B is associative implies product (B,n) is associative )
assume A1: B is associative ; ::_thesis: product (B,n) is associative
now__::_thesis:_for_x,_y,_z_being_Element_of_n_-tuples_on_D_holds_(product_(B,n))_._(((product_(B,n))_._(x,y)),z)_=_(product_(B,n))_._(x,((product_(B,n))_._(y,z)))
let x, y, z be Element of n -tuples_on D; ::_thesis: (product (B,n)) . (((product (B,n)) . (x,y)),z) = (product (B,n)) . (x,((product (B,n)) . (y,z)))
thus (product (B,n)) . (((product (B,n)) . (x,y)),z) = (product (B,n)) . ((B .: (x,y)),z) by Def1
.= B .: ((B .: (x,y)),z) by Def1
.= B .: (x,(B .: (y,z))) by A1, FINSEQOP:28
.= (product (B,n)) . (x,(B .: (y,z))) by Def1
.= (product (B,n)) . (x,((product (B,n)) . (y,z))) by Def1 ; ::_thesis: verum
end;
hence product (B,n) is associative by BINOP_1:def_3; ::_thesis: verum
end;
theorem Th8: :: PRVECT_1:8
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
let n be Nat; ::_thesis: 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)
let D be non empty set ; ::_thesis: 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)
let d be Element of D; ::_thesis: for B being BinOp of D st d is_a_unity_wrt B holds
n |-> d is_a_unity_wrt product (B,n)
let B be BinOp of D; ::_thesis: ( d is_a_unity_wrt B implies n |-> d is_a_unity_wrt product (B,n) )
assume d is_a_unity_wrt B ; ::_thesis: n |-> d is_a_unity_wrt product (B,n)
then A1: ( B is having_a_unity & d = the_unity_wrt B ) by BINOP_1:def_8, SETWISEO:def_2;
now__::_thesis:_for_b_being_Element_of_n_-tuples_on_D_holds_
(_(product_(B,n))_._((n_|->_d),b)_=_b_&_(product_(B,n))_._(b,(n_|->_d))_=_b_)
let b be Element of n -tuples_on D; ::_thesis: ( (product (B,n)) . ((n |-> d),b) = b & (product (B,n)) . (b,(n |-> d)) = b )
reconsider b9 = b as Element of n -tuples_on D ;
thus (product (B,n)) . ((n |-> d),b) = B .: ((n |-> d),b9) by Def1
.= b by A1, FINSEQOP:56 ; ::_thesis: (product (B,n)) . (b,(n |-> d)) = b
thus (product (B,n)) . (b,(n |-> d)) = B .: (b9,(n |-> d)) by Def1
.= b by A1, FINSEQOP:56 ; ::_thesis: verum
end;
hence n |-> d is_a_unity_wrt product (B,n) by BINOP_1:3; ::_thesis: verum
end;
theorem Th9: :: PRVECT_1:9
for n being Nat
for D being non empty set
for B being BinOp of D
for C being UnOp of D st B is having_a_unity & B is associative & C is_an_inverseOp_wrt B holds
product (C,n) is_an_inverseOp_wrt product (B,n)
proof
let n be Nat; ::_thesis: for D being non empty set
for B being BinOp of D
for C being UnOp of D st B is having_a_unity & B is associative & C is_an_inverseOp_wrt B holds
product (C,n) is_an_inverseOp_wrt product (B,n)
let D be non empty set ; ::_thesis: for B being BinOp of D
for C being UnOp of D st B is having_a_unity & B is associative & C is_an_inverseOp_wrt B holds
product (C,n) is_an_inverseOp_wrt product (B,n)
let B be BinOp of D; ::_thesis: for C being UnOp of D st B is having_a_unity & B is associative & C is_an_inverseOp_wrt B holds
product (C,n) is_an_inverseOp_wrt product (B,n)
let C be UnOp of D; ::_thesis: ( B is having_a_unity & B is associative & C is_an_inverseOp_wrt B implies product (C,n) is_an_inverseOp_wrt product (B,n) )
assume that
A1: B is having_a_unity and
A2: B is associative and
A3: C is_an_inverseOp_wrt B ; ::_thesis: product (C,n) is_an_inverseOp_wrt product (B,n)
A4: B is having_an_inverseOp by A3, FINSEQOP:def_2;
then A5: C = the_inverseOp_wrt B by A1, A2, A3, FINSEQOP:def_3;
A6: now__::_thesis:_for_f_being_Element_of_n_-tuples_on_D_holds_
(_(product_(B,n))_._(f,((product_(C,n))_._f))_=_n_|->_(the_unity_wrt_B)_&_(product_(B,n))_._(((product_(C,n))_._f),f)_=_n_|->_(the_unity_wrt_B)_)
let f be Element of n -tuples_on D; ::_thesis: ( (product (B,n)) . (f,((product (C,n)) . f)) = n |-> (the_unity_wrt B) & (product (B,n)) . (((product (C,n)) . f),f) = n |-> (the_unity_wrt B) )
reconsider f9 = f as Element of n -tuples_on D ;
reconsider cf = C * f9 as Element of n -tuples_on D by FINSEQ_2:113;
thus (product (B,n)) . (f,((product (C,n)) . f)) = (product (B,n)) . (f9,(C * f9)) by Def2
.= B .: (f9,cf) by Def1
.= n |-> (the_unity_wrt B) by A1, A2, A4, A5, FINSEQOP:73 ; ::_thesis: (product (B,n)) . (((product (C,n)) . f),f) = n |-> (the_unity_wrt B)
thus (product (B,n)) . (((product (C,n)) . f),f) = (product (B,n)) . ((C * f9),f9) by Def2
.= B .: (cf,f9) by Def1
.= n |-> (the_unity_wrt B) by A1, A2, A4, A5, FINSEQOP:73 ; ::_thesis: verum
end;
ex d being Element of D st d is_a_unity_wrt B by A1, SETWISEO:def_2;
then the_unity_wrt B is_a_unity_wrt B by BINOP_1:def_8;
then n |-> (the_unity_wrt B) is_a_unity_wrt product (B,n) by Th8;
then n |-> (the_unity_wrt B) = the_unity_wrt (product (B,n)) by BINOP_1:def_8;
hence product (C,n) is_an_inverseOp_wrt product (B,n) by A6, FINSEQOP:def_1; ::_thesis: verum
end;
begin
definition
let F be non empty addLoopStr ;
let n be Nat;
assume A1: ( F is Abelian & F is add-associative & F is right_zeroed & F is right_complementable ) ;
funcn -Group_over F -> strict AbGroup equals :Def3: :: PRVECT_1:def 3
addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #);
coherence
addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) is strict AbGroup
proof
set G = addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #);
reconsider G = addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) as non empty addLoopStr ;
( the addF of F is commutative & the addF of F is associative ) by A1, FVSUM_1:1, FVSUM_1:2;
then A2: ( product ( the addF of F,n) is commutative & product ( the addF of F,n) is associative ) by Th6, Th7;
A3: 0. F is_a_unity_wrt the addF of F by A1, Th1;
A4: G is right_complementable
proof
set B = the addF of F;
set C = comp F;
let x be Element of G; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider y = (product ((comp F),n)) . x as Element of G by FUNCT_2:5;
take y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. G
( the addF of F is associative & the addF of F is having_a_unity ) by A1, A3, FVSUM_1:2, SETWISEO:def_2;
then product ((comp F),n) is_an_inverseOp_wrt product ( the addF of F,n) by A1, Lm1, Th9;
then A5: x + y = the_unity_wrt (product ( the addF of F,n)) by FINSEQOP:def_1;
0. G is_a_unity_wrt the addF of G by A1, Th1, Th8;
hence x + y = 0. G by A5, BINOP_1:def_8; ::_thesis: verum
end;
( 0. G = n |-> (0. F) & n |-> (0. F) is_a_unity_wrt product ( the addF of F,n) ) by A1, Th1, Th8;
hence addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) is strict AbGroup by A2, A4, Lm2, Lm3; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines -Group_over PRVECT_1:def_3_:_
for F being non empty addLoopStr
for n being Nat st F is Abelian & F is add-associative & F is right_zeroed & F is right_complementable holds
n -Group_over F = addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #);
registration
let F be AbGroup;
let n be Nat;
clustern -Group_over F -> strict ;
coherence
not n -Group_over F is empty ;
end;
definition
let F be Field;
let n be Nat;
funcn -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 multF of F [;] (x,v);
existence
ex b1 being Function of [: the carrier of F,(n -tuples_on the carrier of F):],(n -tuples_on the carrier of F) st
for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b1 . (x,v) = the multF of F [;] (x,v)
proof
defpred S1[ set , set ] means ex x1 being Element of F ex v being Element of n -tuples_on the carrier of F st
( $1 = [x1,v] & $2 = the multF of F [;] (x1,v) );
A1: for x being set st x in [: the carrier of F,(n -tuples_on the carrier of F):] holds
ex y being set st
( y in n -tuples_on the carrier of F & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in [: the carrier of F,(n -tuples_on the carrier of F):] implies ex y being set st
( y in n -tuples_on the carrier of F & S1[x,y] ) )
assume x in [: the carrier of F,(n -tuples_on the carrier of F):] ; ::_thesis: ex y being set st
( y in n -tuples_on the carrier of F & S1[x,y] )
then consider x1, v being set such that
A2: x1 in the carrier of F and
A3: v in n -tuples_on the carrier of F and
A4: [x1,v] = x by ZFMISC_1:84;
reconsider v = v as Element of n -tuples_on the carrier of F by A3;
reconsider x1 = x1 as Element of F by A2;
take y = the multF of F [;] (x1,v); ::_thesis: ( y in n -tuples_on the carrier of F & S1[x,y] )
y is Element of n -tuples_on the carrier of F by FINSEQ_2:121;
hence y in n -tuples_on the carrier of F ; ::_thesis: S1[x,y]
take x1 ; ::_thesis: ex v being Element of n -tuples_on the carrier of F st
( x = [x1,v] & y = the multF of F [;] (x1,v) )
take v ; ::_thesis: ( x = [x1,v] & y = the multF of F [;] (x1,v) )
thus ( x = [x1,v] & y = the multF of F [;] (x1,v) ) by A4; ::_thesis: verum
end;
consider f being Function of [: the carrier of F,(n -tuples_on the carrier of F):],(n -tuples_on the carrier of F) such that
A5: for x being set st x in [: the carrier of F,(n -tuples_on the carrier of F):] holds
S1[x,f . x] from FUNCT_2:sch_1(A1);
take f ; ::_thesis: for x being Element of F
for v being Element of n -tuples_on the carrier of F holds f . (x,v) = the multF of F [;] (x,v)
let x be Element of F; ::_thesis: for v being Element of n -tuples_on the carrier of F holds f . (x,v) = the multF of F [;] (x,v)
let v be Element of n -tuples_on the carrier of F; ::_thesis: f . (x,v) = the multF of F [;] (x,v)
[x,v] in [: the carrier of F,(n -tuples_on the carrier of F):] by ZFMISC_1:87;
then consider x1 being Element of F, v1 being Element of n -tuples_on the carrier of F such that
A6: [x,v] = [x1,v1] and
A7: f . [x,v] = the multF of F [;] (x1,v1) by A5;
x1 = x by A6, XTUPLE_0:1;
hence f . (x,v) = the multF of F [;] (x,v) by A6, A7, XTUPLE_0:1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of [: the carrier of F,(n -tuples_on the carrier of F):],(n -tuples_on the carrier of F) st ( for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b1 . (x,v) = the multF of F [;] (x,v) ) & ( for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b2 . (x,v) = the multF of F [;] (x,v) ) holds
b1 = b2
proof
let f, g be Function of [: the carrier of F,(n -tuples_on the carrier of F):],(n -tuples_on the carrier of F); ::_thesis: ( ( for x being Element of F
for v being Element of n -tuples_on the carrier of F holds f . (x,v) = the multF of F [;] (x,v) ) & ( for x being Element of F
for v being Element of n -tuples_on the carrier of F holds g . (x,v) = the multF of F [;] (x,v) ) implies f = g )
assume that
A8: for x being Element of F
for v being Element of n -tuples_on the carrier of F holds f . (x,v) = the multF of F [;] (x,v) and
A9: for x being Element of F
for v being Element of n -tuples_on the carrier of F holds g . (x,v) = the multF of F [;] (x,v) ; ::_thesis: f = g
now__::_thesis:_for_x_being_Element_of_F
for_v_being_Element_of_n_-tuples_on_the_carrier_of_F_holds_f_._(x,v)_=_g_._(x,v)
let x be Element of F; ::_thesis: for v being Element of n -tuples_on the carrier of F holds f . (x,v) = g . (x,v)
let v be Element of n -tuples_on the carrier of F; ::_thesis: f . (x,v) = g . (x,v)
f . (x,v) = the multF of F [;] (x,v) by A8;
hence f . (x,v) = g . (x,v) by A9; ::_thesis: verum
end;
hence f = g by BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines -Mult_over PRVECT_1:def_4_:_
for F being Field
for n being Nat
for b3 being Function of [: the carrier of F,(n -tuples_on the carrier of F):],(n -tuples_on the carrier of F) holds
( b3 = n -Mult_over F iff for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b3 . (x,v) = the multF of F [;] (x,v) );
definition
let F be Field;
let n be Nat;
funcn -VectSp_over F -> strict VectSpStr over F means :Def5: :: PRVECT_1:def 5
( addLoopStr(# the carrier of it, the addF of it, the ZeroF of it #) = n -Group_over F & the lmult of it = n -Mult_over F );
existence
ex b1 being strict VectSpStr over F st
( addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = n -Group_over F & the lmult of b1 = n -Mult_over F )
proof
n -Group_over F = addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) by Def3;
then reconsider d = n -Mult_over F as Function of [: the carrier of F, the carrier of (n -Group_over F):], the carrier of (n -Group_over F) ;
set G = n -Group_over F;
take VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #) ; ::_thesis: ( addLoopStr(# the carrier of VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #), the addF of VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #), the ZeroF of VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #) #) = n -Group_over F & the lmult of VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #) = n -Mult_over F )
thus ( addLoopStr(# the carrier of VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #), the addF of VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #), the ZeroF of VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #) #) = n -Group_over F & the lmult of VectSpStr(# H1(n -Group_over F),H2(n -Group_over F),H4(n -Group_over F),d #) = n -Mult_over F ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict VectSpStr over F st addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = n -Group_over F & the lmult of b1 = n -Mult_over F & addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = n -Group_over F & the lmult of b2 = n -Mult_over F holds
b1 = b2 ;
end;
:: deftheorem Def5 defines -VectSp_over PRVECT_1:def_5_:_
for F being Field
for n being Nat
for b3 being strict VectSpStr over F holds
( b3 = n -VectSp_over F iff ( addLoopStr(# the carrier of b3, the addF of b3, the ZeroF of b3 #) = n -Group_over F & the lmult of b3 = n -Mult_over F ) );
registration
let F be Field;
let n be Nat;
clustern -VectSp_over F -> non empty strict ;
coherence
not n -VectSp_over F is empty
proof
addLoopStr(# the carrier of (n -VectSp_over F), the addF of (n -VectSp_over F), the ZeroF of (n -VectSp_over F) #) = n -Group_over F by Def5;
hence not the carrier of (n -VectSp_over F) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
theorem Th10: :: PRVECT_1:10
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
let n be Nat; ::_thesis: 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)))
let D be non empty set ; ::_thesis: 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)))
let H, G be BinOp of D; ::_thesis: 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)))
let d be Element of D; ::_thesis: 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)))
let t1, t2 be Element of n -tuples_on D; ::_thesis: ( H is_distributive_wrt G implies H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2))) )
A1: H [;] (d,(G .: (t1,t2))) = H [;] (d,(G * <:t1,t2:>)) by FUNCOP_1:def_3
.= H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> by FUNCOP_1:def_5 ;
( rng (H * <:((dom t1) --> d),t1:>) c= rng H & rng (H * <:((dom t2) --> d),t2:>) c= rng H ) by RELAT_1:26;
then ( rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:(rng (H * <:((dom t1) --> d),t1:>)),(rng (H * <:((dom t2) --> d),t2:>)):] & [:(rng (H * <:((dom t1) --> d),t1:>)),(rng (H * <:((dom t2) --> d),t2:>)):] c= [:(rng H),(rng H):] ) by FUNCT_3:51, ZFMISC_1:96;
then A2: rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:(rng H),(rng H):] by XBOOLE_1:1;
rng H c= D by RELAT_1:def_19;
then [:(rng H),(rng H):] c= [:D,D:] by ZFMISC_1:96;
then rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= [:D,D:] by A2, XBOOLE_1:1;
then A3: rng <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> c= dom G by FUNCT_2:def_1;
A4: dom t2 = Seg (len t2) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
( rng t1 c= D & rng t2 c= D ) by FINSEQ_1:def_4;
then A5: [:(rng t1),(rng t2):] c= [:D,D:] by ZFMISC_1:96;
rng <:t1,t2:> c= [:(rng t1),(rng t2):] by FUNCT_3:51;
then rng <:t1,t2:> c= [:D,D:] by A5, XBOOLE_1:1;
then A6: rng <:t1,t2:> c= dom G by FUNCT_2:def_1;
A7: dom ((dom t2) --> d) = dom t2 by FUNCOP_1:13
.= Seg (len t2) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
dom t1 = Seg (len t1) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
then dom <:t1,t2:> = Seg n by A4, FUNCT_3:50;
then A8: dom (G * <:t1,t2:>) = Seg n by A6, RELAT_1:27;
then dom ((dom (G * <:t1,t2:>)) --> d) = Seg n by FUNCOP_1:13;
then A9: dom <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> = Seg n by A8, FUNCT_3:50;
rng t2 c= D by FINSEQ_1:def_4;
then ( rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),(rng t2):] & [:(rng ((dom t2) --> d)),(rng t2):] c= [:(rng ((dom t2) --> d)),D:] ) by FUNCT_3:51, ZFMISC_1:96;
then A10: rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),D:] by XBOOLE_1:1;
rng ((dom t2) --> d) c= {d} by FUNCOP_1:13;
then [:(rng ((dom t2) --> d)),D:] c= [:{d},D:] by ZFMISC_1:96;
then A11: rng <:((dom t2) --> d),t2:> c= [:{d},D:] by A10, XBOOLE_1:1;
A12: dom t1 = Seg (len t1) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
rng t1 c= D by FINSEQ_1:def_4;
then ( rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),(rng t1):] & [:(rng ((dom t1) --> d)),(rng t1):] c= [:(rng ((dom t1) --> d)),D:] ) by FUNCT_3:51, ZFMISC_1:96;
then A13: rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),D:] by XBOOLE_1:1;
rng ((dom t1) --> d) c= {d} by FUNCOP_1:13;
then [:(rng ((dom t1) --> d)),D:] c= [:{d},D:] by ZFMISC_1:96;
then A14: rng <:((dom t1) --> d),t1:> c= [:{d},D:] by A13, XBOOLE_1:1;
A15: dom ((dom t1) --> d) = dom t1 by FUNCOP_1:13
.= Seg (len t1) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
{d} c= D by ZFMISC_1:31;
then A16: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;
( rng ((dom (G * <:t1,t2:>)) --> d) c= {d} & {d} c= D ) by FUNCOP_1:13, ZFMISC_1:31;
then A17: rng ((dom (G * <:t1,t2:>)) --> d) c= D by XBOOLE_1:1;
A18: dom t2 = Seg (len t2) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
dom H = [:D,D:] by FUNCT_2:def_1;
then A19: dom (H * <:((dom t2) --> d),t2:>) = dom <:((dom t2) --> d),t2:> by A11, A16, RELAT_1:27, XBOOLE_1:1
.= Seg n by A7, A18, FUNCT_3:50 ;
{d} c= D by ZFMISC_1:31;
then A20: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;
set A = H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>;
A21: G .: ((H [;] (d,t1)),(H [;] (d,t2))) = G .: ((H * <:((dom t1) --> d),t1:>),(H [;] (d,t2))) by FUNCOP_1:def_5
.= G .: ((H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>)) by FUNCOP_1:def_5
.= G * <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> by FUNCOP_1:def_3 ;
dom H = [:D,D:] by FUNCT_2:def_1;
then dom (H * <:((dom t1) --> d),t1:>) = dom <:((dom t1) --> d),t1:> by A14, A20, RELAT_1:27, XBOOLE_1:1
.= Seg n by A15, A12, FUNCT_3:50 ;
then dom <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):> = Seg n by A19, FUNCT_3:50;
then A22: dom (G * <:(H * <:((dom t1) --> d),t1:>),(H * <:((dom t2) --> d),t2:>):>) = Seg n by A3, RELAT_1:27;
rng (G * <:t1,t2:>) c= D by RELAT_1:def_19;
then ( rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= [:(rng ((dom (G * <:t1,t2:>)) --> d)),(rng (G * <:t1,t2:>)):] & [:(rng ((dom (G * <:t1,t2:>)) --> d)),(rng (G * <:t1,t2:>)):] c= [:D,D:] ) by A17, FUNCT_3:51, ZFMISC_1:96;
then rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= [:D,D:] by XBOOLE_1:1;
then A23: rng <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):> c= dom H by FUNCT_2:def_1;
then A24: dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) = Seg n by A9, RELAT_1:27;
assume A25: H is_distributive_wrt G ; ::_thesis: H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2)))
for x being set st x in dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) holds
(H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x
proof
rng t1 c= D by FINSEQ_1:def_4;
then ( rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),(rng t1):] & [:(rng ((dom t1) --> d)),(rng t1):] c= [:(rng ((dom t1) --> d)),D:] ) by FUNCT_3:51, ZFMISC_1:96;
then A26: rng <:((dom t1) --> d),t1:> c= [:(rng ((dom t1) --> d)),D:] by XBOOLE_1:1;
rng ((dom t1) --> d) c= {d} by FUNCOP_1:13;
then [:(rng ((dom t1) --> d)),D:] c= [:{d},D:] by ZFMISC_1:96;
then A27: rng <:((dom t1) --> d),t1:> c= [:{d},D:] by A26, XBOOLE_1:1;
A28: ( rng t1 c= D & rng t2 c= D ) by FINSEQ_1:def_4;
{d} c= D by ZFMISC_1:31;
then A29: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;
A30: dom ((dom t2) --> d) = dom t2 by FUNCOP_1:13
.= Seg (len t2) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
{d} c= D by ZFMISC_1:31;
then A31: [:{d},D:] c= [:D,D:] by ZFMISC_1:96;
A32: dom t1 = Seg (len t1) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
rng t2 c= D by FINSEQ_1:def_4;
then ( rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),(rng t2):] & [:(rng ((dom t2) --> d)),(rng t2):] c= [:(rng ((dom t2) --> d)),D:] ) by FUNCT_3:51, ZFMISC_1:96;
then A33: rng <:((dom t2) --> d),t2:> c= [:(rng ((dom t2) --> d)),D:] by XBOOLE_1:1;
rng ((dom t2) --> d) c= {d} by FUNCOP_1:13;
then [:(rng ((dom t2) --> d)),D:] c= [:{d},D:] by ZFMISC_1:96;
then A34: rng <:((dom t2) --> d),t2:> c= [:{d},D:] by A33, XBOOLE_1:1;
A35: dom ((dom t1) --> d) = dom t1 by FUNCOP_1:13
.= Seg (len t1) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
let x be set ; ::_thesis: ( x in dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) implies (H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x )
A36: dom <:((dom (G .: (t1,t2))) --> d),(G .: (t1,t2)):> = (dom ((dom (G .: (t1,t2))) --> d)) /\ (dom (G .: (t1,t2))) by FUNCT_3:def_7;
assume A37: x in dom (H * <:((dom (G * <:t1,t2:>)) --> d),(G * <:t1,t2:>):>) ; ::_thesis: (H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x
then x in dom (H * <:((dom (G .: (t1,t2))) --> d),(G .: (t1,t2)):>) by A1, FUNCOP_1:def_5;
then x in dom <:((dom (G .: (t1,t2))) --> d),(G .: (t1,t2)):> by FUNCT_1:11;
then A38: x in dom (G .: (t1,t2)) by A36, XBOOLE_0:def_4;
dom t1 = Seg (len t1) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
then A39: t1 . x in rng t1 by A24, A37, FUNCT_1:def_3;
A40: dom t2 = Seg (len t2) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
dom H = [:D,D:] by FUNCT_2:def_1;
then dom (H * <:((dom t1) --> d),t1:>) = dom <:((dom t1) --> d),t1:> by A27, A31, RELAT_1:27, XBOOLE_1:1
.= Seg n by A35, A32, FUNCT_3:50 ;
then A41: x in dom (H [;] (d,t1)) by A24, A37, FUNCOP_1:def_5;
dom t2 = Seg (len t2) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
then A42: t2 . x in rng t2 by A24, A37, FUNCT_1:def_3;
dom H = [:D,D:] by FUNCT_2:def_1;
then dom (H * <:((dom t2) --> d),t2:>) = dom <:((dom t2) --> d),t2:> by A34, A29, RELAT_1:27, XBOOLE_1:1
.= Seg n by A30, A40, FUNCT_3:50 ;
then A43: x in dom (H [;] (d,t2)) by A24, A37, FUNCOP_1:def_5;
(H [;] (d,(G .: (t1,t2)))) . x = H . (d,((G .: (t1,t2)) . x)) by A1, A37, FUNCOP_1:32
.= H . (d,(G . ((t1 . x),(t2 . x)))) by A38, FUNCOP_1:22
.= G . ((H . (d,(t1 . x))),(H . (d,(t2 . x)))) by A25, A39, A28, A42, BINOP_1:11
.= G . (((H [;] (d,t1)) . x),(H . (d,(t2 . x)))) by A41, FUNCOP_1:32
.= G . (((H [;] (d,t1)) . x),((H [;] (d,t2)) . x)) by A43, FUNCOP_1:32
.= (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x by A21, A24, A22, A37, FUNCOP_1:22 ;
hence (H [;] (d,(G .: (t1,t2)))) . x = (G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x ; ::_thesis: verum
end;
hence H [;] (d,(G .: (t1,t2))) = G .: ((H [;] (d,t1)),(H [;] (d,t2))) by A1, A21, A9, A23, A22, FUNCT_1:2, RELAT_1:27; ::_thesis: verum
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 funcF [;] (x,v) -> Element of n -tuples_on D;
coherence
F [;] (x,v) is Element of n -tuples_on D by FINSEQ_2:121;
end;
registration
let F be Field;
let n be Nat;
clustern -VectSp_over F -> strict vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( n -VectSp_over F is vector-distributive & n -VectSp_over F is scalar-distributive & n -VectSp_over F is scalar-associative & n -VectSp_over F is scalar-unital )
proof
A1: ( addLoopStr(# the carrier of (n -VectSp_over F), the addF of (n -VectSp_over F), the ZeroF of (n -VectSp_over F) #) = n -Group_over F & n -Group_over F = addLoopStr(# (n -tuples_on the carrier of F),(product ( the addF of F,n)),(n |-> (0. F)) #) ) by Def3, Def5;
1_ F is_a_unity_wrt the multF of F by Th5;
then A2: ( the multF of F is having_a_unity & the_unity_wrt the multF of F = 1_ F ) by BINOP_1:def_8, SETWISEO:def_2;
A3: n -VectSp_over F is vector-distributive
proof
let x be Element of F; :: according to VECTSP_1:def_14 ::_thesis: for b1, b2 being Element of the carrier of (n -VectSp_over F) holds x * (b1 + b2) = (x * b1) + (x * b2)
let v, w be Element of (n -VectSp_over F); ::_thesis: x * (v + w) = (x * v) + (x * w)
reconsider v9 = v, w9 = w as Element of n -tuples_on the carrier of F by A1;
thus x * (v + w) = (n -Mult_over F) . (x,((product ( the addF of F,n)) . (v,w))) by A1, Def5
.= (n -Mult_over F) . (x,( the addF of F .: (v9,w9))) by Def1
.= the multF of F [;] (x,( the addF of F .: (v9,w9))) by Def4
.= the addF of F .: (( the multF of F [;] (x,v9)),( the multF of F [;] (x,w9))) by Lm5, Th10
.= (product ( the addF of F,n)) . (( the multF of F [;] (x,v9)),( the multF of F [;] (x,w9))) by Def1
.= (product ( the addF of F,n)) . (((n -Mult_over F) . (x,v9)),( the multF of F [;] (x,w9))) by Def4
.= (product ( the addF of F,n)) . (((n -Mult_over F) . (x,v9)),((n -Mult_over F) . (x,w9))) by Def4
.= (product ( the addF of F,n)) . (( the lmult of (n -VectSp_over F) . (x,v)),((n -Mult_over F) . (x,w9))) by Def5
.= (x * v) + (x * w) by A1, Def5 ; ::_thesis: verum
end;
A4: n -VectSp_over F is scalar-distributive
proof
let x, y be Element of F; :: according to VECTSP_1:def_15 ::_thesis: for b1 being Element of the carrier of (n -VectSp_over F) holds (x + y) * b1 = (x * b1) + (y * b1)
let v be Element of (n -VectSp_over F); ::_thesis: (x + y) * v = (x * v) + (y * v)
reconsider v9 = v as Element of n -tuples_on the carrier of F by A1;
thus (x + y) * v = (n -Mult_over F) . ((x + y),v9) by Def5
.= the multF of F [;] (( the addF of F . (x,y)),v9) by Def4
.= the addF of F .: (( the multF of F [;] (x,v9)),( the multF of F [;] (y,v9))) by Lm5, FINSEQOP:46
.= (product ( the addF of F,n)) . (( the multF of F [;] (x,v9)),( the multF of F [;] (y,v9))) by Def1
.= (product ( the addF of F,n)) . (((n -Mult_over F) . (x,v9)),( the multF of F [;] (y,v9))) by Def4
.= (product ( the addF of F,n)) . (((n -Mult_over F) . (x,v9)),((n -Mult_over F) . (y,v9))) by Def4
.= (product ( the addF of F,n)) . (( the lmult of (n -VectSp_over F) . (x,v)),((n -Mult_over F) . (y,v9))) by Def5
.= (x * v) + (y * v) by A1, Def5 ; ::_thesis: verum
end;
A5: n -VectSp_over F is scalar-associative
proof
let x, y be Element of F; :: according to VECTSP_1:def_16 ::_thesis: for b1 being Element of the carrier of (n -VectSp_over F) holds (x * y) * b1 = x * (y * b1)
let v be Element of (n -VectSp_over F); ::_thesis: (x * y) * v = x * (y * v)
reconsider v9 = v as Element of n -tuples_on the carrier of F by A1;
thus (x * y) * v = (n -Mult_over F) . ((x * y),v9) by Def5
.= the multF of F [;] ((x * y),v9) by Def4
.= the multF of F [;] (x,( the multF of F [;] (y,v9))) by Lm4, FINSEQOP:31
.= (n -Mult_over F) . (x,( the multF of F [;] (y,v9))) by Def4
.= (n -Mult_over F) . (x,((n -Mult_over F) . (y,v9))) by Def4
.= (n -Mult_over F) . (x,( the lmult of (n -VectSp_over F) . (y,v))) by Def5
.= x * (y * v) by Def5 ; ::_thesis: verum
end;
n -VectSp_over F is scalar-unital
proof
let v be Element of (n -VectSp_over F); :: according to VECTSP_1:def_17 ::_thesis: (1. F) * v = v
reconsider v9 = v as Element of n -tuples_on the carrier of F by A1;
thus (1. F) * v = (n -Mult_over F) . ((1. F),v9) by Def5
.= the multF of F [;] ((1. F),v9) by Def4
.= v by A2, FINSEQOP:57 ; ::_thesis: verum
end;
hence ( n -VectSp_over F is vector-distributive & n -VectSp_over F is scalar-distributive & n -VectSp_over F is scalar-associative & n -VectSp_over F is scalar-unital ) by A3, A4, A5; ::_thesis: verum
end;
end;
begin
definition
mode Domain-Sequence is non-empty non empty FinSequence;
end;
scheme :: PRVECT_1:sch 1
NEFinSeqLambda{ F1() -> non empty FinSequence, F2( set ) -> set } :
ex p being non empty FinSequence st
( len p = len F1() & ( for i being Element of dom F1() holds p . i = F2(i) ) )
proof
consider p being FinSequence such that
A1: ( len p = len F1() & ( for i being Nat st i in dom p holds
p . i = F2(i) ) ) from FINSEQ_1:sch_2();
dom p = dom F1() by A1, FINSEQ_3:29;
then reconsider p9 = p as non empty FinSequence ;
take p9 ; ::_thesis: ( len p9 = len F1() & ( for i being Element of dom F1() holds p9 . i = F2(i) ) )
thus len p9 = len F1() by A1; ::_thesis: for i being Element of dom F1() holds p9 . i = F2(i)
let i be Element of dom F1(); ::_thesis: p9 . i = F2(i)
A2: dom F1() = Seg (len F1()) by FINSEQ_1:def_3;
dom p = Seg (len F1()) by A1, FINSEQ_1:def_3;
hence p9 . i = F2(i) by A1, A2; ::_thesis: verum
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 funcf . i -> Element of a . i;
coherence
f . i is Element of a . i by CARD_3:9;
end;
begin
definition
let a be non-empty non empty Function;
mode BinOps of a -> Function means :Def6: :: PRVECT_1:def 6
( dom it = dom a & ( for i being Element of dom a holds it . i is BinOp of (a . i) ) );
existence
ex b1 being Function st
( dom b1 = dom a & ( for i being Element of dom a holds b1 . i is BinOp of (a . i) ) )
proof
deffunc H5( set ) -> Element of bool [:[:(a . $1),(a . $1):],(a . $1):] = pr1 ((a . $1),(a . $1));
consider f being Function such that
A1: ( dom f = dom a & ( for x being set st x in dom a holds
f . x = H5(x) ) ) from FUNCT_1:sch_3();
take f ; ::_thesis: ( dom f = dom a & ( for i being Element of dom a holds f . i is BinOp of (a . i) ) )
thus dom f = dom a by A1; ::_thesis: for i being Element of dom a holds f . i is BinOp of (a . i)
let i be Element of dom a; ::_thesis: f . i is BinOp of (a . i)
f . i = pr1 ((a . i),(a . i)) by A1;
hence f . i is BinOp of (a . i) ; ::_thesis: verum
end;
mode UnOps of a -> Function means :Def7: :: PRVECT_1:def 7
( dom it = dom a & ( for i being Element of dom a holds it . i is UnOp of (a . i) ) );
existence
ex b1 being Function st
( dom b1 = dom a & ( for i being Element of dom a holds b1 . i is UnOp of (a . i) ) )
proof
deffunc H5( set ) -> Element of bool [:(a . $1),(a . $1):] = id (a . $1);
consider f being Function such that
A2: ( dom f = dom a & ( for x being set st x in dom a holds
f . x = H5(x) ) ) from FUNCT_1:sch_3();
take f ; ::_thesis: ( dom f = dom a & ( for i being Element of dom a holds f . i is UnOp of (a . i) ) )
thus dom f = dom a by A2; ::_thesis: for i being Element of dom a holds f . i is UnOp of (a . i)
let i be Element of dom a; ::_thesis: f . i is UnOp of (a . i)
f . i = id (a . i) by A2;
hence f . i is UnOp of (a . i) ; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines BinOps PRVECT_1:def_6_:_
for a being non-empty non empty Function
for b2 being Function holds
( b2 is BinOps of a iff ( dom b2 = dom a & ( for i being Element of dom a holds b2 . i is BinOp of (a . i) ) ) );
:: deftheorem Def7 defines UnOps PRVECT_1:def_7_:_
for a being non-empty non empty Function
for b2 being Function holds
( b2 is UnOps of a iff ( dom b2 = dom a & ( for i being Element of dom a holds b2 . i is UnOp of (a . i) ) ) );
registration
let a be Domain-Sequence;
cluster -> FinSequence-like for BinOps of a;
coherence
for b1 being BinOps of a holds b1 is FinSequence-like
proof
let f be BinOps of a; ::_thesis: f is FinSequence-like
( dom a = dom f & dom a = Seg (len a) ) by Def6, FINSEQ_1:def_3;
hence f is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum
end;
cluster -> FinSequence-like for UnOps of a;
coherence
for b1 being UnOps of a holds b1 is FinSequence-like
proof
let f be UnOps of a; ::_thesis: f is FinSequence-like
( dom a = dom f & dom a = Seg (len a) ) by Def7, FINSEQ_1:def_3;
hence f is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum
end;
end;
theorem Th11: :: PRVECT_1:11
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
let a be Domain-Sequence; ::_thesis: 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) ) ) )
let p be FinSequence; ::_thesis: ( 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) ) ) )
( dom p = dom a iff len p = len a ) by FINSEQ_3:29;
hence ( 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) ) ) ) by Def6; ::_thesis: verum
end;
theorem Th12: :: PRVECT_1:12
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
let a be Domain-Sequence; ::_thesis: 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) ) ) )
let p be FinSequence; ::_thesis: ( 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) ) ) )
( dom p = dom a iff len p = len a ) by FINSEQ_3:29;
hence ( 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) ) ) ) by Def7; ::_thesis: verum
end;
definition
let a be Domain-Sequence;
let b be BinOps of a;
let i be Element of dom a;
:: original: .
redefine funcb . i -> BinOp of (a . i);
coherence
b . i is BinOp of (a . i) by Th11;
end;
definition
let a be Domain-Sequence;
let u be UnOps of a;
let i be Element of dom a;
:: original: .
redefine funcu . i -> UnOp of (a . i);
coherence
u . i is UnOp of (a . i) by Th12;
end;
theorem :: PRVECT_1:13
for a being Domain-Sequence
for d, d9 being UnOp of (product a) st ( for f being Element of product a
for i being Element of dom a holds (d . f) . i = (d9 . f) . i ) holds
d = d9
proof
let a be Domain-Sequence; ::_thesis: for d, d9 being UnOp of (product a) st ( for f being Element of product a
for i being Element of dom a holds (d . f) . i = (d9 . f) . i ) holds
d = d9
let d, d9 be UnOp of (product a); ::_thesis: ( ( for f being Element of product a
for i being Element of dom a holds (d . f) . i = (d9 . f) . i ) implies d = d9 )
assume A1: for f being Element of product a
for i being Element of dom a holds (d . f) . i = (d9 . f) . i ; ::_thesis: d = d9
now__::_thesis:_for_f_being_Element_of_product_a_holds_d_._f_=_d9_._f
let f be Element of product a; ::_thesis: d . f = d9 . f
A2: ( dom (d . f) = dom a & dom (d9 . f) = dom a ) by CARD_3:9;
for x being set st x in dom a holds
(d . f) . x = (d9 . f) . x by A1;
hence d . f = d9 . f by A2, FUNCT_1:2; ::_thesis: verum
end;
hence d = d9 by FUNCT_2:63; ::_thesis: verum
end;
theorem Th14: :: PRVECT_1:14
for a being Domain-Sequence
for u being UnOps of a holds
( doms u = a & product (rngs u) c= product a )
proof
let a be Domain-Sequence; ::_thesis: for u being UnOps of a holds
( doms u = a & product (rngs u) c= product a )
let u be UnOps of a; ::_thesis: ( doms u = a & product (rngs u) c= product a )
A1: dom (doms u) = u " (SubFuncs (rng u)) by FUNCT_6:def_2;
A2: ( dom a = Seg (len a) & dom u = Seg (len u) ) by FINSEQ_1:def_3;
A3: len u = len a by Th12;
A4: dom u c= u " (SubFuncs (rng u))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom u or x in u " (SubFuncs (rng u)) )
assume x in dom u ; ::_thesis: x in u " (SubFuncs (rng u))
then reconsider x = x as Element of dom a by A2, Th12;
u . x is UnOp of (a . x) ;
hence x in u " (SubFuncs (rng u)) by A2, A3, FUNCT_6:19; ::_thesis: verum
end;
u " (SubFuncs (rng u)) c= dom u by RELAT_1:132;
then A5: dom (doms u) = dom u by A1, A4, XBOOLE_0:def_10;
A6: now__::_thesis:_for_x_being_set_st_x_in_dom_u_holds_
(rngs_u)_._x_c=_a_._x
let x be set ; ::_thesis: ( x in dom u implies (rngs u) . x c= a . x )
assume x in dom u ; ::_thesis: (rngs u) . x c= a . x
then reconsider i = x as Element of dom a by A2, Th12;
(rngs u) . i = rng (u . i) by A2, A3, FUNCT_6:22;
hence (rngs u) . x c= a . x by RELAT_1:def_19; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_u_holds_
(doms_u)_._x_=_a_._x
let x be set ; ::_thesis: ( x in dom u implies (doms u) . x = a . x )
assume x in dom u ; ::_thesis: (doms u) . x = a . x
then reconsider i = x as Element of dom a by A2, Th12;
(doms u) . i = dom (u . i) by A2, A3, FUNCT_6:22
.= a . i by FUNCT_2:def_1 ;
hence (doms u) . x = a . x ; ::_thesis: verum
end;
hence doms u = a by A2, A3, A5, FUNCT_1:2; ::_thesis: product (rngs u) c= product a
dom (rngs u) = u " (SubFuncs (rng u)) by FUNCT_6:def_3;
hence product (rngs u) c= product a by A1, A2, A3, A5, A6, CARD_3:27; ::_thesis: verum
end;
definition
let a be Domain-Sequence;
let u be UnOps of a;
:: original: Frege
redefine func Frege u -> UnOp of (product a);
coherence
Frege u is UnOp of (product a)
proof
A1: ( product (rngs u) c= product a & rng (Frege u) = product (rngs u) ) by Th14, FUNCT_6:38;
( dom (Frege u) = product (doms u) & doms u = a ) by Th14, FUNCT_6:def_7;
hence Frege u is UnOp of (product a) by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
end;
theorem Th15: :: PRVECT_1:15
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
let a be Domain-Sequence; ::_thesis: 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)
let u be UnOps of a; ::_thesis: for f being Element of product a
for i being Element of dom a holds ((Frege u) . f) . i = (u . i) . (f . i)
let f be Element of product a; ::_thesis: for i being Element of dom a holds ((Frege u) . f) . i = (u . i) . (f . i)
let i be Element of dom a; ::_thesis: ((Frege u) . f) . i = (u . i) . (f . i)
A1: ( dom u = Seg (len u) & doms u = a ) by Th14, FINSEQ_1:def_3;
( dom a = Seg (len a) & len a = len u ) by Th12, FINSEQ_1:def_3;
hence ((Frege u) . f) . i = (u . i) . (f . i) by A1, FUNCT_6:37; ::_thesis: verum
end;
definition
let F be functional non empty set ;
let b be BinOp of F;
let f, g be Element of F;
:: original: .
redefine funcb . (f,g) -> Element of F;
coherence
b . (f,g) is Element of F
proof
b . (f,g) is Element of F ;
hence b . (f,g) is Element of F ; ::_thesis: verum
end;
end;
theorem Th16: :: PRVECT_1:16
for a being Domain-Sequence
for d, d9 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 = (d9 . (f,g)) . i ) holds
d = d9
proof
let a be Domain-Sequence; ::_thesis: for d, d9 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 = (d9 . (f,g)) . i ) holds
d = d9
let d, d9 be BinOp of (product a); ::_thesis: ( ( for f, g being Element of product a
for i being Element of dom a holds (d . (f,g)) . i = (d9 . (f,g)) . i ) implies d = d9 )
assume A1: for f, g being Element of product a
for i being Element of dom a holds (d . (f,g)) . i = (d9 . (f,g)) . i ; ::_thesis: d = d9
now__::_thesis:_for_f,_g_being_Element_of_product_a_holds_d_._(f,g)_=_d9_._(f,g)
let f, g be Element of product a; ::_thesis: d . (f,g) = d9 . (f,g)
A2: ( dom (d . (f,g)) = dom a & dom (d9 . (f,g)) = dom a ) by CARD_3:9;
for x being set st x in dom a holds
(d . (f,g)) . x = (d9 . (f,g)) . x by A1;
hence d . (f,g) = d9 . (f,g) by A2, FUNCT_1:2; ::_thesis: verum
end;
hence d = d9 by BINOP_1:2; ::_thesis: verum
end;
definition
let a be Domain-Sequence;
let b be BinOps of a;
func[:b:] -> BinOp of (product a) means :Def8: :: PRVECT_1:def 8
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
ex b1 being BinOp of (product a) st
for f, g being Element of product a
for i being Element of dom a holds (b1 . (f,g)) . i = (b . i) . ((f . i),(g . i))
proof
defpred S1[ Element of product a, Element of product a, Element of product a] means for i being Element of dom a holds $3 . i = (b . i) . (($1 . i),($2 . i));
A1: for f, g being Element of product a ex z being Element of product a st S1[f,g,z]
proof
let f, g be Element of product a; ::_thesis: ex z being Element of product a st S1[f,g,z]
defpred S2[ set , set ] means ex i being Element of dom a st
( $1 = i & $2 = (b . i) . ((f . i),(g . i)) );
A2: for x being set st x in dom a holds
ex z being set st S2[x,z]
proof
let x be set ; ::_thesis: ( x in dom a implies ex z being set st S2[x,z] )
assume x in dom a ; ::_thesis: ex z being set st S2[x,z]
then reconsider i = x as Element of dom a ;
take (b . i) . ((f . i),(g . i)) ; ::_thesis: S2[x,(b . i) . ((f . i),(g . i))]
thus S2[x,(b . i) . ((f . i),(g . i))] ; ::_thesis: verum
end;
consider z being Function such that
A3: ( dom z = dom a & ( for x being set st x in dom a holds
S2[x,z . x] ) ) from CLASSES1:sch_1(A2);
now__::_thesis:_for_x_being_set_st_x_in_dom_a_holds_
z_._x_in_a_._x
let x be set ; ::_thesis: ( x in dom a implies z . x in a . x )
assume x in dom a ; ::_thesis: z . x in a . x
then ex i being Element of dom a st
( x = i & z . x = (b . i) . ((f . i),(g . i)) ) by A3;
hence z . x in a . x ; ::_thesis: verum
end;
then reconsider z9 = z as Element of product a by A3, CARD_3:9;
take z9 ; ::_thesis: S1[f,g,z9]
let i be Element of dom a; ::_thesis: z9 . i = (b . i) . ((f . i),(g . i))
ex j being Element of dom a st
( j = i & z . i = (b . j) . ((f . j),(g . j)) ) by A3;
hence z9 . i = (b . i) . ((f . i),(g . i)) ; ::_thesis: verum
end;
consider d being BinOp of (product a) such that
A4: for f, g being Element of product a holds S1[f,g,d . (f,g)] from BINOP_1:sch_3(A1);
take d ; ::_thesis: for f, g being Element of product a
for i being Element of dom a holds (d . (f,g)) . i = (b . i) . ((f . i),(g . i))
thus for f, g being Element of product a
for i being Element of dom a holds (d . (f,g)) . i = (b . i) . ((f . i),(g . i)) by A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (product a) st ( for f, g being Element of product a
for i being Element of dom a holds (b1 . (f,g)) . i = (b . i) . ((f . i),(g . i)) ) & ( for f, g being Element of product a
for i being Element of dom a holds (b2 . (f,g)) . i = (b . i) . ((f . i),(g . i)) ) holds
b1 = b2
proof
let d, d9 be BinOp of (product a); ::_thesis: ( ( for f, g being Element of product a
for i being Element of dom a holds (d . (f,g)) . i = (b . i) . ((f . i),(g . i)) ) & ( for f, g being Element of product a
for i being Element of dom a holds (d9 . (f,g)) . i = (b . i) . ((f . i),(g . i)) ) implies d = d9 )
assume that
A5: for f, g being Element of product a
for i being Element of dom a holds (d . (f,g)) . i = (b . i) . ((f . i),(g . i)) and
A6: for f, g being Element of product a
for i being Element of dom a holds (d9 . (f,g)) . i = (b . i) . ((f . i),(g . i)) ; ::_thesis: d = d9
now__::_thesis:_for_f,_g_being_Element_of_product_a
for_i_being_Element_of_dom_a_holds_(d_._(f,g))_._i_=_(d9_._(f,g))_._i
let f, g be Element of product a; ::_thesis: for i being Element of dom a holds (d . (f,g)) . i = (d9 . (f,g)) . i
let i be Element of dom a; ::_thesis: (d . (f,g)) . i = (d9 . (f,g)) . i
thus (d . (f,g)) . i = (b . i) . ((f . i),(g . i)) by A5
.= (d9 . (f,g)) . i by A6 ; ::_thesis: verum
end;
hence d = d9 by Th16; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines [: PRVECT_1:def_8_:_
for a being Domain-Sequence
for b being BinOps of a
for b3 being BinOp of (product a) holds
( b3 = [:b:] iff for f, g being Element of product a
for i being Element of dom a holds (b3 . (f,g)) . i = (b . i) . ((f . i),(g . i)) );
theorem Th17: :: PRVECT_1:17
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
let a be Domain-Sequence; ::_thesis: for b being BinOps of a st ( for i being Element of dom a holds b . i is commutative ) holds
[:b:] is commutative
let b be BinOps of a; ::_thesis: ( ( for i being Element of dom a holds b . i is commutative ) implies [:b:] is commutative )
assume A1: for i being Element of dom a holds b . i is commutative ; ::_thesis: [:b:] is commutative
let x, y be Element of product a; :: according to BINOP_1:def_2 ::_thesis: [:b:] . (x,y) = [:b:] . (y,x)
A2: now__::_thesis:_for_z_being_set_st_z_in_dom_a_holds_
([:b:]_._(x,y))_._z_=_([:b:]_._(y,x))_._z
let z be set ; ::_thesis: ( z in dom a implies ([:b:] . (x,y)) . z = ([:b:] . (y,x)) . z )
assume z in dom a ; ::_thesis: ([:b:] . (x,y)) . z = ([:b:] . (y,x)) . z
then reconsider i = z as Element of dom a ;
A3: ([:b:] . (y,x)) . i = (b . i) . ((y . i),(x . i)) by Def8;
( b . i is commutative & ([:b:] . (x,y)) . i = (b . i) . ((x . i),(y . i)) ) by A1, Def8;
hence ([:b:] . (x,y)) . z = ([:b:] . (y,x)) . z by A3, BINOP_1:def_2; ::_thesis: verum
end;
( dom ([:b:] . (x,y)) = dom a & dom ([:b:] . (y,x)) = dom a ) by CARD_3:9;
hence [:b:] . (x,y) = [:b:] . (y,x) by A2, FUNCT_1:2; ::_thesis: verum
end;
theorem Th18: :: PRVECT_1:18
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
let a be Domain-Sequence; ::_thesis: for b being BinOps of a st ( for i being Element of dom a holds b . i is associative ) holds
[:b:] is associative
let b be BinOps of a; ::_thesis: ( ( for i being Element of dom a holds b . i is associative ) implies [:b:] is associative )
assume A1: for i being Element of dom a holds b . i is associative ; ::_thesis: [:b:] is associative
let x, y, z be Element of product a; :: according to BINOP_1:def_3 ::_thesis: [:b:] . (x,([:b:] . (y,z))) = [:b:] . (([:b:] . (x,y)),z)
A2: now__::_thesis:_for_v_being_set_st_v_in_dom_a_holds_
([:b:]_._(x,([:b:]_._(y,z))))_._v_=_([:b:]_._(([:b:]_._(x,y)),z))_._v
set xy = [:b:] . (x,y);
set yz = [:b:] . (y,z);
let v be set ; ::_thesis: ( v in dom a implies ([:b:] . (x,([:b:] . (y,z)))) . v = ([:b:] . (([:b:] . (x,y)),z)) . v )
assume v in dom a ; ::_thesis: ([:b:] . (x,([:b:] . (y,z)))) . v = ([:b:] . (([:b:] . (x,y)),z)) . v
then reconsider i = v as Element of dom a ;
A3: ( ([:b:] . (y,z)) . i = (b . i) . ((y . i),(z . i)) & ([:b:] . (x,([:b:] . (y,z)))) . i = (b . i) . ((x . i),(([:b:] . (y,z)) . i)) ) by Def8;
A4: ([:b:] . (([:b:] . (x,y)),z)) . i = (b . i) . ((([:b:] . (x,y)) . i),(z . i)) by Def8;
( b . i is associative & ([:b:] . (x,y)) . i = (b . i) . ((x . i),(y . i)) ) by A1, Def8;
hence ([:b:] . (x,([:b:] . (y,z)))) . v = ([:b:] . (([:b:] . (x,y)),z)) . v by A3, A4, BINOP_1:def_3; ::_thesis: verum
end;
( dom ([:b:] . (x,([:b:] . (y,z)))) = dom a & dom ([:b:] . (([:b:] . (x,y)),z)) = dom a ) by CARD_3:9;
hence [:b:] . (x,([:b:] . (y,z))) = [:b:] . (([:b:] . (x,y)),z) by A2, FUNCT_1:2; ::_thesis: verum
end;
theorem Th19: :: PRVECT_1:19
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
let a be Domain-Sequence; ::_thesis: 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:]
let b be BinOps of a; ::_thesis: 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:]
let f be Element of product a; ::_thesis: ( ( for i being Element of dom a holds f . i is_a_unity_wrt b . i ) implies f is_a_unity_wrt [:b:] )
assume A1: for i being Element of dom a holds f . i is_a_unity_wrt b . i ; ::_thesis: f is_a_unity_wrt [:b:]
now__::_thesis:_for_x_being_Element_of_product_a_holds_
(_[:b:]_._(f,x)_=_x_&_[:b:]_._(x,f)_=_x_)
let x be Element of product a; ::_thesis: ( [:b:] . (f,x) = x & [:b:] . (x,f) = x )
A2: dom x = dom a by CARD_3:9;
A3: now__::_thesis:_for_y_being_set_st_y_in_dom_a_holds_
([:b:]_._(f,x))_._y_=_x_._y
let y be set ; ::_thesis: ( y in dom a implies ([:b:] . (f,x)) . y = x . y )
assume y in dom a ; ::_thesis: ([:b:] . (f,x)) . y = x . y
then reconsider i = y as Element of dom a ;
( ([:b:] . (f,x)) . i = (b . i) . ((f . i),(x . i)) & f . i is_a_unity_wrt b . i ) by A1, Def8;
hence ([:b:] . (f,x)) . y = x . y by BINOP_1:3; ::_thesis: verum
end;
dom ([:b:] . (f,x)) = dom a by CARD_3:9;
hence [:b:] . (f,x) = x by A2, A3, FUNCT_1:2; ::_thesis: [:b:] . (x,f) = x
A4: now__::_thesis:_for_y_being_set_st_y_in_dom_a_holds_
([:b:]_._(x,f))_._y_=_x_._y
let y be set ; ::_thesis: ( y in dom a implies ([:b:] . (x,f)) . y = x . y )
assume y in dom a ; ::_thesis: ([:b:] . (x,f)) . y = x . y
then reconsider i = y as Element of dom a ;
( ([:b:] . (x,f)) . i = (b . i) . ((x . i),(f . i)) & f . i is_a_unity_wrt b . i ) by A1, Def8;
hence ([:b:] . (x,f)) . y = x . y by BINOP_1:3; ::_thesis: verum
end;
dom ([:b:] . (x,f)) = dom a by CARD_3:9;
hence [:b:] . (x,f) = x by A2, A4, FUNCT_1:2; ::_thesis: verum
end;
hence f is_a_unity_wrt [:b:] by BINOP_1:3; ::_thesis: verum
end;
theorem Th20: :: PRVECT_1:20
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 is having_a_unity ) ) holds
Frege u is_an_inverseOp_wrt [:b:]
proof
let a be Domain-Sequence; ::_thesis: 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 is having_a_unity ) ) holds
Frege u is_an_inverseOp_wrt [:b:]
let b be BinOps of a; ::_thesis: 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 is having_a_unity ) ) holds
Frege u is_an_inverseOp_wrt [:b:]
let u be UnOps of a; ::_thesis: ( ( for i being Element of dom a holds
( u . i is_an_inverseOp_wrt b . i & b . i is having_a_unity ) ) implies Frege u is_an_inverseOp_wrt [:b:] )
assume A1: for i being Element of dom a holds
( u . i is_an_inverseOp_wrt b . i & b . i is having_a_unity ) ; ::_thesis: Frege u is_an_inverseOp_wrt [:b:]
defpred S1[ set , set ] means ex i being Element of dom a st
( $1 = i & $2 = the_unity_wrt (b . i) );
A2: for x being set st x in dom a holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in dom a implies ex y being set st S1[x,y] )
assume x in dom a ; ::_thesis: ex y being set st S1[x,y]
then reconsider i = x as Element of dom a ;
take the_unity_wrt (b . i) ; ::_thesis: S1[x, the_unity_wrt (b . i)]
thus S1[x, the_unity_wrt (b . i)] ; ::_thesis: verum
end;
consider f being Function such that
A3: ( dom f = dom a & ( for x being set st x in dom a holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A2);
now__::_thesis:_for_x_being_set_st_x_in_dom_a_holds_
f_._x_in_a_._x
let x be set ; ::_thesis: ( x in dom a implies f . x in a . x )
assume x in dom a ; ::_thesis: f . x in a . x
then ex i being Element of dom a st
( x = i & f . x = the_unity_wrt (b . i) ) by A3;
hence f . x in a . x ; ::_thesis: verum
end;
then reconsider f = f as Element of product a by A3, CARD_3:9;
let x be Element of product a; :: according to FINSEQOP:def_1 ::_thesis: ( [:b:] . (x,((Frege u) . x)) = the_unity_wrt [:b:] & [:b:] . (((Frege u) . x),x) = the_unity_wrt [:b:] )
A4: dom f = dom a by CARD_3:9;
A5: now__::_thesis:_for_y_being_set_st_y_in_dom_a_holds_
([:b:]_._(x,((Frege_u)_._x)))_._y_=_f_._y
let y be set ; ::_thesis: ( y in dom a implies ([:b:] . (x,((Frege u) . x))) . y = f . y )
assume y in dom a ; ::_thesis: ([:b:] . (x,((Frege u) . x))) . y = f . y
then reconsider i = y as Element of dom a ;
A6: ( ((Frege u) . x) . i = (u . i) . (x . i) & u . i is_an_inverseOp_wrt b . i ) by A1, Th15;
( ex j being Element of dom a st
( i = j & f . i = the_unity_wrt (b . j) ) & ([:b:] . (x,((Frege u) . x))) . i = (b . i) . ((x . i),(((Frege u) . x) . i)) ) by A3, Def8;
hence ([:b:] . (x,((Frege u) . x))) . y = f . y by A6, FINSEQOP:def_1; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_dom_a_holds_f_._i_is_a_unity_wrt_b_._i
let i be Element of dom a; ::_thesis: f . i is_a_unity_wrt b . i
( ex j being Element of dom a st
( i = j & f . i = the_unity_wrt (b . j) ) & b . i is having_a_unity ) by A1, A3;
hence f . i is_a_unity_wrt b . i by SETWISEO:14; ::_thesis: verum
end;
then f is_a_unity_wrt [:b:] by Th19;
then A7: f = the_unity_wrt [:b:] by BINOP_1:def_8;
A8: now__::_thesis:_for_y_being_set_st_y_in_dom_a_holds_
([:b:]_._(((Frege_u)_._x),x))_._y_=_f_._y
let y be set ; ::_thesis: ( y in dom a implies ([:b:] . (((Frege u) . x),x)) . y = f . y )
assume y in dom a ; ::_thesis: ([:b:] . (((Frege u) . x),x)) . y = f . y
then reconsider i = y as Element of dom a ;
A9: ( ((Frege u) . x) . i = (u . i) . (x . i) & u . i is_an_inverseOp_wrt b . i ) by A1, Th15;
( ex j being Element of dom a st
( i = j & f . i = the_unity_wrt (b . j) ) & ([:b:] . (((Frege u) . x),x)) . i = (b . i) . ((((Frege u) . x) . i),(x . i)) ) by A3, Def8;
hence ([:b:] . (((Frege u) . x),x)) . y = f . y by A9, FINSEQOP:def_1; ::_thesis: verum
end;
dom ([:b:] . (x,((Frege u) . x))) = dom a by CARD_3:9;
hence [:b:] . (x,((Frege u) . x)) = the_unity_wrt [:b:] by A7, A4, A5, FUNCT_1:2; ::_thesis: [:b:] . (((Frege u) . x),x) = the_unity_wrt [:b:]
dom ([:b:] . (((Frege u) . x),x)) = dom a by CARD_3:9;
hence [:b:] . (((Frege u) . x),x) = the_unity_wrt [:b:] by A7, A4, A8, FUNCT_1:2; ::_thesis: verum
end;
begin
definition
let F be Relation;
attrF is AbGroup-yielding means :Def9: :: PRVECT_1:def 9
for x being set st x in rng F holds
x is AbGroup;
end;
:: deftheorem Def9 defines AbGroup-yielding PRVECT_1:def_9_:_
for F being Relation holds
( F is AbGroup-yielding iff for x being set st x in rng F holds
x is AbGroup );
registration
cluster Relation-like NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like AbGroup-yielding for set ;
existence
ex b1 being FinSequence st
( not b1 is empty & b1 is AbGroup-yielding )
proof
set A = the AbGroup;
take <* the AbGroup*> ; ::_thesis: ( not <* the AbGroup*> is empty & <* the AbGroup*> is AbGroup-yielding )
thus not <* the AbGroup*> is empty ; ::_thesis: <* the AbGroup*> is AbGroup-yielding
let x be set ; :: according to PRVECT_1:def_9 ::_thesis: ( x in rng <* the AbGroup*> implies x is AbGroup )
assume that
A1: x in rng <* the AbGroup*> and
A2: x is not AbGroup ; ::_thesis: contradiction
x in { the AbGroup} by A1, FINSEQ_1:38;
hence contradiction by A2, TARSKI:def_1; ::_thesis: verum
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 funcg . i -> AbGroup;
coherence
g . i is AbGroup
proof
g . i in rng g by FUNCT_1:def_3;
hence g . i is AbGroup by Def9; ::_thesis: verum
end;
end;
definition
let g be Group-Sequence;
func carr g -> Domain-Sequence means :Def10: :: PRVECT_1:def 10
( len it = len g & ( for j being Element of dom g holds it . j = the carrier of (g . j) ) );
existence
ex b1 being Domain-Sequence st
( len b1 = len g & ( for j being Element of dom g holds b1 . j = the carrier of (g . j) ) )
proof
defpred S1[ set , set ] means ex j9 being Element of dom g st
( j9 = $1 & $2 = the carrier of (g . j9) );
A1: for j being Nat st j in Seg (len g) holds
ex x being set st S1[j,x]
proof
let j be Nat; ::_thesis: ( j in Seg (len g) implies ex x being set st S1[j,x] )
assume j in Seg (len g) ; ::_thesis: ex x being set st S1[j,x]
then reconsider j9 = j as Element of dom g by FINSEQ_1:def_3;
take the carrier of (g . j9) ; ::_thesis: S1[j, the carrier of (g . j9)]
thus S1[j, the carrier of (g . j9)] ; ::_thesis: verum
end;
consider p being FinSequence such that
A2: ( dom p = Seg (len g) & ( for j being Nat st j in Seg (len g) holds
S1[j,p . j] ) ) from FINSEQ_1:sch_1(A1);
p is non-empty
proof
assume {} in rng p ; :: according to RELAT_1:def_9 ::_thesis: contradiction
then consider x being set such that
A3: x in dom p and
A4: {} = p . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A3;
ex x9 being Element of dom g st
( x9 = x & p . x = the carrier of (g . x9) ) by A2, A3;
hence contradiction by A4; ::_thesis: verum
end;
then reconsider p9 = p as Domain-Sequence by A2;
take p9 ; ::_thesis: ( len p9 = len g & ( for j being Element of dom g holds p9 . j = the carrier of (g . j) ) )
thus len p9 = len g by A2, FINSEQ_1:def_3; ::_thesis: for j being Element of dom g holds p9 . j = the carrier of (g . j)
let j be Element of dom g; ::_thesis: p9 . j = the carrier of (g . j)
reconsider k = j as Element of NAT ;
dom g = Seg (len g) by FINSEQ_1:def_3;
then ex j9 being Element of dom g st
( j9 = k & p9 . k = the carrier of (g . j9) ) by A2;
hence p9 . j = the carrier of (g . j) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Domain-Sequence st len b1 = len g & ( for j being Element of dom g holds b1 . j = the carrier of (g . j) ) & len b2 = len g & ( for j being Element of dom g holds b2 . j = the carrier of (g . j) ) holds
b1 = b2
proof
let f, h be Domain-Sequence; ::_thesis: ( len f = len g & ( for j being Element of dom g holds f . j = the carrier of (g . j) ) & len h = len g & ( for j being Element of dom g holds h . j = the carrier of (g . j) ) implies f = h )
assume that
A5: len f = len g and
A6: for j being Element of dom g holds f . j = the carrier of (g . j) and
A7: len h = len g and
A8: for j being Element of dom g holds h . j = the carrier of (g . j) ; ::_thesis: f = h
reconsider f9 = f, h9 = h as FinSequence ;
A9: now__::_thesis:_for_j_being_Nat_st_j_in_dom_f9_holds_
f9_._j_=_h9_._j
let j be Nat; ::_thesis: ( j in dom f9 implies f9 . j = h9 . j )
assume j in dom f9 ; ::_thesis: f9 . j = h9 . j
then reconsider j9 = j as Element of dom g by A5, FINSEQ_3:29;
f9 . j = the carrier of (g . j9) by A6;
hence f9 . j = h9 . j by A8; ::_thesis: verum
end;
( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def_3;
hence f = h by A5, A7, A9, FINSEQ_1:13; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines carr PRVECT_1:def_10_:_
for g being Group-Sequence
for b2 being Domain-Sequence holds
( b2 = carr g iff ( len b2 = len g & ( for j being Element of dom g holds b2 . j = the carrier of (g . j) ) ) );
definition
let g be Group-Sequence;
let i be Element of dom (carr g);
:: original: .
redefine funcg . i -> AbGroup;
coherence
g . i is AbGroup
proof
( dom g = Seg (len g) & Seg (len (carr g)) = dom (carr g) ) by FINSEQ_1:def_3;
then reconsider i9 = i as Element of dom g by Def10;
g . i9 is AbGroup ;
hence g . i is AbGroup ; ::_thesis: verum
end;
end;
definition
let g be Group-Sequence;
func addop g -> BinOps of carr g means :Def11: :: PRVECT_1:def 11
( len it = len (carr g) & ( for i being Element of dom (carr g) holds it . i = the addF of (g . i) ) );
existence
ex b1 being BinOps of carr g st
( len b1 = len (carr g) & ( for i being Element of dom (carr g) holds b1 . i = the addF of (g . i) ) )
proof
deffunc H5( Element of dom (carr g)) -> Element of bool [:[: the carrier of (g . $1), the carrier of (g . $1):], the carrier of (g . $1):] = the addF of (g . $1);
consider p being non empty FinSequence such that
A1: ( len p = len (carr g) & ( for i being Element of dom (carr g) holds p . i = H5(i) ) ) from PRVECT_1:sch_1();
now__::_thesis:_for_i_being_Element_of_dom_(carr_g)_holds_p_._i_is_BinOp_of_((carr_g)_._i)
let i be Element of dom (carr g); ::_thesis: p . i is BinOp of ((carr g) . i)
len g = len (carr g) by Def10;
then reconsider j = i as Element of dom g by FINSEQ_3:29;
( p . i = the addF of (g . i) & the carrier of (g . j) = (carr g) . j ) by A1, Def10;
hence p . i is BinOp of ((carr g) . i) ; ::_thesis: verum
end;
then reconsider p9 = p as BinOps of carr g by A1, Th11;
take p9 ; ::_thesis: ( len p9 = len (carr g) & ( for i being Element of dom (carr g) holds p9 . i = the addF of (g . i) ) )
thus ( len p9 = len (carr g) & ( for i being Element of dom (carr g) holds p9 . i = the addF of (g . i) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOps of carr g st len b1 = len (carr g) & ( for i being Element of dom (carr g) holds b1 . i = the addF of (g . i) ) & len b2 = len (carr g) & ( for i being Element of dom (carr g) holds b2 . i = the addF of (g . i) ) holds
b1 = b2
proof
let f, h be BinOps of carr g; ::_thesis: ( len f = len (carr g) & ( for i being Element of dom (carr g) holds f . i = the addF of (g . i) ) & len h = len (carr g) & ( for i being Element of dom (carr g) holds h . i = the addF of (g . i) ) implies f = h )
assume that
A2: len f = len (carr g) and
A3: for i being Element of dom (carr g) holds f . i = the addF of (g . i) and
A4: len h = len (carr g) and
A5: for i being Element of dom (carr g) holds h . i = the addF of (g . i) ; ::_thesis: f = h
reconsider f9 = f, h9 = h as FinSequence ;
A6: now__::_thesis:_for_i_being_Nat_st_i_in_dom_f9_holds_
f9_._i_=_h9_._i
let i be Nat; ::_thesis: ( i in dom f9 implies f9 . i = h9 . i )
assume i in dom f9 ; ::_thesis: f9 . i = h9 . i
then reconsider i9 = i as Element of dom (carr g) by A2, FINSEQ_3:29;
f9 . i = the addF of (g . i9) by A3;
hence f9 . i = h9 . i by A5; ::_thesis: verum
end;
( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def_3;
hence f = h by A2, A4, A6, FINSEQ_1:13; ::_thesis: verum
end;
func complop g -> UnOps of carr g means :Def12: :: PRVECT_1:def 12
( len it = len (carr g) & ( for i being Element of dom (carr g) holds it . i = comp (g . i) ) );
existence
ex b1 being UnOps of carr g st
( len b1 = len (carr g) & ( for i being Element of dom (carr g) holds b1 . i = comp (g . i) ) )
proof
deffunc H5( Element of dom (carr g)) -> Element of bool [: the carrier of (g . $1), the carrier of (g . $1):] = comp (g . $1);
consider p being non empty FinSequence such that
A7: ( len p = len (carr g) & ( for i being Element of dom (carr g) holds p . i = H5(i) ) ) from PRVECT_1:sch_1();
now__::_thesis:_for_i_being_Element_of_dom_(carr_g)_holds_p_._i_is_UnOp_of_((carr_g)_._i)
let i be Element of dom (carr g); ::_thesis: p . i is UnOp of ((carr g) . i)
len g = len (carr g) by Def10;
then reconsider j = i as Element of dom g by FINSEQ_3:29;
( p . i = comp (g . i) & the carrier of (g . j) = (carr g) . j ) by A7, Def10;
hence p . i is UnOp of ((carr g) . i) ; ::_thesis: verum
end;
then reconsider p9 = p as UnOps of carr g by A7, Th12;
take p9 ; ::_thesis: ( len p9 = len (carr g) & ( for i being Element of dom (carr g) holds p9 . i = comp (g . i) ) )
thus ( len p9 = len (carr g) & ( for i being Element of dom (carr g) holds p9 . i = comp (g . i) ) ) by A7; ::_thesis: verum
end;
uniqueness
for b1, b2 being UnOps of carr g st len b1 = len (carr g) & ( for i being Element of dom (carr g) holds b1 . i = comp (g . i) ) & len b2 = len (carr g) & ( for i being Element of dom (carr g) holds b2 . i = comp (g . i) ) holds
b1 = b2
proof
let f, h be UnOps of carr g; ::_thesis: ( len f = len (carr g) & ( for i being Element of dom (carr g) holds f . i = comp (g . i) ) & len h = len (carr g) & ( for i being Element of dom (carr g) holds h . i = comp (g . i) ) implies f = h )
assume that
A8: len f = len (carr g) and
A9: for i being Element of dom (carr g) holds f . i = comp (g . i) and
A10: len h = len (carr g) and
A11: for i being Element of dom (carr g) holds h . i = comp (g . i) ; ::_thesis: f = h
reconsider f9 = f, h9 = h as FinSequence ;
A12: now__::_thesis:_for_i_being_Nat_st_i_in_dom_f9_holds_
f_._i_=_h_._i
let i be Nat; ::_thesis: ( i in dom f9 implies f . i = h . i )
assume i in dom f9 ; ::_thesis: f . i = h . i
then reconsider i9 = i as Element of dom (carr g) by A8, FINSEQ_3:29;
f . i = comp (g . i9) by A9;
hence f . i = h . i by A11; ::_thesis: verum
end;
( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def_3;
hence f = h by A8, A10, A12, FINSEQ_1:13; ::_thesis: verum
end;
func zeros g -> Element of product (carr g) means :Def13: :: PRVECT_1:def 13
for i being Element of dom (carr g) holds it . i = 0. (g . i);
existence
ex b1 being Element of product (carr g) st
for i being Element of dom (carr g) holds b1 . i = 0. (g . i)
proof
deffunc H5( Element of dom (carr g)) -> Element of the carrier of (g . $1) = 0. (g . $1);
A13: dom (carr g) = Seg (len (carr g)) by FINSEQ_1:def_3;
consider p being non empty FinSequence such that
A14: ( len p = len (carr g) & ( for i being Element of dom (carr g) holds p . i = H5(i) ) ) from PRVECT_1:sch_1();
A15: dom g = Seg (len g) by FINSEQ_1:def_3;
A16: now__::_thesis:_for_i_being_set_st_i_in_dom_(carr_g)_holds_
p_._i_in_(carr_g)_._i
let i be set ; ::_thesis: ( i in dom (carr g) implies p . i in (carr g) . i )
assume i in dom (carr g) ; ::_thesis: p . i in (carr g) . i
then reconsider x = i as Element of dom (carr g) ;
reconsider x9 = x as Element of dom g by A15, A13, Def10;
( p . x = 0. (g . x) & (carr g) . x9 = the carrier of (g . x9) ) by A14, Def10;
hence p . i in (carr g) . i ; ::_thesis: verum
end;
dom p = Seg (len p) by FINSEQ_1:def_3;
then reconsider t = p as Element of product (carr g) by A14, A13, A16, CARD_3:9;
take t ; ::_thesis: for i being Element of dom (carr g) holds t . i = 0. (g . i)
thus for i being Element of dom (carr g) holds t . i = 0. (g . i) by A14; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of product (carr g) st ( for i being Element of dom (carr g) holds b1 . i = 0. (g . i) ) & ( for i being Element of dom (carr g) holds b2 . i = 0. (g . i) ) holds
b1 = b2
proof
let f, h be Element of product (carr g); ::_thesis: ( ( for i being Element of dom (carr g) holds f . i = 0. (g . i) ) & ( for i being Element of dom (carr g) holds h . i = 0. (g . i) ) implies f = h )
assume that
A17: for i being Element of dom (carr g) holds f . i = 0. (g . i) and
A18: for i being Element of dom (carr g) holds h . i = 0. (g . i) ; ::_thesis: f = h
reconsider f9 = f, h9 = h as Function ;
A19: now__::_thesis:_for_x_being_set_st_x_in_dom_(carr_g)_holds_
f9_._x_=_h9_._x
let x be set ; ::_thesis: ( x in dom (carr g) implies f9 . x = h9 . x )
assume x in dom (carr g) ; ::_thesis: f9 . x = h9 . x
then reconsider i = x as Element of dom (carr g) ;
thus f9 . x = 0. (g . i) by A17
.= h9 . x by A18 ; ::_thesis: verum
end;
( dom f9 = dom (carr g) & dom h9 = dom (carr g) ) by CARD_3:9;
hence f = h by A19, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines addop PRVECT_1:def_11_:_
for g being Group-Sequence
for b2 being BinOps of carr g holds
( b2 = addop g iff ( len b2 = len (carr g) & ( for i being Element of dom (carr g) holds b2 . i = the addF of (g . i) ) ) );
:: deftheorem Def12 defines complop PRVECT_1:def_12_:_
for g being Group-Sequence
for b2 being UnOps of carr g holds
( b2 = complop g iff ( len b2 = len (carr g) & ( for i being Element of dom (carr g) holds b2 . i = comp (g . i) ) ) );
:: deftheorem Def13 defines zeros PRVECT_1:def_13_:_
for g being Group-Sequence
for b2 being Element of product (carr g) holds
( b2 = zeros g iff for i being Element of dom (carr g) holds b2 . i = 0. (g . i) );
definition
let G be Group-Sequence;
func product G -> strict AbGroup equals :: PRVECT_1:def 14
addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);
coherence
addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #) is strict AbGroup
proof
reconsider GS = addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #) as non empty addLoopStr ;
A1: now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_(carr_G)_._i_=_H1(G_._i)
let i be Element of dom (carr G); ::_thesis: (carr G) . i = H1(G . i)
dom G = Seg (len G) by FINSEQ_1:def_3
.= Seg (len (carr G)) by Def10
.= dom (carr G) by FINSEQ_1:def_3 ;
hence (carr G) . i = H1(G . i) by Def10; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_(addop_G)_._i_is_associative
let i be Element of dom (carr G); ::_thesis: (addop G) . i is associative
( (addop G) . i = H2(G . i) & (carr G) . i = H1(G . i) ) by A1, Def11;
hence (addop G) . i is associative by FVSUM_1:2; ::_thesis: verum
end;
then A2: [:(addop G):] is associative by Th18;
now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_(zeros_G)_._i_is_a_unity_wrt_(addop_G)_._i
let i be Element of dom (carr G); ::_thesis: (zeros G) . i is_a_unity_wrt (addop G) . i
A3: (carr G) . i = H1(G . i) by A1;
( (addop G) . i = H2(G . i) & (zeros G) . i = H4(G . i) ) by Def11, Def13;
hence (zeros G) . i is_a_unity_wrt (addop G) . i by A3, Th1; ::_thesis: verum
end;
then A4: zeros G is_a_unity_wrt [:(addop G):] by Th19;
A5: GS is right_complementable
proof
let x be Element of GS; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider y = (Frege (complop G)) . x as Element of GS by FUNCT_2:5;
take y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. GS
now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_
(_(complop_G)_._i_is_an_inverseOp_wrt_(addop_G)_._i_&_(addop_G)_._i_is_having_a_unity_)
let i be Element of dom (carr G); ::_thesis: ( (complop G) . i is_an_inverseOp_wrt (addop G) . i & (addop G) . i is having_a_unity )
A6: ( (addop G) . i = H2(G . i) & (complop G) . i = H3(G . i) ) by Def11, Def12;
( H4(G . i) is_a_unity_wrt H2(G . i) & (carr G) . i = H1(G . i) ) by A1, Th1;
hence ( (complop G) . i is_an_inverseOp_wrt (addop G) . i & (addop G) . i is having_a_unity ) by A6, Th2, SETWISEO:def_2; ::_thesis: verum
end;
then Frege (complop G) is_an_inverseOp_wrt [:(addop G):] by Th20;
then x + y = the_unity_wrt [:(addop G):] by FINSEQOP:def_1;
hence x + y = 0. GS by A4, BINOP_1:def_8; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_dom_(carr_G)_holds_(addop_G)_._i_is_commutative
let i be Element of dom (carr G); ::_thesis: (addop G) . i is commutative
( (addop G) . i = H2(G . i) & (carr G) . i = H1(G . i) ) by A1, Def11;
hence (addop G) . i is commutative by FVSUM_1:1; ::_thesis: verum
end;
then ( 0. GS = zeros G & [:(addop G):] is commutative ) by Th17;
hence addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #) is strict AbGroup by A2, A4, A5, Lm2, Lm3; ::_thesis: verum
end;
end;
:: deftheorem defines product PRVECT_1:def_14_:_
for G being Group-Sequence holds product G = addLoopStr(# (product (carr G)),[:(addop G):],(zeros G) #);