let V be RealLinearSpace; :: thesis: for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)
let L1, L2 be Linear_Combination of V; :: thesis: Sum (L1 + L2) = (Sum L1) + (Sum L2)
consider F being FinSequence of the carrier of V such that
A1: F is one-to-one and
A2: rng F = Carrier (L1 + L2) and
A3: Sum ((L1 + L2) (#) F) = Sum (L1 + L2) by RLVECT_2:def 8;
set A = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2);
set C3 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2));
consider r being FinSequence such that
A4: rng r = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) and
A5: r is one-to-one by FINSEQ_4:58;
reconsider r = r as FinSequence of the carrier of V by ;
set FF = F ^ r;
A6: ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier (L1 + L2)) \/ ((Carrier L1) \/ (Carrier L2)) by XBOOLE_1:4;
rng F misses rng r
proof
set x = the Element of (rng F) /\ (rng r);
assume not rng F misses rng r ; :: thesis: contradiction
then (rng F) /\ (rng r) <> {} ;
then ( the Element of (rng F) /\ (rng r) in Carrier (L1 + L2) & the Element of (rng F) /\ (rng r) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) ) by ;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum
end;
then A7: F ^ r is one-to-one by ;
A8: len r = len ((L1 + L2) (#) r) by RLVECT_2:def 7;
now :: thesis: for k being Nat st k in dom r holds
((L1 + L2) (#) r) . k = 0 * (r /. k)
let k be Nat; :: thesis: ( k in dom r implies ((L1 + L2) (#) r) . k = 0 * (r /. k) )
assume A9: k in dom r ; :: thesis: ((L1 + L2) (#) r) . k = 0 * (r /. k)
then r /. k = r . k by PARTFUN1:def 6;
then r /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) by ;
then A10: not r /. k in Carrier (L1 + L2) by XBOOLE_0:def 5;
k in dom ((L1 + L2) (#) r) by ;
then ((L1 + L2) (#) r) . k = ((L1 + L2) . (r /. k)) * (r /. k) by RLVECT_2:def 7;
hence ((L1 + L2) (#) r) . k = 0 * (r /. k) by A10; :: thesis: verum
end;
then A11: Sum ((L1 + L2) (#) r) = 0 * (Sum r) by
.= 0. V by RLVECT_1:10 ;
set f = (L1 + L2) (#) (F ^ r);
set C1 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1);
consider G being FinSequence of the carrier of V such that
A12: G is one-to-one and
A13: rng G = Carrier L1 and
A14: Sum (L1 (#) G) = Sum L1 by RLVECT_2:def 8;
consider p being FinSequence such that
A15: rng p = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) and
A16: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of the carrier of V by ;
set GG = G ^ p;
A17: Sum ((L1 + L2) (#) (F ^ r)) = Sum (((L1 + L2) (#) F) ^ ((L1 + L2) (#) r)) by Lm1
.= (Sum ((L1 + L2) (#) F)) + (0. V) by
.= Sum ((L1 + L2) (#) F) ;
set C2 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2);
consider H being FinSequence of the carrier of V such that
A18: H is one-to-one and
A19: rng H = Carrier L2 and
A20: Sum (L2 (#) H) = Sum L2 by RLVECT_2:def 8;
consider q being FinSequence such that
A21: rng q = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) and
A22: q is one-to-one by FINSEQ_4:58;
reconsider q = q as FinSequence of the carrier of V by ;
set HH = H ^ q;
rng H misses rng q
proof
set x = the Element of (rng H) /\ (rng q);
assume not rng H misses rng q ; :: thesis: contradiction
then (rng H) /\ (rng q) <> {} ;
then ( the Element of (rng H) /\ (rng q) in Carrier L2 & the Element of (rng H) /\ (rng q) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) ) by ;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum
end;
then A23: H ^ q is one-to-one by ;
set h = L2 (#) (H ^ q);
A24: ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier L1) \/ ((Carrier (L1 + L2)) \/ (Carrier L2)) by XBOOLE_1:4;
rng (G ^ p) = (rng G) \/ (rng p) by FINSEQ_1:31;
then rng (G ^ p) = (Carrier L1) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by ;
then A25: rng (G ^ p) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by ;
A26: len q = len (L2 (#) q) by RLVECT_2:def 7;
now :: thesis: for k being Nat st k in dom q holds
(L2 (#) q) . k = 0 * (q /. k)
let k be Nat; :: thesis: ( k in dom q implies (L2 (#) q) . k = 0 * (q /. k) )
assume A27: k in dom q ; :: thesis: (L2 (#) q) . k = 0 * (q /. k)
then q /. k = q . k by PARTFUN1:def 6;
then q /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) by ;
then A28: not q /. k in Carrier L2 by XBOOLE_0:def 5;
k in dom (L2 (#) q) by ;
then (L2 (#) q) . k = (L2 . (q /. k)) * (q /. k) by RLVECT_2:def 7;
hence (L2 (#) q) . k = 0 * (q /. k) by A28; :: thesis: verum
end;
then A29: Sum (L2 (#) q) = 0 * (Sum q) by
.= 0. V by RLVECT_1:10 ;
A30: Sum (L2 (#) (H ^ q)) = Sum ((L2 (#) H) ^ (L2 (#) q)) by Lm1
.= (Sum (L2 (#) H)) + (0. V) by
.= Sum (L2 (#) H) ;
deffunc H1( Nat) -> set = (F ^ r) <- ((G ^ p) . \$1);
set g = L1 (#) (G ^ p);
consider P being FinSequence such that
A31: len P = len (F ^ r) and
A32: for k being Nat st k in dom P holds
P . k = H1(k) from A33: dom P = Seg (len (F ^ r)) by ;
A34: len p = len (L1 (#) p) by RLVECT_2:def 7;
now :: thesis: for k being Nat st k in dom p holds
(L1 (#) p) . k = 0 * (p /. k)
let k be Nat; :: thesis: ( k in dom p implies (L1 (#) p) . k = 0 * (p /. k) )
assume A35: k in dom p ; :: thesis: (L1 (#) p) . k = 0 * (p /. k)
then p /. k = p . k by PARTFUN1:def 6;
then p /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) by ;
then A36: not p /. k in Carrier L1 by XBOOLE_0:def 5;
k in dom (L1 (#) p) by ;
then (L1 (#) p) . k = (L1 . (p /. k)) * (p /. k) by RLVECT_2:def 7;
hence (L1 (#) p) . k = 0 * (p /. k) by A36; :: thesis: verum
end;
then A37: Sum (L1 (#) p) = 0 * (Sum p) by
.= 0. V by RLVECT_1:10 ;
A38: Sum (L1 (#) (G ^ p)) = Sum ((L1 (#) G) ^ (L1 (#) p)) by Lm1
.= (Sum (L1 (#) G)) + (0. V) by
.= Sum (L1 (#) G) ;
rng (F ^ r) = (rng F) \/ (rng r) by FINSEQ_1:31;
then rng (F ^ r) = (Carrier (L1 + L2)) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by ;
then A39: rng (F ^ r) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by ;
rng G misses rng p
proof
set x = the Element of (rng G) /\ (rng p);
assume not rng G misses rng p ; :: thesis: contradiction
then (rng G) /\ (rng p) <> {} ;
then ( the Element of (rng G) /\ (rng p) in Carrier L1 & the Element of (rng G) /\ (rng p) in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) ) by ;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum
end;
then A40: G ^ p is one-to-one by ;
then A41: len (G ^ p) = len (F ^ r) by ;
A42: dom P = Seg (len (F ^ r)) by ;
A43: now :: thesis: for x being object st x in dom (G ^ p) holds
(G ^ p) . x = (F ^ r) . (P . x)
let x be object ; :: thesis: ( x in dom (G ^ p) implies (G ^ p) . x = (F ^ r) . (P . x) )
assume A44: x in dom (G ^ p) ; :: thesis: (G ^ p) . x = (F ^ r) . (P . x)
then reconsider n = x as Element of NAT by FINSEQ_3:23;
(G ^ p) . n in rng (F ^ r) by ;
then A45: F ^ r just_once_values (G ^ p) . n by ;
n in Seg (len (F ^ r)) by ;
then (F ^ r) . (P . n) = (F ^ r) . ((F ^ r) <- ((G ^ p) . n)) by
.= (G ^ p) . n by ;
hence (G ^ p) . x = (F ^ r) . (P . x) ; :: thesis: verum
end;
A46: rng P c= Seg (len (F ^ r))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng P or x in Seg (len (F ^ r)) )
assume x in rng P ; :: thesis: x in Seg (len (F ^ r))
then consider y being object such that
A47: y in dom P and
A48: P . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by ;
y in Seg (len (F ^ r)) by ;
then y in dom (G ^ p) by ;
then (G ^ p) . y in rng (F ^ r) by ;
then A49: F ^ r just_once_values (G ^ p) . y by ;
P . y = (F ^ r) <- ((G ^ p) . y) by ;
then P . y in dom (F ^ r) by ;
hence x in Seg (len (F ^ r)) by ; :: thesis: verum
end;
now :: thesis: for x being object holds
( ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) & ( x in dom P & P . x in dom (F ^ r) implies x in dom (G ^ p) ) )
let x be object ; :: thesis: ( ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) & ( x in dom P & P . x in dom (F ^ r) implies x in dom (G ^ p) ) )
thus ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) :: thesis: ( x in dom P & P . x in dom (F ^ r) implies x in dom (G ^ p) )
proof
assume x in dom (G ^ p) ; :: thesis: ( x in dom P & P . x in dom (F ^ r) )
then x in Seg (len P) by ;
hence x in dom P by FINSEQ_1:def 3; :: thesis: P . x in dom (F ^ r)
then P . x in rng P by FUNCT_1:def 3;
then P . x in Seg (len (F ^ r)) by A46;
hence P . x in dom (F ^ r) by FINSEQ_1:def 3; :: thesis: verum
end;
assume that
A50: x in dom P and
P . x in dom (F ^ r) ; :: thesis: x in dom (G ^ p)
x in Seg (len P) by ;
hence x in dom (G ^ p) by ; :: thesis: verum
end;
then A51: G ^ p = (F ^ r) * P by ;
Seg (len (F ^ r)) c= rng P
proof
set f = ((F ^ r) ") * (G ^ p);
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg (len (F ^ r)) or x in rng P )
assume A52: x in Seg (len (F ^ r)) ; :: thesis: x in rng P
dom ((F ^ r) ") = rng (G ^ p) by ;
then A53: rng (((F ^ r) ") * (G ^ p)) = rng ((F ^ r) ") by RELAT_1:28
.= dom (F ^ r) by ;
A54: rng P c= dom (F ^ r) by ;
((F ^ r) ") * (G ^ p) = (((F ^ r) ") * (F ^ r)) * P by
.= (id (dom (F ^ r))) * P by
.= P by ;
hence x in rng P by ; :: thesis: verum
end;
then A55: Seg (len (F ^ r)) = rng P by A46;
then A56: P is one-to-one by ;
reconsider P = P as Function of (Seg (len (F ^ r))),(Seg (len (F ^ r))) by ;
reconsider P = P as Permutation of (Seg (len (F ^ r))) by ;
A57: len ((L1 + L2) (#) (F ^ r)) = len (F ^ r) by RLVECT_2:def 7;
then A58: Seg (len (F ^ r)) = dom ((L1 + L2) (#) (F ^ r)) by FINSEQ_1:def 3;
then reconsider Fp = ((L1 + L2) (#) (F ^ r)) * P as FinSequence of the carrier of V by FINSEQ_2:47;
A59: len (L1 (#) (G ^ p)) = len (G ^ p) by RLVECT_2:def 7;
deffunc H2( Nat) -> set = (H ^ q) <- ((G ^ p) . \$1);
consider R being FinSequence such that
A60: len R = len (H ^ q) and
A61: for k being Nat st k in dom R holds
R . k = H2(k) from A62: dom R = Seg (len (H ^ q)) by ;
rng (H ^ q) = (rng H) \/ (rng q) by FINSEQ_1:31;
then rng (H ^ q) = (Carrier L2) \/ (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) by ;
then A63: rng (H ^ q) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by ;
then A64: len (G ^ p) = len (H ^ q) by ;
A65: dom R = Seg (len (H ^ q)) by ;
A66: now :: thesis: for x being object st x in dom (G ^ p) holds
(G ^ p) . x = (H ^ q) . (R . x)
let x be object ; :: thesis: ( x in dom (G ^ p) implies (G ^ p) . x = (H ^ q) . (R . x) )
assume A67: x in dom (G ^ p) ; :: thesis: (G ^ p) . x = (H ^ q) . (R . x)
then reconsider n = x as Element of NAT by FINSEQ_3:23;
(G ^ p) . n in rng (H ^ q) by ;
then A68: H ^ q just_once_values (G ^ p) . n by ;
n in Seg (len (H ^ q)) by ;
then (H ^ q) . (R . n) = (H ^ q) . ((H ^ q) <- ((G ^ p) . n)) by
.= (G ^ p) . n by ;
hence (G ^ p) . x = (H ^ q) . (R . x) ; :: thesis: verum
end;
A69: rng R c= Seg (len (H ^ q))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng R or x in Seg (len (H ^ q)) )
assume x in rng R ; :: thesis: x in Seg (len (H ^ q))
then consider y being object such that
A70: y in dom R and
A71: R . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by ;
y in Seg (len (H ^ q)) by ;
then y in dom (G ^ p) by ;
then (G ^ p) . y in rng (H ^ q) by ;
then A72: H ^ q just_once_values (G ^ p) . y by ;
R . y = (H ^ q) <- ((G ^ p) . y) by ;
then R . y in dom (H ^ q) by ;
hence x in Seg (len (H ^ q)) by ; :: thesis: verum
end;
now :: thesis: for x being object holds
( ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) & ( x in dom R & R . x in dom (H ^ q) implies x in dom (G ^ p) ) )
let x be object ; :: thesis: ( ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) & ( x in dom R & R . x in dom (H ^ q) implies x in dom (G ^ p) ) )
thus ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) :: thesis: ( x in dom R & R . x in dom (H ^ q) implies x in dom (G ^ p) )
proof
assume x in dom (G ^ p) ; :: thesis: ( x in dom R & R . x in dom (H ^ q) )
then x in Seg (len R) by ;
hence x in dom R by FINSEQ_1:def 3; :: thesis: R . x in dom (H ^ q)
then R . x in rng R by FUNCT_1:def 3;
then R . x in Seg (len (H ^ q)) by A69;
hence R . x in dom (H ^ q) by FINSEQ_1:def 3; :: thesis: verum
end;
assume that
A73: x in dom R and
R . x in dom (H ^ q) ; :: thesis: x in dom (G ^ p)
x in Seg (len R) by ;
hence x in dom (G ^ p) by ; :: thesis: verum
end;
then A74: G ^ p = (H ^ q) * R by ;
Seg (len (H ^ q)) c= rng R
proof
set f = ((H ^ q) ") * (G ^ p);
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg (len (H ^ q)) or x in rng R )
assume A75: x in Seg (len (H ^ q)) ; :: thesis: x in rng R
dom ((H ^ q) ") = rng (G ^ p) by ;
then A76: rng (((H ^ q) ") * (G ^ p)) = rng ((H ^ q) ") by RELAT_1:28
.= dom (H ^ q) by ;
A77: rng R c= dom (H ^ q) by ;
((H ^ q) ") * (G ^ p) = (((H ^ q) ") * (H ^ q)) * R by
.= (id (dom (H ^ q))) * R by
.= R by ;
hence x in rng R by ; :: thesis: verum
end;
then A78: Seg (len (H ^ q)) = rng R by A69;
then A79: R is one-to-one by ;
reconsider R = R as Function of (Seg (len (H ^ q))),(Seg (len (H ^ q))) by ;
reconsider R = R as Permutation of (Seg (len (H ^ q))) by ;
A80: len (L2 (#) (H ^ q)) = len (H ^ q) by RLVECT_2:def 7;
then A81: Seg (len (H ^ q)) = dom (L2 (#) (H ^ q)) by FINSEQ_1:def 3;
then reconsider Hp = (L2 (#) (H ^ q)) * R as FinSequence of the carrier of V by FINSEQ_2:47;
A82: len Hp = len (G ^ p) by ;
deffunc H3( Nat) -> Element of the carrier of V = ((L1 (#) (G ^ p)) /. \$1) + (Hp /. \$1);
consider I being FinSequence such that
A83: len I = len (G ^ p) and
A84: for k being Nat st k in dom I holds
I . k = H3(k) from dom I = Seg (len (G ^ p)) by ;
then A85: for k being Nat st k in Seg (len (G ^ p)) holds
I . k = H3(k) by A84;
rng I c= the carrier of V
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng I or x in the carrier of V )
assume x in rng I ; :: thesis: x in the carrier of V
then consider y being object such that
A86: y in dom I and
A87: I . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by ;
I . y = ((L1 (#) (G ^ p)) /. y) + (Hp /. y) by ;
hence x in the carrier of V by A87; :: thesis: verum
end;
then reconsider I = I as FinSequence of the carrier of V by FINSEQ_1:def 4;
A88: len Fp = len I by ;
A89: now :: thesis: for x being object st x in dom I holds
I . x = Fp . x
let x be object ; :: thesis: ( x in dom I implies I . x = Fp . x )
assume A90: x in dom I ; :: thesis: I . x = Fp . x
then reconsider k = x as Element of NAT by FINSEQ_3:23;
A91: x in dom Hp by ;
k in dom R by ;
then A92: R . k in dom R by ;
then reconsider j = R . k as Element of NAT by FINSEQ_3:23;
set v = (G ^ p) /. k;
A93: R . k in dom (H ^ q) by ;
A94: x in dom (G ^ p) by ;
then (H ^ q) . j = (G ^ p) . k by A66
.= (G ^ p) /. k by ;
then A95: (L2 (#) (H ^ q)) . j = (L2 . ((G ^ p) /. k)) * ((G ^ p) /. k) by ;
k in dom P by ;
then A96: P . k in dom P by ;
then reconsider l = P . k as Element of NAT by FINSEQ_3:23;
A97: P . k in dom (F ^ r) by ;
x in dom Fp by ;
then A98: Fp . k = ((L1 + L2) (#) (F ^ r)) . (P . k) by FUNCT_1:12;
k in dom Hp by ;
then A99: Hp /. k = ((L2 (#) (H ^ q)) * R) . k by PARTFUN1:def 6
.= (L2 (#) (H ^ q)) . (R . k) by ;
A100: x in dom (L1 (#) (G ^ p)) by ;
(F ^ r) . l = (G ^ p) . k by
.= (G ^ p) /. k by ;
then A101: ((L1 + L2) (#) (F ^ r)) . l = ((L1 + L2) . ((G ^ p) /. k)) * ((G ^ p) /. k) by
.= ((L1 . ((G ^ p) /. k)) + (L2 . ((G ^ p) /. k))) * ((G ^ p) /. k) by RLVECT_2:def 10
.= ((L1 . ((G ^ p) /. k)) * ((G ^ p) /. k)) + ((L2 . ((G ^ p) /. k)) * ((G ^ p) /. k)) by RLVECT_1:def 6 ;
k in dom (L1 (#) (G ^ p)) by ;
then (L1 (#) (G ^ p)) /. k = (L1 (#) (G ^ p)) . k by PARTFUN1:def 6
.= (L1 . ((G ^ p) /. k)) * ((G ^ p) /. k) by ;
hence I . x = Fp . x by A84, A90, A99, A95, A98, A101; :: thesis: verum
end;
dom (L2 (#) (H ^ q)) = Seg (len (L2 (#) (H ^ q))) by FINSEQ_1:def 3;
then A102: Sum Hp = Sum (L2 (#) (H ^ q)) by ;
dom ((L1 + L2) (#) (F ^ r)) = Seg (len ((L1 + L2) (#) (F ^ r))) by FINSEQ_1:def 3;
then A103: Sum Fp = Sum ((L1 + L2) (#) (F ^ r)) by ;
( dom I = Seg (len I) & dom Fp = Seg (len I) ) by ;
then A104: I = Fp by ;
Seg (len (G ^ p)) = dom (L1 (#) (G ^ p)) by ;
hence Sum (L1 + L2) = (Sum L1) + (Sum L2) by A3, A14, A20, A38, A30, A17, A103, A102, A83, A85, A82, A59, A104, RLVECT_2:2; :: thesis: verum