deffunc H1( addLoopStr ) -> Element of the carrier of G = the ZeroF of G;
reconsider GS = RLSStruct(# (product (carr G)),(),[:():],[:():] #) as non empty RLSStruct ;
deffunc H2( 1-sorted ) -> set = the carrier of G;
deffunc H3( addLoopStr ) -> Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:] = the addF of G;
A1: now :: thesis: for i being Element of dom (carr G) holds (carr G) . i = H2(G . i)
let i be Element of dom (carr G); :: thesis: (carr G) . i = H2(G . i)
dom G = Seg (len G) by FINSEQ_1:def 3
.= Seg (len (carr G)) by Def4
.= dom (carr G) by FINSEQ_1:def 3 ;
hence (carr G) . i = H2(G . i) by Def4; :: thesis: verum
end;
now :: thesis: for i being Element of dom (carr G) holds () . i is associative
let i be Element of dom (carr G); :: thesis: () . i is associative
( (addop G) . i = H3(G . i) & (carr G) . i = H2(G . i) ) by ;
hence (addop G) . i is associative by FVSUM_1:2; :: thesis: verum
end;
then A2: [:():] is associative by PRVECT_1:18;
now :: thesis: for i being Element of dom (carr G) holds () . i is_a_unity_wrt () . i
let i be Element of dom (carr G); :: thesis: () . i is_a_unity_wrt () . i
A3: (zeros G) . i = 0. (G . i) by Def7;
( (addop G) . i = H3(G . i) & (carr G) . i = H2(G . i) ) by ;
hence (zeros G) . i is_a_unity_wrt () . i by ; :: thesis: verum
end;
then A4: zeros G is_a_unity_wrt [:():] by PRVECT_1:19;
A5: GS is right_complementable
proof
let x be Element of GS; :: according to ALGSTR_0:def 16 :: thesis:
reconsider y = (Frege ()) . 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
( () . i is_an_inverseOp_wrt () . i & () . i is having_a_unity )
let i be Element of dom (carr G); :: thesis: ( () . i is_an_inverseOp_wrt () . i & () . i is having_a_unity )
0. (G . i) = H1(G . i) ;
then A6: H1(G . i) is_a_unity_wrt H3(G . i) by PRVECT_1:1;
A7: (complop G) . i = comp (G . i) by Def6;
( (carr G) . i = H2(G . i) & () . i = H3(G . i) ) by ;
hence ( (complop G) . i is_an_inverseOp_wrt () . i & () . i is having_a_unity ) by ; :: thesis: verum
end;
then Frege () is_an_inverseOp_wrt [:():] by PRVECT_1:20;
then [:():] . (x,y) = the_unity_wrt [:():] by FINSEQOP:def 1;
hence x + y = 0. GS by ; :: thesis: verum
end;
now :: thesis: for i being Element of dom (carr G) holds () . i is commutative
let i be Element of dom (carr G); :: thesis: () . i is commutative
( (addop G) . i = H3(G . i) & (carr G) . i = H2(G . i) ) by ;
hence (addop G) . i is commutative by FVSUM_1:1; :: thesis: verum
end;
then [:():] is commutative by PRVECT_1:17;
hence ( product G is Abelian & product G is add-associative & product G is right_zeroed & product G is right_complementable & product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital ) by A2, A4, A5, Lm1, Lm2, Lm5; :: thesis: verum