let X be set ; for a, b being bag of X st support a misses support b holds
Product (a + b) = (Product a) * (Product b)
let a, b be bag of X; ( support a misses support b implies Product (a + b) = (Product a) * (Product b) )
set ab = a + b;
set Pa = Product a;
set Pb = Product b;
set Pab = Product (a + b);
set sab = support (a + b);
set sa = support a;
set sb = support b;
set ca = canFS (support a);
set cb = canFS (support b);
set cg = (canFS (support a)) ^ (canFS (support b));
set cf = canFS (support (a + b));
set p = (((canFS (support a)) ^ (canFS (support b))) ") * (canFS (support (a + b)));
A1:
rng (canFS (support (a + b))) = support (a + b)
by FUNCT_2:def 3;
assume
support a misses support b
; Product (a + b) = (Product a) * (Product b)
then A2:
(support a) /\ (support b) = {}
;
A3:
rng (canFS (support a)) = support a
by FUNCT_2:def 3;
A4:
support (a + b) = (support a) \/ (support b)
by PRE_POLY:38;
A5:
rng (canFS (support b)) = support b
by FUNCT_2:def 3;
then A6:
rng ((canFS (support a)) ^ (canFS (support b))) = support (a + b)
by A4, A3, FINSEQ_1:31;
A7:
( len (canFS (support b)) = card (support b) & len (canFS (support a)) = card (support a) )
by FINSEQ_1:93;
then A8: len ((canFS (support a)) ^ (canFS (support b))) =
((card (support a)) + (card (support b))) - (card {})
by FINSEQ_1:22
.=
card (support (a + b))
by A2, A4, CARD_2:45
;
then A9:
(canFS (support a)) ^ (canFS (support b)) is one-to-one
by A6, FINSEQ_4:62;
then A10:
dom (((canFS (support a)) ^ (canFS (support b))) ") = support (a + b)
by A6, FUNCT_1:33;
then A11:
rng ((((canFS (support a)) ^ (canFS (support b))) ") * (canFS (support (a + b)))) = rng (((canFS (support a)) ^ (canFS (support b))) ")
by A1, RELAT_1:28;
dom ((canFS (support a)) ^ (canFS (support b))) = Seg (card (support (a + b)))
by A8, FINSEQ_1:def 3;
then A12:
rng (((canFS (support a)) ^ (canFS (support b))) ") = Seg (card (support (a + b)))
by A9, FUNCT_1:33;
consider fa being FinSequence of COMPLEX such that
A13:
Product a = Product fa
and
A14:
fa = a * (canFS (support a))
by Def5;
consider fb being FinSequence of COMPLEX such that
A15:
Product b = Product fb
and
A16:
fb = b * (canFS (support b))
by Def5;
set g = fa ^ fb;
consider f being FinSequence of COMPLEX such that
A17:
Product (a + b) = Product f
and
A18:
f = (a + b) * (canFS (support (a + b)))
by Def5;
dom a = X
by PARTFUN1:def 2;
then A19:
dom (canFS (support a)) = dom fa
by A14, A3, RELAT_1:27;
then A20:
len (canFS (support a)) = len fa
by FINSEQ_3:29;
len (canFS (support (a + b))) = card (support (a + b))
by FINSEQ_1:93;
then A21:
dom (canFS (support (a + b))) = Seg (card (support (a + b)))
by FINSEQ_1:def 3;
then A22:
dom ((((canFS (support a)) ^ (canFS (support b))) ") * (canFS (support (a + b)))) = Seg (card (support (a + b)))
by A1, A10, RELAT_1:27;
A23:
dom (a + b) = X
by PARTFUN1:def 2;
then A24:
dom f = Seg (card (support (a + b)))
by A18, A21, A1, RELAT_1:27;
dom b = X
by PARTFUN1:def 2;
then
dom (canFS (support b)) = dom fb
by A16, A5, RELAT_1:27;
then A25:
len (canFS (support b)) = len fb
by FINSEQ_3:29;
then len (fa ^ fb) =
((card (support a)) + (card (support b))) - (card {})
by A7, A20, FINSEQ_1:22
.=
card (support (a + b))
by A2, A4, CARD_2:45
;
then A26:
dom (fa ^ fb) = Seg (card (support (a + b)))
by FINSEQ_1:def 3;
then reconsider p = (((canFS (support a)) ^ (canFS (support b))) ") * (canFS (support (a + b))) as Function of (dom (fa ^ fb)),(dom (fa ^ fb)) by A12, A22, A11, FUNCT_2:1;
p is onto
by A12, A26, A11, FUNCT_2:def 3;
then reconsider p = p as Permutation of (dom (fa ^ fb)) by A9;
A27:
dom ((fa ^ fb) * p) = Seg (card (support (a + b)))
by A12, A22, A26, A11, RELAT_1:27;
A28:
len ((canFS (support a)) ^ (canFS (support b))) = (len (canFS (support a))) + (len (canFS (support b)))
by FINSEQ_1:22;
now for x being object st x in dom f holds
f . x = ((fa ^ fb) * p) . xlet x be
object ;
( x in dom f implies f . b1 = ((fa ^ fb) * p) . b1 )set cgx =
(((canFS (support a)) ^ (canFS (support b))) ") . ((canFS (support (a + b))) . x);
assume A29:
x in dom f
;
f . b1 = ((fa ^ fb) * p) . b1then A30:
((fa ^ fb) * p) . x =
(fa ^ fb) . (p . x)
by A24, A27, FUNCT_1:12
.=
(fa ^ fb) . ((((canFS (support a)) ^ (canFS (support b))) ") . ((canFS (support (a + b))) . x))
by A21, A24, A29, FUNCT_1:13
;
A31:
(canFS (support (a + b))) . x in support (a + b)
by A21, A1, A24, A29, FUNCT_1:3;
then consider d being
object such that A32:
d in dom ((canFS (support a)) ^ (canFS (support b)))
and A33:
((canFS (support a)) ^ (canFS (support b))) . d = (canFS (support (a + b))) . x
by A6, FUNCT_1:def 3;
(((canFS (support a)) ^ (canFS (support b))) ") . ((canFS (support (a + b))) . x) in Seg (card (support (a + b)))
by A10, A12, A31, FUNCT_1:3;
then reconsider cgx =
(((canFS (support a)) ^ (canFS (support b))) ") . ((canFS (support (a + b))) . x) as
Nat ;
reconsider cgxN =
cgx as
Nat ;
A34:
cgx = d
by A9, A32, A33, FUNCT_1:34;
then A35:
1
<= cgxN
by A32, FINSEQ_3:25;
A36:
cgxN <= (len fa) + (len fb)
by A20, A25, A28, A32, A34, FINSEQ_3:25;
per cases
( (canFS (support (a + b))) . x in support a or (canFS (support (a + b))) . x in support b )
by A4, A31, XBOOLE_0:def 3;
suppose
(canFS (support (a + b))) . x in support a
;
f . b1 = ((fa ^ fb) * p) . b1then A37:
not
(canFS (support (a + b))) . x in support b
by A2, XBOOLE_0:def 4;
now not len fa < cgxA38:
cgx - (len (canFS (support a))) <= ((len (canFS (support a))) + (len (canFS (support b)))) - (len (canFS (support a)))
by A20, A25, A36, XREAL_1:9;
assume
len fa < cgx
;
contradictionthen A39:
(len fa) + 1
<= cgx
by NAT_1:13;
then A40:
((len (canFS (support a))) + 1) - (len (canFS (support a))) <= cgx - (len (canFS (support a)))
by A20, XREAL_1:9;
then
cgx - (len (canFS (support a))) is
Element of
NAT
by INT_1:3;
then A41:
cgx - (len (canFS (support a))) in dom (canFS (support b))
by A40, A38, FINSEQ_3:25;
((canFS (support a)) ^ (canFS (support b))) . cgxN = (canFS (support b)) . (cgx - (len (canFS (support a))))
by A20, A25, A36, A39, FINSEQ_1:23;
hence
contradiction
by A5, A33, A34, A37, A41, FUNCT_1:3;
verum end; then A42:
cgxN in dom fa
by A35, FINSEQ_3:25;
then A43:
((canFS (support a)) ^ (canFS (support b))) . cgx = (canFS (support a)) . cgx
by A19, FINSEQ_1:def 7;
A44:
(fa ^ fb) . cgx =
fa . cgxN
by A42, FINSEQ_1:def 7
.=
a . ((canFS (support (a + b))) . x)
by A14, A19, A33, A34, A42, A43, FUNCT_1:13
;
thus f . x =
(a + b) . ((canFS (support (a + b))) . x)
by A18, A29, FUNCT_1:12
.=
(a . ((canFS (support (a + b))) . x)) + (b . ((canFS (support (a + b))) . x))
by PRE_POLY:def 5
.=
(a . ((canFS (support (a + b))) . x)) + 0
by A37, PRE_POLY:def 7
.=
((fa ^ fb) * p) . x
by A30, A44
;
verum end; suppose A45:
(canFS (support (a + b))) . x in support b
;
f . b1 = ((fa ^ fb) * p) . b1then A48:
((canFS (support a)) ^ (canFS (support b))) . cgx = (canFS (support b)) . (cgx - (len (canFS (support a))))
by A20, A25, A36, FINSEQ_1:23;
A49:
cgx - (len (canFS (support a))) <= ((len (canFS (support a))) + (len (canFS (support b)))) - (len (canFS (support a)))
by A20, A25, A36, XREAL_1:9;
A50:
((len (canFS (support a))) + 1) - (len (canFS (support a))) <= cgx - (len (canFS (support a)))
by A20, A46, XREAL_1:9;
then
cgxN - (len (canFS (support a))) in NAT
by INT_1:3;
then A51:
cgxN - (len (canFS (support a))) in dom (canFS (support b))
by A49, A50, FINSEQ_3:25;
A52:
(fa ^ fb) . cgx =
fb . (cgxN - (len fa))
by A36, A46, FINSEQ_1:23
.=
b . ((canFS (support (a + b))) . x)
by A16, A20, A33, A34, A48, A51, FUNCT_1:13
;
A53:
not
(canFS (support (a + b))) . x in support a
by A2, A45, XBOOLE_0:def 4;
thus f . x =
(a + b) . ((canFS (support (a + b))) . x)
by A18, A29, FUNCT_1:12
.=
(a . ((canFS (support (a + b))) . x)) + (b . ((canFS (support (a + b))) . x))
by PRE_POLY:def 5
.=
0 + (b . ((canFS (support (a + b))) . x))
by A53, PRE_POLY:def 7
.=
((fa ^ fb) * p) . x
by A30, A52
;
verum end; end;
then A54:
f = (fa ^ fb) * p
by A18, A21, A1, A23, A27, FUNCT_1:2, RELAT_1:27;
thus Product (a + b) =
multcomplex $$ f
by A17, RVSUM_1:def 13
.=
multcomplex $$ (fa ^ fb)
by A54, FINSOP_1:7
.=
Product (fa ^ fb)
by RVSUM_1:def 13
.=
(Product a) * (Product b)
by A13, A15, RVSUM_1:97
; verum