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)

( Lin A is Subspace of Lin (A \/ B) & Lin B is Subspace of Lin (A \/ B) ) by Th20, XBOOLE_1:7;

then (Lin A) + (Lin B) is Subspace of Lin (A \/ B) by Lm6;

hence Lin (A \/ B) = (Lin A) + (Lin B) by A20, RLSUB_1:26; :: thesis: verum

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)

then A20:
Lin (A \/ B) is Subspace of (Lin A) + (Lin B)
by RLSUB_1:29;v in (Lin A) + (Lin B)

deffunc H_{1}( 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 H_{2}( object ) -> set = l . $1;

set D = (Carrier l) \ A;

set C = (Carrier l) /\ A;

defpred S_{1}[ object ] means $1 in (Carrier l) /\ A;

defpred S_{2}[ object ] means $1 in (Carrier l) \ A;

( ( S_{1}[x] implies H_{2}(x) in REAL ) & ( not S_{1}[x] implies H_{1}(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

( ( S_{1}[x] implies f . x = H_{2}(x) ) & ( not S_{1}[x] implies f . x = H_{1}(x) ) )
from FUNCT_2:sch 5(A2);

reconsider C = (Carrier l) /\ 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

then Carrier f c= A by A4;

then reconsider f = f as Linear_Combination of A by RLVECT_2:def 6;

( ( S_{2}[x] implies H_{2}(x) in REAL ) & ( not S_{2}[x] implies H_{1}(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

( ( S_{2}[x] implies g . x = H_{2}(x) ) & ( not S_{2}[x] implies g . x = H_{1}(x) ) )
from FUNCT_2:sch 5(A6);

reconsider D = (Carrier l) \ 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

then reconsider g = g as Linear_Combination of B by RLVECT_2:def 6;

l = f + g

( Sum f in Lin A & Sum g in Lin B ) by Th14;

hence v in (Lin A) + (Lin B) by A19, RLSUB_2:1; :: thesis: verum

end;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 H

set D = (Carrier l) \ A;

set C = (Carrier l) /\ A;

defpred S

defpred S

now :: thesis: for x being object st x in the carrier of V holds

( ( x in (Carrier l) /\ A implies l . x in REAL ) & ( not x in (Carrier l) /\ A implies 0 in REAL ) )

then A2:
for x being object st x in the carrier of V holds ( ( x in (Carrier l) /\ A implies l . x in REAL ) & ( not x in (Carrier l) /\ A implies 0 in REAL ) )

let x be object ; :: thesis: ( x in the carrier of V implies ( ( x in (Carrier l) /\ A implies l . x in REAL ) & ( not x in (Carrier l) /\ A implies 0 in REAL ) ) )

assume x in the carrier of V ; :: thesis: ( ( x in (Carrier l) /\ A implies l . x in REAL ) & ( not x in (Carrier l) /\ 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 (Carrier l) /\ A implies l . x in REAL ) ; :: thesis: ( not x in (Carrier l) /\ A implies 0 in REAL )

assume not x in (Carrier l) /\ A ; :: thesis: 0 in REAL

thus 0 in REAL by XREAL_0:def 1; :: thesis: verum

end;assume x in the carrier of V ; :: thesis: ( ( x in (Carrier l) /\ A implies l . x in REAL ) & ( not x in (Carrier l) /\ 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 (Carrier l) /\ A implies l . x in REAL ) ; :: thesis: ( not x in (Carrier l) /\ A implies 0 in REAL )

assume not x in (Carrier l) /\ A ; :: thesis: 0 in REAL

thus 0 in REAL by XREAL_0:def 1; :: thesis: verum

( ( S

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

( ( S

reconsider C = (Carrier l) /\ 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

C c= A
by XBOOLE_1:17;
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;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

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 (Carrier l) \ A implies l . x in REAL ) & ( not x in (Carrier l) \ A implies 0 in REAL ) )

then A6:
for x being object st x in the carrier of V holds ( ( x in (Carrier l) \ A implies l . x in REAL ) & ( not x in (Carrier l) \ A implies 0 in REAL ) )

let x be object ; :: thesis: ( x in the carrier of V implies ( ( x in (Carrier l) \ A implies l . x in REAL ) & ( not x in (Carrier l) \ A implies 0 in REAL ) ) )

assume x in the carrier of V ; :: thesis: ( ( x in (Carrier l) \ A implies l . x in REAL ) & ( not x in (Carrier l) \ 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 (Carrier l) \ A implies l . x in REAL ) ; :: thesis: ( not x in (Carrier l) \ A implies 0 in REAL )

assume not x in (Carrier l) \ A ; :: thesis: 0 in REAL

thus 0 in REAL by XREAL_0:def 1; :: thesis: verum

end;assume x in the carrier of V ; :: thesis: ( ( x in (Carrier l) \ A implies l . x in REAL ) & ( not x in (Carrier l) \ 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 (Carrier l) \ A implies l . x in REAL ) ; :: thesis: ( not x in (Carrier l) \ A implies 0 in REAL )

assume not x in (Carrier l) \ A ; :: thesis: 0 in REAL

thus 0 in REAL by XREAL_0:def 1; :: thesis: verum

( ( S

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

( ( S

reconsider D = (Carrier l) \ 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

Carrier g c= D
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 A9, XBOOLE_0:def 3; :: thesis: verum

end;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 A9, XBOOLE_0:def 3; :: thesis: verum

proof

then
Carrier g c= B
by A8;
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;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

then reconsider g = g as Linear_Combination of B by RLVECT_2:def 6;

l = f + g

proof

then A19:
v = (Sum f) + (Sum g)
by A1, Th1;
let v be VECTOR of V; :: according to RLVECT_2:def 9 :: thesis: l . v = (f + g) . v

end;now :: thesis: (f + g) . v = l . vend;

hence
l . v = (f + g) . v
; :: thesis: verumper cases
( v in C or not v in C )
;

end;

suppose A11:
v in C
; :: thesis: (f + g) . v = l . v

.= (l . v) + (g . v) by A3, A11

.= (l . v) + 0 by A7, A12

.= l . v ; :: thesis: verum

end;

A12: now :: thesis: not v in D

thus (f + g) . v =
(f . v) + (g . v)
by RLVECT_2:def 10
assume
v in D
; :: thesis: contradiction

then not v in A by XBOOLE_0:def 5;

hence contradiction by A11, XBOOLE_0:def 4; :: thesis: verum

end;then not v in A by XBOOLE_0:def 5;

hence contradiction by A11, XBOOLE_0:def 4; :: thesis: verum

.= (l . v) + (g . v) by A3, A11

.= (l . v) + 0 by A7, A12

.= l . v ; :: thesis: verum

suppose A13:
not v in C
; :: thesis: l . v = (f + g) . v

end;

now :: thesis: (f + g) . v = l . vend;

hence
l . v = (f + g) . v
; :: thesis: verumper cases
( v in Carrier l or not v in Carrier l )
;

end;

suppose A14:
v in Carrier l
; :: thesis: (f + g) . v = l . v

.= 0 + (g . v) by A3, A13

.= l . v by A7, A15 ; :: thesis: verum

end;

A15: now :: thesis: v in D

thus (f + g) . v =
(f . v) + (g . v)
by RLVECT_2:def 10
assume
not v in D
; :: thesis: contradiction

then ( not v in Carrier l or v in A ) by XBOOLE_0:def 5;

hence contradiction by A13, A14, XBOOLE_0:def 4; :: thesis: verum

end;then ( not v in Carrier l or v in A ) by XBOOLE_0:def 5;

hence contradiction by A13, A14, XBOOLE_0:def 4; :: thesis: verum

.= 0 + (g . v) by A3, A13

.= l . v by A7, A15 ; :: thesis: verum

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 A16, XBOOLE_0:def 4;

thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def 10

.= 0 + (g . v) by A3, A18

.= 0 + 0 by A7, A17

.= l . v by A16 ; :: thesis: verum

end;A18: not v in C by A16, XBOOLE_0:def 4;

thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def 10

.= 0 + (g . v) by A3, A18

.= 0 + 0 by A7, A17

.= l . v by A16 ; :: thesis: verum

( Sum f in Lin A & Sum g in Lin B ) by Th14;

hence v in (Lin A) + (Lin B) by A19, RLSUB_2:1; :: thesis: verum

( Lin A is Subspace of Lin (A \/ B) & Lin B is Subspace of Lin (A \/ B) ) by Th20, XBOOLE_1:7;

then (Lin A) + (Lin B) is Subspace of Lin (A \/ B) by Lm6;

hence Lin (A \/ B) = (Lin A) + (Lin B) by A20, RLSUB_1:26; :: thesis: verum