:: FVSUM_1 semantic presentation
begin
theorem Th1: :: FVSUM_1:1
for K being non empty Abelian addLoopStr holds the addF of K is commutative
proof
let K be non empty Abelian addLoopStr ; ::_thesis: the addF of K is commutative
now__::_thesis:_for_a,_b_being_Element_of_K_holds_the_addF_of_K_._(a,b)_=_the_addF_of_K_._(b,a)
let a, b be Element of K; ::_thesis: the addF of K . (a,b) = the addF of K . (b,a)
thus the addF of K . (a,b) = a + b
.= the addF of K . (b,a) by RLVECT_1:2 ; ::_thesis: verum
end;
hence the addF of K is commutative by BINOP_1:def_2; ::_thesis: verum
end;
theorem Th2: :: FVSUM_1:2
for K being non empty add-associative addLoopStr holds the addF of K is associative
proof
let K be non empty add-associative addLoopStr ; ::_thesis: the addF of K is associative
now__::_thesis:_for_a,_b,_c_being_Element_of_K_holds_the_addF_of_K_._(a,(_the_addF_of_K_._(b,c)))_=_the_addF_of_K_._((_the_addF_of_K_._(a,b)),c)
let a, b, c be Element of K; ::_thesis: the addF of K . (a,( the addF of K . (b,c))) = the addF of K . (( the addF of K . (a,b)),c)
thus the addF of K . (a,( the addF of K . (b,c))) = a + (b + c)
.= (a + b) + c by RLVECT_1:def_3
.= the addF of K . (( the addF of K . (a,b)),c) ; ::_thesis: verum
end;
hence the addF of K is associative by BINOP_1:def_3; ::_thesis: verum
end;
theorem Th3: :: FVSUM_1:3
for K being non empty commutative multMagma holds the multF of K is commutative
proof
let K be non empty commutative multMagma ; ::_thesis: the multF of K is commutative
now__::_thesis:_for_a,_b_being_Element_of_K_holds_the_multF_of_K_._(a,b)_=_the_multF_of_K_._(b,a)
let a, b be Element of K; ::_thesis: the multF of K . (a,b) = the multF of K . (b,a)
thus the multF of K . (a,b) = a * b
.= b * a
.= the multF of K . (b,a) ; ::_thesis: verum
end;
hence the multF of K is commutative by BINOP_1:def_2; ::_thesis: verum
end;
registration
let K be non empty Abelian addLoopStr ;
cluster the addF of K -> commutative ;
coherence
the addF of K is commutative by Th1;
end;
registration
let K be non empty add-associative addLoopStr ;
cluster the addF of K -> associative ;
coherence
the addF of K is associative by Th2;
end;
registration
let K be non empty commutative multMagma ;
cluster the multF of K -> commutative ;
coherence
the multF of K is commutative by Th3;
end;
theorem Th4: :: FVSUM_1:4
for K being non empty commutative left_unital multLoopStr holds 1. K is_a_unity_wrt the multF of K
proof
let K be non empty commutative left_unital multLoopStr ; ::_thesis: 1. K is_a_unity_wrt the multF of K
set o = the multF of K;
now__::_thesis:_for_h_being_Element_of_K_holds_
(_the_multF_of_K_._((1._K),h)_=_h_&_the_multF_of_K_._(h,(1._K))_=_h_)
let h be Element of K; ::_thesis: ( the multF of K . ((1. K),h) = h & the multF of K . (h,(1. K)) = h )
thus the multF of K . ((1. K),h) = (1. K) * h
.= h by VECTSP_1:def_8 ; ::_thesis: the multF of K . (h,(1. K)) = h
thus the multF of K . (h,(1. K)) = h * (1. K)
.= h by VECTSP_1:def_8 ; ::_thesis: verum
end;
hence 1. K is_a_unity_wrt the multF of K by BINOP_1:3; ::_thesis: verum
end;
theorem Th5: :: FVSUM_1:5
for K being non empty commutative left_unital multLoopStr holds the_unity_wrt the multF of K = 1. K
proof
let K be non empty commutative left_unital multLoopStr ; ::_thesis: the_unity_wrt the multF of K = 1. K
reconsider e = 1. K as Element of K ;
e is_a_unity_wrt the multF of K by Th4;
hence the_unity_wrt the multF of K = 1. K by BINOP_1:def_8; ::_thesis: verum
end;
theorem Th6: :: FVSUM_1:6
for K being non empty left_zeroed right_zeroed addLoopStr holds 0. K is_a_unity_wrt the addF of K
proof
let K be non empty left_zeroed right_zeroed addLoopStr ; ::_thesis: 0. K is_a_unity_wrt the addF of K
now__::_thesis:_for_a_being_Element_of_K_holds_
(_the_addF_of_K_._((0._K),a)_=_a_&_the_addF_of_K_._(a,(0._K))_=_a_)
let a be Element of K; ::_thesis: ( the addF of K . ((0. K),a) = a & the addF of K . (a,(0. K)) = a )
thus the addF of K . ((0. K),a) = (0. K) + a
.= a by ALGSTR_1:def_2 ; ::_thesis: the addF of K . (a,(0. K)) = a
thus the addF of K . (a,(0. K)) = a + (0. K)
.= a by RLVECT_1:def_4 ; ::_thesis: verum
end;
hence 0. K is_a_unity_wrt the addF of K by BINOP_1:3; ::_thesis: verum
end;
theorem Th7: :: FVSUM_1:7
for K being non empty left_zeroed right_zeroed addLoopStr holds the_unity_wrt the addF of K = 0. K
proof
let K be non empty left_zeroed right_zeroed addLoopStr ; ::_thesis: the_unity_wrt the addF of K = 0. K
reconsider e = 0. K as Element of K ;
e is_a_unity_wrt the addF of K by Th6;
hence the_unity_wrt the addF of K = 0. K by BINOP_1:def_8; ::_thesis: verum
end;
theorem Th8: :: FVSUM_1:8
for K being non empty left_zeroed right_zeroed addLoopStr holds the addF of K is having_a_unity
proof
let K be non empty left_zeroed right_zeroed addLoopStr ; ::_thesis: the addF of K is having_a_unity
take 0. K ; :: according to SETWISEO:def_2 ::_thesis: 0. K is_a_unity_wrt the addF of K
thus 0. K is_a_unity_wrt the addF of K by Th6; ::_thesis: verum
end;
theorem :: FVSUM_1:9
for K being non empty commutative left_unital multLoopStr holds the multF of K is having_a_unity ;
theorem Th10: :: FVSUM_1:10
for K being non empty distributive doubleLoopStr holds the multF of K is_distributive_wrt the addF of K
proof
let K be non empty distributive doubleLoopStr ; ::_thesis: the multF of K is_distributive_wrt the addF of K
now__::_thesis:_for_a1,_a2,_a3_being_Element_of_K_holds_
(_the_multF_of_K_._(a1,(_the_addF_of_K_._(a2,a3)))_=_the_addF_of_K_._((_the_multF_of_K_._(a1,a2)),(_the_multF_of_K_._(a1,a3)))_&_the_multF_of_K_._((_the_addF_of_K_._(a1,a2)),a3)_=_the_addF_of_K_._((_the_multF_of_K_._(a1,a3)),(_the_multF_of_K_._(a2,a3)))_)
let a1, a2, a3 be Element of K; ::_thesis: ( the multF of K . (a1,( the addF of K . (a2,a3))) = the addF of K . (( the multF of K . (a1,a2)),( the multF of K . (a1,a3))) & the multF of K . (( the addF of K . (a1,a2)),a3) = the addF of K . (( the multF of K . (a1,a3)),( the multF of K . (a2,a3))) )
thus the multF of K . (a1,( the addF of K . (a2,a3))) = a1 * (a2 + a3)
.= (a1 * a2) + (a1 * a3) by VECTSP_1:def_7
.= the addF of K . (( the multF of K . (a1,a2)),( the multF of K . (a1,a3))) ; ::_thesis: the multF of K . (( the addF of K . (a1,a2)),a3) = the addF of K . (( the multF of K . (a1,a3)),( the multF of K . (a2,a3)))
thus the multF of K . (( the addF of K . (a1,a2)),a3) = (a1 + a2) * a3
.= (a1 * a3) + (a2 * a3) by VECTSP_1:def_7
.= the addF of K . (( the multF of K . (a1,a3)),( the multF of K . (a2,a3))) ; ::_thesis: verum
end;
hence the multF of K is_distributive_wrt the addF of K by BINOP_1:11; ::_thesis: verum
end;
definition
let K be non empty multMagma ;
let a be Element of K;
funca multfield -> UnOp of the carrier of K equals :: FVSUM_1:def 1
the multF of K [;] (a,(id the carrier of K));
coherence
the multF of K [;] (a,(id the carrier of K)) is UnOp of the carrier of K ;
end;
:: deftheorem defines multfield FVSUM_1:def_1_:_
for K being non empty multMagma
for a being Element of K holds a multfield = the multF of K [;] (a,(id the carrier of K));
definition
let K be non empty addLoopStr ;
func diffield K -> BinOp of the carrier of K equals :: FVSUM_1:def 2
the addF of K * ((id the carrier of K),(comp K));
correctness
coherence
the addF of K * ((id the carrier of K),(comp K)) is BinOp of the carrier of K;
;
end;
:: deftheorem defines diffield FVSUM_1:def_2_:_
for K being non empty addLoopStr holds diffield K = the addF of K * ((id the carrier of K),(comp K));
theorem Th11: :: FVSUM_1:11
for K being non empty addLoopStr
for a1, a2 being Element of K holds (diffield K) . (a1,a2) = a1 - a2
proof
let K be non empty addLoopStr ; ::_thesis: for a1, a2 being Element of K holds (diffield K) . (a1,a2) = a1 - a2
let a1, a2 be Element of K; ::_thesis: (diffield K) . (a1,a2) = a1 - a2
thus (diffield K) . (a1,a2) = the addF of K . (a1,((comp K) . a2)) by FINSEQOP:82
.= a1 - a2 by VECTSP_1:def_13 ; ::_thesis: verum
end;
Lm1: for K being non empty multMagma
for a, b being Element of K holds ( the multF of K [;] (b,(id the carrier of K))) . a = b * a
proof
let K be non empty multMagma ; ::_thesis: for a, b being Element of K holds ( the multF of K [;] (b,(id the carrier of K))) . a = b * a
let a, b be Element of K; ::_thesis: ( the multF of K [;] (b,(id the carrier of K))) . a = b * a
thus ( the multF of K [;] (b,(id the carrier of K))) . a = the multF of K . (b,((id the carrier of K) . a)) by FUNCOP_1:53
.= b * a by FUNCT_1:18 ; ::_thesis: verum
end;
theorem Th12: :: FVSUM_1:12
for K being non empty distributive doubleLoopStr
for a being Element of K holds a multfield is_distributive_wrt the addF of K by Th10, FINSEQOP:54;
theorem Th13: :: FVSUM_1:13
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr holds comp K is_an_inverseOp_wrt the addF of K
proof
let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: comp K is_an_inverseOp_wrt the addF of K
now__::_thesis:_for_a_being_Element_of_K_holds_
(_the_addF_of_K_._(a,((comp_K)_._a))_=_the_unity_wrt_the_addF_of_K_&_the_addF_of_K_._(((comp_K)_._a),a)_=_the_unity_wrt_the_addF_of_K_)
let a be Element of K; ::_thesis: ( the addF of K . (a,((comp K) . a)) = the_unity_wrt the addF of K & the addF of K . (((comp K) . a),a) = the_unity_wrt the addF of K )
thus the addF of K . (a,((comp K) . a)) = a + (- a) by VECTSP_1:def_13
.= 0. K by RLVECT_1:5
.= the_unity_wrt the addF of K by Th7 ; ::_thesis: the addF of K . (((comp K) . a),a) = the_unity_wrt the addF of K
thus the addF of K . (((comp K) . a),a) = (- a) + a by VECTSP_1:def_13
.= 0. K by RLVECT_1:5
.= the_unity_wrt the addF of K by Th7 ; ::_thesis: verum
end;
hence comp K is_an_inverseOp_wrt the addF of K by FINSEQOP:def_1; ::_thesis: verum
end;
theorem Th14: :: FVSUM_1:14
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr holds the addF of K is having_an_inverseOp
proof
let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: the addF of K is having_an_inverseOp
comp K is_an_inverseOp_wrt the addF of K by Th13;
hence the addF of K is having_an_inverseOp by FINSEQOP:def_2; ::_thesis: verum
end;
theorem Th15: :: FVSUM_1:15
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr holds the_inverseOp_wrt the addF of K = comp K
proof
let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: the_inverseOp_wrt the addF of K = comp K
A1: comp K is_an_inverseOp_wrt the addF of K by Th13;
( the addF of K is having_a_unity & the addF of K is having_an_inverseOp ) by Th8, Th14;
hence the_inverseOp_wrt the addF of K = comp K by A1, FINSEQOP:def_3; ::_thesis: verum
end;
theorem :: FVSUM_1:16
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds comp K is_distributive_wrt the addF of K
proof
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: comp K is_distributive_wrt the addF of K
the addF of K is having_a_unity by Th8;
then the_inverseOp_wrt the addF of K is_distributive_wrt the addF of K by Th14, FINSEQOP:63;
hence comp K is_distributive_wrt the addF of K by Th15; ::_thesis: verum
end;
begin
definition
let K be non empty addLoopStr ;
let p1, p2 be FinSequence of the carrier of K;
funcp1 + p2 -> FinSequence of the carrier of K equals :: FVSUM_1:def 3
the addF of K .: (p1,p2);
correctness
coherence
the addF of K .: (p1,p2) is FinSequence of the carrier of K;
;
end;
:: deftheorem defines + FVSUM_1:def_3_:_
for K being non empty addLoopStr
for p1, p2 being FinSequence of the carrier of K holds p1 + p2 = the addF of K .: (p1,p2);
theorem :: FVSUM_1:17
for K being non empty addLoopStr
for p1, p2 being FinSequence of the carrier of K
for a1, a2 being Element of K
for i being Element of NAT st i in dom (p1 + p2) & a1 = p1 . i & a2 = p2 . i holds
(p1 + p2) . i = a1 + a2 by FUNCOP_1:22;
definition
let i be Element of NAT ;
let K be non empty addLoopStr ;
let R1, R2 be Element of i -tuples_on the carrier of K;
:: original: +
redefine funcR1 + R2 -> Element of i -tuples_on the carrier of K;
coherence
R1 + R2 is Element of i -tuples_on the carrier of K by FINSEQ_2:120;
end;
theorem :: FVSUM_1:18
for i, j being Element of NAT
for K being non empty addLoopStr
for a1, a2 being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds
(R1 + R2) . j = a1 + a2
proof
let i, j be Element of NAT ; ::_thesis: for K being non empty addLoopStr
for a1, a2 being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds
(R1 + R2) . j = a1 + a2
let K be non empty addLoopStr ; ::_thesis: for a1, a2 being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds
(R1 + R2) . j = a1 + a2
let a1, a2 be Element of K; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds
(R1 + R2) . j = a1 + a2
let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( j in Seg i & a1 = R1 . j & a2 = R2 . j implies (R1 + R2) . j = a1 + a2 )
assume j in Seg i ; ::_thesis: ( not a1 = R1 . j or not a2 = R2 . j or (R1 + R2) . j = a1 + a2 )
then j in Seg (len (R1 + R2)) by CARD_1:def_7;
then j in dom (R1 + R2) by FINSEQ_1:def_3;
hence ( not a1 = R1 . j or not a2 = R2 . j or (R1 + R2) . j = a1 + a2 ) by FUNCOP_1:22; ::_thesis: verum
end;
theorem :: FVSUM_1:19
for K being non empty addLoopStr
for a1, a2 being Element of K holds <*a1*> + <*a2*> = <*(a1 + a2)*> by FINSEQ_2:74;
theorem :: FVSUM_1:20
for i being Element of NAT
for K being non empty addLoopStr
for a1, a2 being Element of K holds (i |-> a1) + (i |-> a2) = i |-> (a1 + a2) by FINSEQOP:17;
Lm2: for i being Element of NAT
for K being non empty left_zeroed right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds R + (i |-> (0. K)) = R
proof
let i be Element of NAT ; ::_thesis: for K being non empty left_zeroed right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds R + (i |-> (0. K)) = R
let K be non empty left_zeroed right_zeroed addLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds R + (i |-> (0. K)) = R
let R be Element of i -tuples_on the carrier of K; ::_thesis: R + (i |-> (0. K)) = R
( the_unity_wrt the addF of K = 0. K & the addF of K is having_a_unity ) by Th7, Th8;
hence R + (i |-> (0. K)) = R by FINSEQOP:56; ::_thesis: verum
end;
theorem Th21: :: FVSUM_1:21
for i being Element of NAT
for K being non empty left_zeroed Abelian right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds
( R + (i |-> (0. K)) = R & R = (i |-> (0. K)) + R )
proof
let i be Element of NAT ; ::_thesis: for K being non empty left_zeroed Abelian right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds
( R + (i |-> (0. K)) = R & R = (i |-> (0. K)) + R )
let K be non empty left_zeroed Abelian right_zeroed addLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds
( R + (i |-> (0. K)) = R & R = (i |-> (0. K)) + R )
let R be Element of i -tuples_on the carrier of K; ::_thesis: ( R + (i |-> (0. K)) = R & R = (i |-> (0. K)) + R )
thus R + (i |-> (0. K)) = R by Lm2; ::_thesis: R = (i |-> (0. K)) + R
hence R = (i |-> (0. K)) + R by FINSEQOP:33; ::_thesis: verum
end;
definition
let K be non empty addLoopStr ;
let p be FinSequence of the carrier of K;
func - p -> FinSequence of the carrier of K equals :: FVSUM_1:def 4
(comp K) * p;
correctness
coherence
(comp K) * p is FinSequence of the carrier of K;
;
end;
:: deftheorem defines - FVSUM_1:def_4_:_
for K being non empty addLoopStr
for p being FinSequence of the carrier of K holds - p = (comp K) * p;
theorem Th22: :: FVSUM_1:22
for i being Element of NAT
for K being non empty addLoopStr
for a being Element of K
for p being FinSequence of the carrier of K st i in dom (- p) & a = p . i holds
(- p) . i = - a
proof
let i be Element of NAT ; ::_thesis: for K being non empty addLoopStr
for a being Element of K
for p being FinSequence of the carrier of K st i in dom (- p) & a = p . i holds
(- p) . i = - a
let K be non empty addLoopStr ; ::_thesis: for a being Element of K
for p being FinSequence of the carrier of K st i in dom (- p) & a = p . i holds
(- p) . i = - a
let a be Element of K; ::_thesis: for p being FinSequence of the carrier of K st i in dom (- p) & a = p . i holds
(- p) . i = - a
let p be FinSequence of the carrier of K; ::_thesis: ( i in dom (- p) & a = p . i implies (- p) . i = - a )
assume ( i in dom (- p) & a = p . i ) ; ::_thesis: (- p) . i = - a
then (- p) . i = (comp K) . a by FUNCT_1:12;
hence (- p) . i = - a by VECTSP_1:def_13; ::_thesis: verum
end;
definition
let i be Element of NAT ;
let K be non empty addLoopStr ;
let R be Element of i -tuples_on the carrier of K;
:: original: -
redefine func - R -> Element of i -tuples_on the carrier of K;
coherence
- R is Element of i -tuples_on the carrier of K by FINSEQ_2:113;
end;
theorem :: FVSUM_1:23
for j, i being Element of NAT
for K being non empty addLoopStr
for a being Element of K
for R being Element of i -tuples_on the carrier of K st j in Seg i & a = R . j holds
(- R) . j = - a
proof
let j, i be Element of NAT ; ::_thesis: for K being non empty addLoopStr
for a being Element of K
for R being Element of i -tuples_on the carrier of K st j in Seg i & a = R . j holds
(- R) . j = - a
let K be non empty addLoopStr ; ::_thesis: for a being Element of K
for R being Element of i -tuples_on the carrier of K st j in Seg i & a = R . j holds
(- R) . j = - a
let a be Element of K; ::_thesis: for R being Element of i -tuples_on the carrier of K st j in Seg i & a = R . j holds
(- R) . j = - a
let R be Element of i -tuples_on the carrier of K; ::_thesis: ( j in Seg i & a = R . j implies (- R) . j = - a )
assume j in Seg i ; ::_thesis: ( not a = R . j or (- R) . j = - a )
then j in Seg (len (- R)) by CARD_1:def_7;
then j in dom (- R) by FINSEQ_1:def_3;
hence ( not a = R . j or (- R) . j = - a ) by Th22; ::_thesis: verum
end;
theorem :: FVSUM_1:24
for K being non empty addLoopStr
for a being Element of K holds - <*a*> = <*(- a)*>
proof
let K be non empty addLoopStr ; ::_thesis: for a being Element of K holds - <*a*> = <*(- a)*>
let a be Element of K; ::_thesis: - <*a*> = <*(- a)*>
thus - <*a*> = <*((comp K) . a)*> by FINSEQ_2:35
.= <*(- a)*> by VECTSP_1:def_13 ; ::_thesis: verum
end;
theorem Th25: :: FVSUM_1:25
for i being Element of NAT
for K being non empty addLoopStr
for a being Element of K holds - (i |-> a) = i |-> (- a)
proof
let i be Element of NAT ; ::_thesis: for K being non empty addLoopStr
for a being Element of K holds - (i |-> a) = i |-> (- a)
let K be non empty addLoopStr ; ::_thesis: for a being Element of K holds - (i |-> a) = i |-> (- a)
let a be Element of K; ::_thesis: - (i |-> a) = i |-> (- a)
thus - (i |-> a) = i |-> ((comp K) . a) by FINSEQOP:16
.= i |-> (- a) by VECTSP_1:def_13 ; ::_thesis: verum
end;
Lm3: for i being Element of NAT
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds R + (- R) = i |-> (0. K)
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds R + (- R) = i |-> (0. K)
let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds R + (- R) = i |-> (0. K)
let R be Element of i -tuples_on the carrier of K; ::_thesis: R + (- R) = i |-> (0. K)
A1: ( the addF of K is having_an_inverseOp & the addF of K is having_a_unity ) by Th8, Th14;
thus R + (- R) = the addF of K .: (R,((the_inverseOp_wrt the addF of K) * R)) by Th15
.= i |-> (the_unity_wrt the addF of K) by A1, FINSEQOP:73
.= i |-> (0. K) by Th7 ; ::_thesis: verum
end;
theorem Th26: :: FVSUM_1:26
for i being Element of NAT
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds
( R + (- R) = i |-> (0. K) & (- R) + R = i |-> (0. K) )
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds
( R + (- R) = i |-> (0. K) & (- R) + R = i |-> (0. K) )
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds
( R + (- R) = i |-> (0. K) & (- R) + R = i |-> (0. K) )
let R be Element of i -tuples_on the carrier of K; ::_thesis: ( R + (- R) = i |-> (0. K) & (- R) + R = i |-> (0. K) )
thus R + (- R) = i |-> (0. K) by Lm3; ::_thesis: (- R) + R = i |-> (0. K)
hence (- R) + R = i |-> (0. K) by FINSEQOP:33; ::_thesis: verum
end;
theorem Th27: :: FVSUM_1:27
for i being Element of NAT
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K st R1 + R2 = i |-> (0. K) holds
( R1 = - R2 & R2 = - R1 )
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K st R1 + R2 = i |-> (0. K) holds
( R1 = - R2 & R2 = - R1 )
let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K st R1 + R2 = i |-> (0. K) holds
( R1 = - R2 & R2 = - R1 )
let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( R1 + R2 = i |-> (0. K) implies ( R1 = - R2 & R2 = - R1 ) )
A1: ( the addF of K is having_an_inverseOp & the_inverseOp_wrt the addF of K = comp K ) by Th14, Th15;
( the_unity_wrt the addF of K = 0. K & the addF of K is having_a_unity ) by Th7, Th8;
hence ( R1 + R2 = i |-> (0. K) implies ( R1 = - R2 & R2 = - R1 ) ) by A1, FINSEQOP:74; ::_thesis: verum
end;
theorem Th28: :: FVSUM_1:28
for i being Element of NAT
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds - (- R) = R
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds - (- R) = R
let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds - (- R) = R
let R be Element of i -tuples_on the carrier of K; ::_thesis: - (- R) = R
R + (- R) = i |-> (0. K) by Lm3;
hence - (- R) = R by Th27; ::_thesis: verum
end;
theorem :: FVSUM_1:29
for i being Element of NAT
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K st - R1 = - R2 holds
R1 = R2
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K st - R1 = - R2 holds
R1 = R2
let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K st - R1 = - R2 holds
R1 = R2
let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( - R1 = - R2 implies R1 = R2 )
assume - R1 = - R2 ; ::_thesis: R1 = R2
hence R1 = - (- R2) by Th28
.= R2 by Th28 ;
::_thesis: verum
end;
Lm4: for i being Element of NAT
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R1, R, R2 being Element of i -tuples_on the carrier of K st R1 + R = R2 + R holds
R1 = R2
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R1, R, R2 being Element of i -tuples_on the carrier of K st R1 + R = R2 + R holds
R1 = R2
let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R, R2 being Element of i -tuples_on the carrier of K st R1 + R = R2 + R holds
R1 = R2
let R1, R, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( R1 + R = R2 + R implies R1 = R2 )
assume R1 + R = R2 + R ; ::_thesis: R1 = R2
then R1 + (R + (- R)) = (R2 + R) + (- R) by FINSEQOP:28;
then A1: R1 + (R + (- R)) = R2 + (R + (- R)) by FINSEQOP:28;
R + (- R) = i |-> (0. K) by Lm3;
then R1 = R2 + (i |-> (0. K)) by A1, Lm2;
hence R1 = R2 by Lm2; ::_thesis: verum
end;
theorem :: FVSUM_1:30
for i being Element of NAT
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R, R1, R2 being Element of i -tuples_on the carrier of K st ( R1 + R = R2 + R or R1 + R = R + R2 ) holds
R1 = R2
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R, R1, R2 being Element of i -tuples_on the carrier of K st ( R1 + R = R2 + R or R1 + R = R + R2 ) holds
R1 = R2
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R, R1, R2 being Element of i -tuples_on the carrier of K st ( R1 + R = R2 + R or R1 + R = R + R2 ) holds
R1 = R2
let R, R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( ( R1 + R = R2 + R or R1 + R = R + R2 ) implies R1 = R2 )
( R1 + R = R2 + R iff R1 + R = R + R2 ) by FINSEQOP:33;
hence ( ( R1 + R = R2 + R or R1 + R = R + R2 ) implies R1 = R2 ) by Lm4; ::_thesis: verum
end;
theorem Th31: :: FVSUM_1:31
for i being Element of NAT
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 + R2) = (- R1) + (- R2)
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 + R2) = (- R1) + (- R2)
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 + R2) = (- R1) + (- R2)
let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: - (R1 + R2) = (- R1) + (- R2)
(R1 + R2) + ((- R1) + (- R2)) = ((R1 + R2) + (- R1)) + (- R2) by FINSEQOP:28
.= ((R2 + R1) + (- R1)) + (- R2) by FINSEQOP:33
.= (R2 + (R1 + (- R1))) + (- R2) by FINSEQOP:28
.= (R2 + (i |-> (0. K))) + (- R2) by Lm3
.= R2 + (- R2) by Lm2
.= i |-> (0. K) by Lm3 ;
hence - (R1 + R2) = (- R1) + (- R2) by Th27; ::_thesis: verum
end;
definition
let K be non empty addLoopStr ;
let p1, p2 be FinSequence of the carrier of K;
funcp1 - p2 -> FinSequence of the carrier of K equals :: FVSUM_1:def 5
(diffield K) .: (p1,p2);
correctness
coherence
(diffield K) .: (p1,p2) is FinSequence of the carrier of K;
;
end;
:: deftheorem defines - FVSUM_1:def_5_:_
for K being non empty addLoopStr
for p1, p2 being FinSequence of the carrier of K holds p1 - p2 = (diffield K) .: (p1,p2);
theorem Th32: :: FVSUM_1:32
for i being Element of NAT
for K being non empty addLoopStr
for a1, a2 being Element of K
for p1, p2 being FinSequence of the carrier of K st i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i holds
(p1 - p2) . i = a1 - a2
proof
let i be Element of NAT ; ::_thesis: for K being non empty addLoopStr
for a1, a2 being Element of K
for p1, p2 being FinSequence of the carrier of K st i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i holds
(p1 - p2) . i = a1 - a2
let K be non empty addLoopStr ; ::_thesis: for a1, a2 being Element of K
for p1, p2 being FinSequence of the carrier of K st i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i holds
(p1 - p2) . i = a1 - a2
let a1, a2 be Element of K; ::_thesis: for p1, p2 being FinSequence of the carrier of K st i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i holds
(p1 - p2) . i = a1 - a2
let p1, p2 be FinSequence of the carrier of K; ::_thesis: ( i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i implies (p1 - p2) . i = a1 - a2 )
assume ( i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i ) ; ::_thesis: (p1 - p2) . i = a1 - a2
then (p1 - p2) . i = (diffield K) . (a1,a2) by FUNCOP_1:22;
hence (p1 - p2) . i = a1 - a2 by Th11; ::_thesis: verum
end;
definition
let i be Element of NAT ;
let K be non empty addLoopStr ;
let R1, R2 be Element of i -tuples_on the carrier of K;
:: original: -
redefine funcR1 - R2 -> Element of i -tuples_on the carrier of K;
coherence
R1 - R2 is Element of i -tuples_on the carrier of K by FINSEQ_2:120;
end;
theorem :: FVSUM_1:33
for j, i being Element of NAT
for K being non empty addLoopStr
for a1, a2 being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds
(R1 - R2) . j = a1 - a2
proof
let j, i be Element of NAT ; ::_thesis: for K being non empty addLoopStr
for a1, a2 being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds
(R1 - R2) . j = a1 - a2
let K be non empty addLoopStr ; ::_thesis: for a1, a2 being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds
(R1 - R2) . j = a1 - a2
let a1, a2 be Element of K; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds
(R1 - R2) . j = a1 - a2
let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( j in Seg i & a1 = R1 . j & a2 = R2 . j implies (R1 - R2) . j = a1 - a2 )
assume j in Seg i ; ::_thesis: ( not a1 = R1 . j or not a2 = R2 . j or (R1 - R2) . j = a1 - a2 )
then j in Seg (len (R1 - R2)) by CARD_1:def_7;
then j in dom (R1 - R2) by FINSEQ_1:def_3;
hence ( not a1 = R1 . j or not a2 = R2 . j or (R1 - R2) . j = a1 - a2 ) by Th32; ::_thesis: verum
end;
theorem :: FVSUM_1:34
for K being non empty addLoopStr
for a1, a2 being Element of K holds <*a1*> - <*a2*> = <*(a1 - a2)*>
proof
let K be non empty addLoopStr ; ::_thesis: for a1, a2 being Element of K holds <*a1*> - <*a2*> = <*(a1 - a2)*>
let a1, a2 be Element of K; ::_thesis: <*a1*> - <*a2*> = <*(a1 - a2)*>
thus <*a1*> - <*a2*> = <*((diffield K) . (a1,a2))*> by FINSEQ_2:74
.= <*(a1 - a2)*> by Th11 ; ::_thesis: verum
end;
theorem :: FVSUM_1:35
for i being Element of NAT
for K being non empty addLoopStr
for a1, a2 being Element of K holds (i |-> a1) - (i |-> a2) = i |-> (a1 - a2)
proof
let i be Element of NAT ; ::_thesis: for K being non empty addLoopStr
for a1, a2 being Element of K holds (i |-> a1) - (i |-> a2) = i |-> (a1 - a2)
let K be non empty addLoopStr ; ::_thesis: for a1, a2 being Element of K holds (i |-> a1) - (i |-> a2) = i |-> (a1 - a2)
let a1, a2 be Element of K; ::_thesis: (i |-> a1) - (i |-> a2) = i |-> (a1 - a2)
thus (i |-> a1) - (i |-> a2) = i |-> ((diffield K) . (a1,a2)) by FINSEQOP:17
.= i |-> (a1 - a2) by Th11 ; ::_thesis: verum
end;
theorem :: FVSUM_1:36
for i being Element of NAT
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds R - (i |-> (0. K)) = R
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds R - (i |-> (0. K)) = R
let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds R - (i |-> (0. K)) = R
let R be Element of i -tuples_on the carrier of K; ::_thesis: R - (i |-> (0. K)) = R
thus R - (i |-> (0. K)) = R + (- (i |-> (0. K))) by FINSEQOP:84
.= R + (i |-> (- (0. K))) by Th25
.= R + (i |-> (0. K)) by RLVECT_1:12
.= R by Lm2 ; ::_thesis: verum
end;
theorem :: FVSUM_1:37
for i being Element of NAT
for K being non empty left_zeroed Abelian right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds (i |-> (0. K)) - R = - R
proof
let i be Element of NAT ; ::_thesis: for K being non empty left_zeroed Abelian right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds (i |-> (0. K)) - R = - R
let K be non empty left_zeroed Abelian right_zeroed addLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds (i |-> (0. K)) - R = - R
let R be Element of i -tuples_on the carrier of K; ::_thesis: (i |-> (0. K)) - R = - R
thus (i |-> (0. K)) - R = (i |-> (0. K)) + (- R) by FINSEQOP:84
.= - R by Th21 ; ::_thesis: verum
end;
theorem :: FVSUM_1:38
for i being Element of NAT
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds R1 - (- R2) = R1 + R2
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds R1 - (- R2) = R1 + R2
let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K holds R1 - (- R2) = R1 + R2
let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: R1 - (- R2) = R1 + R2
thus R1 - (- R2) = R1 + (- (- R2)) by FINSEQOP:84
.= R1 + R2 by Th28 ; ::_thesis: verum
end;
theorem :: FVSUM_1:39
for i being Element of NAT
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = R2 - R1
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = R2 - R1
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = R2 - R1
let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: - (R1 - R2) = R2 - R1
thus - (R1 - R2) = - (R1 + (- R2)) by FINSEQOP:84
.= (- R1) + (- (- R2)) by Th31
.= (- R1) + R2 by Th28
.= R2 + (- R1) by FINSEQOP:33
.= R2 - R1 by FINSEQOP:84 ; ::_thesis: verum
end;
theorem Th40: :: FVSUM_1:40
for i being Element of NAT
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = (- R1) + R2
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = (- R1) + R2
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = (- R1) + R2
let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: - (R1 - R2) = (- R1) + R2
thus - (R1 - R2) = - (R1 + (- R2)) by FINSEQOP:84
.= (- R1) + (- (- R2)) by Th31
.= (- R1) + R2 by Th28 ; ::_thesis: verum
end;
theorem Th41: :: FVSUM_1:41
for i being Element of NAT
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds R - R = i |-> (0. K)
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds R - R = i |-> (0. K)
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds R - R = i |-> (0. K)
let R be Element of i -tuples_on the carrier of K; ::_thesis: R - R = i |-> (0. K)
thus R - R = R + (- R) by FINSEQOP:84
.= i |-> (0. K) by Lm3 ; ::_thesis: verum
end;
theorem :: FVSUM_1:42
for i being Element of NAT
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K st R1 - R2 = i |-> (0. K) holds
R1 = R2
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K st R1 - R2 = i |-> (0. K) holds
R1 = R2
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K st R1 - R2 = i |-> (0. K) holds
R1 = R2
let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( R1 - R2 = i |-> (0. K) implies R1 = R2 )
assume R1 - R2 = i |-> (0. K) ; ::_thesis: R1 = R2
then R1 + (- R2) = i |-> (0. K) by FINSEQOP:84;
then R1 = - (- R2) by Th27;
hence R1 = R2 by Th28; ::_thesis: verum
end;
theorem :: FVSUM_1:43
for i being Element of NAT
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2, R3 being Element of i -tuples_on the carrier of K holds (R1 - R2) - R3 = R1 - (R2 + R3)
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2, R3 being Element of i -tuples_on the carrier of K holds (R1 - R2) - R3 = R1 - (R2 + R3)
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2, R3 being Element of i -tuples_on the carrier of K holds (R1 - R2) - R3 = R1 - (R2 + R3)
let R1, R2, R3 be Element of i -tuples_on the carrier of K; ::_thesis: (R1 - R2) - R3 = R1 - (R2 + R3)
thus (R1 - R2) - R3 = (R1 - R2) + (- R3) by FINSEQOP:84
.= (R1 + (- R2)) + (- R3) by FINSEQOP:84
.= R1 + ((- R2) + (- R3)) by FINSEQOP:28
.= R1 + (- (R2 + R3)) by Th31
.= R1 - (R2 + R3) by FINSEQOP:84 ; ::_thesis: verum
end;
theorem Th44: :: FVSUM_1:44
for i being Element of NAT
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 + (R2 - R3) = (R1 + R2) - R3
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 + (R2 - R3) = (R1 + R2) - R3
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 + (R2 - R3) = (R1 + R2) - R3
let R1, R2, R3 be Element of i -tuples_on the carrier of K; ::_thesis: R1 + (R2 - R3) = (R1 + R2) - R3
thus R1 + (R2 - R3) = R1 + (R2 + (- R3)) by FINSEQOP:84
.= (R1 + R2) + (- R3) by FINSEQOP:28
.= (R1 + R2) - R3 by FINSEQOP:84 ; ::_thesis: verum
end;
theorem :: FVSUM_1:45
for i being Element of NAT
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 - (R2 - R3) = (R1 - R2) + R3
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 - (R2 - R3) = (R1 - R2) + R3
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2, R3 being Element of i -tuples_on the carrier of K holds R1 - (R2 - R3) = (R1 - R2) + R3
let R1, R2, R3 be Element of i -tuples_on the carrier of K; ::_thesis: R1 - (R2 - R3) = (R1 - R2) + R3
thus R1 - (R2 - R3) = R1 + (- (R2 - R3)) by FINSEQOP:84
.= R1 + ((- R2) + R3) by Th40
.= (R1 + (- R2)) + R3 by FINSEQOP:28
.= (R1 - R2) + R3 by FINSEQOP:84 ; ::_thesis: verum
end;
theorem :: FVSUM_1:46
for i being Element of NAT
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 + R) - R
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 + R) - R
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 + R) - R
let R1, R be Element of i -tuples_on the carrier of K; ::_thesis: R1 = (R1 + R) - R
thus R1 = R1 + (i |-> (0. K)) by Lm2
.= R1 + (R - R) by Th41
.= (R1 + R) - R by Th44 ; ::_thesis: verum
end;
theorem :: FVSUM_1:47
for i being Element of NAT
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 - R) + R
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 - R) + R
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R being Element of i -tuples_on the carrier of K holds R1 = (R1 - R) + R
let R1, R be Element of i -tuples_on the carrier of K; ::_thesis: R1 = (R1 - R) + R
thus R1 = R1 + (i |-> (0. K)) by Lm2
.= R1 + ((- R) + R) by Th26
.= (R1 + (- R)) + R by FINSEQOP:28
.= (R1 - R) + R by FINSEQOP:84 ; ::_thesis: verum
end;
theorem Th48: :: FVSUM_1:48
for K being non empty multMagma
for a, b being Element of K holds ( the multF of K [;] (a,(id the carrier of K))) . b = a * b
proof
let K be non empty multMagma ; ::_thesis: for a, b being Element of K holds ( the multF of K [;] (a,(id the carrier of K))) . b = a * b
let a, b be Element of K; ::_thesis: ( the multF of K [;] (a,(id the carrier of K))) . b = a * b
thus ( the multF of K [;] (a,(id the carrier of K))) . b = the multF of K . (a,((id the carrier of K) . b)) by FUNCOP_1:53
.= a * b by FUNCT_1:18 ; ::_thesis: verum
end;
theorem :: FVSUM_1:49
for K being non empty multMagma
for a, b being Element of K holds (a multfield) . b = a * b by Th48;
definition
let K be non empty multMagma ;
let p be FinSequence of the carrier of K;
let a be Element of K;
funca * p -> FinSequence of the carrier of K equals :: FVSUM_1:def 6
(a multfield) * p;
correctness
coherence
(a multfield) * p is FinSequence of the carrier of K;
;
end;
:: deftheorem defines * FVSUM_1:def_6_:_
for K being non empty multMagma
for p being FinSequence of the carrier of K
for a being Element of K holds a * p = (a multfield) * p;
theorem Th50: :: FVSUM_1:50
for i being Element of NAT
for K being non empty multMagma
for a, a9 being Element of K
for p being FinSequence of the carrier of K st i in dom (a * p) & a9 = p . i holds
(a * p) . i = a * a9
proof
let i be Element of NAT ; ::_thesis: for K being non empty multMagma
for a, a9 being Element of K
for p being FinSequence of the carrier of K st i in dom (a * p) & a9 = p . i holds
(a * p) . i = a * a9
let K be non empty multMagma ; ::_thesis: for a, a9 being Element of K
for p being FinSequence of the carrier of K st i in dom (a * p) & a9 = p . i holds
(a * p) . i = a * a9
let a, a9 be Element of K; ::_thesis: for p being FinSequence of the carrier of K st i in dom (a * p) & a9 = p . i holds
(a * p) . i = a * a9
let p be FinSequence of the carrier of K; ::_thesis: ( i in dom (a * p) & a9 = p . i implies (a * p) . i = a * a9 )
assume A1: ( i in dom (a * p) & a9 = p . i ) ; ::_thesis: (a * p) . i = a * a9
then A2: a9 in dom ( the multF of K [;] (a,(id the carrier of K))) by FUNCT_1:11;
thus (a * p) . i = ( the multF of K [;] (a,(id the carrier of K))) . a9 by A1, FUNCT_1:12
.= the multF of K . (a,((id the carrier of K) . a9)) by A2, FUNCOP_1:32
.= a * a9 by FUNCT_1:18 ; ::_thesis: verum
end;
definition
let i be Element of NAT ;
let K be non empty multMagma ;
let R be Element of i -tuples_on the carrier of K;
let a be Element of K;
:: original: *
redefine funca * R -> Element of i -tuples_on the carrier of K;
coherence
a * R is Element of i -tuples_on the carrier of K by FINSEQ_2:113;
end;
theorem :: FVSUM_1:51
for j, i being Element of NAT
for K being non empty multMagma
for a9, a being Element of K
for R being Element of i -tuples_on the carrier of K st j in Seg i & a9 = R . j holds
(a * R) . j = a * a9
proof
let j, i be Element of NAT ; ::_thesis: for K being non empty multMagma
for a9, a being Element of K
for R being Element of i -tuples_on the carrier of K st j in Seg i & a9 = R . j holds
(a * R) . j = a * a9
let K be non empty multMagma ; ::_thesis: for a9, a being Element of K
for R being Element of i -tuples_on the carrier of K st j in Seg i & a9 = R . j holds
(a * R) . j = a * a9
let a9, a be Element of K; ::_thesis: for R being Element of i -tuples_on the carrier of K st j in Seg i & a9 = R . j holds
(a * R) . j = a * a9
let R be Element of i -tuples_on the carrier of K; ::_thesis: ( j in Seg i & a9 = R . j implies (a * R) . j = a * a9 )
assume j in Seg i ; ::_thesis: ( not a9 = R . j or (a * R) . j = a * a9 )
then j in Seg (len (a * R)) by CARD_1:def_7;
then j in dom (a * R) by FINSEQ_1:def_3;
hence ( not a9 = R . j or (a * R) . j = a * a9 ) by Th50; ::_thesis: verum
end;
theorem :: FVSUM_1:52
for K being non empty multMagma
for a, a1 being Element of K holds a * <*a1*> = <*(a * a1)*>
proof
let K be non empty multMagma ; ::_thesis: for a, a1 being Element of K holds a * <*a1*> = <*(a * a1)*>
let a, a1 be Element of K; ::_thesis: a * <*a1*> = <*(a * a1)*>
thus a * <*a1*> = <*(( the multF of K [;] (a,(id the carrier of K))) . a1)*> by FINSEQ_2:35
.= <*(a * a1)*> by Th48 ; ::_thesis: verum
end;
theorem Th53: :: FVSUM_1:53
for i being Element of NAT
for K being non empty multMagma
for a1, a2 being Element of K holds a1 * (i |-> a2) = i |-> (a1 * a2)
proof
let i be Element of NAT ; ::_thesis: for K being non empty multMagma
for a1, a2 being Element of K holds a1 * (i |-> a2) = i |-> (a1 * a2)
let K be non empty multMagma ; ::_thesis: for a1, a2 being Element of K holds a1 * (i |-> a2) = i |-> (a1 * a2)
let a1, a2 be Element of K; ::_thesis: a1 * (i |-> a2) = i |-> (a1 * a2)
thus a1 * (i |-> a2) = i |-> (( the multF of K [;] (a1,(id the carrier of K))) . a2) by FINSEQOP:16
.= i |-> (a1 * a2) by Th48 ; ::_thesis: verum
end;
theorem :: FVSUM_1:54
for i being Element of NAT
for K being non empty associative multMagma
for a1, a2 being Element of K
for R being Element of i -tuples_on the carrier of K holds (a1 * a2) * R = a1 * (a2 * R)
proof
let i be Element of NAT ; ::_thesis: for K being non empty associative multMagma
for a1, a2 being Element of K
for R being Element of i -tuples_on the carrier of K holds (a1 * a2) * R = a1 * (a2 * R)
let K be non empty associative multMagma ; ::_thesis: for a1, a2 being Element of K
for R being Element of i -tuples_on the carrier of K holds (a1 * a2) * R = a1 * (a2 * R)
let a1, a2 be Element of K; ::_thesis: for R being Element of i -tuples_on the carrier of K holds (a1 * a2) * R = a1 * (a2 * R)
let R be Element of i -tuples_on the carrier of K; ::_thesis: (a1 * a2) * R = a1 * (a2 * R)
set F = the multF of K;
set f = id the carrier of K;
thus (a1 * a2) * R = ( the multF of K [;] (a1,( the multF of K [;] (a2,(id the carrier of K))))) * R by FUNCOP_1:62
.= (( the multF of K [;] (a1,(id the carrier of K))) * ( the multF of K [;] (a2,(id the carrier of K)))) * R by FUNCOP_1:55
.= a1 * (a2 * R) by RELAT_1:36 ; ::_thesis: verum
end;
theorem :: FVSUM_1:55
for i being Element of NAT
for K being non empty distributive doubleLoopStr
for a1, a2 being Element of K
for R being Element of i -tuples_on the carrier of K holds (a1 + a2) * R = (a1 * R) + (a2 * R)
proof
let i be Element of NAT ; ::_thesis: for K being non empty distributive doubleLoopStr
for a1, a2 being Element of K
for R being Element of i -tuples_on the carrier of K holds (a1 + a2) * R = (a1 * R) + (a2 * R)
let K be non empty distributive doubleLoopStr ; ::_thesis: for a1, a2 being Element of K
for R being Element of i -tuples_on the carrier of K holds (a1 + a2) * R = (a1 * R) + (a2 * R)
let a1, a2 be Element of K; ::_thesis: for R being Element of i -tuples_on the carrier of K holds (a1 + a2) * R = (a1 * R) + (a2 * R)
let R be Element of i -tuples_on the carrier of K; ::_thesis: (a1 + a2) * R = (a1 * R) + (a2 * R)
thus (a1 + a2) * R = ( the addF of K .: (( the multF of K [;] (a1,(id the carrier of K))),( the multF of K [;] (a2,(id the carrier of K))))) * R by Th10, FINSEQOP:35
.= (a1 * R) + (a2 * R) by FUNCOP_1:25 ; ::_thesis: verum
end;
theorem :: FVSUM_1:56
for i being Element of NAT
for K being non empty distributive doubleLoopStr
for a being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K holds a * (R1 + R2) = (a * R1) + (a * R2) by Th12, FINSEQOP:51;
theorem :: FVSUM_1:57
for i being Element of NAT
for K being non empty commutative distributive left_unital doubleLoopStr
for R being Element of i -tuples_on the carrier of K holds (1. K) * R = R
proof
let i be Element of NAT ; ::_thesis: for K being non empty commutative distributive left_unital doubleLoopStr
for R being Element of i -tuples_on the carrier of K holds (1. K) * R = R
let K be non empty commutative distributive left_unital doubleLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds (1. K) * R = R
let R be Element of i -tuples_on the carrier of K; ::_thesis: (1. K) * R = R
A1: rng R c= the carrier of K by FINSEQ_1:def_4;
the_unity_wrt the multF of K = 1. K by Th5;
hence (1. K) * R = (id the carrier of K) * R by FINSEQOP:44
.= R by A1, RELAT_1:53 ;
::_thesis: verum
end;
theorem :: FVSUM_1:58
for i being Element of NAT
for K being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for R being Element of i -tuples_on the carrier of K holds (0. K) * R = i |-> (0. K)
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for R being Element of i -tuples_on the carrier of K holds (0. K) * R = i |-> (0. K)
let K be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds (0. K) * R = i |-> (0. K)
let R be Element of i -tuples_on the carrier of K; ::_thesis: (0. K) * R = i |-> (0. K)
A1: rng R c= the carrier of K by FINSEQ_1:def_4;
A2: the addF of K is having_an_inverseOp by Th14;
A3: ( the_unity_wrt the addF of K = 0. K & the addF of K is having_a_unity ) by Th7, Th8;
thus (0. K) * R = the multF of K [;] ((0. K),((id the carrier of K) * R)) by FUNCOP_1:34
.= the multF of K [;] ((0. K),R) by A1, RELAT_1:53
.= i |-> (0. K) by A3, A2, Th10, FINSEQOP:76 ; ::_thesis: verum
end;
theorem :: FVSUM_1:59
for i being Element of NAT
for K being non empty right_complementable commutative add-associative right_zeroed distributive left_unital doubleLoopStr
for R being Element of i -tuples_on the carrier of K holds (- (1. K)) * R = - R
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable commutative add-associative right_zeroed distributive left_unital doubleLoopStr
for R being Element of i -tuples_on the carrier of K holds (- (1. K)) * R = - R
let K be non empty right_complementable commutative add-associative right_zeroed distributive left_unital doubleLoopStr ; ::_thesis: for R being Element of i -tuples_on the carrier of K holds (- (1. K)) * R = - R
let R be Element of i -tuples_on the carrier of K; ::_thesis: (- (1. K)) * R = - R
A1: ( (comp K) . (1. K) = - (1. K) & the_unity_wrt the multF of K = 1. K ) by Th5, VECTSP_1:def_13;
A2: ( the addF of K is having_an_inverseOp & the_inverseOp_wrt the addF of K = comp K ) by Th14, Th15;
( the multF of K is having_a_unity & the addF of K is having_a_unity ) by Th8;
hence (- (1. K)) * R = - R by A1, A2, Th10, FINSEQOP:68; ::_thesis: verum
end;
definition
let M be non empty multMagma ;
let p1, p2 be FinSequence of the carrier of M;
func mlt (p1,p2) -> FinSequence of the carrier of M equals :: FVSUM_1:def 7
the multF of M .: (p1,p2);
correctness
coherence
the multF of M .: (p1,p2) is FinSequence of the carrier of M;
;
end;
:: deftheorem defines mlt FVSUM_1:def_7_:_
for M being non empty multMagma
for p1, p2 being FinSequence of the carrier of M holds mlt (p1,p2) = the multF of M .: (p1,p2);
theorem :: FVSUM_1:60
for i being Element of NAT
for K being non empty multMagma
for a1, a2 being Element of K
for p1, p2 being FinSequence of the carrier of K st i in dom (mlt (p1,p2)) & a1 = p1 . i & a2 = p2 . i holds
(mlt (p1,p2)) . i = a1 * a2 by FUNCOP_1:22;
definition
let i be Element of NAT ;
let K be non empty multMagma ;
let R1, R2 be Element of i -tuples_on the carrier of K;
:: original: mlt
redefine func mlt (R1,R2) -> Element of i -tuples_on the carrier of K;
coherence
mlt (R1,R2) is Element of i -tuples_on the carrier of K by FINSEQ_2:120;
end;
theorem :: FVSUM_1:61
for j, i being Element of NAT
for K being non empty multMagma
for a1, a2 being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds
(mlt (R1,R2)) . j = a1 * a2
proof
let j, i be Element of NAT ; ::_thesis: for K being non empty multMagma
for a1, a2 being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds
(mlt (R1,R2)) . j = a1 * a2
let K be non empty multMagma ; ::_thesis: for a1, a2 being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds
(mlt (R1,R2)) . j = a1 * a2
let a1, a2 be Element of K; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds
(mlt (R1,R2)) . j = a1 * a2
let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( j in Seg i & a1 = R1 . j & a2 = R2 . j implies (mlt (R1,R2)) . j = a1 * a2 )
assume j in Seg i ; ::_thesis: ( not a1 = R1 . j or not a2 = R2 . j or (mlt (R1,R2)) . j = a1 * a2 )
then j in Seg (len (mlt (R1,R2))) by CARD_1:def_7;
then j in dom (mlt (R1,R2)) by FINSEQ_1:def_3;
hence ( not a1 = R1 . j or not a2 = R2 . j or (mlt (R1,R2)) . j = a1 * a2 ) by FUNCOP_1:22; ::_thesis: verum
end;
theorem :: FVSUM_1:62
for K being non empty multMagma
for a1, a2 being Element of K holds mlt (<*a1*>,<*a2*>) = <*(a1 * a2)*> by FINSEQ_2:74;
Lm5: for K being non empty multMagma
for a1, a2, b1, b2 being Element of K holds mlt (<*a1,a2*>,<*b1,b2*>) = <*(a1 * b1),(a2 * b2)*>
proof
let K be non empty multMagma ; ::_thesis: for a1, a2, b1, b2 being Element of K holds mlt (<*a1,a2*>,<*b1,b2*>) = <*(a1 * b1),(a2 * b2)*>
let a1, a2, b1, b2 be Element of K; ::_thesis: mlt (<*a1,a2*>,<*b1,b2*>) = <*(a1 * b1),(a2 * b2)*>
( <*a1,a2*> = <*a1*> ^ <*a2*> & <*b1,b2*> = <*b1*> ^ <*b2*> ) by FINSEQ_1:def_9;
hence mlt (<*a1,a2*>,<*b1,b2*>) = (mlt (<*a1*>,<*b1*>)) ^ <*(a2 * b2)*> by FINSEQOP:10
.= <*(a1 * b1)*> ^ <*(a2 * b2)*> by FINSEQ_2:74
.= <*(a1 * b1),(a2 * b2)*> by FINSEQ_1:def_9 ;
::_thesis: verum
end;
theorem :: FVSUM_1:63
for i being Element of NAT
for K being non empty commutative multMagma
for R1, R2 being Element of i -tuples_on the carrier of K holds mlt (R1,R2) = mlt (R2,R1) by FINSEQOP:33;
theorem Th64: :: FVSUM_1:64
for K being non empty commutative multMagma
for p, q being FinSequence of the carrier of K holds mlt (p,q) = mlt (q,p)
proof
let K be non empty commutative multMagma ; ::_thesis: for p, q being FinSequence of the carrier of K holds mlt (p,q) = mlt (q,p)
let p, q be FinSequence of the carrier of K; ::_thesis: mlt (p,q) = mlt (q,p)
reconsider r = mlt (p,q) as FinSequence of the carrier of K ;
reconsider s = mlt (q,p) as FinSequence of the carrier of K ;
reconsider k = min ((len p),(len q)) as Element of NAT by XXREAL_0:15;
A1: len r = min ((len p),(len q)) by FINSEQ_2:71;
then A2: dom r = Seg k by FINSEQ_1:def_3;
min ((len p),(len q)) <= len q by XXREAL_0:17;
then Seg k c= Seg (len q) by FINSEQ_1:5;
then A3: Seg k c= dom q by FINSEQ_1:def_3;
min ((len p),(len q)) <= len p by XXREAL_0:17;
then Seg k c= Seg (len p) by FINSEQ_1:5;
then A4: Seg k c= dom p by FINSEQ_1:def_3;
A5: len s = min ((len q),(len p)) by FINSEQ_2:71;
then A6: dom s = Seg k by FINSEQ_1:def_3;
A7: dom r = Seg k by A1, FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_r_holds_
r_._i_=_s_._i
let i be Nat; ::_thesis: ( i in dom r implies r . i = s . i )
assume A8: i in dom r ; ::_thesis: r . i = s . i
then reconsider d1 = p . i, d2 = q . i as Element of K by A4, A3, A2, FINSEQ_2:11;
thus r . i = d1 * d2 by A8, FUNCOP_1:22
.= d2 * d1
.= s . i by A7, A6, A8, FUNCOP_1:22 ; ::_thesis: verum
end;
hence mlt (p,q) = mlt (q,p) by A1, A5, FINSEQ_2:9; ::_thesis: verum
end;
theorem :: FVSUM_1:65
for i being Element of NAT
for K being non empty associative multMagma
for R1, R2, R3 being Element of i -tuples_on the carrier of K holds mlt (R1,(mlt (R2,R3))) = mlt ((mlt (R1,R2)),R3) by FINSEQOP:28;
theorem Th66: :: FVSUM_1:66
for i being Element of NAT
for K being non empty associative commutative multMagma
for a being Element of K
for R being Element of i -tuples_on the carrier of K holds
( mlt ((i |-> a),R) = a * R & mlt (R,(i |-> a)) = a * R )
proof
let i be Element of NAT ; ::_thesis: for K being non empty associative commutative multMagma
for a being Element of K
for R being Element of i -tuples_on the carrier of K holds
( mlt ((i |-> a),R) = a * R & mlt (R,(i |-> a)) = a * R )
let K be non empty associative commutative multMagma ; ::_thesis: for a being Element of K
for R being Element of i -tuples_on the carrier of K holds
( mlt ((i |-> a),R) = a * R & mlt (R,(i |-> a)) = a * R )
let a be Element of K; ::_thesis: for R being Element of i -tuples_on the carrier of K holds
( mlt ((i |-> a),R) = a * R & mlt (R,(i |-> a)) = a * R )
let R be Element of i -tuples_on the carrier of K; ::_thesis: ( mlt ((i |-> a),R) = a * R & mlt (R,(i |-> a)) = a * R )
thus mlt ((i |-> a),R) = the multF of K [;] (a,R) by FINSEQOP:20
.= a * R by FINSEQOP:22 ; ::_thesis: mlt (R,(i |-> a)) = a * R
hence mlt (R,(i |-> a)) = a * R by FINSEQOP:33; ::_thesis: verum
end;
theorem :: FVSUM_1:67
for i being Element of NAT
for K being non empty associative commutative multMagma
for a1, a2 being Element of K holds mlt ((i |-> a1),(i |-> a2)) = i |-> (a1 * a2)
proof
let i be Element of NAT ; ::_thesis: for K being non empty associative commutative multMagma
for a1, a2 being Element of K holds mlt ((i |-> a1),(i |-> a2)) = i |-> (a1 * a2)
let K be non empty associative commutative multMagma ; ::_thesis: for a1, a2 being Element of K holds mlt ((i |-> a1),(i |-> a2)) = i |-> (a1 * a2)
let a1, a2 be Element of K; ::_thesis: mlt ((i |-> a1),(i |-> a2)) = i |-> (a1 * a2)
thus mlt ((i |-> a1),(i |-> a2)) = a1 * (i |-> a2) by Th66
.= i |-> (a1 * a2) by Th53 ; ::_thesis: verum
end;
theorem :: FVSUM_1:68
for i being Element of NAT
for K being non empty associative multMagma
for a being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K holds a * (mlt (R1,R2)) = mlt ((a * R1),R2) by FINSEQOP:26;
theorem :: FVSUM_1:69
for i being Element of NAT
for K being non empty associative commutative multMagma
for a being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K holds
( a * (mlt (R1,R2)) = mlt ((a * R1),R2) & a * (mlt (R1,R2)) = mlt (R1,(a * R2)) )
proof
let i be Element of NAT ; ::_thesis: for K being non empty associative commutative multMagma
for a being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K holds
( a * (mlt (R1,R2)) = mlt ((a * R1),R2) & a * (mlt (R1,R2)) = mlt (R1,(a * R2)) )
let K be non empty associative commutative multMagma ; ::_thesis: for a being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K holds
( a * (mlt (R1,R2)) = mlt ((a * R1),R2) & a * (mlt (R1,R2)) = mlt (R1,(a * R2)) )
let a be Element of K; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K holds
( a * (mlt (R1,R2)) = mlt ((a * R1),R2) & a * (mlt (R1,R2)) = mlt (R1,(a * R2)) )
let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: ( a * (mlt (R1,R2)) = mlt ((a * R1),R2) & a * (mlt (R1,R2)) = mlt (R1,(a * R2)) )
thus a * (mlt (R1,R2)) = mlt ((a * R1),R2) by FINSEQOP:26; ::_thesis: a * (mlt (R1,R2)) = mlt (R1,(a * R2))
thus a * (mlt (R1,R2)) = a * (mlt (R2,R1)) by FINSEQOP:33
.= mlt ((a * R2),R1) by FINSEQOP:26
.= mlt (R1,(a * R2)) by FINSEQOP:33 ; ::_thesis: verum
end;
theorem :: FVSUM_1:70
for i being Element of NAT
for K being non empty associative commutative multMagma
for a being Element of K
for R being Element of i -tuples_on the carrier of K holds a * R = mlt ((i |-> a),R) by Th66;
begin
registration
cluster non empty Abelian right_zeroed -> non empty left_zeroed for addLoopStr ;
coherence
for b1 being non empty addLoopStr st b1 is Abelian & b1 is right_zeroed holds
b1 is left_zeroed
proof
let L be non empty addLoopStr ; ::_thesis: ( L is Abelian & L is right_zeroed implies L is left_zeroed )
assume that
A1: L is Abelian and
A2: L is right_zeroed ; ::_thesis: L is left_zeroed
let x be Element of L; :: according to ALGSTR_1:def_2 ::_thesis: (0. L) + x = x
thus (0. L) + x = x + (0. L) by A1, RLVECT_1:def_2
.= x by A2, RLVECT_1:def_4 ; ::_thesis: verum
end;
end;
definition
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;
let p be FinSequence of the carrier of K;
redefine func Sum p equals :: FVSUM_1:def 8
the addF of K $$ p;
compatibility
for b1 being Element of the carrier of K holds
( b1 = Sum p iff b1 = the addF of K $$ p )
proof
set q = <*> the carrier of K;
deffunc H1( Element of NAT ) -> Element of the carrier of K = the addF of K $$ (p | $1);
let s be Element of K; ::_thesis: ( s = Sum p iff s = the addF of K $$ p )
consider f being Function of NAT, the carrier of K such that
A1: for i being Element of NAT holds f . i = H1(i) from FUNCT_2:sch_4();
hereby ::_thesis: ( s = the addF of K $$ p implies s = Sum p )
defpred S1[ set , set ] means ex q being FinSequence of the carrier of K st
( q = p * (Sgm (dom (p | $1))) & $2 = Sum q );
assume A2: s = Sum p ; ::_thesis: s = the addF of K $$ p
A3: for x being Element of Fin NAT ex y being Element of K st S1[x,y]
proof
let B be Element of Fin NAT; ::_thesis: ex y being Element of K st S1[B,y]
percases ( dom p = {} or dom p <> {} ) ;
supposeA4: dom p = {} ; ::_thesis: ex y being Element of K st S1[B,y]
reconsider u = Sum (<*> the carrier of K) as Element of K ;
reconsider q = <*> the carrier of K as FinSequence of the carrier of K ;
take u ; ::_thesis: S1[B,u]
take q ; ::_thesis: ( q = p * (Sgm (dom (p | B))) & u = Sum q )
p = {} by A4;
hence q = p * (Sgm (dom (p | B))) ; ::_thesis: u = Sum q
thus u = Sum q ; ::_thesis: verum
end;
suppose dom p <> {} ; ::_thesis: ex y being Element of K st S1[B,y]
then reconsider domp = dom p as non empty set ;
reconsider p9 = p as Function of domp, the carrier of K by FINSEQ_2:26;
A5: dom (p | B) c= dom p by RELAT_1:60;
reconsider pB = p | B as FinSubsequence ;
rng (Sgm (dom pB)) = dom pB by FINSEQ_1:50;
then reconsider p99 = Sgm (dom (p | B)) as FinSequence of domp by A5, FINSEQ_1:def_4;
reconsider q = p9 * p99 as FinSequence of the carrier of K ;
reconsider u = Sum q as Element of K ;
take u ; ::_thesis: S1[B,u]
take q ; ::_thesis: ( q = p * (Sgm (dom (p | B))) & u = Sum q )
thus ( q = p * (Sgm (dom (p | B))) & u = Sum q ) ; ::_thesis: verum
end;
end;
end;
consider G being Function of (Fin NAT), the carrier of K such that
A6: for B being Element of Fin NAT holds S1[B,G . B] from FUNCT_2:sch_3(A3);
A7: now__::_thesis:_for_B9_being_Element_of_Fin_NAT_st_B9_c=_dom_p_&_B9_<>_{}_holds_
for_x_being_Element_of_NAT_st_x_in_(dom_p)_\_B9_holds_
G_._(B9_\/_{x})_=_the_addF_of_K_._((G_._B9),(([#]_(p,(the_unity_wrt_the_addF_of_K)))_._x))
let B9 be Element of Fin NAT; ::_thesis: ( B9 c= dom p & B9 <> {} implies for x being Element of NAT st x in (dom p) \ B9 holds
G . (B9 \/ {x}) = the addF of K . ((G . B9),(([#] (p,(the_unity_wrt the addF of K))) . x)) )
assume that
B9 c= dom p and
B9 <> {} ; ::_thesis: for x being Element of NAT st x in (dom p) \ B9 holds
G . (B9 \/ {x}) = the addF of K . ((G . B9),(([#] (p,(the_unity_wrt the addF of K))) . x))
let x be Element of NAT ; ::_thesis: ( x in (dom p) \ B9 implies G . (B9 \/ {x}) = the addF of K . ((G . B9),(([#] (p,(the_unity_wrt the addF of K))) . x)) )
set f2 = Sgm (dom (p | (B9 \/ {x})));
set f3 = (Sgm (dom (p | (B9 \/ {x})))) -| x;
set f4 = (Sgm (dom (p | (B9 \/ {x})))) |-- x;
reconsider Y = (finSeg (len (Sgm (dom (p | (B9 \/ {x})))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x}) as finite set ;
A8: Seg (len (Sgm (dom (p | (B9 \/ {x}))))) = dom (Sgm (dom (p | (B9 \/ {x})))) by FINSEQ_1:def_3;
set R = rng ((Sgm (dom (p | (B9 \/ {x})))) | Y);
set M = (Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y);
A9: rng (Sgm Y) = Y by FINSEQ_1:def_13;
dom (Sgm Y) = finSeg (card Y) by FINSEQ_3:40;
then dom ((Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y)) = Seg (card Y) by A8, A9, RELAT_1:27;
then reconsider M = (Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y) as FinSequence by FINSEQ_1:def_2;
( rng (Sgm (dom (p | (B9 \/ {x})))) c= NAT & rng M c= rng (Sgm (dom (p | (B9 \/ {x})))) ) by FINSEQ_1:def_4, RELAT_1:26;
then rng M c= NAT by XBOOLE_1:1;
then reconsider L = (Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y) as FinSequence of NAT by FINSEQ_1:def_4;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_rng_L_implies_y_in_rng_((Sgm_(dom_(p_|_(B9_\/_{x}))))_|_Y)_)_&_(_y_in_rng_((Sgm_(dom_(p_|_(B9_\/_{x}))))_|_Y)_implies_y_in_rng_L_)_)
let y be set ; ::_thesis: ( ( y in rng L implies y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) ) & ( y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) implies y in rng L ) )
hereby ::_thesis: ( y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) implies y in rng L )
assume y in rng L ; ::_thesis: y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y)
then consider x being set such that
A10: x in dom L and
A11: y = L . x by FUNCT_1:def_3;
x in dom (Sgm Y) by A10, FUNCT_1:11;
then A12: (Sgm Y) . x in Y by A9, FUNCT_1:def_3;
y = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . x) by A10, A11, FUNCT_1:12;
hence y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) by A8, A12, FUNCT_1:50; ::_thesis: verum
end;
assume y in rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) ; ::_thesis: y in rng L
then consider x being set such that
A13: x in dom ((Sgm (dom (p | (B9 \/ {x})))) | Y) and
A14: y = ((Sgm (dom (p | (B9 \/ {x})))) | Y) . x by FUNCT_1:def_3;
A15: x in (dom (Sgm (dom (p | (B9 \/ {x}))))) /\ Y by A13, RELAT_1:61;
then A16: x in Y by XBOOLE_0:def_4;
then consider z being set such that
A17: z in dom (Sgm Y) and
A18: x = (Sgm Y) . z by A9, FUNCT_1:def_3;
x in dom (Sgm (dom (p | (B9 \/ {x})))) by A15, XBOOLE_0:def_4;
then A19: z in dom ((Sgm (dom (p | (B9 \/ {x})))) * (Sgm Y)) by A17, A18, FUNCT_1:11;
then L . z = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . z) by FUNCT_1:12
.= y by A14, A16, A18, FUNCT_1:49 ;
hence y in rng L by A19, FUNCT_1:def_3; ::_thesis: verum
end;
then A20: rng L = rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) by TARSKI:1;
x in {x} by TARSKI:def_1;
then A21: x in B9 \/ {x} by XBOOLE_0:def_3;
dom (p | (B9 \/ {x})) = (dom p) /\ (B9 \/ {x}) by RELAT_1:61;
then dom (p | (B9 \/ {x})) c= dom p by XBOOLE_1:17;
then A22: dom (p | (B9 \/ {x})) c= Seg (len p) by FINSEQ_1:def_3;
reconsider pB9x = p | (B9 \/ {x}) as FinSubsequence ;
rng (Sgm (dom (p | (B9 \/ {x})))) c= Seg (len p) by A22, FINSEQ_1:def_13;
then A23: rng (Sgm (dom (p | (B9 \/ {x})))) c= dom p by FINSEQ_1:def_3;
rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) c= rng (Sgm (dom (p | (B9 \/ {x})))) by RELAT_1:70;
then rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) c= dom p by A23, XBOOLE_1:1;
then A24: rng ((Sgm (dom (p | (B9 \/ {x})))) | Y) c= Seg (len p) by FINSEQ_1:def_3;
reconsider pp = p | (B9 \/ {x}) as FinSubsequence ;
A25: dom (p | B9) = (dom p) /\ B9 by RELAT_1:61;
A26: now__::_thesis:_for_l,_m,_k1,_k2_being_Nat_st_1_<=_l_&_l_<_m_&_m_<=_len_L_&_k1_=_L_._l_&_k2_=_L_._m_holds_
k1_<_k2
let l, m, k1, k2 be Nat; ::_thesis: ( 1 <= l & l < m & m <= len L & k1 = L . l & k2 = L . m implies k1 < k2 )
assume that
A27: 1 <= l and
A28: l < m and
A29: m <= len L and
A30: ( k1 = L . l & k2 = L . m ) ; ::_thesis: k1 < k2
l <= len L by A28, A29, XXREAL_0:2;
then A31: l in dom L by A27, FINSEQ_3:25;
then A32: L . l = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . l) by FUNCT_1:12;
A33: (Sgm Y) . l in dom (Sgm (dom (p | (B9 \/ {x})))) by A31, FUNCT_1:11;
1 <= m by A27, A28, XXREAL_0:2;
then A34: m in dom L by A29, FINSEQ_3:25;
then A35: L . m = (Sgm (dom (p | (B9 \/ {x})))) . ((Sgm Y) . m) by FUNCT_1:12;
m in dom (Sgm Y) by A34, FUNCT_1:11;
then A36: m <= len (Sgm Y) by FINSEQ_3:25;
A37: (Sgm Y) . m in dom (Sgm (dom (p | (B9 \/ {x})))) by A34, FUNCT_1:11;
reconsider l = l, m = m as Element of NAT by ORDINAL1:def_12;
reconsider K1 = (Sgm Y) . l, K2 = (Sgm Y) . m as Element of NAT by A33, A37;
A38: 1 <= K1 by A33, FINSEQ_3:25;
A39: K2 <= len (Sgm (dom (p | (B9 \/ {x})))) by A37, FINSEQ_3:25;
K1 < K2 by A27, A28, A36, FINSEQ_1:def_13;
hence k1 < k2 by A22, A30, A32, A35, A38, A39, FINSEQ_1:def_13; ::_thesis: verum
end;
assume A40: x in (dom p) \ B9 ; ::_thesis: G . (B9 \/ {x}) = the addF of K . ((G . B9),(([#] (p,(the_unity_wrt the addF of K))) . x))
then A41: x in dom p by XBOOLE_0:def_5;
then reconsider D = dom p, E = rng p as non empty set by RELAT_1:42;
x in dom p by A40, XBOOLE_0:def_5;
then A42: {x} c= dom p by ZFMISC_1:31;
p . x = p /. x by A41, PARTFUN1:def_6;
then reconsider px = p . x as Element of K ;
A43: dom <*px*> = Seg 1 by FINSEQ_1:38;
rng <*x*> = {x} by FINSEQ_1:38;
then ( dom <*x*> = Seg 1 & rng <*x*> c= dom p ) by A41, FINSEQ_1:38, ZFMISC_1:31;
then A44: dom (p * <*x*>) = dom <*px*> by A43, RELAT_1:27;
A45: now__::_thesis:_for_e_being_set_st_e_in_dom_<*px*>_holds_
(p_*_<*x*>)_._e_=_<*px*>_._e
let e be set ; ::_thesis: ( e in dom <*px*> implies (p * <*x*>) . e = <*px*> . e )
assume A46: e in dom <*px*> ; ::_thesis: (p * <*x*>) . e = <*px*> . e
then A47: e = 1 by A43, FINSEQ_1:2, TARSKI:def_1;
thus (p * <*x*>) . e = p . (<*x*> . e) by A44, A46, FUNCT_1:12
.= p . x by A47, FINSEQ_1:40
.= <*px*> . e by A47, FINSEQ_1:40 ; ::_thesis: verum
end;
reconsider x9 = x as Element of D by A40, XBOOLE_0:def_5;
reconsider p9 = p as Function of D,E by FUNCT_2:1;
A48: E c= the carrier of K by FINSEQ_1:def_4;
not x in B9 by A40, XBOOLE_0:def_5;
then A49: not x in dom (p | B9) by A25, XBOOLE_0:def_4;
A50: rng (Sgm (dom pp)) = dom pp by FINSEQ_1:50;
then A51: rng (Sgm (dom (p | (B9 \/ {x})))) c= dom p by RELAT_1:60;
dom pp = (dom p) /\ (B9 \/ {x}) by RELAT_1:61;
then A52: x in rng (Sgm (dom (p | (B9 \/ {x})))) by A50, A41, A21, XBOOLE_0:def_4;
then rng ((Sgm (dom (p | (B9 \/ {x})))) |-- x) c= rng (Sgm (dom (p | (B9 \/ {x})))) by FINSEQ_4:44;
then A53: rng ((Sgm (dom (p | (B9 \/ {x})))) |-- x) c= D by A51, XBOOLE_1:1;
rng ((Sgm (dom (p | (B9 \/ {x})))) -| x) c= rng (Sgm (dom (p | (B9 \/ {x})))) by A52, FINSEQ_4:39;
then rng ((Sgm (dom (p | (B9 \/ {x})))) -| x) c= D by A51, XBOOLE_1:1;
then reconsider f39 = (Sgm (dom (p | (B9 \/ {x})))) -| x, f49 = (Sgm (dom (p | (B9 \/ {x})))) |-- x as FinSequence of D by A53, FINSEQ_1:def_4;
consider q2 being FinSequence of the carrier of K such that
A54: q2 = p * (Sgm (dom (p | (B9 \/ {x})))) and
A55: G . (B9 \/ {.x.}) = Sum q2 by A6;
reconsider p3 = p9 * f39, p4 = p9 * f49 as FinSequence of E ;
rng p3 c= E by FINSEQ_1:def_4;
then A56: rng p3 c= the carrier of K by A48, XBOOLE_1:1;
rng p4 c= E by FINSEQ_1:def_4;
then rng p4 c= the carrier of K by A48, XBOOLE_1:1;
then reconsider p3 = p3, p4 = p4 as FinSequence of the carrier of K by A56, FINSEQ_1:def_4;
consider q1 being FinSequence of the carrier of K such that
A57: q1 = p * (Sgm (dom (p | B9))) and
A58: G . B9 = Sum q1 by A6;
A59: Sgm (dom (p | (B9 \/ {x}))) is one-to-one by A22, FINSEQ_3:92;
rng ((Sgm (dom (p | (B9 \/ {x})))) | ((Seg (len (Sgm (dom (p | (B9 \/ {x})))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x}))) = (Sgm (dom (p | (B9 \/ {x})))) .: ((Seg (len (Sgm (dom (p | (B9 \/ {x})))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x})) by RELAT_1:115
.= (Sgm (dom (p | (B9 \/ {x})))) .: ((dom (Sgm (dom (p | (B9 \/ {x}))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x})) by FINSEQ_1:def_3
.= ((Sgm (dom (p | (B9 \/ {x})))) .: (dom (Sgm (dom (p | (B9 \/ {x})))))) \ {x} by SETWISEO:6
.= (rng (Sgm (dom pB9x))) \ {x} by RELAT_1:113
.= (dom (p | (B9 \/ {x}))) \ {x} by FINSEQ_1:50
.= ((dom p) /\ (B9 \/ {x})) \ {x} by RELAT_1:61
.= (((dom p) /\ B9) \/ ((dom p) /\ {x})) \ {x} by XBOOLE_1:23
.= (((dom p) /\ B9) \/ {x}) \ {x} by A42, XBOOLE_1:28
.= (dom (p | B9)) \ {x} by A25, XBOOLE_1:40
.= dom (p | B9) by A49, ZFMISC_1:57 ;
then Sgm (dom (p | B9)) = (Sgm (dom (p | (B9 \/ {x})))) * (Sgm ((Seg (len (Sgm (dom (p | (B9 \/ {x})))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x}))) by A24, A20, A26, FINSEQ_1:def_13
.= (Sgm (dom (p | (B9 \/ {x})))) * (Sgm ((dom (Sgm (dom (p | (B9 \/ {x}))))) \ ((Sgm (dom (p | (B9 \/ {x})))) " {x}))) by FINSEQ_1:def_3
.= (Sgm (dom (p | (B9 \/ {x})))) - {x} by FINSEQ_3:def_1
.= ((Sgm (dom (p | (B9 \/ {x})))) -| x) ^ ((Sgm (dom (p | (B9 \/ {x})))) |-- x) by A52, A59, FINSEQ_4:55 ;
then A60: q1 = p3 ^ p4 by A57, FINSEQOP:9;
q2 = p9 * ((f39 ^ <*x9*>) ^ f49) by A54, A52, FINSEQ_4:51
.= (p9 * (f39 ^ <*x9*>)) ^ (p9 * f49) by FINSEQOP:9
.= ((p9 * f39) ^ (p9 * <*x9*>)) ^ (p9 * f49) by FINSEQOP:9
.= (p3 ^ <*px*>) ^ p4 by A44, A45, FUNCT_1:2 ;
hence G . (B9 \/ {x}) = (Sum (p3 ^ <*px*>)) + (Sum p4) by A55, RLVECT_1:41
.= ((Sum p3) + (Sum <*px*>)) + (Sum p4) by RLVECT_1:41
.= ((Sum p3) + (Sum p4)) + (Sum <*px*>) by RLVECT_1:def_3
.= (Sum q1) + (Sum <*px*>) by A60, RLVECT_1:41
.= the addF of K . ((Sum q1),px) by RLVECT_1:44
.= the addF of K . ((G . B9),(([#] (p,(the_unity_wrt the addF of K))) . x)) by A58, A41, SETWOP_2:20 ;
::_thesis: verum
end;
A61: now__::_thesis:_for_x_being_Element_of_NAT_holds_G_._{x}_=_([#]_(p,(the_unity_wrt_the_addF_of_K)))_._x
let x be Element of NAT ; ::_thesis: G . {b1} = ([#] (p,(the_unity_wrt the addF of K))) . b1
consider q being FinSequence of the carrier of K such that
A62: q = p * (Sgm (dom (p | {x}))) and
A63: G . {.x.} = Sum q by A6;
A64: {} c= Seg 0 ;
percases ( not x in dom p or x in dom p ) ;
supposeA65: not x in dom p ; ::_thesis: G . {b1} = ([#] (p,(the_unity_wrt the addF of K))) . b1
then dom p misses {x} by ZFMISC_1:50;
then (dom p) /\ {x} = {} by XBOOLE_0:def_7;
then q = p * (Sgm {}) by A62, RELAT_1:61
.= p * {} by A64, FINSEQ_1:51
.= <*> the carrier of K ;
hence G . {x} = 0. K by A63, RLVECT_1:43
.= the_unity_wrt the addF of K by Th7
.= ([#] (p,(the_unity_wrt the addF of K))) . x by A65, SETWOP_2:20 ;
::_thesis: verum
end;
supposeA66: x in dom p ; ::_thesis: G . {b1} = ([#] (p,(the_unity_wrt the addF of K))) . b1
then p . x = p /. x by PARTFUN1:def_6;
then reconsider px = p . x as Element of K ;
A67: dom <*px*> = Seg 1 by FINSEQ_1:38;
rng <*x*> = {x} by FINSEQ_1:38;
then ( dom <*x*> = Seg 1 & rng <*x*> c= dom p ) by A66, FINSEQ_1:38, ZFMISC_1:31;
then A68: dom (p * <*x*>) = dom <*px*> by A67, RELAT_1:27;
A69: now__::_thesis:_for_e_being_set_st_e_in_dom_<*px*>_holds_
(p_*_<*x*>)_._e_=_<*px*>_._e
let e be set ; ::_thesis: ( e in dom <*px*> implies (p * <*x*>) . e = <*px*> . e )
assume A70: e in dom <*px*> ; ::_thesis: (p * <*x*>) . e = <*px*> . e
then A71: e = 1 by A67, FINSEQ_1:2, TARSKI:def_1;
thus (p * <*x*>) . e = p . (<*x*> . e) by A68, A70, FUNCT_1:12
.= p . x by A71, FINSEQ_1:40
.= <*px*> . e by A71, FINSEQ_1:40 ; ::_thesis: verum
end;
A72: x <> 0 by A66, FINSEQ_3:25;
q = p * (Sgm ((dom p) /\ {x})) by A62, RELAT_1:61
.= p * (Sgm {x}) by A66, ZFMISC_1:46
.= p * <*x*> by A72, FINSEQ_3:44
.= <*px*> by A68, A69, FUNCT_1:2 ;
hence G . {x} = px by A63, RLVECT_1:44
.= ([#] (p,(the_unity_wrt the addF of K))) . x by A66, SETWOP_2:20 ;
::_thesis: verum
end;
end;
end;
A73: now__::_thesis:_for_e_being_Element_of_K_st_e_is_a_unity_wrt_the_addF_of_K_holds_
e_=_G_._{}
let e be Element of K; ::_thesis: ( e is_a_unity_wrt the addF of K implies e = G . {} )
assume A74: e is_a_unity_wrt the addF of K ; ::_thesis: e = G . {}
0. K is_a_unity_wrt the addF of K by Th6;
then A75: e = 0. K by A74, BINOP_1:10;
A76: {} c= Seg 0 ;
consider q being FinSequence of the carrier of K such that
A77: q = p * (Sgm (dom (p | ({}. NAT)))) and
A78: G . ({}. NAT) = Sum q by A6;
q = p * (Sgm (dom {})) by A77
.= p * {} by A76, FINSEQ_1:51
.= <*> the carrier of K ;
hence e = G . {} by A78, A75, RLVECT_1:43; ::_thesis: verum
end;
consider q1 being FinSequence of the carrier of K such that
A79: q1 = p * (Sgm (dom (p | (dom p)))) and
A80: G . (findom p) = Sum q1 by A6;
A81: the addF of K is having_a_unity by Th8;
q1 = p * (Sgm (dom p)) by A79
.= p * (Sgm (Seg (len p))) by FINSEQ_1:def_3
.= p * (idseq (len p)) by FINSEQ_3:48
.= p by FINSEQ_2:54 ;
hence s = the addF of K $$ ((findom p),([#] (p,(the_unity_wrt the addF of K)))) by A2, A81, A80, A73, A61, A7, SETWISEO:def_3
.= the addF of K $$ p by Th8, SETWOP_2:def_2 ;
::_thesis: verum
end;
A82: p | (len p) = p | (Seg (len p)) by FINSEQ_1:def_15
.= p | (dom p) by FINSEQ_1:def_3
.= p ;
A83: now__::_thesis:_for_j_being_Element_of_NAT_
for_a_being_Element_of_K_st_j_<_len_p_&_a_=_p_._(j_+_1)_holds_
f_._(j_+_1)_=_(f_._j)_+_a
let j be Element of NAT ; ::_thesis: for a being Element of K st j < len p & a = p . (j + 1) holds
f . (j + 1) = (f . j) + a
let a be Element of K; ::_thesis: ( j < len p & a = p . (j + 1) implies f . (j + 1) = (f . j) + a )
assume that
A84: j < len p and
A85: a = p . (j + 1) ; ::_thesis: f . (j + 1) = (f . j) + a
A86: j + 1 <= len p by A84, NAT_1:13;
then A87: len (p | (j + 1)) = j + 1 by FINSEQ_1:59;
j <= j + 1 by NAT_1:11;
then A88: Seg j c= Seg (j + 1) by FINSEQ_1:5;
A89: p | j = p | (Seg j) by FINSEQ_1:def_15
.= (p | (Seg (j + 1))) | (Seg j) by A88, RELAT_1:74
.= (p | (j + 1)) | (Seg j) by FINSEQ_1:def_15 ;
A90: 1 <= j + 1 by NAT_1:11;
then A91: j + 1 in dom (p | (j + 1)) by A87, FINSEQ_3:25;
j + 1 in dom p by A86, A90, FINSEQ_3:25;
then a = p /. (j + 1) by A85, PARTFUN1:def_6
.= (p | (j + 1)) /. (j + 1) by A91, FINSEQ_4:70
.= (p | (j + 1)) . (j + 1) by A91, PARTFUN1:def_6 ;
then p | (j + 1) = (p | j) ^ <*a*> by A87, A89, FINSEQ_3:55;
hence f . (j + 1) = the addF of K $$ ((p | j) ^ <*a*>) by A1
.= the addF of K . (( the addF of K $$ (p | j)),a) by Th8, FINSOP_1:4
.= (f . j) + a by A1 ;
::_thesis: verum
end;
p | 0 = <*> the carrier of K ;
then A92: f . 0 = the addF of K $$ (<*> the carrier of K) by A1
.= the_unity_wrt the addF of K by Th8, FINSOP_1:10
.= 0. K by Th7 ;
assume s = the addF of K $$ p ; ::_thesis: s = Sum p
then s = f . (len p) by A1, A82;
hence s = Sum p by A92, A83, RLVECT_1:def_12; ::_thesis: verum
end;
end;
:: deftheorem defines Sum FVSUM_1:def_8_:_
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for p being FinSequence of the carrier of K holds Sum p = the addF of K $$ p;
theorem :: FVSUM_1:71
for K being non empty right_complementable add-associative right_zeroed addLoopStr
for a being Element of K
for p being FinSequence of the carrier of K holds Sum (p ^ <*a*>) = (Sum p) + a
proof
let K be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for a being Element of K
for p being FinSequence of the carrier of K holds Sum (p ^ <*a*>) = (Sum p) + a
let a be Element of K; ::_thesis: for p being FinSequence of the carrier of K holds Sum (p ^ <*a*>) = (Sum p) + a
let p be FinSequence of the carrier of K; ::_thesis: Sum (p ^ <*a*>) = (Sum p) + a
thus Sum (p ^ <*a*>) = (Sum p) + (Sum <*a*>) by RLVECT_1:41
.= (Sum p) + a by RLVECT_1:44 ; ::_thesis: verum
end;
theorem :: FVSUM_1:72
for K being non empty right_complementable add-associative right_zeroed addLoopStr
for a being Element of K
for p being FinSequence of the carrier of K holds Sum (<*a*> ^ p) = a + (Sum p)
proof
let K be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for a being Element of K
for p being FinSequence of the carrier of K holds Sum (<*a*> ^ p) = a + (Sum p)
let a be Element of K; ::_thesis: for p being FinSequence of the carrier of K holds Sum (<*a*> ^ p) = a + (Sum p)
let p be FinSequence of the carrier of K; ::_thesis: Sum (<*a*> ^ p) = a + (Sum p)
thus Sum (<*a*> ^ p) = (Sum <*a*>) + (Sum p) by RLVECT_1:41
.= a + (Sum p) by RLVECT_1:44 ; ::_thesis: verum
end;
theorem :: FVSUM_1:73
for K being non empty right_complementable Abelian add-associative right_zeroed distributive doubleLoopStr
for a being Element of K
for p being FinSequence of the carrier of K holds Sum (a * p) = a * (Sum p)
proof
let K be non empty right_complementable Abelian add-associative right_zeroed distributive doubleLoopStr ; ::_thesis: for a being Element of K
for p being FinSequence of the carrier of K holds Sum (a * p) = a * (Sum p)
let a be Element of K; ::_thesis: for p being FinSequence of the carrier of K holds Sum (a * p) = a * (Sum p)
let p be FinSequence of the carrier of K; ::_thesis: Sum (a * p) = a * (Sum p)
set rM = the multF of K [;] (a,(id the carrier of K));
( the addF of K is having_a_unity & the multF of K is_distributive_wrt the addF of K ) by Th8, Th10;
hence Sum (a * p) = ( the multF of K [;] (a,(id the carrier of K))) . (Sum p) by Th14, SETWOP_2:30
.= a * (Sum p) by Lm1 ;
::_thesis: verum
end;
theorem :: FVSUM_1:74
for K being non empty addLoopStr
for R being Element of 0 -tuples_on the carrier of K holds Sum R = 0. K
proof
let K be non empty addLoopStr ; ::_thesis: for R being Element of 0 -tuples_on the carrier of K holds Sum R = 0. K
let R be Element of 0 -tuples_on the carrier of K; ::_thesis: Sum R = 0. K
R = <*> the carrier of K ;
hence Sum R = 0. K by RLVECT_1:43; ::_thesis: verum
end;
theorem :: FVSUM_1:75
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for p being FinSequence of the carrier of K holds Sum (- p) = - (Sum p)
proof
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for p being FinSequence of the carrier of K holds Sum (- p) = - (Sum p)
let p be FinSequence of the carrier of K; ::_thesis: Sum (- p) = - (Sum p)
( the addF of K is having_an_inverseOp & the_inverseOp_wrt the addF of K = comp K ) by Th14, Th15;
hence Sum (- p) = (comp K) . (Sum p) by Th8, SETWOP_2:31
.= - (Sum p) by VECTSP_1:def_13 ;
::_thesis: verum
end;
theorem :: FVSUM_1:76
for i being Element of NAT
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 + R2) = (Sum R1) + (Sum R2) by Th8, SETWOP_2:35;
theorem :: FVSUM_1:77
for i being Element of NAT
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 - R2) = (Sum R1) - (Sum R2)
proof
let i be Element of NAT ; ::_thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 - R2) = (Sum R1) - (Sum R2)
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 - R2) = (Sum R1) - (Sum R2)
let R1, R2 be Element of i -tuples_on the carrier of K; ::_thesis: Sum (R1 - R2) = (Sum R1) - (Sum R2)
( the addF of K is having_an_inverseOp & the_inverseOp_wrt the addF of K = comp K ) by Th14, Th15;
hence Sum (R1 - R2) = (diffield K) . ((Sum R1),( the addF of K $$ R2)) by Th8, SETWOP_2:37
.= (Sum R1) - (Sum R2) by Th11 ;
::_thesis: verum
end;
begin
Lm6: for K being non empty commutative well-unital multLoopStr holds Product (<*> the carrier of K) = 1. K
proof
let K be non empty commutative well-unital multLoopStr ; ::_thesis: Product (<*> the carrier of K) = 1. K
1. K = 1_ K ;
hence Product (<*> the carrier of K) = 1. K by GROUP_4:8; ::_thesis: verum
end;
theorem :: FVSUM_1:78
for K being non empty associative commutative well-unital doubleLoopStr
for a being Element of K
for p1 being FinSequence of the carrier of K holds Product (<*a*> ^ p1) = a * (Product p1)
proof
let K be non empty associative commutative well-unital doubleLoopStr ; ::_thesis: for a being Element of K
for p1 being FinSequence of the carrier of K holds Product (<*a*> ^ p1) = a * (Product p1)
let a be Element of K; ::_thesis: for p1 being FinSequence of the carrier of K holds Product (<*a*> ^ p1) = a * (Product p1)
let p1 be FinSequence of the carrier of K; ::_thesis: Product (<*a*> ^ p1) = a * (Product p1)
thus Product (<*a*> ^ p1) = (Product <*a*>) * (Product p1) by GROUP_4:5
.= a * (Product p1) by FINSOP_1:11 ; ::_thesis: verum
end;
theorem :: FVSUM_1:79
for K being non empty associative commutative well-unital doubleLoopStr
for a1, a2, a3 being Element of K holds Product <*a1,a2,a3*> = (a1 * a2) * a3
proof
let K be non empty associative commutative well-unital doubleLoopStr ; ::_thesis: for a1, a2, a3 being Element of K holds Product <*a1,a2,a3*> = (a1 * a2) * a3
let a1, a2, a3 be Element of K; ::_thesis: Product <*a1,a2,a3*> = (a1 * a2) * a3
thus Product <*a1,a2,a3*> = Product (<*a1,a2*> ^ <*a3*>) by FINSEQ_1:43
.= (Product <*a1,a2*>) * a3 by GROUP_4:6
.= (a1 * a2) * a3 by FINSOP_1:12 ; ::_thesis: verum
end;
theorem :: FVSUM_1:80
for K being non empty associative commutative well-unital doubleLoopStr
for R being Element of 0 -tuples_on the carrier of K holds Product R = 1. K
proof
let K be non empty associative commutative well-unital doubleLoopStr ; ::_thesis: for R being Element of 0 -tuples_on the carrier of K holds Product R = 1. K
let R be Element of 0 -tuples_on the carrier of K; ::_thesis: Product R = 1. K
R = <*> the carrier of K ;
hence Product R = 1. K by Lm6; ::_thesis: verum
end;
theorem :: FVSUM_1:81
for i being Element of NAT
for K being non empty associative commutative well-unital doubleLoopStr holds Product (i |-> (1_ K)) = 1_ K
proof
let i be Element of NAT ; ::_thesis: for K being non empty associative commutative well-unital doubleLoopStr holds Product (i |-> (1_ K)) = 1_ K
let K be non empty associative commutative well-unital doubleLoopStr ; ::_thesis: Product (i |-> (1_ K)) = 1_ K
the_unity_wrt the multF of K = 1_ K by Th5;
hence Product (i |-> (1_ K)) = 1_ K by SETWOP_2:25; ::_thesis: verum
end;
theorem :: FVSUM_1:82
for K being non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p being FinSequence of the carrier of K holds
( ex k being Element of NAT st
( k in dom p & p . k = 0. K ) iff Product p = 0. K )
proof
let K be non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: for p being FinSequence of the carrier of K holds
( ex k being Element of NAT st
( k in dom p & p . k = 0. K ) iff Product p = 0. K )
let p be FinSequence of the carrier of K; ::_thesis: ( ex k being Element of NAT st
( k in dom p & p . k = 0. K ) iff Product p = 0. K )
defpred S1[ Element of NAT ] means for p being FinSequence of the carrier of K st len p = $1 holds
( ex k being Element of NAT st
( k in Seg $1 & p . k = 0. K ) iff Product p = 0. K );
A1: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A2: for p being FinSequence of the carrier of K st len p = i holds
( ex k being Element of NAT st
( k in Seg i & p . k = 0. K ) iff Product p = 0. K ) ; ::_thesis: S1[i + 1]
let p be FinSequence of the carrier of K; ::_thesis: ( len p = i + 1 implies ( ex k being Element of NAT st
( k in Seg (i + 1) & p . k = 0. K ) iff Product p = 0. K ) )
assume A3: len p = i + 1 ; ::_thesis: ( ex k being Element of NAT st
( k in Seg (i + 1) & p . k = 0. K ) iff Product p = 0. K )
then consider p9 being FinSequence of the carrier of K, a being Element of K such that
A4: p = p9 ^ <*a*> by FINSEQ_2:19;
A5: i + 1 = (len p9) + 1 by A3, A4, FINSEQ_2:16;
then A6: i = len p9 by XCMPLX_1:2;
A7: Product p = (Product p9) * a by A4, GROUP_4:6;
thus ( ex k being Element of NAT st
( k in Seg (i + 1) & p . k = 0. K ) implies Product p = 0. K ) ::_thesis: ( Product p = 0. K implies ex k being Element of NAT st
( k in Seg (i + 1) & p . k = 0. K ) )
proof
given k being Element of NAT such that A8: k in Seg (i + 1) and
A9: p . k = 0. K ; ::_thesis: Product p = 0. K
now__::_thesis:_Product_p_=_0._K
percases ( k in Seg i or k = i + 1 ) by A8, FINSEQ_2:7;
supposeA10: k in Seg i ; ::_thesis: Product p = 0. K
then k in dom p9 by A6, FINSEQ_1:def_3;
then p9 . k = p . k by A4, FINSEQ_1:def_7;
then Product p9 = 0. K by A2, A6, A9, A10;
hence Product p = 0. K by A7, VECTSP_1:7; ::_thesis: verum
end;
suppose k = i + 1 ; ::_thesis: Product p = 0. K
then a = 0. K by A4, A5, A9, FINSEQ_1:42;
hence Product p = 0. K by A7, VECTSP_1:7; ::_thesis: verum
end;
end;
end;
hence Product p = 0. K ; ::_thesis: verum
end;
assume A11: Product p = 0. K ; ::_thesis: ex k being Element of NAT st
( k in Seg (i + 1) & p . k = 0. K )
percases ( Product p9 = 0. K or a = 0. K ) by A7, A11, VECTSP_1:12;
suppose Product p9 = 0. K ; ::_thesis: ex k being Element of NAT st
( k in Seg (i + 1) & p . k = 0. K )
then consider k being Element of NAT such that
A12: k in Seg i and
A13: p9 . k = 0. K by A2, A6;
k in dom p9 by A6, A12, FINSEQ_1:def_3;
then p . k = 0. K by A4, A13, FINSEQ_1:def_7;
hence ex k being Element of NAT st
( k in Seg (i + 1) & p . k = 0. K ) by A12, FINSEQ_2:8; ::_thesis: verum
end;
suppose a = 0. K ; ::_thesis: ex k being Element of NAT st
( k in Seg (i + 1) & p . k = 0. K )
then p . (i + 1) = 0. K by A4, A5, FINSEQ_1:42;
hence ex k being Element of NAT st
( k in Seg (i + 1) & p . k = 0. K ) by FINSEQ_1:4; ::_thesis: verum
end;
end;
end;
A14: Seg (len p) = dom p by FINSEQ_1:def_3;
A15: S1[ 0 ]
proof
let p be FinSequence of the carrier of K; ::_thesis: ( len p = 0 implies ( ex k being Element of NAT st
( k in Seg 0 & p . k = 0. K ) iff Product p = 0. K ) )
assume len p = 0 ; ::_thesis: ( ex k being Element of NAT st
( k in Seg 0 & p . k = 0. K ) iff Product p = 0. K )
then p = <*> the carrier of K ;
then A16: Product p = 1. K by Lm6;
thus ( ex k being Element of NAT st
( k in Seg 0 & p . k = 0. K ) implies Product p = 0. K ) ; ::_thesis: ( Product p = 0. K implies ex k being Element of NAT st
( k in Seg 0 & p . k = 0. K ) )
assume Product p = 0. K ; ::_thesis: ex k being Element of NAT st
( k in Seg 0 & p . k = 0. K )
hence ex k being Element of NAT st
( k in Seg 0 & p . k = 0. K ) by A16; ::_thesis: verum
end;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(A15, A1);
hence ( ex k being Element of NAT st
( k in dom p & p . k = 0. K ) iff Product p = 0. K ) by A14; ::_thesis: verum
end;
theorem :: FVSUM_1:83
for i, j being Element of NAT
for K being non empty associative commutative well-unital doubleLoopStr
for a being Element of K holds Product ((i + j) |-> a) = (Product (i |-> a)) * (Product (j |-> a)) by SETWOP_2:26;
theorem :: FVSUM_1:84
for i, j being Element of NAT
for K being non empty associative commutative well-unital doubleLoopStr
for a being Element of K holds Product ((i * j) |-> a) = Product (j |-> (Product (i |-> a))) by SETWOP_2:27;
theorem :: FVSUM_1:85
for i being Element of NAT
for K being non empty associative commutative well-unital doubleLoopStr
for a1, a2 being Element of K holds Product (i |-> (a1 * a2)) = (Product (i |-> a1)) * (Product (i |-> a2)) by SETWOP_2:36;
theorem Th86: :: FVSUM_1:86
for i being Element of NAT
for K being non empty associative commutative well-unital doubleLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds Product (mlt (R1,R2)) = (Product R1) * (Product R2) by SETWOP_2:35;
theorem :: FVSUM_1:87
for i being Element of NAT
for K being non empty associative commutative well-unital doubleLoopStr
for a being Element of K
for R1 being Element of i -tuples_on the carrier of K holds Product (a * R1) = (Product (i |-> a)) * (Product R1)
proof
let i be Element of NAT ; ::_thesis: for K being non empty associative commutative well-unital doubleLoopStr
for a being Element of K
for R1 being Element of i -tuples_on the carrier of K holds Product (a * R1) = (Product (i |-> a)) * (Product R1)
let K be non empty associative commutative well-unital doubleLoopStr ; ::_thesis: for a being Element of K
for R1 being Element of i -tuples_on the carrier of K holds Product (a * R1) = (Product (i |-> a)) * (Product R1)
let a be Element of K; ::_thesis: for R1 being Element of i -tuples_on the carrier of K holds Product (a * R1) = (Product (i |-> a)) * (Product R1)
let R1 be Element of i -tuples_on the carrier of K; ::_thesis: Product (a * R1) = (Product (i |-> a)) * (Product R1)
thus Product (a * R1) = Product (mlt ((i |-> a),R1)) by Th66
.= (Product (i |-> a)) * (Product R1) by Th86 ; ::_thesis: verum
end;
begin
definition
let K be non empty doubleLoopStr ;
let p, q be FinSequence of the carrier of K;
funcp "*" q -> Element of K equals :: FVSUM_1:def 9
Sum (mlt (p,q));
coherence
Sum (mlt (p,q)) is Element of K ;
end;
:: deftheorem defines "*" FVSUM_1:def_9_:_
for K being non empty doubleLoopStr
for p, q being FinSequence of the carrier of K holds p "*" q = Sum (mlt (p,q));
theorem :: FVSUM_1:88
for K being non empty right_complementable associative commutative Abelian add-associative right_zeroed left_unital doubleLoopStr
for a, b being Element of K holds <*a*> "*" <*b*> = a * b
proof
let K be non empty right_complementable associative commutative Abelian add-associative right_zeroed left_unital doubleLoopStr ; ::_thesis: for a, b being Element of K holds <*a*> "*" <*b*> = a * b
let a, b be Element of K; ::_thesis: <*a*> "*" <*b*> = a * b
set p = <*a*>;
set q = <*b*>;
set m = mlt (<*a*>,<*b*>);
mlt (<*a*>,<*b*>) = <*(a * b)*> by FINSEQ_2:74;
then mlt (<*a*>,<*b*>) = 1 |-> (a * b) by FINSEQ_2:59;
hence <*a*> "*" <*b*> = a * b by FINSOP_1:16; ::_thesis: verum
end;
theorem :: FVSUM_1:89
for K being non empty right_complementable associative commutative Abelian add-associative right_zeroed left_unital doubleLoopStr
for a1, a2, b1, b2 being Element of K holds <*a1,a2*> "*" <*b1,b2*> = (a1 * b1) + (a2 * b2)
proof
let K be non empty right_complementable associative commutative Abelian add-associative right_zeroed left_unital doubleLoopStr ; ::_thesis: for a1, a2, b1, b2 being Element of K holds <*a1,a2*> "*" <*b1,b2*> = (a1 * b1) + (a2 * b2)
let a1, a2, b1, b2 be Element of K; ::_thesis: <*a1,a2*> "*" <*b1,b2*> = (a1 * b1) + (a2 * b2)
set p = <*a1,a2*>;
set q = <*b1,b2*>;
the addF of K $$ (mlt (<*a1,a2*>,<*b1,b2*>)) = the addF of K $$ <*(a1 * b1),(a2 * b2)*> by Lm5
.= (a1 * b1) + (a2 * b2) by FINSOP_1:12 ;
hence <*a1,a2*> "*" <*b1,b2*> = (a1 * b1) + (a2 * b2) ; ::_thesis: verum
end;
theorem :: FVSUM_1:90
for K being non empty associative commutative well-unital doubleLoopStr
for p, q being FinSequence of the carrier of K holds p "*" q = q "*" p by Th64;