let R be domRing; :: thesis: for V being LeftMod of R
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
let V be LeftMod of R; :: thesis: for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
let A, B be Subset of V; :: thesis: Lin (A \/ B) = (Lin A) + (Lin B)
now
deffunc H1( set ) -> Element of the carrier of R = 0. R;
let v be Vector of V; :: thesis: ( v in Lin (A \/ B) implies v in (Lin A) + (Lin B) )
assume v in Lin (A \/ B) ; :: thesis: v in (Lin A) + (Lin B)
then consider l being Linear_Combination of A \/ B such that
A1: v = Sum l by Th9;
deffunc H2( set ) -> set = l . $1;
set D = (Carrier l) \ A;
set C = (Carrier l) /\ A;
defpred S1[ set ] means $1 in (Carrier l) /\ A;
A2: now
let x be set ; :: thesis: ( x in the carrier of V implies ( ( S1[x] implies H2(x) in the carrier of R ) & ( not S1[x] implies H1(x) in the carrier of R ) ) )
assume x in the carrier of V ; :: thesis: ( ( S1[x] implies H2(x) in the carrier of R ) & ( not S1[x] implies H1(x) in the carrier of R ) )
then reconsider v = x as Vector of V ;
for f being Function of the carrier of V,the carrier of R holds f . v in the carrier of R ;
hence ( S1[x] implies H2(x) in the carrier of R ) ; :: thesis: ( not S1[x] implies H1(x) in the carrier of R )
assume not S1[x] ; :: thesis: H1(x) in the carrier of R
thus H1(x) in the carrier of R ; :: thesis: verum
end;
A3: (Carrier l) \ A c= B
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Carrier l) \ A or x in B )
assume x in (Carrier l) \ A ; :: thesis: x in B
then A4: ( x in Carrier l & not x in A ) by XBOOLE_0:def 5;
Carrier l c= A \/ B by VECTSP_6:def 7;
hence x in B by A4, XBOOLE_0:def 3; :: thesis: verum
end;
consider f being Function of the carrier of V,the carrier of R such that
A5: for x being set st x in the carrier of V holds
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) from FUNCT_2:sch 5(A2);
reconsider f = f as Element of Funcs the carrier of V,the carrier of R by FUNCT_2:11;
for u being Vector of V st not u in (Carrier l) /\ A holds
f . u = 0. R by A5;
then reconsider f = f as Linear_Combination of V by VECTSP_6:def 4;
A6: Carrier f c= (Carrier l) /\ A
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in (Carrier l) /\ A )
assume x in Carrier f ; :: thesis: x in (Carrier l) /\ A
then A7: ex u being Vector of V st
( x = u & f . u <> 0. R ) ;
assume not x in (Carrier l) /\ A ; :: thesis: contradiction
hence contradiction by A5, A7; :: thesis: verum
end;
(Carrier l) /\ A c= A by XBOOLE_1:17;
then Carrier f c= A by A6, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by VECTSP_6:def 7;
defpred S2[ set ] means $1 in (Carrier l) \ A;
A8: now
let x be set ; :: thesis: ( x in the carrier of V implies ( ( S2[x] implies H2(x) in the carrier of R ) & ( not S2[x] implies H1(x) in the carrier of R ) ) )
assume x in the carrier of V ; :: thesis: ( ( S2[x] implies H2(x) in the carrier of R ) & ( not S2[x] implies H1(x) in the carrier of R ) )
then reconsider v = x as Vector of V ;
for g being Function of the carrier of V,the carrier of R holds g . v in the carrier of R ;
hence ( S2[x] implies H2(x) in the carrier of R ) ; :: thesis: ( not S2[x] implies H1(x) in the carrier of R )
assume not S2[x] ; :: thesis: H1(x) in the carrier of R
thus H1(x) in the carrier of R ; :: thesis: verum
end;
consider g being Function of the carrier of V,the carrier of R such that
A9: for x being set st x in the carrier of V holds
( ( S2[x] implies g . x = H2(x) ) & ( not S2[x] implies g . x = H1(x) ) ) from FUNCT_2:sch 5(A8);
reconsider g = g as Element of Funcs the carrier of V,the carrier of R by FUNCT_2:11;
for u being Vector of V st not u in (Carrier l) \ A holds
g . u = 0. R by A9;
then reconsider g = g as Linear_Combination of V by VECTSP_6:def 4;
Carrier g c= (Carrier l) \ A
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier g or x in (Carrier l) \ A )
assume x in Carrier g ; :: thesis: x in (Carrier l) \ A
then A10: ex u being Vector of V st
( x = u & g . u <> 0. R ) ;
assume not x in (Carrier l) \ A ; :: thesis: contradiction
hence contradiction by A9, A10; :: thesis: verum
end;
then Carrier g c= B by A3, XBOOLE_1:1;
then reconsider g = g as Linear_Combination of B by VECTSP_6:def 7;
l = f + g
proof
let v be Vector of V; :: according to VECTSP_6:def 10 :: thesis: l . v = (f + g) . v
now
per cases ( v in (Carrier l) /\ A or not v in (Carrier l) /\ A ) ;
suppose A11: v in (Carrier l) /\ A ; :: thesis: (f + g) . v = l . v
thus (f + g) . v = (f . v) + (g . v) by VECTSP_6:def 11
.= (l . v) + (g . v) by A5, A11
.= (l . v) + (0. R) by A9, A12
.= l . v by RLVECT_1:10 ; :: thesis: verum
end;
suppose A13: not v in (Carrier l) /\ A ; :: thesis: l . v = (f + g) . v
now
per cases ( v in Carrier l or not v in Carrier l ) ;
suppose A14: v in Carrier l ; :: thesis: (f + g) . v = l . v
thus (f + g) . v = (f . v) + (g . v) by VECTSP_6:def 11
.= (0. R) + (g . v) by A5, A13
.= g . v by RLVECT_1:10
.= l . v by A9, A15 ; :: thesis: verum
end;
suppose A16: not v in Carrier l ; :: thesis: (f + g) . v = l . v
then A17: not v in (Carrier l) \ A by XBOOLE_0:def 5;
A18: not v in (Carrier l) /\ A by A16, XBOOLE_0:def 4;
thus (f + g) . v = (f . v) + (g . v) by VECTSP_6:def 11
.= (0. R) + (g . v) by A5, A18
.= (0. R) + (0. R) by A9, A17
.= 0. R by RLVECT_1:10
.= l . v by A16 ; :: thesis: verum
end;
end;
end;
hence l . v = (f + g) . v ; :: thesis: verum
end;
end;
end;
hence l . v = (f + g) . v ; :: thesis: verum
end;
then A19: v = (Sum f) + (Sum g) by A1, VECTSP_6:77;
( Sum f in Lin A & Sum g in Lin B ) by Th9;
hence v in (Lin A) + (Lin B) by A19, VECTSP_5:5; :: thesis: verum
end;
then A20: Lin (A \/ B) is Subspace of (Lin A) + (Lin B) by VECTSP_4:36;
( Lin A is Subspace of Lin (A \/ B) & Lin B is Subspace of Lin (A \/ B) ) by Th15, XBOOLE_1:7;
then (Lin A) + (Lin B) is Subspace of Lin (A \/ B) by VECTSP_5:40;
hence Lin (A \/ B) = (Lin A) + (Lin B) by A20, VECTSP_4:33; :: thesis: verum