let K be Field; :: thesis: for V being VectSp of K
for W1, W2 being Subspace of V st W1 /\ W2 = (0). V holds
for B1 being linearly-independent Subset of W1
for B2 being linearly-independent Subset of W2 holds B1 \/ B2 is linearly-independent Subset of (W1 + W2)
let V be VectSp of K; :: thesis: for W1, W2 being Subspace of V st W1 /\ W2 = (0). V holds
for B1 being linearly-independent Subset of W1
for B2 being linearly-independent Subset of W2 holds B1 \/ B2 is linearly-independent Subset of (W1 + W2)
let W1, W2 be Subspace of V; :: thesis: ( W1 /\ W2 = (0). V implies for B1 being linearly-independent Subset of W1
for B2 being linearly-independent Subset of W2 holds B1 \/ B2 is linearly-independent Subset of (W1 + W2) )
assume A1: W1 /\ W2 = (0). V ; :: thesis: for B1 being linearly-independent Subset of W1
for B2 being linearly-independent Subset of W2 holds B1 \/ B2 is linearly-independent Subset of (W1 + W2)
reconsider W19 = W1, W29 = W2 as Subspace of W1 + W2 by VECTSP_5:7;
let B1 be linearly-independent Subset of W1; :: thesis: for B2 being linearly-independent Subset of W2 holds B1 \/ B2 is linearly-independent Subset of (W1 + W2)
let B2 be linearly-independent Subset of W2; :: thesis: B1 \/ B2 is linearly-independent Subset of (W1 + W2)
A2: W2 is Subspace of W1 + W2 by VECTSP_5:7;
then the carrier of W2 c= the carrier of (W1 + W2) by VECTSP_4:def 2;
then A3: B2 c= the carrier of (W1 + W2) ;
A4: W1 is Subspace of W1 + W2 by VECTSP_5:7;
then the carrier of W1 c= the carrier of (W1 + W2) by VECTSP_4:def 2;
then B1 c= the carrier of (W1 + W2) ;
then reconsider B12 = B1 \/ B2, B19 = B1, B29 = B2 as Subset of (W1 + W2) by A3, XBOOLE_1:8;
B12 is linearly-independent
proof
let L be Linear_Combination of B12; :: according to VECTSP_7:def 1 :: thesis: ( not Sum L = 0. (W1 + W2) or Carrier L = {} )
assume Sum L = 0. (W1 + W2) ; :: thesis: Carrier L = {}
then A5: Sum L = (0. (W1 + W2)) + (0. (W1 + W2)) by RLVECT_1:def 4;
set C = (Carrier L) /\ B1;
defpred S1[ object ] means $1 in (Carrier L) /\ B1;
(Carrier L) /\ B1 c= Carrier L by XBOOLE_1:17;
then reconsider C = (Carrier L) /\ B1 as finite Subset of (W1 + W2) by XBOOLE_1:1;
set D = (Carrier L) \ B1;
deffunc H1( object ) -> set = L . $1;
defpred S2[ object ] means $1 in (Carrier L) \ B1;
reconsider D = (Carrier L) \ B1 as finite Subset of (W1 + W2) ;
A6: D c= B29
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in B29 )
assume x in D ; :: thesis: x in B29
then A7: ( x in Carrier L & not x in B19 ) by XBOOLE_0:def 5;
Carrier L c= B12 by VECTSP_6:def 4;
hence x in B29 by A7, XBOOLE_0:def 3; :: thesis: verum
end;
(0). V = (0). (W1 + W2) by VECTSP_4:36;
then A8: W19 /\ W29 = (0). (W1 + W2) by A1, Th1;
W19 + W29 = W1 + W2 by Th1;
then A9: W1 + W2 is_the_direct_sum_of W19,W29 by A8, VECTSP_5:def 4;
A10: B29 is linearly-independent by A2, VECTSP_9:11;
A11: B19 is linearly-independent by A4, VECTSP_9:11;
deffunc H2( object ) -> Element of the carrier of K = 0. K;
A12: ( 0. W1 in W19 & 0. W2 in W29 ) ;
A13: now :: thesis: for x being object st x in the carrier of (W1 + W2) holds
( ( S1[x] implies H1(x) in the carrier of K ) & ( not S1[x] implies H2(x) in the carrier of K ) )
let x be object ; :: thesis: ( x in the carrier of (W1 + W2) implies ( ( S1[x] implies H1(x) in the carrier of K ) & ( not S1[x] implies H2(x) in the carrier of K ) ) )
assume x in the carrier of (W1 + W2) ; :: thesis: ( ( S1[x] implies H1(x) in the carrier of K ) & ( not S1[x] implies H2(x) in the carrier of K ) )
then reconsider v = x as Vector of (W1 + W2) ;
L . v in the carrier of K ;
hence ( S1[x] implies H1(x) in the carrier of K ) ; :: thesis: ( not S1[x] implies H2(x) in the carrier of K )
assume not S1[x] ; :: thesis: H2(x) in the carrier of K
thus H2(x) in the carrier of K ; :: thesis: verum
end;
consider f being Function of the carrier of (W1 + W2), the carrier of K such that
A14: for x being object st x in the carrier of (W1 + W2) holds
( ( S1[x] implies f . x = H1(x) ) & ( not S1[x] implies f . x = H2(x) ) ) from FUNCT_2:sch 5(A13);
 deffunc H3( object ) -> set = L . $1;
