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