let R, S be non empty right_complementable add-associative right_zeroed doubleLoopStr ; for F being non empty Subset of R
for G being non empty Subset of S
for P being Function of R,S
for lc being LinearCombination of F
for LC being LinearCombination of G
for E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] st P is RingHomomorphism & len lc = len LC & E represents lc & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) holds
P . (Sum lc) = Sum LC
let F be non empty Subset of R; for G being non empty Subset of S
for P being Function of R,S
for lc being LinearCombination of F
for LC being LinearCombination of G
for E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] st P is RingHomomorphism & len lc = len LC & E represents lc & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) holds
P . (Sum lc) = Sum LC
let G be non empty Subset of S; for P being Function of R,S
for lc being LinearCombination of F
for LC being LinearCombination of G
for E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] st P is RingHomomorphism & len lc = len LC & E represents lc & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) holds
P . (Sum lc) = Sum LC
let P be Function of R,S; for lc being LinearCombination of F
for LC being LinearCombination of G
for E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] st P is RingHomomorphism & len lc = len LC & E represents lc & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) holds
P . (Sum lc) = Sum LC
let lc be LinearCombination of F; for LC being LinearCombination of G
for E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] st P is RingHomomorphism & len lc = len LC & E represents lc & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) holds
P . (Sum lc) = Sum LC
let LC be LinearCombination of G; for E being FinSequence of [: the carrier of R, the carrier of R, the carrier of R:] st P is RingHomomorphism & len lc = len LC & E represents lc & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) holds
P . (Sum lc) = Sum LC
let E be FinSequence of [: the carrier of R, the carrier of R, the carrier of R:]; ( P is RingHomomorphism & len lc = len LC & E represents lc & ( for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3)) ) implies P . (Sum lc) = Sum LC )
assume that
A1:
P is RingHomomorphism
and
A2:
len lc = len LC
and
A3:
E represents lc
and
A4:
for i being set st i in dom LC holds
LC . i = ((P . ((E /. i) `1_3)) * (P . ((E /. i) `2_3))) * (P . ((E /. i) `3_3))
; P . (Sum lc) = Sum LC
defpred S1[ Nat] means for lc9 being LinearCombination of F
for LC9 being LinearCombination of G st lc9 = lc | (Seg $1) & LC9 = LC | (Seg $1) holds
P . (Sum lc9) = Sum LC9;
A5:
( P is additive & P is multiplicative )
by A1;
A6:
dom lc = dom LC
by A2, FINSEQ_3:29;
A7:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A8:
S1[
k]
;
S1[k + 1]
thus
S1[
k + 1]
verumproof
let lc9 be
LinearCombination of
F;
for LC9 being LinearCombination of G st lc9 = lc | (Seg (k + 1)) & LC9 = LC | (Seg (k + 1)) holds
P . (Sum lc9) = Sum LC9let LC9 be
LinearCombination of
G;
( lc9 = lc | (Seg (k + 1)) & LC9 = LC | (Seg (k + 1)) implies P . (Sum lc9) = Sum LC9 )
assume that A9:
lc9 = lc | (Seg (k + 1))
and A10:
LC9 = LC | (Seg (k + 1))
;
P . (Sum lc9) = Sum LC9
per cases
( len lc < k + 1 or len lc >= k + 1 )
;
suppose A14:
len lc >= k + 1
;
P . (Sum lc9) = Sum LC9set i =
k + 1;
reconsider LCk =
LC | (Seg k) as
LinearCombination of
G by IDEAL_1:41;
reconsider lck =
lc | (Seg k) as
LinearCombination of
F by IDEAL_1:41;
1
<= k + 1
by NAT_1:11;
then A15:
k + 1
in dom lc
by A14, FINSEQ_3:25;
then A16:
lc . (k + 1) = lc /. (k + 1)
by PARTFUN1:def 6;
A17:
LC . (k + 1) = LC /. (k + 1)
by A6, A15, PARTFUN1:def 6;
lc | (Seg (k + 1)) = lck ^ <*(lc . (k + 1))*>
by A15, FINSEQ_5:10;
hence P . (Sum lc9) =
P . ((Sum lck) + (lc /. (k + 1)))
by A9, A16, FVSUM_1:71
.=
(P . (Sum lck)) + (P . (lc /. (k + 1)))
by A5
.=
(Sum LCk) + (P . (lc /. (k + 1)))
by A8
.=
(Sum LCk) + (P . ((((E /. (k + 1)) `1_3) * ((E /. (k + 1)) `2_3)) * ((E /. (k + 1)) `3_3)))
by A3, A15, A16
.=
(Sum LCk) + ((P . (((E /. (k + 1)) `1_3) * ((E /. (k + 1)) `2_3))) * (P . ((E /. (k + 1)) `3_3)))
by A5
.=
(Sum LCk) + (((P . ((E /. (k + 1)) `1_3)) * (P . ((E /. (k + 1)) `2_3))) * (P . ((E /. (k + 1)) `3_3)))
by A5
.=
(Sum LCk) + (LC /. (k + 1))
by A4, A6, A15, A17
.=
Sum (LCk ^ <*(LC /. (k + 1))*>)
by FVSUM_1:71
.=
Sum LC9
by A6, A10, A15, A17, FINSEQ_5:10
;
verum end; end;
end;
end;
A18:
( lc = lc | (Seg (len lc)) & LC = LC | (Seg (len LC)) )
by FINSEQ_3:49;
A19:
S1[ 0 ]
for k being Nat holds S1[k]
from NAT_1:sch 2(A19, A7);
hence
P . (Sum lc) = Sum LC
by A2, A18; verum