A15: now :: thesis: for x being object st x in the carrier of (W1 + W2) holds
( ( S2[x] implies H3(x) in the carrier of K ) & ( not S2[x] implies H2(x) in the carrier of K ) )
let x be object ; :: thesis: ( x in the carrier of (W1 + W2) implies ( ( S2[x] implies H3(x) in the carrier of K ) & ( not S2[x] implies H2(x) in the carrier of K ) ) )
assume x in the carrier of (W1 + W2) ; :: thesis: ( ( S2[x] implies H3(x) in the carrier of K ) & ( not S2[x] implies H2(x) in the carrier of K ) )
then reconsider v = x as Vector of (W1 + W2) ;
L . v in the carrier of K ;
hence ( S2[x] implies H3(x) in the carrier of K ) ; :: thesis: ( not S2[x] implies H2(x) in the carrier of K )
assume not S2[x] ; :: thesis: H2(x) in the carrier of K
thus H2(x) in the carrier of K ; :: thesis: verum
end;
consider g being Function of the carrier of (W1 + W2), the carrier of K such that
A16: for x being object st x in the carrier of (W1 + W2) holds
( ( S2[x] implies g . x = H3(x) ) & ( not S2[x] implies g . x = H2(x) ) ) from FUNCT_2:sch 5(A15);
 reconsider g = g as Element of Funcs ( the carrier of (W1 + W2), the carrier of K) by FUNCT_2:8;
for u being Vector of (W1 + W2) st not u in D holds
g . u = 0. K by A16;
then reconsider g = g as Linear_Combination of W1 + W2 by VECTSP_6:def 1;
A17: Carrier g c= D
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier g or x in D )
assume x in Carrier g ; :: thesis: x in D
then A18: ex u being Vector of (W1 + W2) st
( x = u & g . u <> 0. K ) ;
assume not x in D ; :: thesis: contradiction
hence contradiction by A16, A18; :: thesis: verum
end;
then Carrier g c= B29 by A6;
then reconsider g = g as Linear_Combination of B29 by VECTSP_6:def 4;
reconsider f = f as Element of Funcs ( the carrier of (W1 + W2), the carrier of K) by FUNCT_2:8;
for u being Vector of (W1 + W2) st not u in C holds
f . u = 0. K by A14;
then reconsider f = f as Linear_Combination of W1 + W2 by VECTSP_6:def 1;
A19: Carrier f c= B19
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in B19 )
assume x in Carrier f ; :: thesis: x in B19
then A20: ex u being Vector of (W1 + W2) st
( x = u & f . u <> 0. K ) ;
assume not x in B19 ; :: thesis: contradiction
then not x in C by XBOOLE_0:def 4;
hence contradiction by A14, A20; :: thesis: verum
end;
then reconsider f = f as Linear_Combination of B19 by VECTSP_6:def 4;
ex f1 being Linear_Combination of W19 st
( Carrier f1 = Carrier f & Sum f = Sum f1 ) by A19, VECTSP_9:9, XBOOLE_1:1;
then A21: Sum f in W19 ;
A22: L = f + g
proof
let v be Vector of (W1 + W2); :: according to VECTSP_6:def 7 :: thesis: L . v = (f + g) . v
now :: thesis: (f + g) . v = L . v
per cases ( v in C or not v in C ) ;
suppose A23: v in C ; :: thesis: (f + g) . v = L . v
thus (f + g) . v = (f . v) + (g . v) by VECTSP_6:22
.= (L . v) + (g . v) by A14, A23
.= (L . v) + (0. K) by A16, A24
.= L . v by RLVECT_1:4 ; :: thesis: verum
end;
suppose A25: not v in C ; :: thesis: L . v = (f + g) . v
now :: thesis: (f + g) . v = L . v
per cases ( v in Carrier L or not v in Carrier L ) ;
suppose A26: v in Carrier L ; :: thesis: (f + g) . v = L . v
thus (f + g) . v = (f . v) + (g . v) by VECTSP_6:22
.= (g . v) + (0. K) by A14, A25
.= g . v by RLVECT_1:4
.= L . v by A16, A27 ; :: thesis: verum
end;
suppose A28: not v in Carrier L ; :: thesis: (f + g) . v = L . v
then A29: not v in D by XBOOLE_0:def 5;
A30: not v in C by A28, XBOOLE_0:def 4;
thus (f + g) . v = (f . v) + (g . v) by VECTSP_6:22
.= (0. K) + (g . v) by A14, A30
.= (0. K) + (0. K) by A16, A29
.= 0. K by RLVECT_1:4
.= L . v by A28 ; :: 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 A31: Sum L = (Sum f) + (Sum g) by VECTSP_6:44;
Carrier g c= B2 by A17, A6;
then ex g1 being Linear_Combination of W29 st
( Carrier g1 = Carrier g & Sum g = Sum g1 ) by VECTSP_9:9, XBOOLE_1:1;
then A32: Sum g in W29 ;
A33: ( 0. (W1 + W2) = 0. W19 & 0. (W1 + W2) = 0. W29 ) by VECTSP_4:11;
then Sum f = 0. (W1 + W2) by A31, A21, A32, A9, A12, A5, VECTSP_5:48;
then A34: Carrier f = {} by A11;
Sum g = 0. (W1 + W2) by A31, A21, A32, A9, A33, A12, A5, VECTSP_5:48;
then A35: Carrier g = {} by A10;
{} \/ {} = {} ;
hence Carrier L = {} by A22, A34, A35, VECTSP_6:23, XBOOLE_1:3; :: thesis: verum
end;
hence B1 \/ B2 is linearly-independent Subset of (W1 + W2) ; :: thesis: verum