let V be RealLinearSpace; :: 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 :: thesis: for v being VECTOR of V st v in Lin (A \/ B) holds
v in (Lin A) + (Lin B)
deffunc H1( object ) -> Element of omega = 0 ;
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 Th14;
deffunc H2( object ) -> set = l . \$1;
set D = () \ A;
set C = () /\ A;
defpred S1[ object ] means \$1 in () /\ A;
defpred S2[ object ] means \$1 in () \ A;
now :: thesis: for x being object st x in the carrier of V holds
( ( x in () /\ A implies l . x in REAL ) & ( not x in () /\ A implies 0 in REAL ) )
let x be object ; :: thesis: ( x in the carrier of V implies ( ( x in () /\ A implies l . x in REAL ) & ( not x in () /\ A implies 0 in REAL ) ) )
assume x in the carrier of V ; :: thesis: ( ( x in () /\ A implies l . x in REAL ) & ( not x in () /\ A implies 0 in REAL ) )
then reconsider v = x as VECTOR of V ;
for f being Function of the carrier of V,REAL holds f . v in REAL ;
hence ( x in () /\ A implies l . x in REAL ) ; :: thesis: ( not x in () /\ A implies 0 in REAL )
assume not x in () /\ A ; :: thesis:
thus 0 in REAL by XREAL_0:def 1; :: thesis: verum
end;
then A2: for x being object st x in the carrier of V holds
( ( S1[x] implies H2(x) in REAL ) & ( not S1[x] implies H1(x) in REAL ) ) ;
consider f being Function of the carrier of V,REAL such that
A3: for x being object st x in the carrier of V holds
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) from reconsider C = () /\ A as finite Subset of V ;
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
for u being VECTOR of V st not u in C holds
f . u = 0 by A3;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def 3;
A4: Carrier f c= C
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in C )
assume x in Carrier f ; :: thesis: x in C
then A5: ex u being VECTOR of V st
( x = u & f . u <> 0 ) ;
assume not x in C ; :: thesis: contradiction
hence contradiction by A3, A5; :: thesis: verum
end;
C c= A by XBOOLE_1:17;
then Carrier f c= A by A4;
then reconsider f = f as Linear_Combination of A by RLVECT_2:def 6;
now :: thesis: for x being object st x in the carrier of V holds
( ( x in () \ A implies l . x in REAL ) & ( not x in () \ A implies 0 in REAL ) )
let x be object ; :: thesis: ( x in the carrier of V implies ( ( x in () \ A implies l . x in REAL ) & ( not x in () \ A implies 0 in REAL ) ) )
assume x in the carrier of V ; :: thesis: ( ( x in () \ A implies l . x in REAL ) & ( not x in () \ A implies 0 in REAL ) )
then reconsider v = x as VECTOR of V ;
for g being Function of the carrier of V,REAL holds g . v in REAL ;
hence ( x in () \ A implies l . x in REAL ) ; :: thesis: ( not x in () \ A implies 0 in REAL )
assume not x in () \ A ; :: thesis:
thus 0 in REAL by XREAL_0:def 1; :: thesis: verum
end;
then A6: for x being object st x in the carrier of V holds
( ( S2[x] implies H2(x) in REAL ) & ( not S2[x] implies H1(x) in REAL ) ) ;
consider g being Function of the carrier of V,REAL such that
A7: for x being object st x in the carrier of V holds
( ( S2[x] implies g . x = H2(x) ) & ( not S2[x] implies g . x = H1(x) ) ) from reconsider D = () \ A as finite Subset of V ;
reconsider g = g as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
for u being VECTOR of V st not u in D holds
g . u = 0 by A7;
then reconsider g = g as Linear_Combination of V by RLVECT_2:def 3;
A8: D c= B
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in B )
assume x in D ; :: thesis: x in B
then A9: ( x in Carrier l & not x in A ) by XBOOLE_0:def 5;
Carrier l c= A \/ B by RLVECT_2:def 6;
hence x in B by ; :: thesis: verum
end;
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 A10: ex u being VECTOR of V st
( x = u & g . u <> 0 ) ;
assume not x in D ; :: thesis: contradiction
hence contradiction by A7, A10; :: thesis: verum
end;
then Carrier g c= B by A8;
then reconsider g = g as Linear_Combination of B by RLVECT_2:def 6;
l = f + g
proof
let v be VECTOR of V; :: according to RLVECT_2:def 9 :: thesis: l . v = (f + g) . v
now :: thesis: (f + g) . v = l . v
per cases ( v in C or not v in C ) ;
suppose A11: v in C ; :: thesis: (f + g) . v = l . v
thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def 10
.= (l . v) + (g . v) by
.= (l . v) + 0 by
.= l . v ; :: thesis: verum
end;
suppose A13: 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 A14: v in Carrier l ; :: thesis: (f + g) . v = l . v
thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def 10
.= 0 + (g . v) by
.= l . v by ; :: thesis: verum
end;
suppose A16: not v in Carrier l ; :: thesis: (f + g) . v = l . v
then A17: not v in D by XBOOLE_0:def 5;
A18: not v in C by ;
thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def 10
.= 0 + (g . v) by
.= 0 + 0 by
.= 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 ;
( Sum f in Lin A & Sum g in Lin B ) by Th14;
hence v in (Lin A) + (Lin B) by ; :: thesis: verum
end;
then A20: Lin (A \/ B) is Subspace of (Lin A) + (Lin B) by RLSUB_1:29;
( Lin A is Subspace of Lin (A \/ B) & Lin B is Subspace of Lin (A \/ B) ) by ;
then (Lin A) + (Lin B) is Subspace of Lin (A \/ B) by Lm6;
hence Lin (A \/ B) = (Lin A) + (Lin B) by ; :: thesis: verum