:: RUSUB_3 semantic presentation
begin
definition
let V be RealUnitarySpace;
let A be Subset of V;
func Lin A -> strict Subspace of V means :Def1: :: RUSUB_3:def 1
the carrier of it = { (Sum l) where l is Linear_Combination of A : verum } ;
existence
ex b1 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum }
proof
set A1 = { (Sum l) where l is Linear_Combination of A : verum } ;
{ (Sum l) where l is Linear_Combination of A : verum } c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Sum l) where l is Linear_Combination of A : verum } or x in the carrier of V )
assume x in { (Sum l) where l is Linear_Combination of A : verum } ; ::_thesis: x in the carrier of V
then ex l being Linear_Combination of A st x = Sum l ;
hence x in the carrier of V ; ::_thesis: verum
end;
then reconsider A1 = { (Sum l) where l is Linear_Combination of A : verum } as Subset of V ;
reconsider l = ZeroLC V as Linear_Combination of A by RLVECT_2:22;
A1: A1 is linearly-closed
proof
thus for v, u being VECTOR of V st v in A1 & u in A1 holds
v + u in A1 :: according to RLSUB_1:def_1 ::_thesis: for b1 being Element of REAL
for b2 being Element of the carrier of V holds
( not b2 in A1 or b1 * b2 in A1 )
proof
let v, u be VECTOR of V; ::_thesis: ( v in A1 & u in A1 implies v + u in A1 )
assume that
A2: v in A1 and
A3: u in A1 ; ::_thesis: v + u in A1
consider l1 being Linear_Combination of A such that
A4: v = Sum l1 by A2;
consider l2 being Linear_Combination of A such that
A5: u = Sum l2 by A3;
reconsider f = l1 + l2 as Linear_Combination of A by RLVECT_2:38;
v + u = Sum f by A4, A5, RLVECT_3:1;
hence v + u in A1 ; ::_thesis: verum
end;
let a be Real; ::_thesis: for b1 being Element of the carrier of V holds
( not b1 in A1 or a * b1 in A1 )
let v be VECTOR of V; ::_thesis: ( not v in A1 or a * v in A1 )
assume v in A1 ; ::_thesis: a * v in A1
then consider l being Linear_Combination of A such that
A6: v = Sum l ;
reconsider f = a * l as Linear_Combination of A by RLVECT_2:44;
a * v = Sum f by A6, RLVECT_3:2;
hence a * v in A1 ; ::_thesis: verum
end;
Sum l = 0. V by RLVECT_2:30;
then 0. V in A1 ;
hence ex b1 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } by A1, RUSUB_1:29; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } & the carrier of b2 = { (Sum l) where l is Linear_Combination of A : verum } holds
b1 = b2 by RUSUB_1:24;
end;
:: deftheorem Def1 defines Lin RUSUB_3:def_1_:_
for V being RealUnitarySpace
for A being Subset of V
for b3 being strict Subspace of V holds
( b3 = Lin A iff the carrier of b3 = { (Sum l) where l is Linear_Combination of A : verum } );
theorem Th1: :: RUSUB_3:1
for V being RealUnitarySpace
for A being Subset of V
for x being set holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
proof
let V be RealUnitarySpace; ::_thesis: for A being Subset of V
for x being set holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
let A be Subset of V; ::_thesis: for x being set holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
let x be set ; ::_thesis: ( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
thus ( x in Lin A implies ex l being Linear_Combination of A st x = Sum l ) ::_thesis: ( ex l being Linear_Combination of A st x = Sum l implies x in Lin A )
proof
assume x in Lin A ; ::_thesis: ex l being Linear_Combination of A st x = Sum l
then x in the carrier of (Lin A) by STRUCT_0:def_5;
then x in { (Sum l) where l is Linear_Combination of A : verum } by Def1;
hence ex l being Linear_Combination of A st x = Sum l ; ::_thesis: verum
end;
given k being Linear_Combination of A such that A1: x = Sum k ; ::_thesis: x in Lin A
x in { (Sum l) where l is Linear_Combination of A : verum } by A1;
then x in the carrier of (Lin A) by Def1;
hence x in Lin A by STRUCT_0:def_5; ::_thesis: verum
end;
theorem Th2: :: RUSUB_3:2
for V being RealUnitarySpace
for A being Subset of V
for x being set st x in A holds
x in Lin A
proof
deffunc H1( set ) -> Element of NAT = 0 ;
let V be RealUnitarySpace; ::_thesis: for A being Subset of V
for x being set st x in A holds
x in Lin A
let A be Subset of V; ::_thesis: for x being set st x in A holds
x in Lin A
let x be set ; ::_thesis: ( x in A implies x in Lin A )
assume A1: x in A ; ::_thesis: x in Lin A
then reconsider v = x as VECTOR of V ;
consider f being Function of the carrier of V,REAL such that
A2: f . v = 1 and
A3: for u being VECTOR of V st u <> v holds
f . u = H1(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
ex T being finite Subset of V st
for u being VECTOR of V st not u in T holds
f . u = 0
proof
take T = {v}; ::_thesis: for u being VECTOR of V st not u in T holds
f . u = 0
let u be VECTOR of V; ::_thesis: ( not u in T implies f . u = 0 )
assume not u in T ; ::_thesis: f . u = 0
then u <> v by TARSKI:def_1;
hence f . u = 0 by A3; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
A4: Carrier f c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} )
assume x in Carrier f ; ::_thesis: x in {v}
then consider u being VECTOR of V such that
A5: x = u and
A6: f . u <> 0 ;
u = v by A3, A6;
hence x in {v} by A5, TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {v} by RLVECT_2:def_6;
A7: Sum f = 1 * v by A2, RLVECT_2:32
.= v by RLVECT_1:def_8 ;
{v} c= A by A1, ZFMISC_1:31;
then Carrier f c= A by A4, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by RLVECT_2:def_6;
Sum f = v by A7;
hence x in Lin A by Th1; ::_thesis: verum
end;
Lm1: for V being RealUnitarySpace
for x being set holds
( x in (0). V iff x = 0. V )
proof
let V be RealUnitarySpace; ::_thesis: for x being set holds
( x in (0). V iff x = 0. V )
let x be set ; ::_thesis: ( x in (0). V iff x = 0. V )
thus ( x in (0). V implies x = 0. V ) ::_thesis: ( x = 0. V implies x in (0). V )
proof
assume x in (0). V ; ::_thesis: x = 0. V
then x in the carrier of ((0). V) by STRUCT_0:def_5;
then x in {(0. V)} by RUSUB_1:def_2;
hence x = 0. V by TARSKI:def_1; ::_thesis: verum
end;
thus ( x = 0. V implies x in (0). V ) by RUSUB_1:11; ::_thesis: verum
end;
theorem :: RUSUB_3:3
for V being RealUnitarySpace holds Lin ({} the carrier of V) = (0). V
proof
let V be RealUnitarySpace; ::_thesis: Lin ({} the carrier of V) = (0). V
set A = Lin ({} the carrier of V);
now__::_thesis:_for_v_being_VECTOR_of_V_holds_
(_(_v_in_Lin_({}_the_carrier_of_V)_implies_v_in_(0)._V_)_&_(_v_in_(0)._V_implies_v_in_Lin_({}_the_carrier_of_V)_)_)
let v be VECTOR of V; ::_thesis: ( ( v in Lin ({} the carrier of V) implies v in (0). V ) & ( v in (0). V implies v in Lin ({} the carrier of V) ) )
thus ( v in Lin ({} the carrier of V) implies v in (0). V ) ::_thesis: ( v in (0). V implies v in Lin ({} the carrier of V) )
proof
assume v in Lin ({} the carrier of V) ; ::_thesis: v in (0). V
then A1: v in the carrier of (Lin ({} the carrier of V)) by STRUCT_0:def_5;
the carrier of (Lin ({} the carrier of V)) = { (Sum l0) where l0 is Linear_Combination of {} the carrier of V : verum } by Def1;
then ex l0 being Linear_Combination of {} the carrier of V st v = Sum l0 by A1;
then v = 0. V by RLVECT_2:31;
hence v in (0). V by Lm1; ::_thesis: verum
end;
assume v in (0). V ; ::_thesis: v in Lin ({} the carrier of V)
then v = 0. V by Lm1;
hence v in Lin ({} the carrier of V) by RUSUB_1:11; ::_thesis: verum
end;
hence Lin ({} the carrier of V) = (0). V by RUSUB_1:25; ::_thesis: verum
end;
theorem :: RUSUB_3:4
for V being RealUnitarySpace
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
proof
let V be RealUnitarySpace; ::_thesis: for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
let A be Subset of V; ::_thesis: ( not Lin A = (0). V or A = {} or A = {(0. V)} )
assume that
A1: Lin A = (0). V and
A2: A <> {} ; ::_thesis: A = {(0. V)}
thus A c= {(0. V)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. V)} c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in {(0. V)} )
assume x in A ; ::_thesis: x in {(0. V)}
then x in Lin A by Th2;
then x = 0. V by A1, Lm1;
hence x in {(0. V)} by TARSKI:def_1; ::_thesis: verum
end;
set y = the Element of A;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. V)} or x in A )
assume x in {(0. V)} ; ::_thesis: x in A
then A3: x = 0. V by TARSKI:def_1;
( the Element of A in A & the Element of A in Lin A ) by A2, Th2;
hence x in A by A1, A3, Lm1; ::_thesis: verum
end;
theorem Th5: :: RUSUB_3:5
for V being RealUnitarySpace
for W being strict Subspace of V
for A being Subset of V st A = the carrier of W holds
Lin A = W
proof
let V be RealUnitarySpace; ::_thesis: for W being strict Subspace of V
for A being Subset of V st A = the carrier of W holds
Lin A = W
let W be strict Subspace of V; ::_thesis: for A being Subset of V st A = the carrier of W holds
Lin A = W
let A be Subset of V; ::_thesis: ( A = the carrier of W implies Lin A = W )
assume A1: A = the carrier of W ; ::_thesis: Lin A = W
now__::_thesis:_for_v_being_VECTOR_of_V_holds_
(_(_v_in_Lin_A_implies_v_in_W_)_&_(_v_in_W_implies_v_in_Lin_A_)_)
let v be VECTOR of V; ::_thesis: ( ( v in Lin A implies v in W ) & ( v in W implies v in Lin A ) )
thus ( v in Lin A implies v in W ) ::_thesis: ( v in W implies v in Lin A )
proof
assume v in Lin A ; ::_thesis: v in W
then A2: ex l being Linear_Combination of A st v = Sum l by Th1;
A is linearly-closed by A1, RUSUB_1:28;
then v in the carrier of W by A1, A2, RLVECT_2:29;
hence v in W by STRUCT_0:def_5; ::_thesis: verum
end;
( v in W iff v in the carrier of W ) by STRUCT_0:def_5;
hence ( v in W implies v in Lin A ) by A1, Th2; ::_thesis: verum
end;
hence Lin A = W by RUSUB_1:25; ::_thesis: verum
end;
theorem :: RUSUB_3:6
for V being strict RealUnitarySpace
for A being Subset of V st A = the carrier of V holds
Lin A = V
proof
let V be strict RealUnitarySpace; ::_thesis: for A being Subset of V st A = the carrier of V holds
Lin A = V
let A be Subset of V; ::_thesis: ( A = the carrier of V implies Lin A = V )
assume A = the carrier of V ; ::_thesis: Lin A = V
then A = the carrier of ((Omega). V) by RUSUB_1:def_3;
hence Lin A = (Omega). V by Th5
.= V by RUSUB_1:def_3 ;
::_thesis: verum
end;
Lm2: for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 is Subspace of W3 implies W1 /\ W2 is Subspace of W3 )
A1: W1 /\ W2 is Subspace of W1 by RUSUB_2:16;
assume W1 is Subspace of W3 ; ::_thesis: W1 /\ W2 is Subspace of W3
hence W1 /\ W2 is Subspace of W3 by A1, RUSUB_1:21; ::_thesis: verum
end;
Lm3: for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 & W1 is Subspace of W3 holds
W1 is Subspace of W2 /\ W3
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 & W1 is Subspace of W3 holds
W1 is Subspace of W2 /\ W3
let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 is Subspace of W2 & W1 is Subspace of W3 implies W1 is Subspace of W2 /\ W3 )
assume A1: ( W1 is Subspace of W2 & W1 is Subspace of W3 ) ; ::_thesis: W1 is Subspace of W2 /\ W3
now__::_thesis:_for_v_being_VECTOR_of_V_st_v_in_W1_holds_
v_in_W2_/\_W3
let v be VECTOR of V; ::_thesis: ( v in W1 implies v in W2 /\ W3 )
assume v in W1 ; ::_thesis: v in W2 /\ W3
then ( v in W2 & v in W3 ) by A1, RUSUB_1:1;
hence v in W2 /\ W3 by RUSUB_2:3; ::_thesis: verum
end;
hence W1 is Subspace of W2 /\ W3 by RUSUB_1:23; ::_thesis: verum
end;
Lm4: for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 is Subspace of W2 implies W1 is Subspace of W2 + W3 )
A1: W2 is Subspace of W2 + W3 by RUSUB_2:7;
assume W1 is Subspace of W2 ; ::_thesis: W1 is Subspace of W2 + W3
hence W1 is Subspace of W2 + W3 by A1, RUSUB_1:21; ::_thesis: verum
end;
Lm5: for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 & W2 is Subspace of W3 holds
W1 + W2 is Subspace of W3
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 & W2 is Subspace of W3 holds
W1 + W2 is Subspace of W3
let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 is Subspace of W3 & W2 is Subspace of W3 implies W1 + W2 is Subspace of W3 )
assume A1: ( W1 is Subspace of W3 & W2 is Subspace of W3 ) ; ::_thesis: W1 + W2 is Subspace of W3
now__::_thesis:_for_v_being_VECTOR_of_V_st_v_in_W1_+_W2_holds_
v_in_W3
let v be VECTOR of V; ::_thesis: ( v in W1 + W2 implies v in W3 )
assume v in W1 + W2 ; ::_thesis: v in W3
then consider v1, v2 being VECTOR of V such that
A2: ( v1 in W1 & v2 in W2 ) and
A3: v = v1 + v2 by RUSUB_2:1;
( v1 in W3 & v2 in W3 ) by A1, A2, RUSUB_1:1;
hence v in W3 by A3, RUSUB_1:14; ::_thesis: verum
end;
hence W1 + W2 is Subspace of W3 by RUSUB_1:23; ::_thesis: verum
end;
theorem Th7: :: RUSUB_3:7
for V being RealUnitarySpace
for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
proof
let V be RealUnitarySpace; ::_thesis: for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
let A, B be Subset of V; ::_thesis: ( A c= B implies Lin A is Subspace of Lin B )
assume A1: A c= B ; ::_thesis: Lin A is Subspace of Lin B
now__::_thesis:_for_v_being_VECTOR_of_V_st_v_in_Lin_A_holds_
v_in_Lin_B
let v be VECTOR of V; ::_thesis: ( v in Lin A implies v in Lin B )
assume v in Lin A ; ::_thesis: v in Lin B
then consider l being Linear_Combination of A such that
A2: v = Sum l by Th1;
reconsider l = l as Linear_Combination of B by A1, RLVECT_2:21;
Sum l = v by A2;
hence v in Lin B by Th1; ::_thesis: verum
end;
hence Lin A is Subspace of Lin B by RUSUB_1:23; ::_thesis: verum
end;
theorem :: RUSUB_3:8
for V being strict RealUnitarySpace
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
proof
let V be strict RealUnitarySpace; ::_thesis: for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
let A, B be Subset of V; ::_thesis: ( Lin A = V & A c= B implies Lin B = V )
assume ( Lin A = V & A c= B ) ; ::_thesis: Lin B = V
then V is Subspace of Lin B by Th7;
hence Lin B = V by RUSUB_1:20; ::_thesis: verum
end;
theorem :: RUSUB_3:9
for V being RealUnitarySpace
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
proof
let V be RealUnitarySpace; ::_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( set ) -> Element of NAT = 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 Th1;
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;
defpred S2[ set ] means $1 in (Carrier l) \ A;
now__::_thesis:_for_x_being_set_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 set ; ::_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 ; ::_thesis: verum
end;
then A2: for x being set 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 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 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
let x be set ; :: 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, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by RLVECT_2:def_6;
now__::_thesis:_for_x_being_set_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 set ; ::_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 ; ::_thesis: verum
end;
then A6: for x being set 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 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(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
proof
let x be set ; :: 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;
Carrier g c= D
proof
let x be set ; :: 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, XBOOLE_1:1;
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
percases ( v in C or not v in C ) ;
supposeA11: v in C ; ::_thesis: (f + g) . v = l . v
A12: now__::_thesis:_not_v_in_D
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;
thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def_10
.= (l . v) + (g . v) by A3, A11
.= (l . v) + 0 by A7, A12
.= l . v ; ::_thesis: verum
end;
supposeA13: not v in C ; ::_thesis: l . v = (f + g) . v
now__::_thesis:_(f_+_g)_._v_=_l_._v
percases ( v in Carrier l or not v in Carrier l ) ;
supposeA14: v in Carrier l ; ::_thesis: (f + g) . v = l . v
A15: now__::_thesis:_v_in_D
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;
thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def_10
.= 0 + (g . v) by A3, A13
.= l . v by A7, A15 ; ::_thesis: verum
end;
supposeA16: 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;
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, RLVECT_3:1;
( Sum f in Lin A & Sum g in Lin B ) by Th1;
hence v in (Lin A) + (Lin B) by A19, RUSUB_2:1; ::_thesis: verum
end;
then A20: Lin (A \/ B) is Subspace of (Lin A) + (Lin B) by RUSUB_1:23;
( Lin A is Subspace of Lin (A \/ B) & Lin B is Subspace of Lin (A \/ B) ) by Th7, XBOOLE_1:7;
then (Lin A) + (Lin B) is Subspace of Lin (A \/ B) by Lm5;
hence Lin (A \/ B) = (Lin A) + (Lin B) by A20, RUSUB_1:20; ::_thesis: verum
end;
theorem :: RUSUB_3:10
for V being RealUnitarySpace
for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
proof
let V be RealUnitarySpace; ::_thesis: for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
let A, B be Subset of V; ::_thesis: Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
( Lin (A /\ B) is Subspace of Lin A & Lin (A /\ B) is Subspace of Lin B ) by Th7, XBOOLE_1:17;
hence Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) by Lm3; ::_thesis: verum
end;
theorem Th11: :: RUSUB_3:11
for V being RealUnitarySpace
for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) )
proof
let V be RealUnitarySpace; ::_thesis: for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) )
let A be Subset of V; ::_thesis: ( A is linearly-independent implies ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) )
defpred S1[ set ] means ex B being Subset of V st
( B = $1 & A c= B & B is linearly-independent );
consider Q being set such that
A1: for Z being set holds
( Z in Q iff ( Z in bool the carrier of V & S1[Z] ) ) from XBOOLE_0:sch_1();
A2: now__::_thesis:_for_Z_being_set_st_Z_<>_{}_&_Z_c=_Q_&_Z_is_c=-linear_holds_
union_Z_in_Q
let Z be set ; ::_thesis: ( Z <> {} & Z c= Q & Z is c=-linear implies union Z in Q )
assume that
A3: Z <> {} and
A4: Z c= Q and
A5: Z is c=-linear ; ::_thesis: union Z in Q
set x = the Element of Z;
the Element of Z in Q by A3, A4, TARSKI:def_3;
then A6: ex B being Subset of V st
( B = the Element of Z & A c= B & B is linearly-independent ) by A1;
set W = union Z;
union Z c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Z or x in the carrier of V )
assume x in union Z ; ::_thesis: x in the carrier of V
then consider X being set such that
A7: x in X and
A8: X in Z by TARSKI:def_4;
X in bool the carrier of V by A1, A4, A8;
hence x in the carrier of V by A7; ::_thesis: verum
end;
then reconsider W = union Z as Subset of V ;
A9: W is linearly-independent
proof
deffunc H1( set ) -> set = { C where C is Subset of V : ( $1 in C & C in Z ) } ;
let l be Linear_Combination of W; :: according to RLVECT_3:def_1 ::_thesis: ( not Sum l = 0. V or Carrier l = {} )
assume that
A10: Sum l = 0. V and
A11: Carrier l <> {} ; ::_thesis: contradiction
consider f being Function such that
A12: dom f = Carrier l and
A13: for x being set st x in Carrier l holds
f . x = H1(x) from FUNCT_1:sch_3();
reconsider M = rng f as non empty set by A11, A12, RELAT_1:42;
set F = the Choice_Function of M;
set S = rng the Choice_Function of M;
A14: now__::_thesis:_not_{}_in_M
assume {} in M ; ::_thesis: contradiction
then consider x being set such that
A15: x in dom f and
A16: f . x = {} by FUNCT_1:def_3;
Carrier l c= W by RLVECT_2:def_6;
then consider X being set such that
A17: x in X and
A18: X in Z by A12, A15, TARSKI:def_4;
reconsider X = X as Subset of V by A1, A4, A18;
X in { C where C is Subset of V : ( x in C & C in Z ) } by A17, A18;
hence contradiction by A12, A13, A15, A16; ::_thesis: verum
end;
then A19: dom the Choice_Function of M = M by RLVECT_3:28;
then dom the Choice_Function of M is finite by A12, FINSET_1:8;
then A20: rng the Choice_Function of M is finite by FINSET_1:8;
A21: now__::_thesis:_for_X_being_set_st_X_in_rng_the_Choice_Function_of_M_holds_
X_in_Z
let X be set ; ::_thesis: ( X in rng the Choice_Function of M implies X in Z )
assume X in rng the Choice_Function of M ; ::_thesis: X in Z
then consider x being set such that
A22: x in dom the Choice_Function of M and
A23: the Choice_Function of M . x = X by FUNCT_1:def_3;
consider y being set such that
A24: ( y in dom f & f . y = x ) by A19, A22, FUNCT_1:def_3;
A25: x = { C where C is Subset of V : ( y in C & C in Z ) } by A12, A13, A24;
X in x by A14, A19, A22, A23, ORDERS_1:def_1;
then ex C being Subset of V st
( C = X & y in C & C in Z ) by A25;
hence X in Z ; ::_thesis: verum
end;
A26: now__::_thesis:_for_X,_Y_being_set_st_X_in_rng_the_Choice_Function_of_M_&_Y_in_rng_the_Choice_Function_of_M_&_not_X_c=_Y_holds_
Y_c=_X
let X, Y be set ; ::_thesis: ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M & not X c= Y implies Y c= X )
assume ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M ) ; ::_thesis: ( X c= Y or Y c= X )
then ( X in Z & Y in Z ) by A21;
then X,Y are_c=-comparable by A5, ORDINAL1:def_8;
hence ( X c= Y or Y c= X ) by XBOOLE_0:def_9; ::_thesis: verum
end;
rng the Choice_Function of M <> {} by A19, RELAT_1:42;
then union (rng the Choice_Function of M) in rng the Choice_Function of M by A26, A20, CARD_2:62;
then union (rng the Choice_Function of M) in Z by A21;
then consider B being Subset of V such that
A27: B = union (rng the Choice_Function of M) and
A c= B and
A28: B is linearly-independent by A1, A4;
Carrier l c= union (rng the Choice_Function of M)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in union (rng the Choice_Function of M) )
set X = f . x;
assume A29: x in Carrier l ; ::_thesis: x in union (rng the Choice_Function of M)
then A30: f . x = { C where C is Subset of V : ( x in C & C in Z ) } by A13;
A31: f . x in M by A12, A29, FUNCT_1:def_3;
then the Choice_Function of M . (f . x) in f . x by A14, ORDERS_1:def_1;
then A32: ex C being Subset of V st
( the Choice_Function of M . (f . x) = C & x in C & C in Z ) by A30;
the Choice_Function of M . (f . x) in rng the Choice_Function of M by A19, A31, FUNCT_1:def_3;
hence x in union (rng the Choice_Function of M) by A32, TARSKI:def_4; ::_thesis: verum
end;
then l is Linear_Combination of B by A27, RLVECT_2:def_6;
hence contradiction by A10, A11, A28, RLVECT_3:def_1; ::_thesis: verum
end;
the Element of Z c= W by A3, ZFMISC_1:74;
then A c= W by A6, XBOOLE_1:1;
hence union Z in Q by A1, A9; ::_thesis: verum
end;
A33: (Omega). V = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) by RUSUB_1:def_3;
assume A is linearly-independent ; ::_thesis: ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) )
then Q <> {} by A1;
then consider X being set such that
A34: X in Q and
A35: for Z being set st Z in Q & Z <> X holds
not X c= Z by A2, ORDERS_1:67;
consider B being Subset of V such that
A36: B = X and
A37: A c= B and
A38: B is linearly-independent by A1, A34;
take B ; ::_thesis: ( A c= B & B is linearly-independent & Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) )
thus ( A c= B & B is linearly-independent ) by A37, A38; ::_thesis: Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #)
assume Lin B <> UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ; ::_thesis: contradiction
then consider v being VECTOR of V such that
A39: ( ( v in Lin B & not v in UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) or ( v in UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) & not v in Lin B ) ) by A33, RUSUB_1:25;
A40: B \/ {v} is linearly-independent
proof
let l be Linear_Combination of B \/ {v}; :: according to RLVECT_3:def_1 ::_thesis: ( not Sum l = 0. V or Carrier l = {} )
assume A41: Sum l = 0. V ; ::_thesis: Carrier l = {}
now__::_thesis:_Carrier_l_=_{}
percases ( v in Carrier l or not v in Carrier l ) ;
suppose v in Carrier l ; ::_thesis: Carrier l = {}
then A42: - (l . v) <> 0 by RLVECT_2:19;
deffunc H1( set ) -> Element of NAT = 0 ;
deffunc H2( VECTOR of V) -> Element of REAL = l . $1;
consider f being Function of the carrier of V,REAL such that
A43: f . v = 0 and
A44: for u being VECTOR of V st u <> v holds
f . u = H2(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_(Carrier_l)_\_{v}_holds_
f_._u_=_0
let u be VECTOR of V; ::_thesis: ( not u in (Carrier l) \ {v} implies f . u = 0 )
assume not u in (Carrier l) \ {v} ; ::_thesis: f . u = 0
then ( not u in Carrier l or u in {v} ) by XBOOLE_0:def_5;
then ( ( l . u = 0 & u <> v ) or u = v ) by TARSKI:def_1;
hence f . u = 0 by A43, A44; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
Carrier f c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in B )
A45: Carrier l c= B \/ {v} by RLVECT_2:def_6;
assume x in Carrier f ; ::_thesis: x in B
then consider u being VECTOR of V such that
A46: u = x and
A47: f . u <> 0 ;
f . u = l . u by A43, A44, A47;
then u in Carrier l by A47;
then ( u in B or u in {v} ) by A45, XBOOLE_0:def_3;
hence x in B by A43, A46, A47, TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of B by RLVECT_2:def_6;
consider g being Function of the carrier of V,REAL such that
A48: g . v = - (l . v) and
A49: for u being VECTOR of V st u <> v holds
g . u = H1(u) from FUNCT_2:sch_6();
reconsider g = g as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{v}_holds_
g_._u_=_0
let u be VECTOR of V; ::_thesis: ( not u in {v} implies g . u = 0 )
assume not u in {v} ; ::_thesis: g . u = 0
then u <> v by TARSKI:def_1;
hence g . u = 0 by A49; ::_thesis: verum
end;
then reconsider g = g as Linear_Combination of V by RLVECT_2:def_3;
Carrier g c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in {v} )
assume x in Carrier g ; ::_thesis: x in {v}
then ex u being VECTOR of V st
( x = u & g . u <> 0 ) ;
then x = v by A49;
hence x in {v} by TARSKI:def_1; ::_thesis: verum
end;
then reconsider g = g as Linear_Combination of {v} by RLVECT_2:def_6;
A50: Sum g = (- (l . v)) * v by A48, RLVECT_2:32;
f - g = l
proof
let u be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (f - g) . u = l . u
now__::_thesis:_(f_-_g)_._u_=_l_._u
percases ( v = u or v <> u ) ;
supposeA51: v = u ; ::_thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by RLVECT_2:54
.= l . u by A43, A48, A51 ; ::_thesis: verum
end;
supposeA52: v <> u ; ::_thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by RLVECT_2:54
.= (l . u) - (g . u) by A44, A52
.= (l . u) - 0 by A49, A52
.= l . u ; ::_thesis: verum
end;
end;
end;
hence (f - g) . u = l . u ; ::_thesis: verum
end;
then 0. V = (Sum f) - (Sum g) by A41, RLVECT_3:4;
then Sum f = (0. V) + (Sum g) by RLSUB_2:61
.= (- (l . v)) * v by A50, RLVECT_1:4 ;
then A53: (- (l . v)) * v in Lin B by Th1;
((- (l . v)) ") * ((- (l . v)) * v) = (((- (l . v)) ") * (- (l . v))) * v by RLVECT_1:def_7
.= 1 * v by A42, XCMPLX_0:def_7
.= v by RLVECT_1:def_8 ;
hence Carrier l = {} by A39, A53, RLVECT_1:1, RUSUB_1:15; ::_thesis: verum
end;
supposeA54: not v in Carrier l ; ::_thesis: Carrier l = {}
Carrier l c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in B )
assume A55: x in Carrier l ; ::_thesis: x in B
Carrier l c= B \/ {v} by RLVECT_2:def_6;
then ( x in B or x in {v} ) by A55, XBOOLE_0:def_3;
hence x in B by A54, A55, TARSKI:def_1; ::_thesis: verum
end;
then l is Linear_Combination of B by RLVECT_2:def_6;
hence Carrier l = {} by A38, A41, RLVECT_3:def_1; ::_thesis: verum
end;
end;
end;
hence Carrier l = {} ; ::_thesis: verum
end;
v in {v} by TARSKI:def_1;
then A56: v in B \/ {v} by XBOOLE_0:def_3;
A57: not v in B by A39, Th2, RLVECT_1:1;
B c= B \/ {v} by XBOOLE_1:7;
then A c= B \/ {v} by A37, XBOOLE_1:1;
then B \/ {v} in Q by A1, A40;
hence contradiction by A35, A36, A56, A57, XBOOLE_1:7; ::_thesis: verum
end;
theorem Th12: :: RUSUB_3:12
for V being RealUnitarySpace
for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V )
proof
let V be RealUnitarySpace; ::_thesis: for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V )
let A be Subset of V; ::_thesis: ( Lin A = V implies ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V ) )
assume A1: Lin A = V ; ::_thesis: ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V )
defpred S1[ set ] means ex B being Subset of V st
( B = $1 & B c= A & B is linearly-independent );
consider Q being set such that
A2: for Z being set holds
( Z in Q iff ( Z in bool the carrier of V & S1[Z] ) ) from XBOOLE_0:sch_1();
A3: now__::_thesis:_for_Z_being_set_st_Z_<>_{}_&_Z_c=_Q_&_Z_is_c=-linear_holds_
union_Z_in_Q
let Z be set ; ::_thesis: ( Z <> {} & Z c= Q & Z is c=-linear implies union Z in Q )
assume that
Z <> {} and
A4: Z c= Q and
A5: Z is c=-linear ; ::_thesis: union Z in Q
set W = union Z;
union Z c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Z or x in the carrier of V )
assume x in union Z ; ::_thesis: x in the carrier of V
then consider X being set such that
A6: x in X and
A7: X in Z by TARSKI:def_4;
X in bool the carrier of V by A2, A4, A7;
hence x in the carrier of V by A6; ::_thesis: verum
end;
then reconsider W = union Z as Subset of V ;
A8: W is linearly-independent
proof
deffunc H1( set ) -> set = { C where C is Subset of V : ( $1 in C & C in Z ) } ;
let l be Linear_Combination of W; :: according to RLVECT_3:def_1 ::_thesis: ( not Sum l = 0. V or Carrier l = {} )
assume that
A9: Sum l = 0. V and
A10: Carrier l <> {} ; ::_thesis: contradiction
consider f being Function such that
A11: dom f = Carrier l and
A12: for x being set st x in Carrier l holds
f . x = H1(x) from FUNCT_1:sch_3();
reconsider M = rng f as non empty set by A10, A11, RELAT_1:42;
set F = the Choice_Function of M;
set S = rng the Choice_Function of M;
A13: now__::_thesis:_not_{}_in_M
assume {} in M ; ::_thesis: contradiction
then consider x being set such that
A14: x in dom f and
A15: f . x = {} by FUNCT_1:def_3;
Carrier l c= W by RLVECT_2:def_6;
then consider X being set such that
A16: x in X and
A17: X in Z by A11, A14, TARSKI:def_4;
reconsider X = X as Subset of V by A2, A4, A17;
X in { C where C is Subset of V : ( x in C & C in Z ) } by A16, A17;
hence contradiction by A11, A12, A14, A15; ::_thesis: verum
end;
then A18: dom the Choice_Function of M = M by RLVECT_3:28;
then dom the Choice_Function of M is finite by A11, FINSET_1:8;
then A19: rng the Choice_Function of M is finite by FINSET_1:8;
A20: now__::_thesis:_for_X_being_set_st_X_in_rng_the_Choice_Function_of_M_holds_
X_in_Z
let X be set ; ::_thesis: ( X in rng the Choice_Function of M implies X in Z )
assume X in rng the Choice_Function of M ; ::_thesis: X in Z
then consider x being set such that
A21: x in dom the Choice_Function of M and
A22: the Choice_Function of M . x = X by FUNCT_1:def_3;
consider y being set such that
A23: ( y in dom f & f . y = x ) by A18, A21, FUNCT_1:def_3;
A24: x = { C where C is Subset of V : ( y in C & C in Z ) } by A11, A12, A23;
X in x by A13, A18, A21, A22, ORDERS_1:def_1;
then ex C being Subset of V st
( C = X & y in C & C in Z ) by A24;
hence X in Z ; ::_thesis: verum
end;
A25: now__::_thesis:_for_X,_Y_being_set_st_X_in_rng_the_Choice_Function_of_M_&_Y_in_rng_the_Choice_Function_of_M_&_not_X_c=_Y_holds_
Y_c=_X
let X, Y be set ; ::_thesis: ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M & not X c= Y implies Y c= X )
assume ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M ) ; ::_thesis: ( X c= Y or Y c= X )
then ( X in Z & Y in Z ) by A20;
then X,Y are_c=-comparable by A5, ORDINAL1:def_8;
hence ( X c= Y or Y c= X ) by XBOOLE_0:def_9; ::_thesis: verum
end;
rng the Choice_Function of M <> {} by A18, RELAT_1:42;
then union (rng the Choice_Function of M) in rng the Choice_Function of M by A25, A19, CARD_2:62;
then union (rng the Choice_Function of M) in Z by A20;
then consider B being Subset of V such that
A26: B = union (rng the Choice_Function of M) and
B c= A and
A27: B is linearly-independent by A2, A4;
Carrier l c= union (rng the Choice_Function of M)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in union (rng the Choice_Function of M) )
set X = f . x;
assume A28: x in Carrier l ; ::_thesis: x in union (rng the Choice_Function of M)
then A29: f . x = { C where C is Subset of V : ( x in C & C in Z ) } by A12;
A30: f . x in M by A11, A28, FUNCT_1:def_3;
then the Choice_Function of M . (f . x) in f . x by A13, ORDERS_1:def_1;
then A31: ex C being Subset of V st
( the Choice_Function of M . (f . x) = C & x in C & C in Z ) by A29;
the Choice_Function of M . (f . x) in rng the Choice_Function of M by A18, A30, FUNCT_1:def_3;
hence x in union (rng the Choice_Function of M) by A31, TARSKI:def_4; ::_thesis: verum
end;
then l is Linear_Combination of B by A26, RLVECT_2:def_6;
hence contradiction by A9, A10, A27, RLVECT_3:def_1; ::_thesis: verum
end;
W c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W or x in A )
assume x in W ; ::_thesis: x in A
then consider X being set such that
A32: x in X and
A33: X in Z by TARSKI:def_4;
ex B being Subset of V st
( B = X & B c= A & B is linearly-independent ) by A2, A4, A33;
hence x in A by A32; ::_thesis: verum
end;
hence union Z in Q by A2, A8; ::_thesis: verum
end;
( {} the carrier of V c= A & {} the carrier of V is linearly-independent ) by RLVECT_3:7, XBOOLE_1:2;
then Q <> {} by A2;
then consider X being set such that
A34: X in Q and
A35: for Z being set st Z in Q & Z <> X holds
not X c= Z by A3, ORDERS_1:67;
consider B being Subset of V such that
A36: B = X and
A37: B c= A and
A38: B is linearly-independent by A2, A34;
take B ; ::_thesis: ( B c= A & B is linearly-independent & Lin B = V )
thus ( B c= A & B is linearly-independent ) by A37, A38; ::_thesis: Lin B = V
assume A39: Lin B <> V ; ::_thesis: contradiction
now__::_thesis:_ex_v_being_VECTOR_of_V_st_
(_v_in_A_&_not_v_in_Lin_B_)
assume A40: for v being VECTOR of V st v in A holds
v in Lin B ; ::_thesis: contradiction
now__::_thesis:_for_v_being_VECTOR_of_V_st_v_in_Lin_A_holds_
v_in_Lin_B
reconsider F = the carrier of (Lin B) as Subset of V by RUSUB_1:def_1;
let v be VECTOR of V; ::_thesis: ( v in Lin A implies v in Lin B )
assume v in Lin A ; ::_thesis: v in Lin B
then consider l being Linear_Combination of A such that
A41: v = Sum l by Th1;
Carrier l c= the carrier of (Lin B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in the carrier of (Lin B) )
assume A42: x in Carrier l ; ::_thesis: x in the carrier of (Lin B)
then reconsider a = x as VECTOR of V ;
Carrier l c= A by RLVECT_2:def_6;
then a in Lin B by A40, A42;
hence x in the carrier of (Lin B) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider l = l as Linear_Combination of F by RLVECT_2:def_6;
Sum l = v by A41;
then v in Lin F by Th1;
hence v in Lin B by Th5; ::_thesis: verum
end;
then Lin A is Subspace of Lin B by RUSUB_1:23;
hence contradiction by A1, A39, RUSUB_1:20; ::_thesis: verum
end;
then consider v being VECTOR of V such that
A43: v in A and
A44: not v in Lin B ;
A45: B \/ {v} is linearly-independent
proof
let l be Linear_Combination of B \/ {v}; :: according to RLVECT_3:def_1 ::_thesis: ( not Sum l = 0. V or Carrier l = {} )
assume A46: Sum l = 0. V ; ::_thesis: Carrier l = {}
now__::_thesis:_Carrier_l_=_{}
percases ( v in Carrier l or not v in Carrier l ) ;
suppose v in Carrier l ; ::_thesis: Carrier l = {}
then A47: - (l . v) <> 0 by RLVECT_2:19;
deffunc H1( set ) -> Element of NAT = 0 ;
deffunc H2( VECTOR of V) -> Element of REAL = l . $1;
consider f being Function of the carrier of V,REAL such that
A48: f . v = 0 and
A49: for u being VECTOR of V st u <> v holds
f . u = H2(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_(Carrier_l)_\_{v}_holds_
f_._u_=_0
let u be VECTOR of V; ::_thesis: ( not u in (Carrier l) \ {v} implies f . u = 0 )
assume not u in (Carrier l) \ {v} ; ::_thesis: f . u = 0
then ( not u in Carrier l or u in {v} ) by XBOOLE_0:def_5;
then ( ( l . u = 0 & u <> v ) or u = v ) by TARSKI:def_1;
hence f . u = 0 by A48, A49; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
Carrier f c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in B )
A50: Carrier l c= B \/ {v} by RLVECT_2:def_6;
assume x in Carrier f ; ::_thesis: x in B
then consider u being VECTOR of V such that
A51: u = x and
A52: f . u <> 0 ;
f . u = l . u by A48, A49, A52;
then u in Carrier l by A52;
then ( u in B or u in {v} ) by A50, XBOOLE_0:def_3;
hence x in B by A48, A51, A52, TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of B by RLVECT_2:def_6;
consider g being Function of the carrier of V,REAL such that
A53: g . v = - (l . v) and
A54: for u being VECTOR of V st u <> v holds
g . u = H1(u) from FUNCT_2:sch_6();
reconsider g = g as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{v}_holds_
g_._u_=_0
let u be VECTOR of V; ::_thesis: ( not u in {v} implies g . u = 0 )
assume not u in {v} ; ::_thesis: g . u = 0
then u <> v by TARSKI:def_1;
hence g . u = 0 by A54; ::_thesis: verum
end;
then reconsider g = g as Linear_Combination of V by RLVECT_2:def_3;
Carrier g c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in {v} )
assume x in Carrier g ; ::_thesis: x in {v}
then ex u being VECTOR of V st
( x = u & g . u <> 0 ) ;
then x = v by A54;
hence x in {v} by TARSKI:def_1; ::_thesis: verum
end;
then reconsider g = g as Linear_Combination of {v} by RLVECT_2:def_6;
A55: Sum g = (- (l . v)) * v by A53, RLVECT_2:32;
f - g = l
proof
let u be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (f - g) . u = l . u
now__::_thesis:_(f_-_g)_._u_=_l_._u
percases ( v = u or v <> u ) ;
supposeA56: v = u ; ::_thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by RLVECT_2:54
.= l . u by A48, A53, A56 ; ::_thesis: verum
end;
supposeA57: v <> u ; ::_thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by RLVECT_2:54
.= (l . u) - (g . u) by A49, A57
.= (l . u) - 0 by A54, A57
.= l . u ; ::_thesis: verum
end;
end;
end;
hence (f - g) . u = l . u ; ::_thesis: verum
end;
then 0. V = (Sum f) - (Sum g) by A46, RLVECT_3:4;
then Sum f = (0. V) + (Sum g) by RLSUB_2:61
.= (- (l . v)) * v by A55, RLVECT_1:4 ;
then A58: (- (l . v)) * v in Lin B by Th1;
((- (l . v)) ") * ((- (l . v)) * v) = (((- (l . v)) ") * (- (l . v))) * v by RLVECT_1:def_7
.= 1 * v by A47, XCMPLX_0:def_7
.= v by RLVECT_1:def_8 ;
hence Carrier l = {} by A44, A58, RUSUB_1:15; ::_thesis: verum
end;
supposeA59: not v in Carrier l ; ::_thesis: Carrier l = {}
Carrier l c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in B )
assume A60: x in Carrier l ; ::_thesis: x in B
Carrier l c= B \/ {v} by RLVECT_2:def_6;
then ( x in B or x in {v} ) by A60, XBOOLE_0:def_3;
hence x in B by A59, A60, TARSKI:def_1; ::_thesis: verum
end;
then l is Linear_Combination of B by RLVECT_2:def_6;
hence Carrier l = {} by A38, A46, RLVECT_3:def_1; ::_thesis: verum
end;
end;
end;
hence Carrier l = {} ; ::_thesis: verum
end;
{v} c= A by A43, ZFMISC_1:31;
then B \/ {v} c= A by A37, XBOOLE_1:8;
then A61: B \/ {v} in Q by A2, A45;
v in {v} by TARSKI:def_1;
then A62: v in B \/ {v} by XBOOLE_0:def_3;
not v in B by A44, Th2;
hence contradiction by A35, A36, A62, A61, XBOOLE_1:7; ::_thesis: verum
end;
begin
definition
let V be RealUnitarySpace;
mode Basis of V -> Subset of V means :Def2: :: RUSUB_3:def 2
( it is linearly-independent & Lin it = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) );
existence
ex b1 being Subset of V st
( b1 is linearly-independent & Lin b1 = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) )
proof
{} the carrier of V is linearly-independent by RLVECT_3:7;
then ex B being Subset of V st
( {} the carrier of V c= B & B is linearly-independent & Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) by Th11;
hence ex b1 being Subset of V st
( b1 is linearly-independent & Lin b1 = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Basis RUSUB_3:def_2_:_
for V being RealUnitarySpace
for b2 being Subset of V holds
( b2 is Basis of V iff ( b2 is linearly-independent & Lin b2 = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) );
theorem :: RUSUB_3:13
for V being strict RealUnitarySpace
for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I
proof
let V be strict RealUnitarySpace; ::_thesis: for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I
let A be Subset of V; ::_thesis: ( A is linearly-independent implies ex I being Basis of V st A c= I )
assume A is linearly-independent ; ::_thesis: ex I being Basis of V st A c= I
then consider B being Subset of V such that
A1: A c= B and
A2: ( B is linearly-independent & Lin B = V ) by Th11;
reconsider B = B as Basis of V by A2, Def2;
take B ; ::_thesis: A c= B
thus A c= B by A1; ::_thesis: verum
end;
theorem :: RUSUB_3:14
for V being RealUnitarySpace
for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A
proof
let V be RealUnitarySpace; ::_thesis: for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A
let A be Subset of V; ::_thesis: ( Lin A = V implies ex I being Basis of V st I c= A )
assume Lin A = V ; ::_thesis: ex I being Basis of V st I c= A
then consider B being Subset of V such that
A1: B c= A and
A2: ( B is linearly-independent & Lin B = V ) by Th12;
reconsider B = B as Basis of V by A2, Def2;
take B ; ::_thesis: B c= A
thus B c= A by A1; ::_thesis: verum
end;
theorem Th15: :: RUSUB_3:15
for V being RealUnitarySpace
for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I
proof
let V be RealUnitarySpace; ::_thesis: for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I
let A be Subset of V; ::_thesis: ( A is linearly-independent implies ex I being Basis of V st A c= I )
assume A is linearly-independent ; ::_thesis: ex I being Basis of V st A c= I
then consider B being Subset of V such that
A1: A c= B and
A2: ( B is linearly-independent & Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) by Th11;
reconsider B = B as Basis of V by A2, Def2;
take B ; ::_thesis: A c= B
thus A c= B by A1; ::_thesis: verum
end;
begin
theorem Th16: :: RUSUB_3:16
for V being RealUnitarySpace
for L being Linear_Combination of V
for A being Subset of V
for F being FinSequence of V st rng F c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
proof
let V be RealUnitarySpace; ::_thesis: for L being Linear_Combination of V
for A being Subset of V
for F being FinSequence of V st rng F c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
let L be Linear_Combination of V; ::_thesis: for A being Subset of V
for F being FinSequence of V st rng F c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
let A be Subset of V; ::_thesis: for F being FinSequence of V st rng F c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
defpred S1[ Element of NAT ] means for F being FinSequence of V st rng F c= the carrier of (Lin A) & len F = $1 holds
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K;
let F be FinSequence of V; ::_thesis: ( rng F c= the carrier of (Lin A) implies ex K being Linear_Combination of A st Sum (L (#) F) = Sum K )
assume A1: rng F c= the carrier of (Lin A) ; ::_thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
A2: len F is Nat ;
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
let F be FinSequence of V; ::_thesis: ( rng F c= the carrier of (Lin A) & len F = n + 1 implies ex K being Linear_Combination of A st Sum (L (#) F) = Sum K )
assume that
A5: rng F c= the carrier of (Lin A) and
A6: len F = n + 1 ; ::_thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
consider G being FinSequence, x being set such that
A7: F = G ^ <*x*> by A6, FINSEQ_2:18;
reconsider G = G, x9 = <*x*> as FinSequence of V by A7, FINSEQ_1:36;
A8: rng (G ^ <*x*>) = (rng G) \/ (rng <*x*>) by FINSEQ_1:31
.= (rng G) \/ {x} by FINSEQ_1:38 ;
then A9: rng G c= rng F by A7, XBOOLE_1:7;
{x} c= rng F by A7, A8, XBOOLE_1:7;
then {x} c= the carrier of (Lin A) by A5, XBOOLE_1:1;
then ( x in {x} implies x in the carrier of (Lin A) ) ;
then A10: x in Lin A by STRUCT_0:def_5, TARSKI:def_1;
then A11: x in V by RUSUB_1:2;
consider LA1 being Linear_Combination of A such that
A12: x = Sum LA1 by A10, Th1;
reconsider x = x as VECTOR of V by A11, STRUCT_0:def_5;
len (G ^ <*x*>) = (len G) + (len <*x*>) by FINSEQ_1:22
.= (len G) + 1 by FINSEQ_1:39 ;
then consider LA2 being Linear_Combination of A such that
A13: Sum (L (#) G) = Sum LA2 by A4, A5, A6, A7, A9, XBOOLE_1:1;
(L . x) * LA1 is Linear_Combination of A by RLVECT_2:44;
then A14: LA2 + ((L . x) * LA1) is Linear_Combination of A by RLVECT_2:38;
Sum (L (#) F) = Sum ((L (#) G) ^ (L (#) x9)) by A7, RLVECT_3:34
.= (Sum LA2) + (Sum (L (#) x9)) by A13, RLVECT_1:41
.= (Sum LA2) + (Sum <*((L . x) * x)*>) by RLVECT_2:26
.= (Sum LA2) + ((L . x) * (Sum LA1)) by A12, RLVECT_1:44
.= (Sum LA2) + (Sum ((L . x) * LA1)) by RLVECT_3:2
.= Sum (LA2 + ((L . x) * LA1)) by RLVECT_3:1 ;
hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by A14; ::_thesis: verum
end;
A15: S1[ 0 ]
proof
let F be FinSequence of V; ::_thesis: ( rng F c= the carrier of (Lin A) & len F = 0 implies ex K being Linear_Combination of A st Sum (L (#) F) = Sum K )
assume that
rng F c= the carrier of (Lin A) and
A16: len F = 0 ; ::_thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
F = <*> the carrier of V by A16;
then L (#) F = <*> the carrier of V by RLVECT_2:25;
then A17: Sum (L (#) F) = 0. V by RLVECT_1:43
.= Sum (ZeroLC V) by RLVECT_2:30 ;
ZeroLC V is Linear_Combination of A by RLVECT_2:22;
hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by A17; ::_thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A15, A3);
hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by A1, A2; ::_thesis: verum
end;
theorem :: RUSUB_3:17
for V being RealUnitarySpace
for L being Linear_Combination of V
for A being Subset of V st Carrier L c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum L = Sum K
proof
let V be RealUnitarySpace; ::_thesis: for L being Linear_Combination of V
for A being Subset of V st Carrier L c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum L = Sum K
let L be Linear_Combination of V; ::_thesis: for A being Subset of V st Carrier L c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum L = Sum K
let A be Subset of V; ::_thesis: ( Carrier L c= the carrier of (Lin A) implies ex K being Linear_Combination of A st Sum L = Sum K )
consider F being FinSequence of V such that
F is one-to-one and
A1: rng F = Carrier L and
A2: Sum L = Sum (L (#) F) by RLVECT_2:def_8;
assume Carrier L c= the carrier of (Lin A) ; ::_thesis: ex K being Linear_Combination of A st Sum L = Sum K
then consider K being Linear_Combination of A such that
A3: Sum (L (#) F) = Sum K by A1, Th16;
take K ; ::_thesis: Sum L = Sum K
thus Sum L = Sum K by A2, A3; ::_thesis: verum
end;
theorem Th18: :: RUSUB_3:18
for V being RealUnitarySpace
for W being Subspace of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )
let W be Subspace of V; ::_thesis: for L being Linear_Combination of V st Carrier L c= the carrier of W holds
for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )
let L be Linear_Combination of V; ::_thesis: ( Carrier L c= the carrier of W implies for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K ) )
assume A1: Carrier L c= the carrier of W ; ::_thesis: for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )
let K be Linear_Combination of W; ::_thesis: ( K = L | the carrier of W implies ( Carrier L = Carrier K & Sum L = Sum K ) )
assume A2: K = L | the carrier of W ; ::_thesis: ( Carrier L = Carrier K & Sum L = Sum K )
A3: dom K = the carrier of W by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_Carrier_K_holds_
x_in_Carrier_L
let x be set ; ::_thesis: ( x in Carrier K implies x in Carrier L )
assume x in Carrier K ; ::_thesis: x in Carrier L
then consider w being VECTOR of W such that
A4: x = w and
A5: K . w <> 0 ;
A6: w is VECTOR of V by RUSUB_1:3;
L . w <> 0 by A2, A3, A5, FUNCT_1:47;
hence x in Carrier L by A4, A6; ::_thesis: verum
end;
then A7: Carrier K c= Carrier L by TARSKI:def_3;
consider G being FinSequence of W such that
A8: ( G is one-to-one & rng G = Carrier K ) and
A9: Sum K = Sum (K (#) G) by RLVECT_2:def_8;
consider F being FinSequence of V such that
A10: F is one-to-one and
A11: rng F = Carrier L and
A12: Sum L = Sum (L (#) F) by RLVECT_2:def_8;
now__::_thesis:_for_x_being_set_st_x_in_Carrier_L_holds_
x_in_Carrier_K
let x be set ; ::_thesis: ( x in Carrier L implies x in Carrier K )
assume A13: x in Carrier L ; ::_thesis: x in Carrier K
then consider v being VECTOR of V such that
A14: x = v and
A15: L . v <> 0 ;
K . v <> 0 by A1, A2, A3, A13, A14, A15, FUNCT_1:47;
hence x in Carrier K by A1, A13, A14; ::_thesis: verum
end;
then A16: Carrier L c= Carrier K by TARSKI:def_3;
then A17: Carrier K = Carrier L by A7, XBOOLE_0:def_10;
then F,G are_fiberwise_equipotent by A10, A11, A8, RFINSEQ:26;
then consider P being Permutation of (dom G) such that
A18: F = G * P by RFINSEQ:4;
len (K (#) G) = len G by RLVECT_2:def_7;
then A19: dom (K (#) G) = dom G by FINSEQ_3:29;
then reconsider q = (K (#) G) * P as FinSequence of W by FINSEQ_2:47;
A20: len q = len (K (#) G) by A19, FINSEQ_2:44;
then len q = len G by RLVECT_2:def_7;
then A21: dom q = dom G by FINSEQ_3:29;
set p = L (#) F;
A22: the carrier of W c= the carrier of V by RUSUB_1:def_1;
rng q c= the carrier of W by FINSEQ_1:def_4;
then rng q c= the carrier of V by A22, XBOOLE_1:1;
then reconsider q9 = q as FinSequence of V by FINSEQ_1:def_4;
consider f being Function of NAT, the carrier of W such that
A23: Sum q = f . (len q) and
A24: f . 0 = 0. W and
A25: for i being Element of NAT
for w being VECTOR of W st i < len q & w = q . (i + 1) holds
f . (i + 1) = (f . i) + w by RLVECT_1:def_12;
( dom f = NAT & rng f c= the carrier of W ) by FUNCT_2:def_1, RELAT_1:def_19;
then reconsider f9 = f as Function of NAT, the carrier of V by A22, FUNCT_2:2, XBOOLE_1:1;
A26: for i being Element of NAT
for v being VECTOR of V st i < len q9 & v = q9 . (i + 1) holds
f9 . (i + 1) = (f9 . i) + v
proof
let i be Element of NAT ; ::_thesis: for v being VECTOR of V st i < len q9 & v = q9 . (i + 1) holds
f9 . (i + 1) = (f9 . i) + v
let v be VECTOR of V; ::_thesis: ( i < len q9 & v = q9 . (i + 1) implies f9 . (i + 1) = (f9 . i) + v )
assume that
A27: i < len q9 and
A28: v = q9 . (i + 1) ; ::_thesis: f9 . (i + 1) = (f9 . i) + v
( 1 <= i + 1 & i + 1 <= len q ) by A27, NAT_1:11, NAT_1:13;
then i + 1 in dom q by FINSEQ_3:25;
then reconsider v9 = v as VECTOR of W by A28, FINSEQ_2:11;
f . (i + 1) = (f . i) + v9 by A25, A27, A28;
hence f9 . (i + 1) = (f9 . i) + v by RUSUB_1:6; ::_thesis: verum
end;
A29: len G = len F by A18, FINSEQ_2:44;
then A30: dom G = dom F by FINSEQ_3:29;
len G = len (L (#) F) by A29, RLVECT_2:def_7;
then A31: dom (L (#) F) = dom G by FINSEQ_3:29;
A32: dom q = dom (K (#) G) by A20, FINSEQ_3:29;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(L_(#)_F)_holds_
(L_(#)_F)_._i_=_q_._i
let i be Nat; ::_thesis: ( i in dom (L (#) F) implies (L (#) F) . i = q . i )
set v = F /. i;
set j = P . i;
A33: i in NAT by ORDINAL1:def_12;
assume A34: i in dom (L (#) F) ; ::_thesis: (L (#) F) . i = q . i
then A35: F /. i = F . i by A31, A30, PARTFUN1:def_6;
then F /. i in rng F by A31, A30, A34, FUNCT_1:def_3;
then reconsider w = F /. i as VECTOR of W by A17, A11;
( dom P = dom G & rng P = dom G ) by FUNCT_2:52, FUNCT_2:def_3;
then A36: P . i in dom G by A31, A34, FUNCT_1:def_3;
then P . i in Seg (card G) by FINSEQ_1:def_3;
then reconsider j = P . i as Element of NAT ;
A37: G /. j = G . (P . i) by A36, PARTFUN1:def_6
.= F /. i by A18, A31, A30, A34, A35, FUNCT_1:12 ;
q . i = (K (#) G) . j by A31, A21, A34, FUNCT_1:12
.= (K . w) * w by A32, A21, A36, A37, RLVECT_2:def_7
.= (L . (F /. i)) * w by A2, A3, FUNCT_1:47
.= (L . (F /. i)) * (F /. i) by RUSUB_1:7 ;
hence (L (#) F) . i = q . i by A34, A33, RLVECT_2:def_7; ::_thesis: verum
end;
then A38: L (#) F = (K (#) G) * P by A31, A21, FINSEQ_1:13;
len G = len (K (#) G) by RLVECT_2:def_7;
then dom G = dom (K (#) G) by FINSEQ_3:29;
then reconsider P = P as Permutation of (dom (K (#) G)) ;
q = (K (#) G) * P ;
then A39: Sum (K (#) G) = Sum q by RLVECT_2:7;
A40: f9 . (len q9) is Element of V ;
f9 . 0 = 0. V by A24, RUSUB_1:4;
hence ( Carrier L = Carrier K & Sum L = Sum K ) by A7, A16, A12, A9, A38, A39, A23, A26, A40, RLVECT_1:def_12, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th19: :: RUSUB_3:19
for V being RealUnitarySpace
for W being Subspace of V
for K being Linear_Combination of W ex L being Linear_Combination of V st
( Carrier K = Carrier L & Sum K = Sum L )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for K being Linear_Combination of W ex L being Linear_Combination of V st
( Carrier K = Carrier L & Sum K = Sum L )
let W be Subspace of V; ::_thesis: for K being Linear_Combination of W ex L being Linear_Combination of V st
( Carrier K = Carrier L & Sum K = Sum L )
let K be Linear_Combination of W; ::_thesis: ex L being Linear_Combination of V st
( Carrier K = Carrier L & Sum K = Sum L )
defpred S1[ set , set ] means ( ( $1 in W & $2 = K . $1 ) or ( not $1 in W & $2 = 0 ) );
reconsider K9 = K as Function of the carrier of W,REAL ;
A1: the carrier of W c= the carrier of V by RUSUB_1:def_1;
then reconsider C = Carrier K as finite Subset of V by XBOOLE_1:1;
A2: for x being set st x in the carrier of V holds
ex y being set st
( y in REAL & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier of V implies ex y being set st
( y in REAL & S1[x,y] ) )
assume x in the carrier of V ; ::_thesis: ex y being set st
( y in REAL & S1[x,y] )
then reconsider x = x as VECTOR of V ;
percases ( x in W or not x in W ) ;
supposeA3: x in W ; ::_thesis: ex y being set st
( y in REAL & S1[x,y] )
then reconsider x = x as VECTOR of W by STRUCT_0:def_5;
S1[x,K . x] by A3;
hence ex y being set st
( y in REAL & S1[x,y] ) ; ::_thesis: verum
end;
suppose not x in W ; ::_thesis: ex y being set st
( y in REAL & S1[x,y] )
hence ex y being set st
( y in REAL & S1[x,y] ) ; ::_thesis: verum
end;
end;
end;
ex L being Function of the carrier of V,REAL st
for x being set st x in the carrier of V holds
S1[x,L . x] from FUNCT_2:sch_1(A2);
then consider L being Function of the carrier of V,REAL such that
A4: for x being set st x in the carrier of V holds
S1[x,L . x] ;
A5: now__::_thesis:_for_v_being_VECTOR_of_V_st_not_v_in_C_holds_
L_._v_=_0
let v be VECTOR of V; ::_thesis: ( not v in C implies L . v = 0 )
assume not v in C ; ::_thesis: L . v = 0
then ( ( S1[v,K . v] & not v in C & v in the carrier of W ) or S1[v, 0 ] ) by STRUCT_0:def_5;
then ( ( S1[v,K . v] & K . v = 0 ) or S1[v, 0 ] ) ;
hence L . v = 0 by A4; ::_thesis: verum
end;
L is Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
then reconsider L = L as Linear_Combination of V by A5, RLVECT_2:def_3;
reconsider L9 = L | the carrier of W as Function of the carrier of W,REAL by A1, FUNCT_2:32;
take L ; ::_thesis: ( Carrier K = Carrier L & Sum K = Sum L )
now__::_thesis:_for_x_being_set_st_x_in_Carrier_L_holds_
x_in_the_carrier_of_W
let x be set ; ::_thesis: ( x in Carrier L implies x in the carrier of W )
assume ( x in Carrier L & not x in the carrier of W ) ; ::_thesis: contradiction
then ( ex v being VECTOR of V st
( x = v & L . v <> 0 ) & not x in W ) by STRUCT_0:def_5;
hence contradiction by A4; ::_thesis: verum
end;
then A6: Carrier L c= the carrier of W by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_W_holds_
K9_._x_=_L9_._x
let x be set ; ::_thesis: ( x in the carrier of W implies K9 . x = L9 . x )
assume A7: x in the carrier of W ; ::_thesis: K9 . x = L9 . x
then S1[x,L . x] by A4, A1;
hence K9 . x = L9 . x by A7, FUNCT_1:49, STRUCT_0:def_5; ::_thesis: verum
end;
then K9 = L9 by FUNCT_2:12;
hence ( Carrier K = Carrier L & Sum K = Sum L ) by A6, Th18; ::_thesis: verum
end;
theorem Th20: :: RUSUB_3:20
for V being RealUnitarySpace
for W being Subspace of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L )
let W be Subspace of V; ::_thesis: for L being Linear_Combination of V st Carrier L c= the carrier of W holds
ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L )
let L be Linear_Combination of V; ::_thesis: ( Carrier L c= the carrier of W implies ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L ) )
assume A1: Carrier L c= the carrier of W ; ::_thesis: ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L )
then reconsider C = Carrier L as finite Subset of W ;
the carrier of W c= the carrier of V by RUSUB_1:def_1;
then reconsider K = L | the carrier of W as Function of the carrier of W,REAL by FUNCT_2:32;
A2: K is Element of Funcs ( the carrier of W,REAL) by FUNCT_2:8;
A3: dom K = the carrier of W by FUNCT_2:def_1;
now__::_thesis:_for_w_being_VECTOR_of_W_st_not_w_in_C_holds_
K_._w_=_0
let w be VECTOR of W; ::_thesis: ( not w in C implies K . w = 0 )
A4: w is VECTOR of V by RUSUB_1:3;
assume not w in C ; ::_thesis: K . w = 0
then L . w = 0 by A4;
hence K . w = 0 by A3, FUNCT_1:47; ::_thesis: verum
end;
then reconsider K = K as Linear_Combination of W by A2, RLVECT_2:def_3;
take K ; ::_thesis: ( Carrier K = Carrier L & Sum K = Sum L )
thus ( Carrier K = Carrier L & Sum K = Sum L ) by A1, Th18; ::_thesis: verum
end;
theorem Th21: :: RUSUB_3:21
for V being RealUnitarySpace
for I being Basis of V
for v being VECTOR of V holds v in Lin I
proof
let V be RealUnitarySpace; ::_thesis: for I being Basis of V
for v being VECTOR of V holds v in Lin I
let I be Basis of V; ::_thesis: for v being VECTOR of V holds v in Lin I
let v be VECTOR of V; ::_thesis: v in Lin I
v in UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) by STRUCT_0:def_5;
hence v in Lin I by Def2; ::_thesis: verum
end;
theorem Th22: :: RUSUB_3:22
for V being RealUnitarySpace
for W being Subspace of V
for A being Subset of W st A is linearly-independent holds
A is linearly-independent Subset of V
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for A being Subset of W st A is linearly-independent holds
A is linearly-independent Subset of V
let W be Subspace of V; ::_thesis: for A being Subset of W st A is linearly-independent holds
A is linearly-independent Subset of V
let A be Subset of W; ::_thesis: ( A is linearly-independent implies A is linearly-independent Subset of V )
the carrier of W c= the carrier of V by RUSUB_1:def_1;
then reconsider A9 = A as Subset of V by XBOOLE_1:1;
assume A1: A is linearly-independent ; ::_thesis: A is linearly-independent Subset of V
now__::_thesis:_not_A9_is_linearly-dependent
assume A9 is linearly-dependent ; ::_thesis: contradiction
then consider L being Linear_Combination of A9 such that
A2: Sum L = 0. V and
A3: Carrier L <> {} by RLVECT_3:def_1;
Carrier L c= A by RLVECT_2:def_6;
then consider LW being Linear_Combination of W such that
A4: Carrier LW = Carrier L and
A5: Sum LW = Sum L by Th20, XBOOLE_1:1;
reconsider LW = LW as Linear_Combination of A by A4, RLVECT_2:def_6;
Sum LW = 0. W by A2, A5, RUSUB_1:4;
hence contradiction by A1, A3, A4, RLVECT_3:def_1; ::_thesis: verum
end;
hence A is linearly-independent Subset of V ; ::_thesis: verum
end;
theorem :: RUSUB_3:23
for V being RealUnitarySpace
for W being Subspace of V
for A being Subset of V st A is linearly-independent & A c= the carrier of W holds
A is linearly-independent Subset of W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for A being Subset of V st A is linearly-independent & A c= the carrier of W holds
A is linearly-independent Subset of W
let W be Subspace of V; ::_thesis: for A being Subset of V st A is linearly-independent & A c= the carrier of W holds
A is linearly-independent Subset of W
let A be Subset of V; ::_thesis: ( A is linearly-independent & A c= the carrier of W implies A is linearly-independent Subset of W )
assume that
A1: A is linearly-independent and
A2: A c= the carrier of W ; ::_thesis: A is linearly-independent Subset of W
reconsider A9 = A as Subset of W by A2;
now__::_thesis:_not_A9_is_linearly-dependent
assume A9 is linearly-dependent ; ::_thesis: contradiction
then consider K being Linear_Combination of A9 such that
A3: Sum K = 0. W and
A4: Carrier K <> {} by RLVECT_3:def_1;
consider L being Linear_Combination of V such that
A5: Carrier L = Carrier K and
A6: Sum L = Sum K by Th19;
reconsider L = L as Linear_Combination of A by A5, RLVECT_2:def_6;
Sum L = 0. V by A3, A6, RUSUB_1:4;
hence contradiction by A1, A4, A5, RLVECT_3:def_1; ::_thesis: verum
end;
hence A is linearly-independent Subset of W ; ::_thesis: verum
end;
theorem :: RUSUB_3:24
for V being RealUnitarySpace
for W being Subspace of V
for A being Basis of W ex B being Basis of V st A c= B
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for A being Basis of W ex B being Basis of V st A c= B
let W be Subspace of V; ::_thesis: for A being Basis of W ex B being Basis of V st A c= B
let A be Basis of W; ::_thesis: ex B being Basis of V st A c= B
A is linearly-independent by Def2;
then reconsider B = A as linearly-independent Subset of V by Th22;
consider I being Basis of V such that
A1: B c= I by Th15;
take I ; ::_thesis: A c= I
thus A c= I by A1; ::_thesis: verum
end;
theorem Th25: :: RUSUB_3:25
for V being RealUnitarySpace
for A being Subset of V st A is linearly-independent holds
for v being VECTOR of V st v in A holds
for B being Subset of V st B = A \ {v} holds
not v in Lin B
proof
let V be RealUnitarySpace; ::_thesis: for A being Subset of V st A is linearly-independent holds
for v being VECTOR of V st v in A holds
for B being Subset of V st B = A \ {v} holds
not v in Lin B
let A be Subset of V; ::_thesis: ( A is linearly-independent implies for v being VECTOR of V st v in A holds
for B being Subset of V st B = A \ {v} holds
not v in Lin B )
assume A1: A is linearly-independent ; ::_thesis: for v being VECTOR of V st v in A holds
for B being Subset of V st B = A \ {v} holds
not v in Lin B
let v be VECTOR of V; ::_thesis: ( v in A implies for B being Subset of V st B = A \ {v} holds
not v in Lin B )
assume v in A ; ::_thesis: for B being Subset of V st B = A \ {v} holds
not v in Lin B
then A2: {v} is Subset of A by SUBSET_1:41;
let B be Subset of V; ::_thesis: ( B = A \ {v} implies not v in Lin B )
assume A3: B = A \ {v} ; ::_thesis: not v in Lin B
B c= A by A3, XBOOLE_1:36;
then A4: B \/ {v} c= A \/ A by A2, XBOOLE_1:13;
assume v in Lin B ; ::_thesis: contradiction
then consider L being Linear_Combination of B such that
A5: v = Sum L by Th1;
{v} is linearly-independent by A1, A2, RLVECT_3:5;
then v <> 0. V by RLVECT_3:8;
then not Carrier L is empty by A5, RLVECT_2:34;
then A6: ex w being set st w in Carrier L by XBOOLE_0:def_1;
v in {v} by TARSKI:def_1;
then v in Lin {v} by Th2;
then consider K being Linear_Combination of {v} such that
A7: v = Sum K by Th1;
A8: ( Carrier L c= B & Carrier K c= {v} ) by RLVECT_2:def_6;
then (Carrier L) \/ (Carrier K) c= B \/ {v} by XBOOLE_1:13;
then ( Carrier (L - K) c= (Carrier L) \/ (Carrier K) & (Carrier L) \/ (Carrier K) c= A ) by A4, RLVECT_2:55, XBOOLE_1:1;
then Carrier (L - K) c= A by XBOOLE_1:1;
then A9: L - K is Linear_Combination of A by RLVECT_2:def_6;
A10: for x being VECTOR of V st x in Carrier L holds
K . x = 0
proof
let x be VECTOR of V; ::_thesis: ( x in Carrier L implies K . x = 0 )
assume x in Carrier L ; ::_thesis: K . x = 0
then not x in Carrier K by A3, A8, XBOOLE_0:def_5;
hence K . x = 0 ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_Carrier_L_holds_
x_in_Carrier_(L_-_K)
let x be set ; ::_thesis: ( x in Carrier L implies x in Carrier (L - K) )
assume that
A11: x in Carrier L and
A12: not x in Carrier (L - K) ; ::_thesis: contradiction
reconsider x = x as VECTOR of V by A11;
A13: L . x <> 0 by A11, RLVECT_2:19;
(L - K) . x = (L . x) - (K . x) by RLVECT_2:54
.= (L . x) - 0 by A10, A11
.= L . x ;
hence contradiction by A12, A13; ::_thesis: verum
end;
then A14: Carrier L c= Carrier (L - K) by TARSKI:def_3;
0. V = (Sum L) + (- (Sum K)) by A5, A7, RLVECT_1:5
.= (Sum L) + (Sum (- K)) by RLVECT_3:3
.= Sum (L - K) by RLVECT_3:1 ;
hence contradiction by A1, A6, A9, A14, RLVECT_3:def_1; ::_thesis: verum
end;
Lm6: for X, x being set st not x in X holds
X \ {x} = X
proof
let X, x be set ; ::_thesis: ( not x in X implies X \ {x} = X )
assume A1: not x in X ; ::_thesis: X \ {x} = X
now__::_thesis:_not_X_meets_{x}
assume X meets {x} ; ::_thesis: contradiction
then consider y being set such that
A2: y in X /\ {x} by XBOOLE_0:4;
( y in X & y in {x} ) by A2, XBOOLE_0:def_4;
hence contradiction by A1, TARSKI:def_1; ::_thesis: verum
end;
hence X \ {x} = X by XBOOLE_1:83; ::_thesis: verum
end;
theorem :: RUSUB_3:26
for V being RealUnitarySpace
for I being Basis of V
for A being non empty Subset of V st A misses I holds
for B being Subset of V st B = I \/ A holds
B is linearly-dependent
proof
let V be RealUnitarySpace; ::_thesis: for I being Basis of V
for A being non empty Subset of V st A misses I holds
for B being Subset of V st B = I \/ A holds
B is linearly-dependent
let I be Basis of V; ::_thesis: for A being non empty Subset of V st A misses I holds
for B being Subset of V st B = I \/ A holds
B is linearly-dependent
let A be non empty Subset of V; ::_thesis: ( A misses I implies for B being Subset of V st B = I \/ A holds
B is linearly-dependent )
assume A1: A misses I ; ::_thesis: for B being Subset of V st B = I \/ A holds
B is linearly-dependent
consider v being set such that
A2: v in A by XBOOLE_0:def_1;
let B be Subset of V; ::_thesis: ( B = I \/ A implies B is linearly-dependent )
assume A3: B = I \/ A ; ::_thesis: B is linearly-dependent
A4: A c= B by A3, XBOOLE_1:7;
reconsider v = v as VECTOR of V by A2;
reconsider Bv = B \ {v} as Subset of V ;
A5: I \ {v} c= B \ {v} by A3, XBOOLE_1:7, XBOOLE_1:33;
not v in I by A1, A2, XBOOLE_0:3;
then I c= Bv by A5, Lm6;
then A6: Lin I is Subspace of Lin Bv by Th7;
assume A7: B is linearly-independent ; ::_thesis: contradiction
v in Lin I by Th21;
hence contradiction by A7, A2, A4, A6, Th25, RUSUB_1:1; ::_thesis: verum
end;
theorem :: RUSUB_3:27
for V being RealUnitarySpace
for W being Subspace of V
for A being Subset of V st A c= the carrier of W holds
Lin A is Subspace of W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for A being Subset of V st A c= the carrier of W holds
Lin A is Subspace of W
let W be Subspace of V; ::_thesis: for A being Subset of V st A c= the carrier of W holds
Lin A is Subspace of W
let A be Subset of V; ::_thesis: ( A c= the carrier of W implies Lin A is Subspace of W )
assume A1: A c= the carrier of W ; ::_thesis: Lin A is Subspace of W
now__::_thesis:_for_w_being_set_st_w_in_the_carrier_of_(Lin_A)_holds_
w_in_the_carrier_of_W
let w be set ; ::_thesis: ( w in the carrier of (Lin A) implies w in the carrier of W )
assume w in the carrier of (Lin A) ; ::_thesis: w in the carrier of W
then w in Lin A by STRUCT_0:def_5;
then consider L being Linear_Combination of A such that
A2: w = Sum L by Th1;
Carrier L c= A by RLVECT_2:def_6;
then ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum L = Sum K ) by A1, Th20, XBOOLE_1:1;
hence w in the carrier of W by A2; ::_thesis: verum
end;
then the carrier of (Lin A) c= the carrier of W by TARSKI:def_3;
hence Lin A is Subspace of W by RUSUB_1:22; ::_thesis: verum
end;
theorem :: RUSUB_3:28
for V being RealUnitarySpace
for W being Subspace of V
for A being Subset of V
for B being Subset of W st A = B holds
Lin A = Lin B
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for A being Subset of V
for B being Subset of W st A = B holds
Lin A = Lin B
let W be Subspace of V; ::_thesis: for A being Subset of V
for B being Subset of W st A = B holds
Lin A = Lin B
let A be Subset of V; ::_thesis: for B being Subset of W st A = B holds
Lin A = Lin B
let B be Subset of W; ::_thesis: ( A = B implies Lin A = Lin B )
reconsider B9 = Lin B, V9 = V as RealUnitarySpace ;
A1: B9 is Subspace of V9 by RUSUB_1:21;
assume A2: A = B ; ::_thesis: Lin A = Lin B
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(Lin_A)_holds_
x_in_the_carrier_of_(Lin_B)
let x be set ; ::_thesis: ( x in the carrier of (Lin A) implies x in the carrier of (Lin B) )
assume x in the carrier of (Lin A) ; ::_thesis: x in the carrier of (Lin B)
then x in Lin A by STRUCT_0:def_5;
then consider L being Linear_Combination of A such that
A3: x = Sum L by Th1;
Carrier L c= A by RLVECT_2:def_6;
then consider K being Linear_Combination of W such that
A4: Carrier K = Carrier L and
A5: Sum K = Sum L by A2, Th20, XBOOLE_1:1;
reconsider K = K as Linear_Combination of B by A2, A4, RLVECT_2:def_6;
x = Sum K by A3, A5;
then x in Lin B by Th1;
hence x in the carrier of (Lin B) by STRUCT_0:def_5; ::_thesis: verum
end;
then A6: the carrier of (Lin A) c= the carrier of (Lin B) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(Lin_B)_holds_
x_in_the_carrier_of_(Lin_A)
let x be set ; ::_thesis: ( x in the carrier of (Lin B) implies x in the carrier of (Lin A) )
assume x in the carrier of (Lin B) ; ::_thesis: x in the carrier of (Lin A)
then x in Lin B by STRUCT_0:def_5;
then consider K being Linear_Combination of B such that
A7: x = Sum K by Th1;
consider L being Linear_Combination of V such that
A8: Carrier L = Carrier K and
A9: Sum L = Sum K by Th19;
reconsider L = L as Linear_Combination of A by A2, A8, RLVECT_2:def_6;
x = Sum L by A7, A9;
then x in Lin A by Th1;
hence x in the carrier of (Lin A) by STRUCT_0:def_5; ::_thesis: verum
end;
then the carrier of (Lin B) c= the carrier of (Lin A) by TARSKI:def_3;
then the carrier of (Lin A) = the carrier of (Lin B) by A6, XBOOLE_0:def_10;
hence Lin A = Lin B by A1, RUSUB_1:24; ::_thesis: verum
end;
begin
theorem Th29: :: RUSUB_3:29
for V being RealUnitarySpace
for v being VECTOR of V
for x being set holds
( x in Lin {v} iff ex a being Real st x = a * v )
proof
deffunc H1( set ) -> Element of NAT = 0 ;
let V be RealUnitarySpace; ::_thesis: for v being VECTOR of V
for x being set holds
( x in Lin {v} iff ex a being Real st x = a * v )
let v be VECTOR of V; ::_thesis: for x being set holds
( x in Lin {v} iff ex a being Real st x = a * v )
let x be set ; ::_thesis: ( x in Lin {v} iff ex a being Real st x = a * v )
thus ( x in Lin {v} implies ex a being Real st x = a * v ) ::_thesis: ( ex a being Real st x = a * v implies x in Lin {v} )
proof
assume x in Lin {v} ; ::_thesis: ex a being Real st x = a * v
then consider l being Linear_Combination of {v} such that
A1: x = Sum l by Th1;
Sum l = (l . v) * v by RLVECT_2:32;
hence ex a being Real st x = a * v by A1; ::_thesis: verum
end;
given a being Real such that A2: x = a * v ; ::_thesis: x in Lin {v}
consider f being Function of the carrier of V,REAL such that
A3: f . v = a and
A4: for z being VECTOR of V st z <> v holds
f . z = H1(z) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_z_being_VECTOR_of_V_st_not_z_in_{v}_holds_
f_._z_=_0
let z be VECTOR of V; ::_thesis: ( not z in {v} implies f . z = 0 )
assume not z in {v} ; ::_thesis: f . z = 0
then z <> v by TARSKI:def_1;
hence f . z = 0 by A4; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
Carrier f c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} )
assume A5: x in Carrier f ; ::_thesis: x in {v}
then f . x <> 0 by RLVECT_2:19;
then x = v by A4, A5;
hence x in {v} by TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {v} by RLVECT_2:def_6;
Sum f = x by A2, A3, RLVECT_2:32;
hence x in Lin {v} by Th1; ::_thesis: verum
end;
theorem :: RUSUB_3:30
for V being RealUnitarySpace
for v being VECTOR of V holds v in Lin {v}
proof
let V be RealUnitarySpace; ::_thesis: for v being VECTOR of V holds v in Lin {v}
let v be VECTOR of V; ::_thesis: v in Lin {v}
v in {v} by TARSKI:def_1;
hence v in Lin {v} by Th2; ::_thesis: verum
end;
theorem :: RUSUB_3:31
for V being RealUnitarySpace
for v, w being VECTOR of V
for x being set holds
( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) )
proof
let V be RealUnitarySpace; ::_thesis: for v, w being VECTOR of V
for x being set holds
( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) )
let v, w be VECTOR of V; ::_thesis: for x being set holds
( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) )
let x be set ; ::_thesis: ( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) )
thus ( x in v + (Lin {w}) implies ex a being Real st x = v + (a * w) ) ::_thesis: ( ex a being Real st x = v + (a * w) implies x in v + (Lin {w}) )
proof
assume x in v + (Lin {w}) ; ::_thesis: ex a being Real st x = v + (a * w)
then consider u being VECTOR of V such that
A1: u in Lin {w} and
A2: x = v + u by RUSUB_2:63;
ex a being Real st u = a * w by A1, Th29;
hence ex a being Real st x = v + (a * w) by A2; ::_thesis: verum
end;
given a being Real such that A3: x = v + (a * w) ; ::_thesis: x in v + (Lin {w})
a * w in Lin {w} by Th29;
hence x in v + (Lin {w}) by A3, RUSUB_2:63; ::_thesis: verum
end;
theorem Th32: :: RUSUB_3:32
for V being RealUnitarySpace
for w1, w2 being VECTOR of V
for x being set holds
( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )
proof
let V be RealUnitarySpace; ::_thesis: for w1, w2 being VECTOR of V
for x being set holds
( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )
let w1, w2 be VECTOR of V; ::_thesis: for x being set holds
( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )
let x be set ; ::_thesis: ( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )
thus ( x in Lin {w1,w2} implies ex a, b being Real st x = (a * w1) + (b * w2) ) ::_thesis: ( ex a, b being Real st x = (a * w1) + (b * w2) implies x in Lin {w1,w2} )
proof
assume A1: x in Lin {w1,w2} ; ::_thesis: ex a, b being Real st x = (a * w1) + (b * w2)
now__::_thesis:_ex_a,_b_being_Real_st_x_=_(a_*_w1)_+_(b_*_w2)
percases ( w1 = w2 or w1 <> w2 ) ;
suppose w1 = w2 ; ::_thesis: ex a, b being Real st x = (a * w1) + (b * w2)
then {w1,w2} = {w1} by ENUMSET1:29;
then consider a being Real such that
A2: x = a * w1 by A1, Th29;
x = (a * w1) + (0. V) by A2, RLVECT_1:4
.= (a * w1) + (0 * w2) by RLVECT_1:10 ;
hence ex a, b being Real st x = (a * w1) + (b * w2) ; ::_thesis: verum
end;
supposeA3: w1 <> w2 ; ::_thesis: ex a, b being Real st x = (a * w1) + (b * w2)
consider l being Linear_Combination of {w1,w2} such that
A4: x = Sum l by A1, Th1;
x = ((l . w1) * w1) + ((l . w2) * w2) by A3, A4, RLVECT_2:33;
hence ex a, b being Real st x = (a * w1) + (b * w2) ; ::_thesis: verum
end;
end;
end;
hence ex a, b being Real st x = (a * w1) + (b * w2) ; ::_thesis: verum
end;
given a, b being Real such that A5: x = (a * w1) + (b * w2) ; ::_thesis: x in Lin {w1,w2}
now__::_thesis:_x_in_Lin_{w1,w2}
percases ( w1 = w2 or w1 <> w2 ) ;
supposeA6: w1 = w2 ; ::_thesis: x in Lin {w1,w2}
then x = (a + b) * w1 by A5, RLVECT_1:def_6;
then x in Lin {w1} by Th29;
hence x in Lin {w1,w2} by A6, ENUMSET1:29; ::_thesis: verum
end;
supposeA7: w1 <> w2 ; ::_thesis: x in Lin {w1,w2}
deffunc H1( set ) -> Element of NAT = 0 ;
consider f being Function of the carrier of V,REAL such that
A8: ( f . w1 = a & f . w2 = b ) and
A9: for u being VECTOR of V st u <> w1 & u <> w2 holds
f . u = H1(u) from FUNCT_2:sch_7(A7);
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{w1,w2}_holds_
f_._u_=_0
let u be VECTOR of V; ::_thesis: ( not u in {w1,w2} implies f . u = 0 )
assume not u in {w1,w2} ; ::_thesis: f . u = 0
then ( u <> w1 & u <> w2 ) by TARSKI:def_2;
hence f . u = 0 by A9; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
Carrier f c= {w1,w2}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {w1,w2} )
assume that
A10: x in Carrier f and
A11: not x in {w1,w2} ; ::_thesis: contradiction
( x <> w1 & x <> w2 ) by A11, TARSKI:def_2;
then f . x = 0 by A9, A10;
hence contradiction by A10, RLVECT_2:19; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {w1,w2} by RLVECT_2:def_6;
x = Sum f by A5, A7, A8, RLVECT_2:33;
hence x in Lin {w1,w2} by Th1; ::_thesis: verum
end;
end;
end;
hence x in Lin {w1,w2} ; ::_thesis: verum
end;
theorem :: RUSUB_3:33
for V being RealUnitarySpace
for w1, w2 being VECTOR of V holds
( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} )
proof
let V be RealUnitarySpace; ::_thesis: for w1, w2 being VECTOR of V holds
( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} )
let w1, w2 be VECTOR of V; ::_thesis: ( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} )
( w1 in {w1,w2} & w2 in {w1,w2} ) by TARSKI:def_2;
hence ( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} ) by Th2; ::_thesis: verum
end;
theorem :: RUSUB_3:34
for V being RealUnitarySpace
for v, w1, w2 being VECTOR of V
for x being set holds
( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )
proof
let V be RealUnitarySpace; ::_thesis: for v, w1, w2 being VECTOR of V
for x being set holds
( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )
let v, w1, w2 be VECTOR of V; ::_thesis: for x being set holds
( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )
let x be set ; ::_thesis: ( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )
thus ( x in v + (Lin {w1,w2}) implies ex a, b being Real st x = (v + (a * w1)) + (b * w2) ) ::_thesis: ( ex a, b being Real st x = (v + (a * w1)) + (b * w2) implies x in v + (Lin {w1,w2}) )
proof
assume x in v + (Lin {w1,w2}) ; ::_thesis: ex a, b being Real st x = (v + (a * w1)) + (b * w2)
then consider u being VECTOR of V such that
A1: u in Lin {w1,w2} and
A2: x = v + u by RUSUB_2:63;
consider a, b being Real such that
A3: u = (a * w1) + (b * w2) by A1, Th32;
take a ; ::_thesis: ex b being Real st x = (v + (a * w1)) + (b * w2)
take b ; ::_thesis: x = (v + (a * w1)) + (b * w2)
thus x = (v + (a * w1)) + (b * w2) by A2, A3, RLVECT_1:def_3; ::_thesis: verum
end;
given a, b being Real such that A4: x = (v + (a * w1)) + (b * w2) ; ::_thesis: x in v + (Lin {w1,w2})
(a * w1) + (b * w2) in Lin {w1,w2} by Th32;
then v + ((a * w1) + (b * w2)) in v + (Lin {w1,w2}) by RUSUB_2:63;
hence x in v + (Lin {w1,w2}) by A4, RLVECT_1:def_3; ::_thesis: verum
end;
theorem Th35: :: RUSUB_3:35
for V being RealUnitarySpace
for v1, v2, v3 being VECTOR of V
for x being set holds
( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) )
proof
let V be RealUnitarySpace; ::_thesis: for v1, v2, v3 being VECTOR of V
for x being set holds
( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) )
let v1, v2, v3 be VECTOR of V; ::_thesis: for x being set holds
( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) )
let x be set ; ::_thesis: ( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) )
thus ( x in Lin {v1,v2,v3} implies ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ) ::_thesis: ( ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) implies x in Lin {v1,v2,v3} )
proof
assume A1: x in Lin {v1,v2,v3} ; ::_thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3)
now__::_thesis:_ex_a,_b,_c_being_Real_st_x_=_((a_*_v1)_+_(b_*_v2))_+_(c_*_v3)
percases ( ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) or v1 = v2 or v1 = v3 or v2 = v3 ) ;
supposeA2: ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ; ::_thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3)
consider l being Linear_Combination of {v1,v2,v3} such that
A3: x = Sum l by A1, Th1;
x = (((l . v1) * v1) + ((l . v2) * v2)) + ((l . v3) * v3) by A2, A3, RLVECT_4:6;
hence ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum
end;
suppose ( v1 = v2 or v1 = v3 or v2 = v3 ) ; ::_thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3)
then A4: ( {v1,v2,v3} = {v1,v3} or {v1,v2,v3} = {v1,v1,v2} or {v1,v2,v3} = {v3,v3,v1} ) by ENUMSET1:30, ENUMSET1:59;
now__::_thesis:_ex_a,_b,_c_being_Real_st_x_=_((a_*_v1)_+_(b_*_v2))_+_(c_*_v3)
percases ( {v1,v2,v3} = {v1,v2} or {v1,v2,v3} = {v1,v3} ) by A4, ENUMSET1:30;
suppose {v1,v2,v3} = {v1,v2} ; ::_thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3)
then consider a, b being Real such that
A5: x = (a * v1) + (b * v2) by A1, Th32;
x = ((a * v1) + (b * v2)) + (0. V) by A5, RLVECT_1:4
.= ((a * v1) + (b * v2)) + (0 * v3) by RLVECT_1:10 ;
hence ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum
end;
suppose {v1,v2,v3} = {v1,v3} ; ::_thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3)
then consider a, b being Real such that
A6: x = (a * v1) + (b * v3) by A1, Th32;
x = ((a * v1) + (0. V)) + (b * v3) by A6, RLVECT_1:4
.= ((a * v1) + (0 * v2)) + (b * v3) by RLVECT_1:10 ;
hence ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum
end;
end;
end;
hence ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum
end;
end;
end;
hence ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum
end;
given a, b, c being Real such that A7: x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: x in Lin {v1,v2,v3}
now__::_thesis:_x_in_Lin_{v1,v2,v3}
percases ( v1 = v2 or v1 = v3 or v2 = v3 or ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ) ;
supposeA8: ( v1 = v2 or v1 = v3 or v2 = v3 ) ; ::_thesis: x in Lin {v1,v2,v3}
now__::_thesis:_x_in_Lin_{v1,v2,v3}
percases ( v1 = v2 or v1 = v3 or v2 = v3 ) by A8;
suppose v1 = v2 ; ::_thesis: x in Lin {v1,v2,v3}
then ( {v1,v2,v3} = {v1,v3} & x = ((a + b) * v1) + (c * v3) ) by A7, ENUMSET1:30, RLVECT_1:def_6;
hence x in Lin {v1,v2,v3} by Th32; ::_thesis: verum
end;
supposeA9: v1 = v3 ; ::_thesis: x in Lin {v1,v2,v3}
then A10: {v1,v2,v3} = {v1,v1,v2} by ENUMSET1:57
.= {v2,v1} by ENUMSET1:30 ;
x = (b * v2) + ((a * v1) + (c * v1)) by A7, A9, RLVECT_1:def_3
.= (b * v2) + ((a + c) * v1) by RLVECT_1:def_6 ;
hence x in Lin {v1,v2,v3} by A10, Th32; ::_thesis: verum
end;
supposeA11: v2 = v3 ; ::_thesis: x in Lin {v1,v2,v3}
then A12: {v1,v2,v3} = {v2,v2,v1} by ENUMSET1:59
.= {v1,v2} by ENUMSET1:30 ;
x = (a * v1) + ((b * v2) + (c * v2)) by A7, A11, RLVECT_1:def_3
.= (a * v1) + ((b + c) * v2) by RLVECT_1:def_6 ;
hence x in Lin {v1,v2,v3} by A12, Th32; ::_thesis: verum
end;
end;
end;
hence x in Lin {v1,v2,v3} ; ::_thesis: verum
end;
supposeA13: ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ; ::_thesis: x in Lin {v1,v2,v3}
deffunc H1( set ) -> Element of NAT = 0 ;
A14: v1 <> v3 by A13;
A15: v2 <> v3 by A13;
A16: v1 <> v2 by A13;
consider f being Function of the carrier of V,REAL such that
A17: ( f . v1 = a & f . v2 = b & f . v3 = c ) and
A18: for v being VECTOR of V st v <> v1 & v <> v2 & v <> v3 holds
f . v = H1(v) from RLVECT_4:sch_1(A16, A14, A15);
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_v_being_VECTOR_of_V_st_not_v_in_{v1,v2,v3}_holds_
f_._v_=_0
let v be VECTOR of V; ::_thesis: ( not v in {v1,v2,v3} implies f . v = 0 )
assume A19: not v in {v1,v2,v3} ; ::_thesis: f . v = 0
then A20: v <> v3 by ENUMSET1:def_1;
( v <> v1 & v <> v2 ) by A19, ENUMSET1:def_1;
hence f . v = 0 by A18, A20; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
Carrier f c= {v1,v2,v3}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v1,v2,v3} )
assume that
A21: x in Carrier f and
A22: not x in {v1,v2,v3} ; ::_thesis: contradiction
A23: x <> v3 by A22, ENUMSET1:def_1;
( x <> v1 & x <> v2 ) by A22, ENUMSET1:def_1;
then f . x = 0 by A18, A21, A23;
hence contradiction by A21, RLVECT_2:19; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {v1,v2,v3} by RLVECT_2:def_6;
x = Sum f by A7, A13, A17, RLVECT_4:6;
hence x in Lin {v1,v2,v3} by Th1; ::_thesis: verum
end;
end;
end;
hence x in Lin {v1,v2,v3} ; ::_thesis: verum
end;
theorem :: RUSUB_3:36
for V being RealUnitarySpace
for w1, w2, w3 being VECTOR of V holds
( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} )
proof
let V be RealUnitarySpace; ::_thesis: for w1, w2, w3 being VECTOR of V holds
( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} )
let w1, w2, w3 be VECTOR of V; ::_thesis: ( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} )
A1: w3 in {w1,w2,w3} by ENUMSET1:def_1;
( w1 in {w1,w2,w3} & w2 in {w1,w2,w3} ) by ENUMSET1:def_1;
hence ( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} ) by A1, Th2; ::_thesis: verum
end;
theorem :: RUSUB_3:37
for V being RealUnitarySpace
for v, w1, w2, w3 being VECTOR of V
for x being set holds
( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )
proof
let V be RealUnitarySpace; ::_thesis: for v, w1, w2, w3 being VECTOR of V
for x being set holds
( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )
let v, w1, w2, w3 be VECTOR of V; ::_thesis: for x being set holds
( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )
let x be set ; ::_thesis: ( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) )
thus ( x in v + (Lin {w1,w2,w3}) implies ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) ) ::_thesis: ( ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) implies x in v + (Lin {w1,w2,w3}) )
proof
assume x in v + (Lin {w1,w2,w3}) ; ::_thesis: ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3)
then consider u being VECTOR of V such that
A1: u in Lin {w1,w2,w3} and
A2: x = v + u by RUSUB_2:63;
consider a, b, c being Real such that
A3: u = ((a * w1) + (b * w2)) + (c * w3) by A1, Th35;
take a ; ::_thesis: ex b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3)
take b ; ::_thesis: ex c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3)
take c ; ::_thesis: x = ((v + (a * w1)) + (b * w2)) + (c * w3)
x = (v + ((a * w1) + (b * w2))) + (c * w3) by A2, A3, RLVECT_1:def_3;
hence x = ((v + (a * w1)) + (b * w2)) + (c * w3) by RLVECT_1:def_3; ::_thesis: verum
end;
given a, b, c being Real such that A4: x = ((v + (a * w1)) + (b * w2)) + (c * w3) ; ::_thesis: x in v + (Lin {w1,w2,w3})
((a * w1) + (b * w2)) + (c * w3) in Lin {w1,w2,w3} by Th35;
then v + (((a * w1) + (b * w2)) + (c * w3)) in v + (Lin {w1,w2,w3}) by RUSUB_2:63;
then (v + ((a * w1) + (b * w2))) + (c * w3) in v + (Lin {w1,w2,w3}) by RLVECT_1:def_3;
hence x in v + (Lin {w1,w2,w3}) by A4, RLVECT_1:def_3; ::_thesis: verum
end;
theorem :: RUSUB_3:38
for V being RealUnitarySpace
for v, w being VECTOR of V st v in Lin {w} & v <> 0. V holds
Lin {v} = Lin {w}
proof
let V be RealUnitarySpace; ::_thesis: for v, w being VECTOR of V st v in Lin {w} & v <> 0. V holds
Lin {v} = Lin {w}
let v, w be VECTOR of V; ::_thesis: ( v in Lin {w} & v <> 0. V implies Lin {v} = Lin {w} )
assume that
A1: v in Lin {w} and
A2: v <> 0. V ; ::_thesis: Lin {v} = Lin {w}
consider a being Real such that
A3: v = a * w by A1, Th29;
now__::_thesis:_for_u_being_VECTOR_of_V_holds_
(_(_u_in_Lin_{v}_implies_u_in_Lin_{w}_)_&_(_u_in_Lin_{w}_implies_u_in_Lin_{v}_)_)
let u be VECTOR of V; ::_thesis: ( ( u in Lin {v} implies u in Lin {w} ) & ( u in Lin {w} implies u in Lin {v} ) )
A4: a <> 0 by A2, A3, RLVECT_1:10;
thus ( u in Lin {v} implies u in Lin {w} ) ::_thesis: ( u in Lin {w} implies u in Lin {v} )
proof
assume u in Lin {v} ; ::_thesis: u in Lin {w}
then consider b being Real such that
A5: u = b * v by Th29;
u = (b * a) * w by A3, A5, RLVECT_1:def_7;
hence u in Lin {w} by Th29; ::_thesis: verum
end;
assume u in Lin {w} ; ::_thesis: u in Lin {v}
then consider b being Real such that
A6: u = b * w by Th29;
(a ") * v = ((a ") * a) * w by A3, RLVECT_1:def_7
.= 1 * w by A4, XCMPLX_0:def_7
.= w by RLVECT_1:def_8 ;
then u = (b * (a ")) * v by A6, RLVECT_1:def_7;
hence u in Lin {v} by Th29; ::_thesis: verum
end;
hence Lin {v} = Lin {w} by RUSUB_1:25; ::_thesis: verum
end;
theorem :: RUSUB_3:39
for V being RealUnitarySpace
for v1, v2, w1, w2 being VECTOR of V st v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin {w1,w2} & v2 in Lin {w1,w2} holds
( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 )
proof
let V be RealUnitarySpace; ::_thesis: for v1, v2, w1, w2 being VECTOR of V st v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin {w1,w2} & v2 in Lin {w1,w2} holds
( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 )
let v1, v2, w1, w2 be VECTOR of V; ::_thesis: ( v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin {w1,w2} & v2 in Lin {w1,w2} implies ( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 ) )
assume that
A1: v1 <> v2 and
A2: {v1,v2} is linearly-independent and
A3: v1 in Lin {w1,w2} and
A4: v2 in Lin {w1,w2} ; ::_thesis: ( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 )
consider r1, r2 being Real such that
A5: v1 = (r1 * w1) + (r2 * w2) by A3, Th32;
consider r3, r4 being Real such that
A6: v2 = (r3 * w1) + (r4 * w2) by A4, Th32;
set t = (r1 * r4) - (r2 * r3);
A7: now__::_thesis:_(_r1_=_0_implies_not_r2_=_0_)
assume ( r1 = 0 & r2 = 0 ) ; ::_thesis: contradiction
then v1 = (0. V) + (0 * w2) by A5, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence contradiction by A2, RLVECT_3:11; ::_thesis: verum
end;
now__::_thesis:_not_r1_*_r4_=_r2_*_r3
assume A8: r1 * r4 = r2 * r3 ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( r1 <> 0 or r2 <> 0 ) by A7;
supposeA9: r1 <> 0 ; ::_thesis: contradiction
((r1 ") * r1) * r4 = (r1 ") * (r2 * r3) by A8, XCMPLX_1:4;
then 1 * r4 = (r1 ") * (r2 * r3) by A9, XCMPLX_0:def_7;
then v2 = (r3 * w1) + ((r3 * ((r1 ") * r2)) * w2) by A6
.= (r3 * w1) + (r3 * (((r1 ") * r2) * w2)) by RLVECT_1:def_7
.= (r3 * 1) * (w1 + (((r1 ") * r2) * w2)) by RLVECT_1:def_5
.= (r3 * ((r1 ") * r1)) * (w1 + (((r1 ") * r2) * w2)) by A9, XCMPLX_0:def_7
.= ((r3 * (r1 ")) * r1) * (w1 + (((r1 ") * r2) * w2))
.= (r3 * (r1 ")) * (r1 * (w1 + (((r1 ") * r2) * w2))) by RLVECT_1:def_7
.= (r3 * (r1 ")) * ((r1 * w1) + (r1 * (((r1 ") * r2) * w2))) by RLVECT_1:def_5
.= (r3 * (r1 ")) * ((r1 * w1) + ((r1 * ((r1 ") * r2)) * w2)) by RLVECT_1:def_7
.= (r3 * (r1 ")) * ((r1 * w1) + (((r1 * (r1 ")) * r2) * w2))
.= (r3 * (r1 ")) * ((r1 * w1) + ((1 * r2) * w2)) by A9, XCMPLX_0:def_7
.= (r3 * (r1 ")) * ((r1 * w1) + (r2 * w2)) ;
hence contradiction by A1, A2, A5, RLVECT_3:12; ::_thesis: verum
end;
supposeA10: r2 <> 0 ; ::_thesis: contradiction
(r2 ") * (r1 * r4) = (r2 ") * (r2 * r3) by A8
.= ((r2 ") * r2) * r3
.= 1 * r3 by A10, XCMPLX_0:def_7
.= r3 ;
then v2 = ((r4 * ((r2 ") * r1)) * w1) + (r4 * w2) by A6
.= (r4 * (((r2 ") * r1) * w1)) + (r4 * w2) by RLVECT_1:def_7
.= (r4 * 1) * ((((r2 ") * r1) * w1) + w2) by RLVECT_1:def_5
.= (r4 * ((r2 ") * r2)) * ((((r2 ") * r1) * w1) + w2) by A10, XCMPLX_0:def_7
.= ((r4 * (r2 ")) * r2) * ((((r2 ") * r1) * w1) + w2)
.= (r4 * (r2 ")) * (r2 * ((((r2 ") * r1) * w1) + w2)) by RLVECT_1:def_7
.= (r4 * (r2 ")) * ((r2 * (((r2 ") * r1) * w1)) + (r2 * w2)) by RLVECT_1:def_5
.= (r4 * (r2 ")) * (((r2 * ((r2 ") * r1)) * w1) + (r2 * w2)) by RLVECT_1:def_7
.= (r4 * (r2 ")) * ((((r2 * (r2 ")) * r1) * w1) + (r2 * w2))
.= (r4 * (r2 ")) * (((1 * r1) * w1) + (r2 * w2)) by A10, XCMPLX_0:def_7
.= (r4 * (r2 ")) * ((r1 * w1) + (r2 * w2)) ;
hence contradiction by A1, A2, A5, RLVECT_3:12; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
then A11: (r1 * r4) - (r2 * r3) <> 0 ;
A12: now__::_thesis:_(_r2_<>_0_implies_(_w1_=_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r4)_*_v1)_+_(-_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r2)_*_v2))_&_w2_=_(-_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r3)_*_v1))_+_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r1)_*_v2)_)_)
assume A13: r2 <> 0 ; ::_thesis: ( w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) & w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) )
(r2 ") * v1 = ((r2 ") * (r1 * w1)) + ((r2 ") * (r2 * w2)) by A5, RLVECT_1:def_5
.= (((r2 ") * r1) * w1) + ((r2 ") * (r2 * w2)) by RLVECT_1:def_7
.= (((r2 ") * r1) * w1) + (((r2 ") * r2) * w2) by RLVECT_1:def_7
.= (((r2 ") * r1) * w1) + (1 * w2) by A13, XCMPLX_0:def_7
.= (((r2 ") * r1) * w1) + w2 by RLVECT_1:def_8 ;
then A14: w2 = ((r2 ") * v1) - (((r2 ") * r1) * w1) by RLSUB_2:61;
then w2 = ((r2 ") * v1) - ((r2 ") * (r1 * w1)) by RLVECT_1:def_7;
then v2 = (r3 * w1) + (r4 * ((r2 ") * (v1 - (r1 * w1)))) by A6, RLVECT_1:34
.= (r3 * w1) + ((r4 * (r2 ")) * (v1 - (r1 * w1))) by RLVECT_1:def_7
.= (r3 * w1) + (((r4 * (r2 ")) * v1) - ((r4 * (r2 ")) * (r1 * w1))) by RLVECT_1:34
.= ((r3 * w1) + ((r4 * (r2 ")) * v1)) - ((r4 * (r2 ")) * (r1 * w1)) by RLVECT_1:def_3
.= (((r4 * (r2 ")) * v1) + (r3 * w1)) - (((r4 * (r2 ")) * r1) * w1) by RLVECT_1:def_7
.= ((r4 * (r2 ")) * v1) + ((r3 * w1) - (((r4 * (r2 ")) * r1) * w1)) by RLVECT_1:def_3
.= ((r4 * (r2 ")) * v1) + ((r3 - ((r4 * (r2 ")) * r1)) * w1) by RLVECT_1:35 ;
then r2 * v2 = (r2 * ((r4 * (r2 ")) * v1)) + (r2 * ((r3 - ((r4 * (r2 ")) * r1)) * w1)) by RLVECT_1:def_5
.= ((r2 * (r4 * (r2 "))) * v1) + (r2 * ((r3 - ((r4 * (r2 ")) * r1)) * w1)) by RLVECT_1:def_7
.= ((r4 * (r2 * (r2 "))) * v1) + (r2 * ((r3 - ((r4 * (r2 ")) * r1)) * w1))
.= ((r4 * 1) * v1) + (r2 * ((r3 - ((r4 * (r2 ")) * r1)) * w1)) by A13, XCMPLX_0:def_7
.= (r4 * v1) + ((r2 * (r3 - ((r4 * (r2 ")) * r1))) * w1) by RLVECT_1:def_7
.= (r4 * v1) + (((r2 * r3) - ((r2 * (r2 ")) * (r4 * r1))) * w1)
.= (r4 * v1) + (((r2 * r3) - (1 * (r4 * r1))) * w1) by A13, XCMPLX_0:def_7
.= (r4 * v1) + ((- ((r1 * r4) - (r2 * r3))) * w1)
.= (r4 * v1) + (- (((r1 * r4) - (r2 * r3)) * w1)) by RLVECT_4:3 ;
then - (((r1 * r4) - (r2 * r3)) * w1) = (r2 * v2) - (r4 * v1) by RLSUB_2:61;
then ((r1 * r4) - (r2 * r3)) * w1 = - ((r2 * v2) - (r4 * v1)) by RLVECT_1:17
.= (r4 * v1) + (- (r2 * v2)) by RLVECT_1:33 ;
then ((((r1 * r4) - (r2 * r3)) ") * ((r1 * r4) - (r2 * r3))) * w1 = (((r1 * r4) - (r2 * r3)) ") * ((r4 * v1) + (- (r2 * v2))) by RLVECT_1:def_7;
then 1 * w1 = (((r1 * r4) - (r2 * r3)) ") * ((r4 * v1) + (- (r2 * v2))) by A11, XCMPLX_0:def_7;
then w1 = (((r1 * r4) - (r2 * r3)) ") * ((r4 * v1) + (- (r2 * v2))) by RLVECT_1:def_8
.= ((((r1 * r4) - (r2 * r3)) ") * (r4 * v1)) + ((((r1 * r4) - (r2 * r3)) ") * (- (r2 * v2))) by RLVECT_1:def_5
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + ((((r1 * r4) - (r2 * r3)) ") * (- (r2 * v2))) by RLVECT_1:def_7
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + ((((r1 * r4) - (r2 * r3)) ") * ((- r2) * v2)) by RLVECT_4:3
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (((((r1 * r4) - (r2 * r3)) ") * (- r2)) * v2) by RLVECT_1:def_7
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (((- (((r1 * r4) - (r2 * r3)) ")) * r2) * v2)
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + ((- (((r1 * r4) - (r2 * r3)) ")) * (r2 * v2)) by RLVECT_1:def_7
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- ((((r1 * r4) - (r2 * r3)) ") * (r2 * v2))) by RLVECT_4:3 ;
hence w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) by RLVECT_1:def_7; ::_thesis: w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2)
then A15: w2 = ((r2 ") * v1) - (((r2 ") * r1) * (((((r1 * r4) - (r2 * r3)) ") * (r4 * v1)) - (((((r1 * r4) - (r2 * r3)) ") * r2) * v2))) by A14, RLVECT_1:def_7
.= ((r2 ") * v1) - (((r2 ") * r1) * (((((r1 * r4) - (r2 * r3)) ") * (r4 * v1)) - ((((r1 * r4) - (r2 * r3)) ") * (r2 * v2)))) by RLVECT_1:def_7
.= ((r2 ") * v1) - (((r2 ") * r1) * ((((r1 * r4) - (r2 * r3)) ") * ((r4 * v1) - (r2 * v2)))) by RLVECT_1:34
.= ((r2 ") * v1) - (((r1 * (r2 ")) * (((r1 * r4) - (r2 * r3)) ")) * ((r4 * v1) - (r2 * v2))) by RLVECT_1:def_7
.= ((r2 ") * v1) - ((r1 * ((((r1 * r4) - (r2 * r3)) ") * (r2 "))) * ((r4 * v1) - (r2 * v2)))
.= ((r2 ") * v1) - (r1 * (((((r1 * r4) - (r2 * r3)) ") * (r2 ")) * ((r4 * v1) - (r2 * v2)))) by RLVECT_1:def_7
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * ((r2 ") * ((r4 * v1) - (r2 * v2))))) by RLVECT_1:def_7
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * v1)) - ((r2 ") * (r2 * v2))))) by RLVECT_1:34
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * v1)) - (((r2 ") * r2) * v2)))) by RLVECT_1:def_7
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * v1) - (((r2 ") * r2) * v2)))) by RLVECT_1:def_7
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * v1) - (1 * v2)))) by A13, XCMPLX_0:def_7
.= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * v1) - v2))) by RLVECT_1:def_8
.= ((r2 ") * v1) - (r1 * (((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * r4) * v1)) - ((((r1 * r4) - (r2 * r3)) ") * v2))) by RLVECT_1:34
.= ((r2 ") * v1) - ((r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * r4) * v1))) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * v2))) by RLVECT_1:34
.= (((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * r4) * v1)))) + (r1 * ((((r1 * r4) - (r2 * r3)) ") * v2)) by RLVECT_1:29
.= (((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * r4) * v1)))) + ((r1 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:def_7
.= (((r2 ") * v1) - ((r1 * (((r1 * r4) - (r2 * r3)) ")) * (((r2 ") * r4) * v1))) + ((r1 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:def_7
.= (((r2 ") * v1) - (((r1 * (((r1 * r4) - (r2 * r3)) ")) * ((r2 ") * r4)) * v1)) + ((r1 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:def_7
.= (((r2 ") - ((r1 * (((r1 * r4) - (r2 * r3)) ")) * ((r2 ") * r4))) * v1) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) by RLVECT_1:35 ;
(r2 ") - ((r1 * (((r1 * r4) - (r2 * r3)) ")) * ((r2 ") * r4)) = (r2 ") * (1 - (r1 * ((((r1 * r4) - (r2 * r3)) ") * r4)))
.= (r2 ") * (((((r1 * r4) - (r2 * r3)) ") * ((r1 * r4) - (r2 * r3))) - ((((r1 * r4) - (r2 * r3)) ") * (r1 * r4))) by A11, XCMPLX_0:def_7
.= (((r2 ") * r2) * (((r1 * r4) - (r2 * r3)) ")) * (- r3)
.= (1 * (((r1 * r4) - (r2 * r3)) ")) * (- r3) by A13, XCMPLX_0:def_7
.= - ((((r1 * r4) - (r2 * r3)) ") * r3) ;
hence w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) by A15, RLVECT_4:3; ::_thesis: verum
end;
set a4 = (((r1 * r4) - (r2 * r3)) ") * r1;
set a3 = - ((((r1 * r4) - (r2 * r3)) ") * r3);
set a2 = - ((((r1 * r4) - (r2 * r3)) ") * r2);
set a1 = (((r1 * r4) - (r2 * r3)) ") * r4;
now__::_thesis:_(_r1_<>_0_implies_(_w2_=_(-_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r3)_*_v1))_+_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r1)_*_v2)_&_w1_=_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r4)_*_v1)_+_(-_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r2)_*_v2))_)_)
assume A16: r1 <> 0 ; ::_thesis: ( w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) & w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) )
A17: (r1 ") + ((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * r3) = (r1 ") * (1 + ((((r1 * r4) - (r2 * r3)) ") * (r2 * r3)))
.= (r1 ") * (((((r1 * r4) - (r2 * r3)) ") * ((r1 * r4) - (r2 * r3))) + ((((r1 * r4) - (r2 * r3)) ") * (r2 * r3))) by A11, XCMPLX_0:def_7
.= (((r1 * r4) - (r2 * r3)) ") * (((r1 ") * r1) * r4)
.= (((r1 * r4) - (r2 * r3)) ") * (1 * r4) by A16, XCMPLX_0:def_7
.= (((r1 * r4) - (r2 * r3)) ") * r4 ;
(r1 ") * v1 = ((r1 ") * (r1 * w1)) + ((r1 ") * (r2 * w2)) by A5, RLVECT_1:def_5
.= (((r1 ") * r1) * w1) + ((r1 ") * (r2 * w2)) by RLVECT_1:def_7
.= (1 * w1) + ((r1 ") * (r2 * w2)) by A16, XCMPLX_0:def_7
.= w1 + ((r1 ") * (r2 * w2)) by RLVECT_1:def_8
.= w1 + ((r2 * (r1 ")) * w2) by RLVECT_1:def_7 ;
then A18: w1 = ((r1 ") * v1) - ((r2 * (r1 ")) * w2) by RLSUB_2:61;
then v2 = ((r3 * ((r1 ") * v1)) - (r3 * ((r2 * (r1 ")) * w2))) + (r4 * w2) by A6, RLVECT_1:34
.= (((r3 * (r1 ")) * v1) - (r3 * (((r1 ") * r2) * w2))) + (r4 * w2) by RLVECT_1:def_7
.= (((r3 * (r1 ")) * v1) - ((r3 * ((r1 ") * r2)) * w2)) + (r4 * w2) by RLVECT_1:def_7
.= (((r3 * (r1 ")) * v1) - (((r1 ") * (r3 * r2)) * w2)) + (r4 * w2)
.= ((((r1 ") * r3) * v1) - ((r1 ") * ((r3 * r2) * w2))) + (r4 * w2) by RLVECT_1:def_7
.= (((r1 ") * (r3 * v1)) - ((r1 ") * ((r3 * r2) * w2))) + (r4 * w2) by RLVECT_1:def_7 ;
then r1 * v2 = (r1 * (((r1 ") * (r3 * v1)) - ((r1 ") * ((r3 * r2) * w2)))) + (r1 * (r4 * w2)) by RLVECT_1:def_5
.= (r1 * (((r1 ") * (r3 * v1)) - ((r1 ") * ((r3 * r2) * w2)))) + ((r1 * r4) * w2) by RLVECT_1:def_7
.= ((r1 * ((r1 ") * (r3 * v1))) - (r1 * ((r1 ") * ((r3 * r2) * w2)))) + ((r1 * r4) * w2) by RLVECT_1:34
.= (((r1 * (r1 ")) * (r3 * v1)) - (r1 * ((r1 ") * ((r3 * r2) * w2)))) + ((r1 * r4) * w2) by RLVECT_1:def_7
.= (((r1 * (r1 ")) * (r3 * v1)) - ((r1 * (r1 ")) * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by RLVECT_1:def_7
.= ((1 * (r3 * v1)) - ((r1 * (r1 ")) * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by A16, XCMPLX_0:def_7
.= ((1 * (r3 * v1)) - (1 * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by A16, XCMPLX_0:def_7
.= ((r3 * v1) - (1 * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by RLVECT_1:def_8
.= ((r3 * v1) - ((r3 * r2) * w2)) + ((r1 * r4) * w2) by RLVECT_1:def_8
.= (r3 * v1) - (((r3 * r2) * w2) - ((r1 * r4) * w2)) by RLVECT_1:29
.= (r3 * v1) + (- (((r3 * r2) - (r1 * r4)) * w2)) by RLVECT_1:35
.= (r3 * v1) + ((- ((r3 * r2) - (r1 * r4))) * w2) by RLVECT_4:3
.= (r3 * v1) + (((r1 * r4) - (r2 * r3)) * w2) ;
then (((r1 * r4) - (r2 * r3)) ") * (r1 * v2) = ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) + ((((r1 * r4) - (r2 * r3)) ") * (((r1 * r4) - (r2 * r3)) * w2)) by RLVECT_1:def_5
.= ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) + (((((r1 * r4) - (r2 * r3)) ") * ((r1 * r4) - (r2 * r3))) * w2) by RLVECT_1:def_7
.= ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) + (1 * w2) by A11, XCMPLX_0:def_7
.= ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) + w2 by RLVECT_1:def_8 ;
hence w2 = ((((r1 * r4) - (r2 * r3)) ") * (r1 * v2)) - ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) by RLSUB_2:61
.= (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) - ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) by RLVECT_1:def_7
.= (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) by RLVECT_1:def_7 ;
::_thesis: w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2))
hence w1 = ((r1 ") * v1) - (((r2 * (r1 ")) * (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1))) + ((r2 * (r1 ")) * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by A18, RLVECT_1:def_5
.= ((r1 ") * v1) - (((r2 * (r1 ")) * (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1))) + (((r2 * (r1 ")) * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_7
.= ((r1 ") * v1) - (((r2 * (r1 ")) * (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1))) + ((r2 * (((r1 ") * r1) * (((r1 * r4) - (r2 * r3)) "))) * v2))
.= ((r1 ") * v1) - (((r2 * (r1 ")) * (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1))) + ((r2 * (1 * (((r1 * r4) - (r2 * r3)) "))) * v2)) by A16, XCMPLX_0:def_7
.= ((r1 ") * v1) - (((r2 * (r1 ")) * (- ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7
.= ((r1 ") * v1) - (((r2 * (r1 ")) * ((- (((r1 * r4) - (r2 * r3)) ")) * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_4:3
.= ((r1 ") * v1) - ((((r2 * (r1 ")) * (- (((r1 * r4) - (r2 * r3)) "))) * (r3 * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7
.= ((r1 ") * v1) - ((((((- 1) * (((r1 * r4) - (r2 * r3)) ")) * r2) * (r1 ")) * (r3 * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2))
.= ((r1 ") * v1) - (((((- 1) * (((r1 * r4) - (r2 * r3)) ")) * r2) * ((r1 ") * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7
.= ((r1 ") * v1) - ((((- 1) * (((r1 * r4) - (r2 * r3)) ")) * (r2 * ((r1 ") * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7
.= ((r1 ") * v1) - (((- 1) * ((((r1 * r4) - (r2 * r3)) ") * (r2 * ((r1 ") * (r3 * v1))))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7
.= ((r1 ") * v1) - ((- ((((r1 * r4) - (r2 * r3)) ") * (r2 * ((r1 ") * (r3 * v1))))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:16
.= ((r1 ") * v1) - ((- (((((r1 * r4) - (r2 * r3)) ") * r2) * ((r1 ") * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7
.= ((r1 ") * v1) - ((- ((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7
.= ((r1 ") * v1) - ((- (((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * r3) * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7
.= (((r1 ") * v1) - (- (((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * r3) * v1))) - ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:27
.= (((r1 ") * v1) + (((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * r3) * v1)) - ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:17
.= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) by A17, RLVECT_1:def_6 ;
::_thesis: verum
end;
then A19: ( w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2) & w2 = ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) ) by A7, A12, RLVECT_4:3;
now__::_thesis:_for_u_being_VECTOR_of_V_holds_
(_(_u_in_Lin_{w1,w2}_implies_u_in_Lin_{v1,v2}_)_&_(_u_in_Lin_{v1,v2}_implies_u_in_Lin_{w1,w2}_)_)
let u be VECTOR of V; ::_thesis: ( ( u in Lin {w1,w2} implies u in Lin {v1,v2} ) & ( u in Lin {v1,v2} implies u in Lin {w1,w2} ) )
thus ( u in Lin {w1,w2} implies u in Lin {v1,v2} ) ::_thesis: ( u in Lin {v1,v2} implies u in Lin {w1,w2} )
proof
assume u in Lin {w1,w2} ; ::_thesis: u in Lin {v1,v2}
then consider r5, r6 being Real such that
A20: u = (r5 * w1) + (r6 * w2) by Th32;
u = ((r5 * (((((r1 * r4) - (r2 * r3)) ") * r4) * v1)) + (r5 * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + (r6 * (((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by A19, A20, RLVECT_1:def_5
.= ((r5 * (((((r1 * r4) - (r2 * r3)) ") * r4) * v1)) + (r5 * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((r6 * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (r6 * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_5
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (r5 * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((r6 * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (r6 * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_7
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2)) + ((r6 * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (r6 * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_7
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2)) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + (r6 * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_7
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2)) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_7
.= ((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2))) by RLVECT_1:def_3
.= ((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2))) by RLVECT_1:def_3
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1)) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_3
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) + (r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3)))) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_6
.= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) + (r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3)))) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) + (r6 * ((((r1 * r4) - (r2 * r3)) ") * r1))) * v2) by RLVECT_1:def_6 ;
hence u in Lin {v1,v2} by Th32; ::_thesis: verum
end;
assume u in Lin {v1,v2} ; ::_thesis: u in Lin {w1,w2}
then consider r5, r6 being Real such that
A21: u = (r5 * v1) + (r6 * v2) by Th32;
u = (r5 * ((r1 * w1) + (r2 * w2))) + ((r6 * (r3 * w1)) + (r6 * (r4 * w2))) by A5, A6, A21, RLVECT_1:def_5
.= ((r5 * (r1 * w1)) + (r5 * (r2 * w2))) + ((r6 * (r3 * w1)) + (r6 * (r4 * w2))) by RLVECT_1:def_5
.= (((r5 * (r1 * w1)) + (r5 * (r2 * w2))) + (r6 * (r3 * w1))) + (r6 * (r4 * w2)) by RLVECT_1:def_3
.= (((r5 * (r1 * w1)) + (r6 * (r3 * w1))) + (r5 * (r2 * w2))) + (r6 * (r4 * w2)) by RLVECT_1:def_3
.= ((((r5 * r1) * w1) + (r6 * (r3 * w1))) + (r5 * (r2 * w2))) + (r6 * (r4 * w2)) by RLVECT_1:def_7
.= ((((r5 * r1) * w1) + ((r6 * r3) * w1)) + (r5 * (r2 * w2))) + (r6 * (r4 * w2)) by RLVECT_1:def_7
.= ((((r5 * r1) * w1) + ((r6 * r3) * w1)) + ((r5 * r2) * w2)) + (r6 * (r4 * w2)) by RLVECT_1:def_7
.= ((((r5 * r1) * w1) + ((r6 * r3) * w1)) + ((r5 * r2) * w2)) + ((r6 * r4) * w2) by RLVECT_1:def_7
.= ((((r5 * r1) + (r6 * r3)) * w1) + ((r5 * r2) * w2)) + ((r6 * r4) * w2) by RLVECT_1:def_6
.= (((r5 * r1) + (r6 * r3)) * w1) + (((r5 * r2) * w2) + ((r6 * r4) * w2)) by RLVECT_1:def_3
.= (((r5 * r1) + (r6 * r3)) * w1) + (((r5 * r2) + (r6 * r4)) * w2) by RLVECT_1:def_6 ;
hence u in Lin {w1,w2} by Th32; ::_thesis: verum
end;
hence Lin {w1,w2} = Lin {v1,v2} by RUSUB_1:25; ::_thesis: ( {w1,w2} is linearly-independent & w1 <> w2 )
now__::_thesis:_for_a,_b_being_Real_st_(a_*_w1)_+_(b_*_w2)_=_0._V_holds_
(_not_a_<>_0_&_not_b_<>_0_)
let a, b be Real; ::_thesis: ( (a * w1) + (b * w2) = 0. V implies ( not a <> 0 & not b <> 0 ) )
A22: ((r1 * r4) - (r2 * r3)) " <> 0 by A11, XCMPLX_1:202;
assume (a * w1) + (b * w2) = 0. V ; ::_thesis: ( not a <> 0 & not b <> 0 )
then A23: 0. V = ((a * (((((r1 * r4) - (r2 * r3)) ") * r4) * v1)) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + (b * (((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by A19, RLVECT_1:def_5
.= ((a * (((((r1 * r4) - (r2 * r3)) ") * r4) * v1)) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((b * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (b * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_5
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((b * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (b * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_7
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((b * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_7
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + (((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_7
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2)) + (((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_7
.= ((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + (((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2))) by RLVECT_1:def_3
.= ((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2))) by RLVECT_1:def_3
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1)) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_3
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) + (b * (- ((((r1 * r4) - (r2 * r3)) ") * r3)))) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_6
.= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) + (b * (- ((((r1 * r4) - (r2 * r3)) ") * r3)))) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) + (b * ((((r1 * r4) - (r2 * r3)) ") * r1))) * v2) by RLVECT_1:def_6 ;
then 0 = (((r1 * r4) - (r2 * r3)) ") * ((r4 * a) + ((- r3) * b)) by A1, A2, RLVECT_3:13;
then A24: (r4 * a) - (r3 * b) = 0 by A22, XCMPLX_1:6;
0 = (((r1 * r4) - (r2 * r3)) ") * (((- r2) * a) + (r1 * b)) by A1, A2, A23, RLVECT_3:13;
then A25: (r1 * b) + (- (r2 * a)) = 0 by A22, XCMPLX_1:6;
assume A26: ( a <> 0 or b <> 0 ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( a <> 0 or b <> 0 ) by A26;
supposeA27: a <> 0 ; ::_thesis: contradiction
(a ") * (r1 * b) = ((a ") * a) * r2 by A25, XCMPLX_1:4;
then (a ") * (r1 * b) = 1 * r2 by A27, XCMPLX_0:def_7;
then r2 = r1 * ((a ") * b) ;
then v1 = (r1 * w1) + (r1 * (((a ") * b) * w2)) by A5, RLVECT_1:def_7;
then A28: v1 = r1 * (w1 + (((a ") * b) * w2)) by RLVECT_1:def_5;
((a ") * a) * r4 = (a ") * (r3 * b) by A24, XCMPLX_1:4;
then 1 * r4 = (a ") * (r3 * b) by A27, XCMPLX_0:def_7;
then r4 = r3 * ((a ") * b) ;
then v2 = (r3 * w1) + (r3 * (((a ") * b) * w2)) by A6, RLVECT_1:def_7;
then v2 = r3 * (w1 + (((a ") * b) * w2)) by RLVECT_1:def_5;
hence contradiction by A1, A2, A28, RLVECT_4:21; ::_thesis: verum
end;
supposeA29: b <> 0 ; ::_thesis: contradiction
((b ") * b) * r1 = (b ") * (r2 * a) by A25, XCMPLX_1:4;
then 1 * r1 = (b ") * (r2 * a) by A29, XCMPLX_0:def_7;
then r1 = r2 * ((b ") * a) ;
then v1 = (r2 * (((b ") * a) * w1)) + (r2 * w2) by A5, RLVECT_1:def_7;
then A30: v1 = r2 * ((((b ") * a) * w1) + w2) by RLVECT_1:def_5;
((b ") * b) * r3 = (b ") * (r4 * a) by A24, XCMPLX_1:4;
then 1 * r3 = (b ") * (r4 * a) by A29, XCMPLX_0:def_7;
then r3 = r4 * ((b ") * a) ;
then v2 = (r4 * (((b ") * a) * w1)) + (r4 * w2) by A6, RLVECT_1:def_7;
then v2 = r4 * ((((b ") * a) * w1) + w2) by RLVECT_1:def_5;
hence contradiction by A1, A2, A30, RLVECT_4:21; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence ( {w1,w2} is linearly-independent & w1 <> w2 ) by RLVECT_3:13; ::_thesis: verum
end;
begin
theorem :: RUSUB_3:40
for V being RealUnitarySpace
for x being set holds
( x in (0). V iff x = 0. V ) by Lm1;
theorem :: RUSUB_3:41
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3 by Lm2;
theorem :: RUSUB_3:42
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 & W1 is Subspace of W3 holds
W1 is Subspace of W2 /\ W3 by Lm3;
theorem :: RUSUB_3:43
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 & W2 is Subspace of W3 holds
W1 + W2 is Subspace of W3 by Lm5;
theorem :: RUSUB_3:44
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3 by Lm4;
theorem :: RUSUB_3:45
for V being RealUnitarySpace
for W1, W2 being Subspace of V
for v being VECTOR of V st W1 is Subspace of W2 holds
v + W1 c= v + W2
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V
for v being VECTOR of V st W1 is Subspace of W2 holds
v + W1 c= v + W2
let W1, W2 be Subspace of V; ::_thesis: for v being VECTOR of V st W1 is Subspace of W2 holds
v + W1 c= v + W2
let v be VECTOR of V; ::_thesis: ( W1 is Subspace of W2 implies v + W1 c= v + W2 )
assume A1: W1 is Subspace of W2 ; ::_thesis: v + W1 c= v + W2
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + W1 or x in v + W2 )
assume x in v + W1 ; ::_thesis: x in v + W2
then consider u being VECTOR of V such that
A2: u in W1 and
A3: x = v + u by RUSUB_2:63;
u in W2 by A1, A2, RUSUB_1:1;
hence x in v + W2 by A3, RUSUB_2:63; ::_thesis: verum
end;