let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for b1 being bag of st ex u being set st support b1 = {u} holds
for b2 being bag of
for x being Function of n,L holds eval (b1 + b2),x = (eval b1,x) * (eval b2,x)
let L be non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for b1 being bag of st ex u being set st support b1 = {u} holds
for b2 being bag of
for x being Function of n,L holds eval (b1 + b2),x = (eval b1,x) * (eval b2,x)
let b1 be bag of ; :: thesis: ( ex u being set st support b1 = {u} implies for b2 being bag of
for x being Function of n,L holds eval (b1 + b2),x = (eval b1,x) * (eval b2,x) )
assume A1: ex u being set st support b1 = {u} ; :: thesis: for b2 being bag of
for x being Function of n,L holds eval (b1 + b2),x = (eval b1,x) * (eval b2,x)
let b2 be bag of ; :: thesis: for x being Function of n,L holds eval (b1 + b2),x = (eval b1,x) * (eval b2,x)
let x be Function of n,L; :: thesis: eval (b1 + b2),x = (eval b1,x) * (eval b2,x)
A2: n c= dom x by FUNCT_2:def 1;
consider u being set such that
A3: support b1 = {u} by A1;
A4: for u' being set st u' <> u holds
(b1 + b2) . u' = b2 . u'
proof
let u' be set ; :: thesis: ( u' <> u implies (b1 + b2) . u' = b2 . u' )
assume u' <> u ; :: thesis: (b1 + b2) . u' = b2 . u'
then A5: not u' in support b1 by A3, TARSKI:def 1;
thus (b1 + b2) . u' = (b1 . u') + (b2 . u') by POLYNOM1:def 5
.= 0 + (b2 . u') by A5, POLYNOM1:def 7
.= b2 . u' ; :: thesis: verum
end;
set sb2 = SgmX (RelIncl n),(support b2);
set sb1b2 = SgmX (RelIncl n),(support (b1 + b2));
consider yb1b2 being FinSequence of the carrier of L such that
A6: ( len yb1b2 = len (SgmX (RelIncl n),(support (b1 + b2))) & eval (b1 + b2),x = Product yb1b2 & ( for i being Element of NAT st 1 <= i & i <= len yb1b2 holds
yb1b2 /. i = (power L) . ((x * (SgmX (RelIncl n),(support (b1 + b2)))) /. i),(((b1 + b2) * (SgmX (RelIncl n),(support (b1 + b2)))) /. i) ) ) by Def2;
consider yb2 being FinSequence of the carrier of L such that
A7: ( len yb2 = len (SgmX (RelIncl n),(support b2)) & eval b2,x = Product yb2 & ( for i being Element of NAT st 1 <= i & i <= len yb2 holds
yb2 /. i = (power L) . ((x * (SgmX (RelIncl n),(support b2))) /. i),((b2 * (SgmX (RelIncl n),(support b2))) /. i) ) ) by Def2;
A8: ( RelIncl n linearly_orders support b2 & RelIncl n linearly_orders support (b1 + b2) ) by Th15;
A9: support (b1 + b2) = (support b2) \/ {u} by A3, POLYNOM1:42;
per cases ( u in support b2 or not u in support b2 ) ;
suppose A10: u in support b2 ; :: thesis: eval (b1 + b2),x = (eval b1,x) * (eval b2,x)
A11: for v being set st v in support (b1 + b2) holds
v in support b2
proof
let v be set ; :: thesis: ( v in support (b1 + b2) implies v in support b2 )
assume A12: v in support (b1 + b2) ; :: thesis: v in support b2
hence v in support b2 ; :: thesis: verum
end;
A13: for v being set st v in support b2 holds
v in support (b1 + b2)
proof
let v be set ; :: thesis: ( v in support b2 implies v in support (b1 + b2) )
assume A14: v in support b2 ; :: thesis: v in support (b1 + b2)
now
per cases ( u = v or u <> v ) ;
case u <> v ; :: thesis: v in support (b1 + b2)
then (b1 + b2) . v = b2 . v by A4;
then (b1 + b2) . v <> 0 by A14, POLYNOM1:def 7;
hence v in support (b1 + b2) by POLYNOM1:def 7; :: thesis: verum
end;
end;
end;
hence v in support (b1 + b2) ; :: thesis: verum
end;
then A15: support (b1 + b2) = support b2 by A11, TARSKI:2;
A16: len yb1b2 = len yb2 by A6, A7, A11, A13, TARSKI:2;
u in rng (SgmX (RelIncl n),(support b2)) by A8, A10, TRIANG_1:def 2;
then consider k being Nat such that
A17: ( k in dom (SgmX (RelIncl n),(support b2)) & (SgmX (RelIncl n),(support b2)) . k = u ) by FINSEQ_2:11;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
consider sb2k being Nat such that
A18: dom (SgmX (RelIncl n),(support b2)) = Seg sb2k by FINSEQ_1:def 2;
consider sb1b2k being Nat such that
A19: dom (SgmX (RelIncl n),(support (b1 + b2))) = Seg sb1b2k by FINSEQ_1:def 2;
reconsider sb2k = sb2k, sb1b2k = sb1b2k as Element of NAT by ORDINAL1:def 13;
A20: sb2k = len (SgmX (RelIncl n),(support b2)) by A18, FINSEQ_1:def 3
.= len (SgmX (RelIncl n),(support (b1 + b2))) by A11, A13, TARSKI:2
.= sb1b2k by A19, FINSEQ_1:def 3 ;
A21: ( 1 <= k & k <= sb2k ) by A17, A18, FINSEQ_1:3;
consider i being Nat such that
A22: dom yb2 = Seg i by FINSEQ_1:def 2;
i in NAT by ORDINAL1:def 13;
then A23: len yb2 = i by A22, FINSEQ_1:def 3;
A24: sb2k = len yb2 by A7, A18, FINSEQ_1:def 3;
then A25: k in dom yb2 by A17, A18, FINSEQ_1:def 3;
A26: len yb1b2 = sb2k by A6, A19, A20, FINSEQ_1:def 3;
A27: support b2 c= dom b2 by POLYNOM1:41;
then A28: k in dom (b2 * (SgmX (RelIncl n),(support b2))) by A10, A17, FUNCT_1:21;
A29: dom (b1 + b2) = n by PARTFUN1:def 4;
support (b1 + b2) c= dom (b1 + b2) by POLYNOM1:41;
then A30: k in dom ((b1 + b2) * (SgmX (RelIncl n),(support b2))) by A10, A15, A17, FUNCT_1:21;
then A31: ((b1 + b2) * (SgmX (RelIncl n),(support b2))) /. k = ((b1 + b2) * (SgmX (RelIncl n),(support b2))) . k by PARTFUN1:def 8
.= (b1 + b2) . u by A17, A30, FUNCT_1:22 ;
A32: (b2 * (SgmX (RelIncl n),(support b2))) /. k = (b2 * (SgmX (RelIncl n),(support b2))) . k by A28, PARTFUN1:def 8
.= b2 . u by A17, A28, FUNCT_1:22 ;
A33: yb1b2 /. k = (power L) . ((x * (SgmX (RelIncl n),(support b2))) /. k),(((b1 + b2) * (SgmX (RelIncl n),(support b2))) /. k) by A6, A15, A21, A26
.= (power L) . ((x * (SgmX (RelIncl n),(support b2))) /. k),((b1 . u) + (b2 . u)) by A31, POLYNOM1:def 5
.= ((power L) . ((x * (SgmX (RelIncl n),(support b2))) /. k),(b1 . u)) * ((power L) . ((x * (SgmX (RelIncl n),(support b2))) /. k),((b2 * (SgmX (RelIncl n),(support b2))) /. k)) by A32, Th2
.= ((power L) . ((x * (SgmX (RelIncl n),(support b2))) /. k),(b1 . u)) * (yb2 /. k) by A7, A21, A24 ;
A34: for i' being Element of NAT st i' in dom yb2 & i' <> k holds
yb1b2 /. i' = yb2 /. i'
proof
let i' be Element of NAT ; :: thesis: ( i' in dom yb2 & i' <> k implies yb1b2 /. i' = yb2 /. i' )
assume A35: ( i' in dom yb2 & i' <> k ) ; :: thesis: yb1b2 /. i' = yb2 /. i'
then A36: ( 1 <= i' & i' <= len yb2 ) by A22, A23, FINSEQ_1:3;
A37: i' in Seg sb1b2k by A20, A24, A35, FINSEQ_1:def 3;
A38: (SgmX (RelIncl n),(support (b1 + b2))) /. i' <> u
proof
assume (SgmX (RelIncl n),(support (b1 + b2))) /. i' = u ; :: thesis: contradiction
then A39: (SgmX (RelIncl n),(support (b1 + b2))) . i' = u by A19, A37, PARTFUN1:def 8;
A40: (SgmX (RelIncl n),(support (b1 + b2))) . k = u by A11, A13, A17, TARSKI:2;
SgmX (RelIncl n),(support (b1 + b2)) is one-to-one by Th15, TRIANG_1:8;
hence contradiction by A17, A18, A19, A20, A35, A37, A39, A40, FUNCT_1:def 8; :: thesis: verum
end;
rng (SgmX (RelIncl n),(support (b1 + b2))) c= dom b2 by A8, A15, A27, TRIANG_1:def 2;
then A41: rng (SgmX (RelIncl n),(support (b1 + b2))) c= n by PARTFUN1:def 4;
(SgmX (RelIncl n),(support (b1 + b2))) . i' in rng (SgmX (RelIncl n),(support (b1 + b2))) by A19, A37, FUNCT_1:def 5;
then A42: i' in dom ((b1 + b2) * (SgmX (RelIncl n),(support (b1 + b2)))) by A19, A29, A37, A41, FUNCT_1:21;
then A43: ((b1 + b2) * (SgmX (RelIncl n),(support (b1 + b2)))) /. i' = ((b1 + b2) * (SgmX (RelIncl n),(support (b1 + b2)))) . i' by PARTFUN1:def 8
.= (b1 + b2) . ((SgmX (RelIncl n),(support (b1 + b2))) . i') by A42, FUNCT_1:22
.= (b1 + b2) . ((SgmX (RelIncl n),(support (b1 + b2))) /. i') by A19, A37, PARTFUN1:def 8 ;
A44: i' in dom (SgmX (RelIncl n),(support b2)) by A7, A22, A23, A35, FINSEQ_1:def 3;
A45: rng (SgmX (RelIncl n),(support b2)) c= dom b2 by A8, A27, TRIANG_1:def 2;
(SgmX (RelIncl n),(support b2)) . i' in rng (SgmX (RelIncl n),(support b2)) by A44, FUNCT_1:def 5;
then A46: i' in dom (b2 * (SgmX (RelIncl n),(support b2))) by A44, A45, FUNCT_1:21;
then A47: (b2 * (SgmX (RelIncl n),(support b2))) /. i' = (b2 * (SgmX (RelIncl n),(support b2))) . i' by PARTFUN1:def 8
.= b2 . ((SgmX (RelIncl n),(support b2)) . i') by A46, FUNCT_1:22
.= b2 . ((SgmX (RelIncl n),(support b2)) /. i') by A44, PARTFUN1:def 8 ;
thus yb1b2 /. i' = (power L) . ((x * (SgmX (RelIncl n),(support (b1 + b2)))) /. i'),((b1 + b2) . ((SgmX (RelIncl n),(support (b1 + b2))) /. i')) by A6, A16, A36, A43
.= (power L) . ((x * (SgmX (RelIncl n),(support b2))) /. i'),(b2 . ((SgmX (RelIncl n),(support b2)) /. i')) by A4, A15, A38
.= yb2 /. i' by A7, A36, A47 ; :: thesis: verum
end;
A48: u in support b1 by A3, TARSKI:def 1;
support b1 c= dom b1 by POLYNOM1:41;
then A49: u in dom b1 by A48;
A50: dom b1 = n by PARTFUN1:def 4;
then A51: x . u in rng x by A2, A49, FUNCT_1:def 5;
rng x c= the carrier of L by RELAT_1:def 19;
then reconsider xu = x . u as Element of L by A51;
consider a being Element of L such that
A52: a = (power L) . xu,(b1 . u) ;
A53: k in dom (x * (SgmX (RelIncl n),(support b2))) by A2, A17, A49, A50, FUNCT_1:21;
then (x * (SgmX (RelIncl n),(support b2))) . k = x . ((SgmX (RelIncl n),(support b2)) . k) by FUNCT_1:22;
then yb1b2 /. k = a * (yb2 /. k) by A17, A33, A52, A53, PARTFUN1:def 8;
hence eval (b1 + b2),x = a * (Product yb2) by A6, A16, A25, A34, Th8
.= (eval b1,x) * (eval b2,x) by A3, A7, A52, Th17 ;
:: thesis: verum
end;
suppose A54: not u in support b2 ; :: thesis: eval (b1 + b2),x = (eval b1,x) * (eval b2,x)
A55: (b1 + b2) . u = (b1 . u) + (b2 . u) by POLYNOM1:def 5
.= (b1 . u) + 0 by A54, POLYNOM1:def 7 ;
A56: u in support b1 by A3, TARSKI:def 1;
support b1 c= dom b1 by POLYNOM1:41;
then A57: u in dom b1 by A56;
dom b1 = n by PARTFUN1:def 4;
then A58: x . u in rng x by A2, A57, FUNCT_1:def 5;
rng x c= the carrier of L by RELAT_1:def 19;
then reconsider xu = x . u as Element of L by A58;
consider a being Element of L such that
A59: a = (power L) . xu,((b1 + b2) . u) ;
thus eval (b1 + b2),x = a * (eval b2,x) by A4, A9, A54, A59, Lm8
.= (eval b1,x) * (eval b2,x) by A3, A55, A59, Th17 ; :: thesis: verum
end;
end;