:: RUSUB_4 semantic presentation
begin
theorem Th1: :: RUSUB_4:1
for V being RealUnitarySpace
for A, B being finite Subset of V
for v being VECTOR of V st v in Lin (A \/ B) & not v in Lin B holds
ex w being VECTOR of V st
( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )
proof
let V be RealUnitarySpace; ::_thesis: for A, B being finite Subset of V
for v being VECTOR of V st v in Lin (A \/ B) & not v in Lin B holds
ex w being VECTOR of V st
( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )
let A, B be finite Subset of V; ::_thesis: for v being VECTOR of V st v in Lin (A \/ B) & not v in Lin B holds
ex w being VECTOR of V st
( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )
let v be VECTOR of V; ::_thesis: ( v in Lin (A \/ B) & not v in Lin B implies ex w being VECTOR of V st
( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) ) )
assume that
A1: v in Lin (A \/ B) and
A2: not v in Lin B ; ::_thesis: ex w being VECTOR of V st
( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )
consider L being Linear_Combination of A \/ B such that
A3: v = Sum L by A1, RUSUB_3:1;
v in {v} by TARSKI:def_1;
then v in Lin {v} by RUSUB_3:2;
then consider Lv being Linear_Combination of {v} such that
A4: v = Sum Lv by RUSUB_3:1;
A5: Carrier L c= A \/ B by RLVECT_2:def_6;
now__::_thesis:_ex_w_being_VECTOR_of_V_st_
(_w_in_A_&_not_L_._w_=_0_)
assume A6: for w being VECTOR of V st w in A holds
L . w = 0 ; ::_thesis: contradiction
now__::_thesis:_for_x_being_set_st_x_in_Carrier_L_holds_
not_x_in_A
let x be set ; ::_thesis: ( x in Carrier L implies not x in A )
assume that
A7: x in Carrier L and
A8: x in A ; ::_thesis: contradiction
ex u being VECTOR of V st
( x = u & L . u <> 0 ) by A7, RLVECT_5:3;
hence contradiction by A6, A8; ::_thesis: verum
end;
then Carrier L misses A by XBOOLE_0:3;
then Carrier L c= B by A5, XBOOLE_1:73;
then L is Linear_Combination of B by RLVECT_2:def_6;
hence contradiction by A2, A3, RUSUB_3:1; ::_thesis: verum
end;
then consider w being VECTOR of V such that
A9: w in A and
A10: L . w <> 0 ;
consider F being FinSequence of the carrier of V such that
A11: F is one-to-one and
A12: rng F = Carrier L and
A13: Sum L = Sum (L (#) F) by RLVECT_2:def_8;
A14: w in rng F by A10, A12, RLVECT_5:3;
then reconsider Fw1 = F -| w as FinSequence of the carrier of V by FINSEQ_4:41;
reconsider Fw2 = F |-- w as FinSequence of the carrier of V by A14, FINSEQ_4:50;
A15: rng Fw1 misses rng Fw2 by A11, A14, FINSEQ_4:57;
set Fw = Fw1 ^ Fw2;
consider K being Linear_Combination of V such that
A16: Carrier K = (rng (Fw1 ^ Fw2)) /\ (Carrier L) and
A17: L (#) (Fw1 ^ Fw2) = K (#) (Fw1 ^ Fw2) by RLVECT_5:7;
F just_once_values w by A11, A14, FINSEQ_4:8;
then Fw1 ^ Fw2 = F - {w} by FINSEQ_4:54;
then A18: rng (Fw1 ^ Fw2) = (Carrier L) \ {w} by A12, FINSEQ_3:65;
then A19: Carrier K = rng (Fw1 ^ Fw2) by A16, XBOOLE_1:28, XBOOLE_1:36;
then A20: Carrier K c= (A \/ B) \ {w} by A5, A18, XBOOLE_1:33;
take w ; ::_thesis: ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) )
set a = L . w;
A21: (L . w) " <> 0 by A10, XCMPLX_1:202;
F = ((F -| w) ^ <*w*>) ^ (F |-- w) by A14, FINSEQ_4:51;
then F = Fw1 ^ (<*w*> ^ Fw2) by FINSEQ_1:32;
then L (#) F = (L (#) Fw1) ^ (L (#) (<*w*> ^ Fw2)) by RLVECT_3:34
.= (L (#) Fw1) ^ ((L (#) <*w*>) ^ (L (#) Fw2)) by RLVECT_3:34
.= ((L (#) Fw1) ^ (L (#) <*w*>)) ^ (L (#) Fw2) by FINSEQ_1:32
.= ((L (#) Fw1) ^ <*((L . w) * w)*>) ^ (L (#) Fw2) by RLVECT_2:26 ;
then A22: Sum (L (#) F) = Sum ((L (#) Fw1) ^ (<*((L . w) * w)*> ^ (L (#) Fw2))) by FINSEQ_1:32
.= (Sum (L (#) Fw1)) + (Sum (<*((L . w) * w)*> ^ (L (#) Fw2))) by RLVECT_1:41
.= (Sum (L (#) Fw1)) + ((Sum <*((L . w) * w)*>) + (Sum (L (#) Fw2))) by RLVECT_1:41
.= (Sum (L (#) Fw1)) + ((Sum (L (#) Fw2)) + ((L . w) * w)) by RLVECT_1:44
.= ((Sum (L (#) Fw1)) + (Sum (L (#) Fw2))) + ((L . w) * w) by RLVECT_1:def_3
.= (Sum ((L (#) Fw1) ^ (L (#) Fw2))) + ((L . w) * w) by RLVECT_1:41
.= (Sum (L (#) (Fw1 ^ Fw2))) + ((L . w) * w) by RLVECT_3:34 ;
reconsider K = K as Linear_Combination of (A \/ B) \ {w} by A20, RLVECT_2:def_6;
Carrier ((- K) + Lv) c= (Carrier (- K)) \/ (Carrier Lv) by RLVECT_2:37;
then A23: Carrier ((- K) + Lv) c= (Carrier K) \/ (Carrier Lv) by RLVECT_2:51;
set LC = ((L . w) ") * ((- K) + Lv);
Carrier Lv c= {v} by RLVECT_2:def_6;
then (Carrier K) \/ (Carrier Lv) c= ((A \/ B) \ {w}) \/ {v} by A20, XBOOLE_1:13;
then Carrier ((- K) + Lv) c= ((A \/ B) \ {w}) \/ {v} by A23, XBOOLE_1:1;
then Carrier (((L . w) ") * ((- K) + Lv)) c= ((A \/ B) \ {w}) \/ {v} by A21, RLVECT_2:42;
then A24: ((L . w) ") * ((- K) + Lv) is Linear_Combination of ((A \/ B) \ {w}) \/ {v} by RLVECT_2:def_6;
( Fw1 is one-to-one & Fw2 is one-to-one ) by A11, A14, FINSEQ_4:52, FINSEQ_4:53;
then Fw1 ^ Fw2 is one-to-one by A15, FINSEQ_3:91;
then Sum (K (#) (Fw1 ^ Fw2)) = Sum K by A19, RLVECT_2:def_8;
then ((L . w) ") * v = (((L . w) ") * (Sum K)) + (((L . w) ") * ((L . w) * w)) by A3, A13, A22, A17, RLVECT_1:def_5
.= (((L . w) ") * (Sum K)) + ((((L . w) ") * (L . w)) * w) by RLVECT_1:def_7
.= (((L . w) ") * (Sum K)) + (1 * w) by A10, XCMPLX_0:def_7
.= (((L . w) ") * (Sum K)) + w by RLVECT_1:def_8 ;
then w = (((L . w) ") * v) - (((L . w) ") * (Sum K)) by RLSUB_2:61
.= ((L . w) ") * (v - (Sum K)) by RLVECT_1:34
.= ((L . w) ") * ((- (Sum K)) + v) by RLVECT_1:def_11 ;
then w = ((L . w) ") * ((Sum (- K)) + (Sum Lv)) by A4, RLVECT_3:3
.= ((L . w) ") * (Sum ((- K) + Lv)) by RLVECT_3:1
.= Sum (((L . w) ") * ((- K) + Lv)) by RLVECT_3:2 ;
hence ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) ) by A9, A24, RUSUB_3:1; ::_thesis: verum
end;
Lm1: for X, x being set st x in X holds
(X \ {x}) \/ {x} = X
proof
let X, x be set ; ::_thesis: ( x in X implies (X \ {x}) \/ {x} = X )
assume x in X ; ::_thesis: (X \ {x}) \/ {x} = X
then A1: {x} is Subset of X by SUBSET_1:41;
{x} \/ (X \ {x}) = {x} \/ X by XBOOLE_1:39
.= X by A1, XBOOLE_1:12 ;
hence (X \ {x}) \/ {x} = X ; ::_thesis: verum
end;
Lm2: 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 Th2: :: RUSUB_4:2
for V being RealUnitarySpace
for A, B being finite Subset of V st UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent holds
( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )
proof
let V be RealUnitarySpace; ::_thesis: for A, B being finite Subset of V st UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent holds
( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )
defpred S1[ Element of NAT ] means for n being Element of NAT
for A, B being finite Subset of V st card A = n & card B = $1 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent holds
( $1 <= n & ex C being finite Subset of V st
( C c= A & card C = n - $1 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) );
A1: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A2: S1[m] ; ::_thesis: S1[m + 1]
let n be Element of NAT ; ::_thesis: for A, B being finite Subset of V st card A = n & card B = m + 1 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent holds
( m + 1 <= n & ex C being finite Subset of V st
( C c= A & card C = n - (m + 1) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )
let A, B be finite Subset of V; ::_thesis: ( card A = n & card B = m + 1 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent implies ( m + 1 <= n & ex C being finite Subset of V st
( C c= A & card C = n - (m + 1) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) )
assume that
A3: card A = n and
A4: card B = m + 1 and
A5: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A and
A6: B is linearly-independent ; ::_thesis: ( m + 1 <= n & ex C being finite Subset of V st
( C c= A & card C = n - (m + 1) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )
consider v being set such that
A7: v in B by A4, CARD_1:27, XBOOLE_0:def_1;
reconsider v = v as VECTOR of V by A7;
set Bv = B \ {v};
A8: B \ {v} is linearly-independent by A6, RLVECT_3:5, XBOOLE_1:36;
{v} is Subset of B by A7, SUBSET_1:41;
then A9: card (B \ {v}) = (card B) - (card {v}) by CARD_2:44
.= (m + 1) - 1 by A4, CARD_1:30
.= m ;
then consider C being finite Subset of V such that
A10: C c= A and
A11: card C = n - m and
A12: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin ((B \ {v}) \/ C) by A2, A3, A5, A8;
A13: not v in Lin (B \ {v}) by A6, A7, RUSUB_3:25;
A14: now__::_thesis:_not_m_=_n
assume m = n ; ::_thesis: contradiction
then consider C being finite Subset of V such that
C c= A and
A15: card C = m - m and
A16: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin ((B \ {v}) \/ C) by A2, A3, A5, A9, A8;
C = {} by A15;
then B \ {v} is Basis of V by A8, A16, RUSUB_3:def_2;
hence contradiction by A13, RUSUB_3:21; ::_thesis: verum
end;
v in Lin ((B \ {v}) \/ C) by A12, STRUCT_0:def_5;
then consider w being VECTOR of V such that
A17: w in C and
A18: w in Lin (((C \/ (B \ {v})) \ {w}) \/ {v}) by A13, Th1;
set Cw = C \ {w};
((B \ {v}) \ {w}) \/ {v} c= (B \ {v}) \/ {v} by XBOOLE_1:9, XBOOLE_1:36;
then (C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) c= (C \ {w}) \/ ((B \ {v}) \/ {v}) by XBOOLE_1:9;
then A19: (C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) c= B \/ (C \ {w}) by A7, Lm1;
{w} is Subset of C by A17, SUBSET_1:41;
then A20: card (C \ {w}) = (card C) - (card {w}) by CARD_2:44
.= (n - m) - 1 by A11, CARD_1:30
.= n - (m + 1) ;
C \ {w} c= C by XBOOLE_1:36;
then A21: C \ {w} c= A by A10, XBOOLE_1:1;
((C \/ (B \ {v})) \ {w}) \/ {v} = ((C \ {w}) \/ ((B \ {v}) \ {w})) \/ {v} by XBOOLE_1:42
.= (C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) by XBOOLE_1:4 ;
then Lin (((C \/ (B \ {v})) \ {w}) \/ {v}) is Subspace of Lin (B \/ (C \ {w})) by A19, RUSUB_3:7;
then A22: w in Lin (B \/ (C \ {w})) by A18, RUSUB_1:1;
A23: ( B \ {v} c= B & C = (C \ {w}) \/ {w} ) by A17, Lm1, XBOOLE_1:36;
now__::_thesis:_for_x_being_set_st_x_in_(B_\_{v})_\/_C_holds_
x_in_the_carrier_of_(Lin_(B_\/_(C_\_{w})))
let x be set ; ::_thesis: ( x in (B \ {v}) \/ C implies x in the carrier of (Lin (B \/ (C \ {w}))) )
assume x in (B \ {v}) \/ C ; ::_thesis: x in the carrier of (Lin (B \/ (C \ {w})))
then ( x in B \ {v} or x in C ) by XBOOLE_0:def_3;
then ( x in B or x in C \ {w} or x in {w} ) by A23, XBOOLE_0:def_3;
then ( x in B \/ (C \ {w}) or x in {w} ) by XBOOLE_0:def_3;
then ( x in Lin (B \/ (C \ {w})) or x = w ) by RUSUB_3:2, TARSKI:def_1;
hence x in the carrier of (Lin (B \/ (C \ {w}))) by A22, STRUCT_0:def_5; ::_thesis: verum
end;
then (B \ {v}) \/ C c= the carrier of (Lin (B \/ (C \ {w}))) by TARSKI:def_3;
then Lin ((B \ {v}) \/ C) is Subspace of Lin (B \/ (C \ {w})) by RUSUB_3:27;
then A24: the carrier of (Lin ((B \ {v}) \/ C)) c= the carrier of (Lin (B \/ (C \ {w}))) by RUSUB_1:def_1;
the carrier of (Lin (B \/ (C \ {w}))) c= the carrier of V by RUSUB_1:def_1;
then the carrier of (Lin (B \/ (C \ {w}))) = the carrier of V by A12, A24, XBOOLE_0:def_10;
then A25: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ (C \ {w})) by A12, RUSUB_1:24;
m <= n by A2, A3, A5, A9, A8;
then m < n by A14, XXREAL_0:1;
hence ( m + 1 <= n & ex C being finite Subset of V st
( C c= A & card C = n - (m + 1) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) by A21, A20, A25, NAT_1:13; ::_thesis: verum
end;
A26: S1[ 0 ]
proof
let n be Element of NAT ; ::_thesis: for A, B being finite Subset of V st card A = n & card B = 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent holds
( 0 <= n & ex C being finite Subset of V st
( C c= A & card C = n - 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )
let A, B be finite Subset of V; ::_thesis: ( card A = n & card B = 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent implies ( 0 <= n & ex C being finite Subset of V st
( C c= A & card C = n - 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) )
assume that
A27: card A = n and
A28: card B = 0 and
A29: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A and
B is linearly-independent ; ::_thesis: ( 0 <= n & ex C being finite Subset of V st
( C c= A & card C = n - 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )
B = {} by A28;
then A = B \/ A ;
hence ( 0 <= n & ex C being finite Subset of V st
( C c= A & card C = n - 0 & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) by A27, A29, NAT_1:2; ::_thesis: verum
end;
A30: for m being Element of NAT holds S1[m] from NAT_1:sch_1(A26, A1);
let A, B be finite Subset of V; ::_thesis: ( UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent implies ( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) )
assume ( UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B is linearly-independent ) ; ::_thesis: ( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) )
hence ( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin (B \/ C) ) ) by A30; ::_thesis: verum
end;
definition
let V be RealUnitarySpace;
attrV is finite-dimensional means :Def1: :: RUSUB_4:def 1
ex A being finite Subset of V st A is Basis of V;
end;
:: deftheorem Def1 defines finite-dimensional RUSUB_4:def_1_:_
for V being RealUnitarySpace holds
( V is finite-dimensional iff ex A being finite Subset of V st A is Basis of V );
registration
cluster non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like finite-dimensional for UNITSTR ;
existence
ex b1 being RealUnitarySpace st
( b1 is strict & b1 is finite-dimensional )
proof
set V = the RealUnitarySpace;
take (0). the RealUnitarySpace ; ::_thesis: ( (0). the RealUnitarySpace is strict & (0). the RealUnitarySpace is finite-dimensional )
thus (0). the RealUnitarySpace is strict ; ::_thesis: (0). the RealUnitarySpace is finite-dimensional
take A = {} the carrier of ((0). the RealUnitarySpace); :: according to RUSUB_4:def_1 ::_thesis: A is Basis of (0). the RealUnitarySpace
Lin A = (0). ((0). the RealUnitarySpace) by RUSUB_3:3;
then ( A is linearly-independent & Lin A = UNITSTR(# the carrier of ((0). the RealUnitarySpace), the ZeroF of ((0). the RealUnitarySpace), the addF of ((0). the RealUnitarySpace), the Mult of ((0). the RealUnitarySpace), the scalar of ((0). the RealUnitarySpace) #) ) by RLVECT_3:7, RUSUB_1:30;
hence A is Basis of (0). the RealUnitarySpace by RUSUB_3:def_2; ::_thesis: verum
end;
end;
theorem Th3: :: RUSUB_4:3
for V being RealUnitarySpace st V is finite-dimensional holds
for I being Basis of V holds I is finite
proof
let V be RealUnitarySpace; ::_thesis: ( V is finite-dimensional implies for I being Basis of V holds I is finite )
assume V is finite-dimensional ; ::_thesis: for I being Basis of V holds I is finite
then consider A being finite Subset of V such that
A1: A is Basis of V by Def1;
let B be Basis of V; ::_thesis: B is finite
consider p being FinSequence such that
A2: rng p = A by FINSEQ_1:52;
reconsider p = p as FinSequence of the carrier of V by A2, FINSEQ_1:def_4;
set Car = { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } ;
set C = union { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } ;
A3: union { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } or x in B )
assume x in union { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } ; ::_thesis: x in B
then consider R being set such that
A4: x in R and
A5: R in { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } by TARSKI:def_4;
ex L being Linear_Combination of B st
( R = Carrier L & ex i being Element of NAT st
( i in dom p & Sum L = p . i ) ) by A5;
then R c= B by RLVECT_2:def_6;
hence x in B by A4; ::_thesis: verum
end;
then reconsider C = union { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } as Subset of V by XBOOLE_1:1;
for v being VECTOR of V holds
( v in (Omega). V iff v in Lin C )
proof
let v be VECTOR of V; ::_thesis: ( v in (Omega). V iff v in Lin C )
hereby ::_thesis: ( v in Lin C implies v in (Omega). V )
assume v in (Omega). V ; ::_thesis: v in Lin C
then v in UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) by RUSUB_1:def_3;
then v in Lin A by A1, RUSUB_3:def_2;
then consider LA being Linear_Combination of A such that
A6: v = Sum LA by RUSUB_3:1;
Carrier LA c= the carrier of (Lin C)
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in Carrier LA or w in the carrier of (Lin C) )
assume A7: w in Carrier LA ; ::_thesis: w in the carrier of (Lin C)
then reconsider w9 = w as VECTOR of V ;
w9 in Lin B by RUSUB_3:21;
then consider LB being Linear_Combination of B such that
A8: w = Sum LB by RUSUB_3:1;
Carrier LA c= A by RLVECT_2:def_6;
then ex i being set st
( i in dom p & w = p . i ) by A2, A7, FUNCT_1:def_3;
then A9: Carrier LB in { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } by A8;
Carrier LB c= C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier LB or x in C )
assume x in Carrier LB ; ::_thesis: x in C
hence x in C by A9, TARSKI:def_4; ::_thesis: verum
end;
then LB is Linear_Combination of C by RLVECT_2:def_6;
then w in Lin C by A8, RUSUB_3:1;
hence w in the carrier of (Lin C) by STRUCT_0:def_5; ::_thesis: verum
end;
then ex LC being Linear_Combination of C st Sum LA = Sum LC by RUSUB_3:17;
hence v in Lin C by A6, RUSUB_3:1; ::_thesis: verum
end;
assume v in Lin C ; ::_thesis: v in (Omega). V
v in the carrier of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) ;
then v in the carrier of ((Omega). V) by RUSUB_1:def_3;
hence v in (Omega). V by STRUCT_0:def_5; ::_thesis: verum
end;
then (Omega). V = Lin C by RUSUB_1:25;
then A10: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin C by RUSUB_1:def_3;
A11: B is linearly-independent by RUSUB_3:def_2;
then C is linearly-independent by A3, RLVECT_3:5;
then A12: C is Basis of V by A10, RUSUB_3:def_2;
B c= C
proof
set D = B \ C;
assume not B c= C ; ::_thesis: contradiction
then ex v being set st
( v in B & not v in C ) by TARSKI:def_3;
then reconsider D = B \ C as non empty Subset of V by XBOOLE_0:def_5;
reconsider B = B as Subset of V ;
C \/ (B \ C) = C \/ B by XBOOLE_1:39
.= B by A3, XBOOLE_1:12 ;
then B = C \/ D ;
hence contradiction by A11, A12, RUSUB_3:26, XBOOLE_1:79; ::_thesis: verum
end;
then A13: B = C by A3, XBOOLE_0:def_10;
defpred S1[ set , set ] means ex L being Linear_Combination of B st
( $2 = Carrier L & Sum L = p . $1 );
A14: for i being Nat st i in Seg (len p) holds
ex x being set st S1[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg (len p) implies ex x being set st S1[i,x] )
assume i in Seg (len p) ; ::_thesis: ex x being set st S1[i,x]
then i in dom p by FINSEQ_1:def_3;
then p . i in the carrier of V by FINSEQ_2:11;
then p . i in Lin B by RUSUB_3:21;
then consider L being Linear_Combination of B such that
A15: p . i = Sum L by RUSUB_3:1;
S1[i, Carrier L] by A15;
hence ex x being set st S1[i,x] ; ::_thesis: verum
end;
ex q being FinSequence st
( dom q = Seg (len p) & ( for i being Nat st i in Seg (len p) holds
S1[i,q . i] ) ) from FINSEQ_1:sch_1(A14);
then consider q being FinSequence such that
A16: dom q = Seg (len p) and
A17: for i being Nat st i in Seg (len p) holds
S1[i,q . i] ;
A18: dom p = dom q by A16, FINSEQ_1:def_3;
A19: for i being Nat
for y1, y2 being set st i in Seg (len p) & S1[i,y1] & S1[i,y2] holds
y1 = y2
proof
let i be Nat; ::_thesis: for y1, y2 being set st i in Seg (len p) & S1[i,y1] & S1[i,y2] holds
y1 = y2
let y1, y2 be set ; ::_thesis: ( i in Seg (len p) & S1[i,y1] & S1[i,y2] implies y1 = y2 )
assume that
i in Seg (len p) and
A20: S1[i,y1] and
A21: S1[i,y2] ; ::_thesis: y1 = y2
consider L1 being Linear_Combination of B such that
A22: ( y1 = Carrier L1 & Sum L1 = p . i ) by A20;
consider L2 being Linear_Combination of B such that
A23: ( y2 = Carrier L2 & Sum L2 = p . i ) by A21;
( Carrier L1 c= B & Carrier L2 c= B ) by RLVECT_2:def_6;
hence y1 = y2 by A11, A22, A23, RLVECT_5:1; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in__{__(Carrier_L)_where_L_is_Linear_Combination_of_B_:_ex_i_being_Element_of_NAT_st_
(_i_in_dom_p_&_Sum_L_=_p_._i_)__}__holds_
x_in_rng_q
let x be set ; ::_thesis: ( x in { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } implies x in rng q )
assume x in { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } ; ::_thesis: x in rng q
then consider L being Linear_Combination of B such that
A24: x = Carrier L and
A25: ex i being Element of NAT st
( i in dom p & Sum L = p . i ) ;
consider i being Element of NAT such that
A26: i in dom p and
A27: Sum L = p . i by A25;
S1[i,q . i] by A16, A17, A18, A26;
then x = q . i by A19, A16, A18, A24, A26, A27;
hence x in rng q by A18, A26, FUNCT_1:def_3; ::_thesis: verum
end;
then A28: { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } c= rng q by TARSKI:def_3;
for R being set st R in { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } holds
R is finite
proof
let R be set ; ::_thesis: ( R in { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } implies R is finite )
assume R in { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st
( i in dom p & Sum L = p . i ) } ; ::_thesis: R is finite
then ex L being Linear_Combination of B st
( R = Carrier L & ex i being Element of NAT st
( i in dom p & Sum L = p . i ) ) ;
hence R is finite ; ::_thesis: verum
end;
hence B is finite by A13, A28, FINSET_1:7; ::_thesis: verum
end;
theorem :: RUSUB_4:4
for V being RealUnitarySpace
for A being Subset of V st V is finite-dimensional & A is linearly-independent holds
A is finite
proof
let V be RealUnitarySpace; ::_thesis: for A being Subset of V st V is finite-dimensional & A is linearly-independent holds
A is finite
let A be Subset of V; ::_thesis: ( V is finite-dimensional & A is linearly-independent implies A is finite )
assume that
A1: V is finite-dimensional and
A2: A is linearly-independent ; ::_thesis: A is finite
consider B being Basis of V such that
A3: A c= B by A2, RUSUB_3:15;
B is finite by A1, Th3;
hence A is finite by A3; ::_thesis: verum
end;
theorem Th5: :: RUSUB_4:5
for V being RealUnitarySpace
for A, B being Basis of V st V is finite-dimensional holds
card A = card B
proof
let V be RealUnitarySpace; ::_thesis: for A, B being Basis of V st V is finite-dimensional holds
card A = card B
let A, B be Basis of V; ::_thesis: ( V is finite-dimensional implies card A = card B )
assume V is finite-dimensional ; ::_thesis: card A = card B
then reconsider A9 = A, B9 = B as finite Subset of V by Th3;
( UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin B & A9 is linearly-independent ) by RUSUB_3:def_2;
then A1: card A9 <= card B9 by Th2;
( UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = Lin A & B9 is linearly-independent ) by RUSUB_3:def_2;
then card B9 <= card A9 by Th2;
hence card A = card B by A1, XXREAL_0:1; ::_thesis: verum
end;
theorem Th6: :: RUSUB_4:6
for V being RealUnitarySpace holds (0). V is finite-dimensional
proof
let V be RealUnitarySpace; ::_thesis: (0). V is finite-dimensional
reconsider V9 = (0). V as strict RealUnitarySpace ;
reconsider I = {} the carrier of V9 as finite Subset of V9 ;
the carrier of V9 = {(0. V)} by RUSUB_1:def_2
.= {(0. V9)} by RUSUB_1:4
.= the carrier of ((0). V9) by RUSUB_1:def_2 ;
then A1: V9 = (0). V9 by RUSUB_1:26;
( I is linearly-independent & Lin I = (0). V9 ) by RLVECT_3:7, RUSUB_3:3;
then I is Basis of V9 by A1, RUSUB_3:def_2;
hence (0). V is finite-dimensional by Def1; ::_thesis: verum
end;
theorem Th7: :: RUSUB_4:7
for V being RealUnitarySpace
for W being Subspace of V st V is finite-dimensional holds
W is finite-dimensional
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V st V is finite-dimensional holds
W is finite-dimensional
let W be Subspace of V; ::_thesis: ( V is finite-dimensional implies W is finite-dimensional )
set A = the Basis of W;
consider I being Basis of V such that
A1: the Basis of W c= I by RUSUB_3:24;
assume V is finite-dimensional ; ::_thesis: W is finite-dimensional
then I is finite by Th3;
hence W is finite-dimensional by A1, Def1; ::_thesis: verum
end;
registration
let V be RealUnitarySpace;
cluster non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like finite-dimensional for Subspace of V;
existence
ex b1 being Subspace of V st
( b1 is finite-dimensional & b1 is strict )
proof
take (0). V ; ::_thesis: ( (0). V is finite-dimensional & (0). V is strict )
thus ( (0). V is finite-dimensional & (0). V is strict ) by Th6; ::_thesis: verum
end;
end;
registration
let V be finite-dimensional RealUnitarySpace;
cluster -> finite-dimensional for Subspace of V;
correctness
coherence
for b1 being Subspace of V holds b1 is finite-dimensional ;
by Th7;
end;
registration
let V be finite-dimensional RealUnitarySpace;
cluster non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like finite-dimensional for Subspace of V;
existence
ex b1 being Subspace of V st b1 is strict
proof
(0). V is strict finite-dimensional Subspace of V ;
hence ex b1 being Subspace of V st b1 is strict ; ::_thesis: verum
end;
end;
begin
definition
let V be RealUnitarySpace;
assume A1: V is finite-dimensional ;
func dim V -> Element of NAT means :Def2: :: RUSUB_4:def 2
for I being Basis of V holds it = card I;
existence
ex b1 being Element of NAT st
for I being Basis of V holds b1 = card I
proof
consider A being finite Subset of V such that
A2: A is Basis of V by A1, Def1;
consider n being Element of NAT such that
A3: n = card A ;
for I being Basis of V holds card I = n by A1, A2, A3, Th5;
hence ex b1 being Element of NAT st
for I being Basis of V holds b1 = card I ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of NAT st ( for I being Basis of V holds b1 = card I ) & ( for I being Basis of V holds b2 = card I ) holds
b1 = b2
proof
let n, m be Element of NAT ; ::_thesis: ( ( for I being Basis of V holds n = card I ) & ( for I being Basis of V holds m = card I ) implies n = m )
assume that
A4: for I being Basis of V holds card I = n and
A5: for I being Basis of V holds card I = m ; ::_thesis: n = m
consider A being finite Subset of V such that
A6: A is Basis of V by A1, Def1;
card A = n by A4, A6;
hence n = m by A5, A6; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines dim RUSUB_4:def_2_:_
for V being RealUnitarySpace st V is finite-dimensional holds
for b2 being Element of NAT holds
( b2 = dim V iff for I being Basis of V holds b2 = card I );
theorem Th8: :: RUSUB_4:8
for V being finite-dimensional RealUnitarySpace
for W being Subspace of V holds dim W <= dim V
proof
let V be finite-dimensional RealUnitarySpace; ::_thesis: for W being Subspace of V holds dim W <= dim V
let W be Subspace of V; ::_thesis: dim W <= dim V
set A = the Basis of W;
reconsider A = the Basis of W as Subset of W ;
A is linearly-independent by RUSUB_3:def_2;
then reconsider B = A as linearly-independent Subset of V by RUSUB_3:22;
reconsider A9 = B as finite Subset of V by Th3;
reconsider V9 = V as RealUnitarySpace ;
set I = the Basis of V9;
A1: Lin the Basis of V9 = UNITSTR(# the carrier of V9, the ZeroF of V9, the addF of V9, the Mult of V9, the scalar of V9 #) by RUSUB_3:def_2;
reconsider I = the Basis of V9 as finite Subset of V by Th3;
A2: dim V = card I by Def2;
card A9 <= card I by A1, Th2;
hence dim W <= dim V by A2, Def2; ::_thesis: verum
end;
theorem Th9: :: RUSUB_4:9
for V being finite-dimensional RealUnitarySpace
for A being Subset of V st A is linearly-independent holds
card A = dim (Lin A)
proof
let V be finite-dimensional RealUnitarySpace; ::_thesis: for A being Subset of V st A is linearly-independent holds
card A = dim (Lin A)
let A be Subset of V; ::_thesis: ( A is linearly-independent implies card A = dim (Lin A) )
assume A1: A is linearly-independent ; ::_thesis: card A = dim (Lin A)
set W = Lin A;
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
x_in_the_carrier_of_(Lin_A)
let x be set ; ::_thesis: ( x in A implies x in the carrier of (Lin A) )
assume x in A ; ::_thesis: x in the carrier of (Lin A)
then x in Lin A by RUSUB_3:2;
hence x in the carrier of (Lin A) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider B = A as linearly-independent Subset of (Lin A) by A1, RUSUB_3:23, TARSKI:def_3;
Lin A = Lin B by RUSUB_3:28;
then reconsider B = B as Basis of Lin A by RUSUB_3:def_2;
card B = dim (Lin A) by Def2;
hence card A = dim (Lin A) ; ::_thesis: verum
end;
theorem Th10: :: RUSUB_4:10
for V being finite-dimensional RealUnitarySpace holds dim V = dim ((Omega). V)
proof
let V be finite-dimensional RealUnitarySpace; ::_thesis: dim V = dim ((Omega). V)
consider I being finite Subset of V such that
A1: I is Basis of V by Def1;
A2: (Omega). V = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) by RUSUB_1:def_3
.= Lin I by A1, RUSUB_3:def_2 ;
( card I = dim V & I is linearly-independent ) by A1, Def2, RUSUB_3:def_2;
hence dim V = dim ((Omega). V) by A2, Th9; ::_thesis: verum
end;
theorem :: RUSUB_4:11
for V being finite-dimensional RealUnitarySpace
for W being Subspace of V holds
( dim V = dim W iff (Omega). V = (Omega). W )
proof
let V be finite-dimensional RealUnitarySpace; ::_thesis: for W being Subspace of V holds
( dim V = dim W iff (Omega). V = (Omega). W )
let W be Subspace of V; ::_thesis: ( dim V = dim W iff (Omega). V = (Omega). W )
consider A being finite Subset of V such that
A1: A is Basis of V by Def1;
hereby ::_thesis: ( (Omega). V = (Omega). W implies dim V = dim W )
set A = the Basis of W;
consider B being Basis of V such that
A2: the Basis of W c= B by RUSUB_3:24;
the carrier of W c= the carrier of V by RUSUB_1:def_1;
then reconsider A9 = the Basis of W as finite Subset of V by Th3, XBOOLE_1:1;
reconsider B9 = B as finite Subset of V by Th3;
assume dim V = dim W ; ::_thesis: (Omega). V = (Omega). W
then A3: card the Basis of W = dim V by Def2
.= card B by Def2 ;
A4: now__::_thesis:_not_the_Basis_of_W_<>_B
assume the Basis of W <> B ; ::_thesis: contradiction
then the Basis of W c< B by A2, XBOOLE_0:def_8;
then card A9 < card B9 by CARD_2:48;
hence contradiction by A3; ::_thesis: verum
end;
reconsider B = B as Subset of V ;
reconsider A = the Basis of W as Subset of W ;
(Omega). V = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) by RUSUB_1:def_3
.= Lin B by RUSUB_3:def_2
.= Lin A by A4, RUSUB_3:28
.= UNITSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the scalar of W #) by RUSUB_3:def_2
.= (Omega). W by RUSUB_1:def_3 ;
hence (Omega). V = (Omega). W ; ::_thesis: verum
end;
consider B being finite Subset of W such that
A5: B is Basis of W by Def1;
A6: A is linearly-independent by A1, RUSUB_3:def_2;
assume (Omega). V = (Omega). W ; ::_thesis: dim V = dim W
then UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = (Omega). W by RUSUB_1:def_3
.= UNITSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the scalar of W #) by RUSUB_1:def_3 ;
then A7: Lin A = UNITSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the scalar of W #) by A1, RUSUB_3:def_2
.= Lin B by A5, RUSUB_3:def_2 ;
A8: B is linearly-independent by A5, RUSUB_3:def_2;
reconsider B = B as Subset of W ;
reconsider A = A as Subset of V ;
dim V = card A by A1, Def2
.= dim (Lin B) by A6, A7, Th9
.= card B by A8, Th9
.= dim W by A5, Def2 ;
hence dim V = dim W ; ::_thesis: verum
end;
theorem Th12: :: RUSUB_4:12
for V being finite-dimensional RealUnitarySpace holds
( dim V = 0 iff (Omega). V = (0). V )
proof
let V be finite-dimensional RealUnitarySpace; ::_thesis: ( dim V = 0 iff (Omega). V = (0). V )
consider I being finite Subset of V such that
A1: I is Basis of V by Def1;
hereby ::_thesis: ( (Omega). V = (0). V implies dim V = 0 )
consider I being finite Subset of V such that
A2: I is Basis of V by Def1;
assume dim V = 0 ; ::_thesis: (Omega). V = (0). V
then card I = 0 by A2, Def2;
then A3: I = {} the carrier of V ;
(Omega). V = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) by RUSUB_1:def_3
.= Lin I by A2, RUSUB_3:def_2
.= (0). V by A3, RUSUB_3:3 ;
hence (Omega). V = (0). V ; ::_thesis: verum
end;
A4: now__::_thesis:_not_I_=_{(0._V)}
assume I = {(0. V)} ; ::_thesis: contradiction
then I is linearly-dependent by RLVECT_3:8;
hence contradiction by A1, RUSUB_3:def_2; ::_thesis: verum
end;
assume (Omega). V = (0). V ; ::_thesis: dim V = 0
then UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = (0). V by RUSUB_1:def_3;
then Lin I = (0). V by A1, RUSUB_3:def_2;
then ( I = {} or I = {(0. V)} ) by RUSUB_3:4;
hence dim V = 0 by A1, A4, Def2, CARD_1:27; ::_thesis: verum
end;
theorem :: RUSUB_4:13
for V being finite-dimensional RealUnitarySpace holds
( dim V = 1 iff ex v being VECTOR of V st
( v <> 0. V & (Omega). V = Lin {v} ) )
proof
let V be finite-dimensional RealUnitarySpace; ::_thesis: ( dim V = 1 iff ex v being VECTOR of V st
( v <> 0. V & (Omega). V = Lin {v} ) )
hereby ::_thesis: ( ex v being VECTOR of V st
( v <> 0. V & (Omega). V = Lin {v} ) implies dim V = 1 )
consider I being finite Subset of V such that
A1: I is Basis of V by Def1;
assume dim V = 1 ; ::_thesis: ex v being VECTOR of V st
( v <> 0. V & (Omega). V = Lin {v} )
then card I = 1 by A1, Def2;
then consider v being set such that
A2: I = {v} by CARD_2:42;
v in I by A2, TARSKI:def_1;
then reconsider v = v as VECTOR of V ;
{v} is linearly-independent by A1, A2, RUSUB_3:def_2;
then A3: v <> 0. V by RLVECT_3:8;
Lin {v} = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) by A1, A2, RUSUB_3:def_2;
hence ex v being VECTOR of V st
( v <> 0. V & (Omega). V = Lin {v} ) by A3, RUSUB_1:def_3; ::_thesis: verum
end;
given v being VECTOR of V such that A4: ( v <> 0. V & (Omega). V = Lin {v} ) ; ::_thesis: dim V = 1
( {v} is linearly-independent & Lin {v} = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) ) by A4, RLVECT_3:8, RUSUB_1:def_3;
then A5: {v} is Basis of V by RUSUB_3:def_2;
card {v} = 1 by CARD_1:30;
hence dim V = 1 by A5, Def2; ::_thesis: verum
end;
theorem :: RUSUB_4:14
for V being finite-dimensional RealUnitarySpace holds
( dim V = 2 iff ex u, v being VECTOR of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )
proof
let V be finite-dimensional RealUnitarySpace; ::_thesis: ( dim V = 2 iff ex u, v being VECTOR of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) )
hereby ::_thesis: ( ex u, v being VECTOR of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) implies dim V = 2 )
consider I being finite Subset of V such that
A1: I is Basis of V by Def1;
assume dim V = 2 ; ::_thesis: ex u, v being VECTOR of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} )
then A2: card I = 2 by A1, Def2;
then consider u being set such that
A3: u in I by CARD_1:27, XBOOLE_0:def_1;
reconsider u = u as VECTOR of V by A3;
now__::_thesis:_not_I_c=_{u}
assume I c= {u} ; ::_thesis: contradiction
then card I <= card {u} by NAT_1:43;
then 2 <= 1 by A2, CARD_1:30;
hence contradiction ; ::_thesis: verum
end;
then consider v being set such that
A4: v in I and
A5: not v in {u} by TARSKI:def_3;
reconsider v = v as VECTOR of V by A4;
A6: v <> u by A5, TARSKI:def_1;
A7: now__::_thesis:_I_c=_{u,v}
assume not I c= {u,v} ; ::_thesis: contradiction
then consider w being set such that
A8: w in I and
A9: not w in {u,v} by TARSKI:def_3;
for x being set st x in {u,v,w} holds
x in I by A3, A4, A8, ENUMSET1:def_1;
then {u,v,w} c= I by TARSKI:def_3;
then A10: card {u,v,w} <= card I by NAT_1:43;
( w <> u & w <> v ) by A9, TARSKI:def_2;
then 3 <= 2 by A2, A6, A10, CARD_2:58;
hence contradiction ; ::_thesis: verum
end;
for x being set st x in {u,v} holds
x in I by A3, A4, TARSKI:def_2;
then {u,v} c= I by TARSKI:def_3;
then A11: I = {u,v} by A7, XBOOLE_0:def_10;
then A12: {u,v} is linearly-independent by A1, RUSUB_3:def_2;
Lin {u,v} = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) by A1, A11, RUSUB_3:def_2
.= (Omega). V by RUSUB_1:def_3 ;
hence ex u, v being VECTOR of V st
( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) by A6, A12; ::_thesis: verum
end;
given u, v being VECTOR of V such that A13: u <> v and
A14: {u,v} is linearly-independent and
A15: (Omega). V = Lin {u,v} ; ::_thesis: dim V = 2
Lin {u,v} = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) by A15, RUSUB_1:def_3;
then A16: {u,v} is Basis of V by A14, RUSUB_3:def_2;
card {u,v} = 2 by A13, CARD_2:57;
hence dim V = 2 by A16, Def2; ::_thesis: verum
end;
theorem Th15: :: RUSUB_4:15
for V being finite-dimensional RealUnitarySpace
for W1, W2 being Subspace of V holds (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)
proof
let V be finite-dimensional RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)
let W1, W2 be Subspace of V; ::_thesis: (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)
reconsider V = V as RealUnitarySpace ;
reconsider W1 = W1, W2 = W2 as Subspace of V ;
consider I being finite Subset of (W1 /\ W2) such that
A1: I is Basis of W1 /\ W2 by Def1;
W1 /\ W2 is Subspace of W2 by RUSUB_2:16;
then consider I2 being Basis of W2 such that
A2: I c= I2 by A1, RUSUB_3:24;
W1 /\ W2 is Subspace of W1 by RUSUB_2:16;
then consider I1 being Basis of W1 such that
A3: I c= I1 by A1, RUSUB_3:24;
reconsider I2 = I2 as finite Subset of W2 by Th3;
reconsider I1 = I1 as finite Subset of W1 by Th3;
A4: now__::_thesis:_I1_/\_I2_c=_I
I1 is linearly-independent by RUSUB_3:def_2;
then reconsider I19 = I1 as linearly-independent Subset of V by RUSUB_3:22;
the carrier of (W1 /\ W2) c= the carrier of V by RUSUB_1:def_1;
then reconsider I9 = I as Subset of V by XBOOLE_1:1;
assume not I1 /\ I2 c= I ; ::_thesis: contradiction
then consider x being set such that
A5: x in I1 /\ I2 and
A6: not x in I by TARSKI:def_3;
x in I1 by A5, XBOOLE_0:def_4;
then x in Lin I1 by RUSUB_3:2;
then x in UNITSTR(# the carrier of W1, the ZeroF of W1, the addF of W1, the Mult of W1, the scalar of W1 #) by RUSUB_3:def_2;
then A7: x in the carrier of W1 by STRUCT_0:def_5;
A8: the carrier of W1 c= the carrier of V by RUSUB_1:def_1;
then reconsider x9 = x as VECTOR of V by A7;
now__::_thesis:_for_y_being_set_st_y_in_I_\/_{x}_holds_
y_in_the_carrier_of_V
let y be set ; ::_thesis: ( y in I \/ {x} implies y in the carrier of V )
the carrier of (W1 /\ W2) c= the carrier of V by RUSUB_1:def_1;
then A9: I c= the carrier of V by XBOOLE_1:1;
assume y in I \/ {x} ; ::_thesis: y in the carrier of V
then ( y in I or y in {x} ) by XBOOLE_0:def_3;
then ( y in the carrier of V or y = x ) by A9, TARSKI:def_1;
hence y in the carrier of V by A7, A8; ::_thesis: verum
end;
then reconsider Ix = I \/ {x} as Subset of V by TARSKI:def_3;
now__::_thesis:_for_y_being_set_st_y_in_I_\/_{x}_holds_
y_in_I19
let y be set ; ::_thesis: ( y in I \/ {x} implies y in I19 )
assume y in I \/ {x} ; ::_thesis: y in I19
then ( y in I or y in {x} ) by XBOOLE_0:def_3;
then ( y in I1 or y = x ) by A3, TARSKI:def_1;
hence y in I19 by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
then A10: Ix c= I19 by TARSKI:def_3;
x in {x} by TARSKI:def_1;
then A11: x9 in Ix by XBOOLE_0:def_3;
x in I2 by A5, XBOOLE_0:def_4;
then x in Lin I2 by RUSUB_3:2;
then x in UNITSTR(# the carrier of W2, the ZeroF of W2, the addF of W2, the Mult of W2, the scalar of W2 #) by RUSUB_3:def_2;
then x in the carrier of W2 by STRUCT_0:def_5;
then x in the carrier of W1 /\ the carrier of W2 by A7, XBOOLE_0:def_4;
then x in the carrier of (W1 /\ W2) by RUSUB_2:def_2;
then x in UNITSTR(# the carrier of (W1 /\ W2), the ZeroF of (W1 /\ W2), the addF of (W1 /\ W2), the Mult of (W1 /\ W2), the scalar of (W1 /\ W2) #) by STRUCT_0:def_5;
then A12: x in Lin I by A1, RUSUB_3:def_2;
Ix \ {x} = I \ {x} by XBOOLE_1:40
.= I by A6, Lm2 ;
then not x9 in Lin I9 by A10, A11, RLVECT_3:5, RUSUB_3:25;
hence contradiction by A12, RUSUB_3:28; ::_thesis: verum
end;
set A = I1 \/ I2;
now__::_thesis:_for_v_being_set_st_v_in_I1_\/_I2_holds_
v_in_the_carrier_of_(W1_+_W2)
let v be set ; ::_thesis: ( v in I1 \/ I2 implies v in the carrier of (W1 + W2) )
A13: ( the carrier of W1 c= the carrier of V & the carrier of W2 c= the carrier of V ) by RUSUB_1:def_1;
assume v in I1 \/ I2 ; ::_thesis: v in the carrier of (W1 + W2)
then A14: ( v in I1 or v in I2 ) by XBOOLE_0:def_3;
then ( v in the carrier of W1 or v in the carrier of W2 ) ;
then reconsider v9 = v as VECTOR of V by A13;
( v9 in W1 or v9 in W2 ) by A14, STRUCT_0:def_5;
then v9 in W1 + W2 by RUSUB_2:2;
hence v in the carrier of (W1 + W2) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider A = I1 \/ I2 as finite Subset of (W1 + W2) by TARSKI:def_3;
I c= I1 /\ I2 by A3, A2, XBOOLE_1:19;
then I = I1 /\ I2 by A4, XBOOLE_0:def_10;
then A15: card A = ((card I1) + (card I2)) - (card I) by CARD_2:45;
for L being Linear_Combination of A st Sum L = 0. (W1 + W2) holds
Carrier L = {}
proof
( W1 is Subspace of W1 + W2 & I1 is linearly-independent ) by RUSUB_2:7, RUSUB_3:def_2;
then reconsider I19 = I1 as linearly-independent Subset of (W1 + W2) by RUSUB_3:22;
reconsider W29 = W2 as Subspace of W1 + W2 by RUSUB_2:7;
reconsider W19 = W1 as Subspace of W1 + W2 by RUSUB_2:7;
let L be Linear_Combination of A; ::_thesis: ( Sum L = 0. (W1 + W2) implies Carrier L = {} )
assume A16: Sum L = 0. (W1 + W2) ; ::_thesis: Carrier L = {}
A17: I1 misses (Carrier L) \ I1 by XBOOLE_1:79;
set B = (Carrier L) /\ I1;
consider F being FinSequence of the carrier of (W1 + W2) such that
A18: F is one-to-one and
A19: rng F = Carrier L and
A20: Sum L = Sum (L (#) F) by RLVECT_2:def_8;
reconsider B = (Carrier L) /\ I1 as Subset of (rng F) by A19, XBOOLE_1:17;
reconsider F1 = F - (B `), F2 = F - B as FinSequence of the carrier of (W1 + W2) by FINSEQ_3:86;
consider L1 being Linear_Combination of W1 + W2 such that
A21: Carrier L1 = (rng F1) /\ (Carrier L) and
A22: L1 (#) F1 = L (#) F1 by RLVECT_5:7;
F1 is one-to-one by A18, FINSEQ_3:87;
then A23: Sum (L (#) F1) = Sum L1 by A21, A22, RLVECT_5:6, XBOOLE_1:17;
rng F c= rng F ;
then reconsider X = rng F as Subset of (rng F) ;
consider L2 being Linear_Combination of W1 + W2 such that
A24: Carrier L2 = (rng F2) /\ (Carrier L) and
A25: L2 (#) F2 = L (#) F2 by RLVECT_5:7;
F2 is one-to-one by A18, FINSEQ_3:87;
then A26: Sum (L (#) F2) = Sum L2 by A24, A25, RLVECT_5:6, XBOOLE_1:17;
X \ (B `) = X /\ ((B `) `) by SUBSET_1:13
.= B by XBOOLE_1:28 ;
then rng F1 = B by FINSEQ_3:65;
then A27: Carrier L1 = I1 /\ ((Carrier L) /\ (Carrier L)) by A21, XBOOLE_1:16
.= (Carrier L) /\ I1 ;
then consider K1 being Linear_Combination of W19 such that
Carrier K1 = Carrier L1 and
A28: Sum K1 = Sum L1 by RUSUB_3:20;
rng F2 = (Carrier L) \ ((Carrier L) /\ I1) by A19, FINSEQ_3:65
.= (Carrier L) \ I1 by XBOOLE_1:47 ;
then A29: Carrier L2 = (Carrier L) \ I1 by A24, XBOOLE_1:28, XBOOLE_1:36;
then (Carrier L1) /\ (Carrier L2) = (Carrier L) /\ (I1 /\ ((Carrier L) \ I1)) by A27, XBOOLE_1:16
.= (Carrier L) /\ {} by A17, XBOOLE_0:def_7
.= {} ;
then A30: Carrier L1 misses Carrier L2 by XBOOLE_0:def_7;
A31: Carrier L c= I1 \/ I2 by RLVECT_2:def_6;
then A32: Carrier L2 c= I2 by A29, XBOOLE_1:43;
Carrier L2 c= I2 by A31, A29, XBOOLE_1:43;
then consider K2 being Linear_Combination of W29 such that
Carrier K2 = Carrier L2 and
A33: Sum K2 = Sum L2 by RUSUB_3:20, XBOOLE_1:1;
A34: Sum K1 in W1 by STRUCT_0:def_5;
ex P being Permutation of (dom F) st (F - (B `)) ^ (F - B) = F * P by FINSEQ_3:115;
then A35: 0. (W1 + W2) = Sum (L (#) (F1 ^ F2)) by A16, A20, RLVECT_5:4
.= Sum ((L (#) F1) ^ (L (#) F2)) by RLVECT_3:34
.= (Sum L1) + (Sum L2) by A23, A26, RLVECT_1:41 ;
then Sum L1 = - (Sum L2) by RLVECT_1:def_10
.= - (Sum K2) by A33, RUSUB_1:9 ;
then Sum K1 in W2 by A28, STRUCT_0:def_5;
then Sum K1 in W1 /\ W2 by A34, RUSUB_2:3;
then Sum K1 in Lin I by A1, RUSUB_3:def_2;
then consider KI being Linear_Combination of I such that
A36: Sum K1 = Sum KI by RUSUB_3:1;
A37: Carrier L = (Carrier L1) \/ (Carrier L2) by A27, A29, XBOOLE_1:51;
A38: now__::_thesis:_Carrier_L_c=_Carrier_(L1_+_L2)
assume not Carrier L c= Carrier (L1 + L2) ; ::_thesis: contradiction
then consider x being set such that
A39: x in Carrier L and
A40: not x in Carrier (L1 + L2) by TARSKI:def_3;
reconsider x = x as VECTOR of (W1 + W2) by A39;
A41: 0 = (L1 + L2) . x by A40, RLVECT_2:19
.= (L1 . x) + (L2 . x) by RLVECT_2:def_10 ;
percases ( x in Carrier L1 or x in Carrier L2 ) by A37, A39, XBOOLE_0:def_3;
supposeA42: x in Carrier L1 ; ::_thesis: contradiction
then not x in Carrier L2 by A30, XBOOLE_0:3;
then A43: L2 . x = 0 by RLVECT_2:19;
ex v being VECTOR of (W1 + W2) st
( x = v & L1 . v <> 0 ) by A42, RLVECT_5:3;
hence contradiction by A41, A43; ::_thesis: verum
end;
supposeA44: x in Carrier L2 ; ::_thesis: contradiction
then not x in Carrier L1 by A30, XBOOLE_0:3;
then A45: L1 . x = 0 by RLVECT_2:19;
ex v being VECTOR of (W1 + W2) st
( x = v & L2 . v <> 0 ) by A44, RLVECT_5:3;
hence contradiction by A41, A45; ::_thesis: verum
end;
end;
end;
A46: I \/ I2 = I2 by A2, XBOOLE_1:12;
A47: I2 is linearly-independent by RUSUB_3:def_2;
A48: Carrier L1 c= I1 by A27, XBOOLE_1:17;
W1 /\ W2 is Subspace of W1 + W2 by RUSUB_2:22;
then consider LI being Linear_Combination of W1 + W2 such that
A49: Carrier LI = Carrier KI and
A50: Sum LI = Sum KI by RUSUB_3:19;
Carrier LI c= I by A49, RLVECT_2:def_6;
then Carrier LI c= I19 by A3, XBOOLE_1:1;
then A51: LI = L1 by A48, A28, A36, A50, RLVECT_5:1;
Carrier LI c= I by A49, RLVECT_2:def_6;
then ( Carrier (LI + L2) c= (Carrier LI) \/ (Carrier L2) & (Carrier LI) \/ (Carrier L2) c= I2 ) by A46, A32, RLVECT_2:37, XBOOLE_1:13;
then A52: Carrier (LI + L2) c= I2 by XBOOLE_1:1;
W2 is Subspace of W1 + W2 by RUSUB_2:7;
then consider K being Linear_Combination of W2 such that
A53: Carrier K = Carrier (LI + L2) and
A54: Sum K = Sum (LI + L2) by A52, RUSUB_3:20, XBOOLE_1:1;
reconsider K = K as Linear_Combination of I2 by A52, A53, RLVECT_2:def_6;
0. W2 = (Sum LI) + (Sum L2) by A28, A35, A36, A50, RUSUB_1:5
.= Sum K by A54, RLVECT_3:1 ;
then {} = Carrier (L1 + L2) by A53, A51, A47, RLVECT_3:def_1;
hence Carrier L = {} by A38; ::_thesis: verum
end;
then A55: A is linearly-independent by RLVECT_3:def_1;
the carrier of (W1 + W2) c= the carrier of V by RUSUB_1:def_1;
then reconsider A9 = A as Subset of V by XBOOLE_1:1;
A56: card I2 = dim W2 by Def2;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(W1_+_W2)_holds_
x_in_the_carrier_of_(Lin_A9)
let x be set ; ::_thesis: ( x in the carrier of (W1 + W2) implies x in the carrier of (Lin A9) )
assume x in the carrier of (W1 + W2) ; ::_thesis: x in the carrier of (Lin A9)
then x in W1 + W2 by STRUCT_0:def_5;
then consider w1, w2 being VECTOR of V such that
A57: w1 in W1 and
A58: w2 in W2 and
A59: x = w1 + w2 by RUSUB_2:1;
reconsider w1 = w1 as VECTOR of W1 by A57, STRUCT_0:def_5;
w1 in Lin I1 by RUSUB_3:21;
then consider K1 being Linear_Combination of I1 such that
A60: w1 = Sum K1 by RUSUB_3:1;
reconsider w2 = w2 as VECTOR of W2 by A58, STRUCT_0:def_5;
w2 in Lin I2 by RUSUB_3:21;
then consider K2 being Linear_Combination of I2 such that
A61: w2 = Sum K2 by RUSUB_3:1;
consider L2 being Linear_Combination of V such that
A62: Carrier L2 = Carrier K2 and
A63: Sum L2 = Sum K2 by RUSUB_3:19;
A64: Carrier L2 c= I2 by A62, RLVECT_2:def_6;
consider L1 being Linear_Combination of V such that
A65: Carrier L1 = Carrier K1 and
A66: Sum L1 = Sum K1 by RUSUB_3:19;
set L = L1 + L2;
Carrier L1 c= I1 by A65, RLVECT_2:def_6;
then ( Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) & (Carrier L1) \/ (Carrier L2) c= I1 \/ I2 ) by A64, RLVECT_2:37, XBOOLE_1:13;
then Carrier (L1 + L2) c= I1 \/ I2 by XBOOLE_1:1;
then reconsider L = L1 + L2 as Linear_Combination of A9 by RLVECT_2:def_6;
x = Sum L by A59, A60, A66, A61, A63, RLVECT_3:1;
then x in Lin A9 by RUSUB_3:1;
hence x in the carrier of (Lin A9) by STRUCT_0:def_5; ::_thesis: verum
end;
then the carrier of (W1 + W2) c= the carrier of (Lin A9) by TARSKI:def_3;
then ( Lin A9 = Lin A & W1 + W2 is Subspace of Lin A9 ) by RUSUB_1:22, RUSUB_3:28;
then Lin A = W1 + W2 by RUSUB_1:20;
then A67: A is Basis of W1 + W2 by A55, RUSUB_3:def_2;
card I = dim (W1 /\ W2) by A1, Def2;
then (dim (W1 + W2)) + (dim (W1 /\ W2)) = (((card I1) + (card I2)) + (- (card I))) + (card I) by A15, A67, Def2
.= (dim W1) + (dim W2) by A56, Def2 ;
hence (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2) ; ::_thesis: verum
end;
theorem :: RUSUB_4:16
for V being finite-dimensional RealUnitarySpace
for W1, W2 being Subspace of V holds dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V)
proof
let V be finite-dimensional RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V)
let W1, W2 be Subspace of V; ::_thesis: dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V)
A1: ( dim (W1 + W2) <= dim V & (dim V) + ((dim (W1 /\ W2)) - (dim V)) = dim (W1 /\ W2) ) by Th8;
((dim W1) + (dim W2)) - (dim V) = ((dim (W1 + W2)) + (dim (W1 /\ W2))) - (dim V) by Th15
.= (dim (W1 + W2)) + ((dim (W1 /\ W2)) - (dim V)) ;
hence dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V) by A1, XREAL_1:6; ::_thesis: verum
end;
theorem :: RUSUB_4:17
for V being finite-dimensional RealUnitarySpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
dim V = (dim W1) + (dim W2)
proof
let V be finite-dimensional RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
dim V = (dim W1) + (dim W2)
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies dim V = (dim W1) + (dim W2) )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: dim V = (dim W1) + (dim W2)
then A2: UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) = W1 + W2 by RUSUB_2:def_4;
W1 /\ W2 = (0). V by A1, RUSUB_2:def_4;
then (Omega). (W1 /\ W2) = (0). V by RUSUB_1:def_3
.= (0). (W1 /\ W2) by RUSUB_1:30 ;
then dim (W1 /\ W2) = 0 by Th12;
then (dim W1) + (dim W2) = (dim (W1 + W2)) + 0 by Th15
.= dim ((Omega). V) by A2, RUSUB_1:def_3
.= dim V by Th10 ;
hence dim V = (dim W1) + (dim W2) ; ::_thesis: verum
end;
begin
Lm3: for V being finite-dimensional RealUnitarySpace
for n being Element of NAT st n <= dim V holds
ex W being strict Subspace of V st dim W = n
proof
let V be finite-dimensional RealUnitarySpace; ::_thesis: for n being Element of NAT st n <= dim V holds
ex W being strict Subspace of V st dim W = n
let n be Element of NAT ; ::_thesis: ( n <= dim V implies ex W being strict Subspace of V st dim W = n )
consider I being finite Subset of V such that
A1: I is Basis of V by Def1;
assume n <= dim V ; ::_thesis: ex W being strict Subspace of V st dim W = n
then n <= card I by A1, Def2;
then consider A being finite Subset of I such that
A2: card A = n by FINSEQ_4:72;
reconsider A = A as Subset of V by XBOOLE_1:1;
reconsider W = Lin A as strict finite-dimensional Subspace of V ;
I is linearly-independent by A1, RUSUB_3:def_2;
then dim W = n by A2, Th9, RLVECT_3:5;
hence ex W being strict Subspace of V st dim W = n ; ::_thesis: verum
end;
theorem :: RUSUB_4:18
for V being finite-dimensional RealUnitarySpace
for W being Subspace of V
for n being Element of NAT holds
( n <= dim V iff ex W being strict Subspace of V st dim W = n ) by Lm3, Th8;
definition
let V be finite-dimensional RealUnitarySpace;
let n be Element of NAT ;
funcn Subspaces_of V -> set means :Def3: :: RUSUB_4:def 3
for x being set holds
( x in it iff ex W being strict Subspace of V st
( W = x & dim W = n ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex W being strict Subspace of V st
( W = x & dim W = n ) )
proof
set S = { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ;
take { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ; ::_thesis: for x being set holds
( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st
( W = x & dim W = n ) )
for x being set holds
( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st
( W = x & dim W = n ) )
proof
let x be set ; ::_thesis: ( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st
( W = x & dim W = n ) )
hereby ::_thesis: ( ex W being strict Subspace of V st
( W = x & dim W = n ) implies x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } )
assume x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ; ::_thesis: ex W being strict Subspace of V st
( W = x & dim W = n )
then A1: ex A being Subset of V st
( x = Lin A & A is linearly-independent & card A = n ) ;
then reconsider W = x as strict Subspace of V ;
dim W = n by A1, Th9;
hence ex W being strict Subspace of V st
( W = x & dim W = n ) ; ::_thesis: verum
end;
given W being strict Subspace of V such that A2: W = x and
A3: dim W = n ; ::_thesis: x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) }
consider A being finite Subset of W such that
A4: A is Basis of W by Def1;
reconsider A = A as Subset of W ;
A is linearly-independent by A4, RUSUB_3:def_2;
then reconsider B = A as linearly-independent Subset of V by RUSUB_3:22;
A5: x = Lin A by A2, A4, RUSUB_3:def_2
.= Lin B by RUSUB_3:28 ;
then card B = n by A2, A3, Th9;
hence x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } by A5; ::_thesis: verum
end;
hence for x being set holds
( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) ) & ( for x being set holds
( x in b2 iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ex W being strict Subspace of V st
( W = $1 & dim W = n );
for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3();
hence for b1, b2 being set st ( for x being set holds
( x in b1 iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) ) & ( for x being set holds
( x in b2 iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) ) holds
b1 = b2 ; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Subspaces_of RUSUB_4:def_3_:_
for V being finite-dimensional RealUnitarySpace
for n being Element of NAT
for b3 being set holds
( b3 = n Subspaces_of V iff for x being set holds
( x in b3 iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) );
theorem :: RUSUB_4:19
for V being finite-dimensional RealUnitarySpace
for n being Element of NAT st n <= dim V holds
not n Subspaces_of V is empty
proof
let V be finite-dimensional RealUnitarySpace; ::_thesis: for n being Element of NAT st n <= dim V holds
not n Subspaces_of V is empty
let n be Element of NAT ; ::_thesis: ( n <= dim V implies not n Subspaces_of V is empty )
assume n <= dim V ; ::_thesis: not n Subspaces_of V is empty
then ex W being strict Subspace of V st dim W = n by Lm3;
hence not n Subspaces_of V is empty by Def3; ::_thesis: verum
end;
theorem :: RUSUB_4:20
for V being finite-dimensional RealUnitarySpace
for n being Element of NAT st dim V < n holds
n Subspaces_of V = {}
proof
let V be finite-dimensional RealUnitarySpace; ::_thesis: for n being Element of NAT st dim V < n holds
n Subspaces_of V = {}
let n be Element of NAT ; ::_thesis: ( dim V < n implies n Subspaces_of V = {} )
assume that
A1: dim V < n and
A2: n Subspaces_of V <> {} ; ::_thesis: contradiction
consider x being set such that
A3: x in n Subspaces_of V by A2, XBOOLE_0:def_1;
ex W being strict Subspace of V st
( W = x & dim W = n ) by A3, Def3;
hence contradiction by A1, Th8; ::_thesis: verum
end;
theorem :: RUSUB_4:21
for V being finite-dimensional RealUnitarySpace
for W being Subspace of V
for n being Element of NAT holds n Subspaces_of W c= n Subspaces_of V
proof
let V be finite-dimensional RealUnitarySpace; ::_thesis: for W being Subspace of V
for n being Element of NAT holds n Subspaces_of W c= n Subspaces_of V
let W be Subspace of V; ::_thesis: for n being Element of NAT holds n Subspaces_of W c= n Subspaces_of V
let n be Element of NAT ; ::_thesis: n Subspaces_of W c= n Subspaces_of V
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in n Subspaces_of W or x in n Subspaces_of V )
assume x in n Subspaces_of W ; ::_thesis: x in n Subspaces_of V
then consider W1 being strict Subspace of W such that
A1: W1 = x and
A2: dim W1 = n by Def3;
reconsider W1 = W1 as strict Subspace of V by RUSUB_1:21;
W1 in n Subspaces_of V by A2, Def3;
hence x in n Subspaces_of V by A1; ::_thesis: verum
end;
begin
definition
let V be non empty RLSStruct ;
let S be Subset of V;
attrS is Affine means :Def4: :: RUSUB_4:def 4
for x, y being VECTOR of V
for a being Real st x in S & y in S holds
((1 - a) * x) + (a * y) in S;
end;
:: deftheorem Def4 defines Affine RUSUB_4:def_4_:_
for V being non empty RLSStruct
for S being Subset of V holds
( S is Affine iff for x, y being VECTOR of V
for a being Real st x in S & y in S holds
((1 - a) * x) + (a * y) in S );
theorem Th22: :: RUSUB_4:22
for V being non empty RLSStruct holds
( [#] V is Affine & {} V is Affine )
proof
let V be non empty RLSStruct ; ::_thesis: ( [#] V is Affine & {} V is Affine )
for x, y being VECTOR of V
for a being Real st x in [#] V & y in [#] V holds
((1 - a) * x) + (a * y) in [#] V ;
hence [#] V is Affine by Def4; ::_thesis: {} V is Affine
for x, y being VECTOR of V
for a being Real st x in {} V & y in {} V holds
((1 - a) * x) + (a * y) in {} V ;
hence {} V is Affine by Def4; ::_thesis: verum
end;
theorem :: RUSUB_4:23
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for v being VECTOR of V holds {v} is Affine
proof
let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for v being VECTOR of V holds {v} is Affine
let v be VECTOR of V; ::_thesis: {v} is Affine
for x, y being VECTOR of V
for a being Real st x in {v} & y in {v} holds
((1 - a) * x) + (a * y) in {v}
proof
let x, y be VECTOR of V; ::_thesis: for a being Real st x in {v} & y in {v} holds
((1 - a) * x) + (a * y) in {v}
let a be Real; ::_thesis: ( x in {v} & y in {v} implies ((1 - a) * x) + (a * y) in {v} )
assume ( x in {v} & y in {v} ) ; ::_thesis: ((1 - a) * x) + (a * y) in {v}
then ( x = v & y = v ) by TARSKI:def_1;
then ((1 - a) * x) + (a * y) = ((1 - a) + a) * v by RLVECT_1:def_6
.= v by RLVECT_1:def_8 ;
hence ((1 - a) * x) + (a * y) in {v} by TARSKI:def_1; ::_thesis: verum
end;
hence {v} is Affine by Def4; ::_thesis: verum
end;
registration
let V be non empty RLSStruct ;
cluster non empty Affine for Element of K11( the carrier of V);
existence
ex b1 being Subset of V st
( not b1 is empty & b1 is Affine )
proof
take [#] V ; ::_thesis: ( not [#] V is empty & [#] V is Affine )
thus ( not [#] V is empty & [#] V is Affine ) by Th22; ::_thesis: verum
end;
cluster empty Affine for Element of K11( the carrier of V);
existence
ex b1 being Subset of V st
( b1 is empty & b1 is Affine )
proof
take {} V ; ::_thesis: ( {} V is empty & {} V is Affine )
thus ( {} V is empty & {} V is Affine ) by Th22; ::_thesis: verum
end;
end;
definition
let V be RealLinearSpace;
let W be Subspace of V;
func Up W -> non empty Subset of V equals :: RUSUB_4:def 5
the carrier of W;
coherence
the carrier of W is non empty Subset of V by RLSUB_1:def_2;
end;
:: deftheorem defines Up RUSUB_4:def_5_:_
for V being RealLinearSpace
for W being Subspace of V holds Up W = the carrier of W;
definition
let V be RealUnitarySpace;
let W be Subspace of V;
func Up W -> non empty Subset of V equals :: RUSUB_4:def 6
the carrier of W;
coherence
the carrier of W is non empty Subset of V by RUSUB_1:def_1;
end;
:: deftheorem defines Up RUSUB_4:def_6_:_
for V being RealUnitarySpace
for W being Subspace of V holds Up W = the carrier of W;
theorem :: RUSUB_4:24
for V being RealLinearSpace
for W being Subspace of V holds
( Up W is Affine & 0. V in the carrier of W )
proof
let V be RealLinearSpace; ::_thesis: for W being Subspace of V holds
( Up W is Affine & 0. V in the carrier of W )
let W be Subspace of V; ::_thesis: ( Up W is Affine & 0. V in the carrier of W )
for x, y being VECTOR of V
for a being Real st x in Up W & y in Up W holds
((1 - a) * x) + (a * y) in Up W
proof
let x, y be VECTOR of V; ::_thesis: for a being Real st x in Up W & y in Up W holds
((1 - a) * x) + (a * y) in Up W
let a be Real; ::_thesis: ( x in Up W & y in Up W implies ((1 - a) * x) + (a * y) in Up W )
assume that
A1: x in Up W and
A2: y in Up W ; ::_thesis: ((1 - a) * x) + (a * y) in Up W
y in W by A2, STRUCT_0:def_5;
then A3: a * y in W by RLSUB_1:21;
x in W by A1, STRUCT_0:def_5;
then (1 - a) * x in W by RLSUB_1:21;
then ((1 - a) * x) + (a * y) in W by A3, RLSUB_1:20;
hence ((1 - a) * x) + (a * y) in Up W by STRUCT_0:def_5; ::_thesis: verum
end;
hence Up W is Affine by Def4; ::_thesis: 0. V in the carrier of W
0. V in W by RLSUB_1:17;
hence 0. V in the carrier of W by STRUCT_0:def_5; ::_thesis: verum
end;
theorem Th25: :: RUSUB_4:25
for V being RealLinearSpace
for A being Affine Subset of V st 0. V in A holds
for x being VECTOR of V
for a being Real st x in A holds
a * x in A
proof
let V be RealLinearSpace; ::_thesis: for A being Affine Subset of V st 0. V in A holds
for x being VECTOR of V
for a being Real st x in A holds
a * x in A
let A be Affine Subset of V; ::_thesis: ( 0. V in A implies for x being VECTOR of V
for a being Real st x in A holds
a * x in A )
assume A1: 0. V in A ; ::_thesis: for x being VECTOR of V
for a being Real st x in A holds
a * x in A
for x being VECTOR of V
for a being Real st x in A holds
a * x in A
proof
let x be VECTOR of V; ::_thesis: for a being Real st x in A holds
a * x in A
let a be Real; ::_thesis: ( x in A implies a * x in A )
assume x in A ; ::_thesis: a * x in A
then ((1 - a) * (0. V)) + (a * x) in A by A1, Def4;
then (0. V) + (a * x) in A by RLVECT_1:10;
hence a * x in A by RLVECT_1:4; ::_thesis: verum
end;
hence for x being VECTOR of V
for a being Real st x in A holds
a * x in A ; ::_thesis: verum
end;
definition
let V be non empty RLSStruct ;
let S be non empty Subset of V;
attrS is Subspace-like means :Def7: :: RUSUB_4:def 7
( 0. V in S & ( for x, y being Element of V
for a being Real st x in S & y in S holds
( x + y in S & a * x in S ) ) );
end;
:: deftheorem Def7 defines Subspace-like RUSUB_4:def_7_:_
for V being non empty RLSStruct
for S being non empty Subset of V holds
( S is Subspace-like iff ( 0. V in S & ( for x, y being Element of V
for a being Real st x in S & y in S holds
( x + y in S & a * x in S ) ) ) );
theorem Th26: :: RUSUB_4:26
for V being RealLinearSpace
for A being non empty Affine Subset of V st 0. V in A holds
( A is Subspace-like & A = the carrier of (Lin A) )
proof
let V be RealLinearSpace; ::_thesis: for A being non empty Affine Subset of V st 0. V in A holds
( A is Subspace-like & A = the carrier of (Lin A) )
let A be non empty Affine Subset of V; ::_thesis: ( 0. V in A implies ( A is Subspace-like & A = the carrier of (Lin A) ) )
assume A1: 0. V in A ; ::_thesis: ( A is Subspace-like & A = the carrier of (Lin A) )
A2: for x, y being Element of V
for a being Real st x in A & y in A holds
( x + y in A & a * x in A )
proof
let x, y be Element of V; ::_thesis: for a being Real st x in A & y in A holds
( x + y in A & a * x in A )
let a be Real; ::_thesis: ( x in A & y in A implies ( x + y in A & a * x in A ) )
assume that
A3: x in A and
A4: y in A ; ::_thesis: ( x + y in A & a * x in A )
reconsider x = x, y = y as VECTOR of V ;
A5: 2 * (((1 - (1 / 2)) * x) + ((1 / 2) * y)) = (2 * ((1 - (1 / 2)) * x)) + (2 * ((1 / 2) * y)) by RLVECT_1:def_5
.= ((2 * (1 - (1 / 2))) * x) + (2 * ((1 / 2) * y)) by RLVECT_1:def_7
.= ((2 - 1) * x) + ((2 * (1 / 2)) * y) by RLVECT_1:def_7
.= x + (1 * y) by RLVECT_1:def_8
.= x + y by RLVECT_1:def_8 ;
((1 - (1 / 2)) * x) + ((1 / 2) * y) in A by A3, A4, Def4;
hence ( x + y in A & a * x in A ) by A1, A3, A5, Th25; ::_thesis: verum
end;
hence A is Subspace-like by A1, Def7; ::_thesis: A = the carrier of (Lin A)
for x being set st x in the carrier of (Lin A) holds
x in A
proof
let x be set ; ::_thesis: ( x in the carrier of (Lin A) implies x in A )
assume x in the carrier of (Lin A) ; ::_thesis: x in A
then x in Lin A by STRUCT_0:def_5;
then A6: ex l being Linear_Combination of A st x = Sum l by RLVECT_3:14;
( ( for v, u being VECTOR of V st v in A & u in A holds
v + u in A ) & ( for a being Real
for v being VECTOR of V st v in A holds
a * v in A ) ) by A2;
then A is linearly-closed by RLSUB_1:def_1;
hence x in A by A6, RLVECT_2:29; ::_thesis: verum
end;
then A7: the carrier of (Lin A) c= A by TARSKI:def_3;
for x being set st x in A holds
x in the carrier of (Lin A)
proof
let x be set ; ::_thesis: ( x in A implies x in the carrier of (Lin A) )
assume x in A ; ::_thesis: x in the carrier of (Lin A)
then x in Lin A by RLVECT_3:15;
hence x in the carrier of (Lin A) by STRUCT_0:def_5; ::_thesis: verum
end;
then A c= the carrier of (Lin A) by TARSKI:def_3;
hence A = the carrier of (Lin A) by A7, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: RUSUB_4:27
for V being RealLinearSpace
for W being Subspace of V holds Up W is Subspace-like
proof
let V be RealLinearSpace; ::_thesis: for W being Subspace of V holds Up W is Subspace-like
let W be Subspace of V; ::_thesis: Up W is Subspace-like
0. V in W by RLSUB_1:17;
hence 0. V in Up W by STRUCT_0:def_5; :: according to RUSUB_4:def_7 ::_thesis: for x, y being Element of V
for a being Real st x in Up W & y in Up W holds
( x + y in Up W & a * x in Up W )
thus for x, y being Element of V
for a being Real st x in Up W & y in Up W holds
( x + y in Up W & a * x in Up W ) ::_thesis: verum
proof
let x, y be Element of V; ::_thesis: for a being Real st x in Up W & y in Up W holds
( x + y in Up W & a * x in Up W )
let a be Real; ::_thesis: ( x in Up W & y in Up W implies ( x + y in Up W & a * x in Up W ) )
assume that
A1: x in Up W and
A2: y in Up W ; ::_thesis: ( x + y in Up W & a * x in Up W )
reconsider x = x, y = y as Element of V ;
A3: x in W by A1, STRUCT_0:def_5;
then A4: a * x in W by RLSUB_1:21;
y in W by A2, STRUCT_0:def_5;
then x + y in W by A3, RLSUB_1:20;
hence ( x + y in Up W & a * x in Up W ) by A4, STRUCT_0:def_5; ::_thesis: verum
end;
end;
theorem :: RUSUB_4:28
for V being RealUnitarySpace
for A being non empty Affine Subset of V st 0. V in A holds
A = the carrier of (Lin A)
proof
let V be RealUnitarySpace; ::_thesis: for A being non empty Affine Subset of V st 0. V in A holds
A = the carrier of (Lin A)
let A be non empty Affine Subset of V; ::_thesis: ( 0. V in A implies A = the carrier of (Lin A) )
assume 0. V in A ; ::_thesis: A = the carrier of (Lin A)
then A1: A is Subspace-like by Th26;
for x being set st x in the carrier of (Lin A) holds
x in A
proof
let x be set ; ::_thesis: ( x in the carrier of (Lin A) implies x in A )
assume x in the carrier of (Lin A) ; ::_thesis: x in A
then x in Lin A by STRUCT_0:def_5;
then A2: ex l being Linear_Combination of A st x = Sum l by RUSUB_3:1;
( ( for v, u being VECTOR of V st v in A & u in A holds
v + u in A ) & ( for a being Real
for v being VECTOR of V st v in A holds
a * v in A ) ) by A1, Def7;
then A is linearly-closed by RLSUB_1:def_1;
hence x in A by A2, RLVECT_2:29; ::_thesis: verum
end;
then A3: the carrier of (Lin A) c= A by TARSKI:def_3;
for x being set st x in A holds
x in the carrier of (Lin A)
proof
let x be set ; ::_thesis: ( x in A implies x in the carrier of (Lin A) )
assume x in A ; ::_thesis: x in the carrier of (Lin A)
then x in Lin A by RUSUB_3:2;
hence x in the carrier of (Lin A) by STRUCT_0:def_5; ::_thesis: verum
end;
then A c= the carrier of (Lin A) by TARSKI:def_3;
hence A = the carrier of (Lin A) by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: RUSUB_4:29
for V being RealUnitarySpace
for W being Subspace of V holds Up W is Subspace-like
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V holds Up W is Subspace-like
let W be Subspace of V; ::_thesis: Up W is Subspace-like
0. V in W by RUSUB_1:11;
hence 0. V in Up W by STRUCT_0:def_5; :: according to RUSUB_4:def_7 ::_thesis: for x, y being Element of V
for a being Real st x in Up W & y in Up W holds
( x + y in Up W & a * x in Up W )
thus for x, y being Element of V
for a being Real st x in Up W & y in Up W holds
( x + y in Up W & a * x in Up W ) ::_thesis: verum
proof
let x, y be Element of V; ::_thesis: for a being Real st x in Up W & y in Up W holds
( x + y in Up W & a * x in Up W )
let a be Real; ::_thesis: ( x in Up W & y in Up W implies ( x + y in Up W & a * x in Up W ) )
assume that
A1: x in Up W and
A2: y in Up W ; ::_thesis: ( x + y in Up W & a * x in Up W )
reconsider x = x, y = y as Element of V ;
A3: x in W by A1, STRUCT_0:def_5;
then A4: a * x in W by RUSUB_1:15;
y in W by A2, STRUCT_0:def_5;
then x + y in W by A3, RUSUB_1:14;
hence ( x + y in Up W & a * x in Up W ) by A4, STRUCT_0:def_5; ::_thesis: verum
end;
end;
definition
let V be non empty addLoopStr ;
let M be Subset of V;
let v be Element of V;
funcv + M -> Subset of V equals :: RUSUB_4:def 8
{ (v + u) where u is Element of V : u in M } ;
coherence
{ (v + u) where u is Element of V : u in M } is Subset of V
proof
set Y = { (v + u) where u is Element of V : u in M } ;
defpred S1[ set ] means ex u being Element of V st
( $1 = v + u & u in M );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in the carrier of V & S1[x] ) ) from XBOOLE_0:sch_1();
X c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in the carrier of V )
assume x in X ; ::_thesis: x in the carrier of V
hence x in the carrier of V by A1; ::_thesis: verum
end;
then reconsider X = X as Subset of V ;
reconsider X = X as Subset of V ;
A2: { (v + u) where u is Element of V : u in M } c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v + u) where u is Element of V : u in M } or x in X )
assume x in { (v + u) where u is Element of V : u in M } ; ::_thesis: x in X
then ex u being Element of V st
( x = v + u & u in M ) ;
hence x in X by A1; ::_thesis: verum
end;
X c= { (v + u) where u is Element of V : u in M }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in { (v + u) where u is Element of V : u in M } )
assume x in X ; ::_thesis: x in { (v + u) where u is Element of V : u in M }
then ex u being Element of V st
( x = v + u & u in M ) by A1;
hence x in { (v + u) where u is Element of V : u in M } ; ::_thesis: verum
end;
hence { (v + u) where u is Element of V : u in M } is Subset of V by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem defines + RUSUB_4:def_8_:_
for V being non empty addLoopStr
for M being Subset of V
for v being Element of V holds v + M = { (v + u) where u is Element of V : u in M } ;
theorem :: RUSUB_4:30
for V being RealLinearSpace
for W being strict Subspace of V
for M being Subset of V
for v being VECTOR of V st Up W = M holds
v + W = v + M
proof
let V be RealLinearSpace; ::_thesis: for W being strict Subspace of V
for M being Subset of V
for v being VECTOR of V st Up W = M holds
v + W = v + M
let W be strict Subspace of V; ::_thesis: for M being Subset of V
for v being VECTOR of V st Up W = M holds
v + W = v + M
let M be Subset of V; ::_thesis: for v being VECTOR of V st Up W = M holds
v + W = v + M
let v be VECTOR of V; ::_thesis: ( Up W = M implies v + W = v + M )
assume A1: Up W = M ; ::_thesis: v + W = v + M
for x being set st x in v + M holds
x in v + W
proof
let x be set ; ::_thesis: ( x in v + M implies x in v + W )
assume x in v + M ; ::_thesis: x in v + W
then consider u being Element of V such that
A2: x = v + u and
A3: u in M ;
u in W by A1, A3, STRUCT_0:def_5;
then x in { (v + u9) where u9 is VECTOR of V : u9 in W } by A2;
hence x in v + W by RLSUB_1:def_5; ::_thesis: verum
end;
then A4: v + M c= v + W by TARSKI:def_3;
for x being set st x in v + W holds
x in v + M
proof
let x be set ; ::_thesis: ( x in v + W implies x in v + M )
assume x in v + W ; ::_thesis: x in v + M
then x in { (v + u) where u is VECTOR of V : u in W } by RLSUB_1:def_5;
then consider u being VECTOR of V such that
A5: x = v + u and
A6: u in W ;
u in M by A1, A6, STRUCT_0:def_5;
hence x in v + M by A5; ::_thesis: verum
end;
then v + W c= v + M by TARSKI:def_3;
hence v + W = v + M by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th31: :: RUSUB_4:31
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Affine Subset of V
for v being VECTOR of V holds v + M is Affine
proof
let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M being Affine Subset of V
for v being VECTOR of V holds v + M is Affine
let M be Affine Subset of V; ::_thesis: for v being VECTOR of V holds v + M is Affine
let v be VECTOR of V; ::_thesis: v + M is Affine
for x, y being VECTOR of V
for a being Real st x in v + M & y in v + M holds
((1 - a) * x) + (a * y) in v + M
proof
let x, y be VECTOR of V; ::_thesis: for a being Real st x in v + M & y in v + M holds
((1 - a) * x) + (a * y) in v + M
let a be Real; ::_thesis: ( x in v + M & y in v + M implies ((1 - a) * x) + (a * y) in v + M )
assume that
A1: x in v + M and
A2: y in v + M ; ::_thesis: ((1 - a) * x) + (a * y) in v + M
consider x9 being Element of V such that
A3: x = v + x9 and
A4: x9 in M by A1;
consider y9 being Element of V such that
A5: y = v + y9 and
A6: y9 in M by A2;
A7: ((1 - a) * x) + (a * y) = (((1 - a) * v) + ((1 - a) * x9)) + (a * (v + y9)) by A3, A5, RLVECT_1:def_5
.= (((1 - a) * v) + ((1 - a) * x9)) + ((a * v) + (a * y9)) by RLVECT_1:def_5
.= ((((1 - a) * v) + ((1 - a) * x9)) + (a * v)) + (a * y9) by RLVECT_1:def_3
.= (((1 - a) * x9) + (((1 - a) * v) + (a * v))) + (a * y9) by RLVECT_1:def_3
.= (((1 - a) * x9) + (((1 - a) + a) * v)) + (a * y9) by RLVECT_1:def_6
.= (((1 - a) * x9) + v) + (a * y9) by RLVECT_1:def_8
.= v + (((1 - a) * x9) + (a * y9)) by RLVECT_1:def_3 ;
((1 - a) * x9) + (a * y9) in M by A4, A6, Def4;
hence ((1 - a) * x) + (a * y) in v + M by A7; ::_thesis: verum
end;
hence v + M is Affine by Def4; ::_thesis: verum
end;
theorem :: RUSUB_4:32
for V being RealUnitarySpace
for W being strict Subspace of V
for M being Subset of V
for v being VECTOR of V st Up W = M holds
v + W = v + M
proof
let V be RealUnitarySpace; ::_thesis: for W being strict Subspace of V
for M being Subset of V
for v being VECTOR of V st Up W = M holds
v + W = v + M
let W be strict Subspace of V; ::_thesis: for M being Subset of V
for v being VECTOR of V st Up W = M holds
v + W = v + M
let M be Subset of V; ::_thesis: for v being VECTOR of V st Up W = M holds
v + W = v + M
let v be VECTOR of V; ::_thesis: ( Up W = M implies v + W = v + M )
assume A1: Up W = M ; ::_thesis: v + W = v + M
for x being set st x in v + M holds
x in v + W
proof
let x be set ; ::_thesis: ( x in v + M implies x in v + W )
assume x in v + M ; ::_thesis: x in v + W
then consider u being Element of V such that
A2: x = v + u and
A3: u in M ;
u in W by A1, A3, STRUCT_0:def_5;
then x in { (v + u9) where u9 is VECTOR of V : u9 in W } by A2;
hence x in v + W by RUSUB_1:def_4; ::_thesis: verum
end;
then A4: v + M c= v + W by TARSKI:def_3;
for x being set st x in v + W holds
x in v + M
proof
let x be set ; ::_thesis: ( x in v + W implies x in v + M )
assume x in v + W ; ::_thesis: x in v + M
then x in { (v + u) where u is VECTOR of V : u in W } by RUSUB_1:def_4;
then consider u being VECTOR of V such that
A5: x = v + u and
A6: u in W ;
u in M by A1, A6, STRUCT_0:def_5;
hence x in v + M by A5; ::_thesis: verum
end;
then v + W c= v + M by TARSKI:def_3;
hence v + W = v + M by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
definition
let V be non empty addLoopStr ;
let M, N be Subset of V;
funcM + N -> Subset of V equals :: RUSUB_4:def 9
{ (u + v) where u, v is Element of V : ( u in M & v in N ) } ;
coherence
{ (u + v) where u, v is Element of V : ( u in M & v in N ) } is Subset of V
proof
defpred S1[ set , set ] means ( $1 in M & $2 in N );
deffunc H1( Element of V, Element of V) -> Element of the carrier of V = $1 + $2;
{ H1(u,v) where u, v is Element of V : S1[u,v] } is Subset of V from DOMAIN_1:sch_9();
hence { (u + v) where u, v is Element of V : ( u in M & v in N ) } is Subset of V ; ::_thesis: verum
end;
end;
:: deftheorem defines + RUSUB_4:def_9_:_
for V being non empty addLoopStr
for M, N being Subset of V holds M + N = { (u + v) where u, v is Element of V : ( u in M & v in N ) } ;
definition
let V be non empty Abelian addLoopStr ;
let M, N be Subset of V;
:: original: +
redefine funcM + N -> Subset of V;
commutativity
for M, N being Subset of V holds M + N = N + M
proof
let M, N be Subset of V; ::_thesis: M + N = N + M
for x being set st x in M + N holds
x in N + M
proof
let x be set ; ::_thesis: ( x in M + N implies x in N + M )
assume x in M + N ; ::_thesis: x in N + M
then ex u1, v1 being Element of V st
( x = u1 + v1 & u1 in M & v1 in N ) ;
hence x in N + M ; ::_thesis: verum
end;
then A1: M + N c= N + M by TARSKI:def_3;
for x being set st x in N + M holds
x in M + N
proof
let x be set ; ::_thesis: ( x in N + M implies x in M + N )
assume x in N + M ; ::_thesis: x in M + N
then ex u1, v1 being Element of V st
( x = u1 + v1 & u1 in N & v1 in M ) ;
hence x in M + N ; ::_thesis: verum
end;
then N + M c= M + N by TARSKI:def_3;
hence M + N = N + M by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
theorem Th33: :: RUSUB_4:33
for V being non empty addLoopStr
for M being Subset of V
for v being Element of V holds {v} + M = v + M
proof
let V be non empty addLoopStr ; ::_thesis: for M being Subset of V
for v being Element of V holds {v} + M = v + M
let M be Subset of V; ::_thesis: for v being Element of V holds {v} + M = v + M
let v be Element of V; ::_thesis: {v} + M = v + M
for x being set st x in v + M holds
x in {v} + M
proof
let x be set ; ::_thesis: ( x in v + M implies x in {v} + M )
assume x in v + M ; ::_thesis: x in {v} + M
then A1: ex u being Element of V st
( x = v + u & u in M ) ;
v in {v} by TARSKI:def_1;
hence x in {v} + M by A1; ::_thesis: verum
end;
then A2: v + M c= {v} + M by TARSKI:def_3;
for x being set st x in {v} + M holds
x in v + M
proof
let x be set ; ::_thesis: ( x in {v} + M implies x in v + M )
assume x in {v} + M ; ::_thesis: x in v + M
then consider v1, u1 being Element of V such that
A3: x = v1 + u1 and
A4: v1 in {v} and
A5: u1 in M ;
v1 = v by A4, TARSKI:def_1;
hence x in v + M by A3, A5; ::_thesis: verum
end;
then {v} + M c= v + M by TARSKI:def_3;
hence {v} + M = v + M by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: RUSUB_4:34
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Affine Subset of V
for v being VECTOR of V holds {v} + M is Affine
proof
let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M being Affine Subset of V
for v being VECTOR of V holds {v} + M is Affine
let M be Affine Subset of V; ::_thesis: for v being VECTOR of V holds {v} + M is Affine
let v be VECTOR of V; ::_thesis: {v} + M is Affine
{v} + M = v + M by Th33;
hence {v} + M is Affine by Th31; ::_thesis: verum
end;
theorem :: RUSUB_4:35
for V being non empty RLSStruct
for M, N being Affine Subset of V holds M /\ N is Affine
proof
let V be non empty RLSStruct ; ::_thesis: for M, N being Affine Subset of V holds M /\ N is Affine
let M, N be Affine Subset of V; ::_thesis: M /\ N is Affine
for x, y being VECTOR of V
for a being Real st x in M /\ N & y in M /\ N holds
((1 - a) * x) + (a * y) in M /\ N
proof
let x, y be VECTOR of V; ::_thesis: for a being Real st x in M /\ N & y in M /\ N holds
((1 - a) * x) + (a * y) in M /\ N
let a be Real; ::_thesis: ( x in M /\ N & y in M /\ N implies ((1 - a) * x) + (a * y) in M /\ N )
assume A1: ( x in M /\ N & y in M /\ N ) ; ::_thesis: ((1 - a) * x) + (a * y) in M /\ N
then ( x in N & y in N ) by XBOOLE_0:def_4;
then A2: ((1 - a) * x) + (a * y) in N by Def4;
( x in M & y in M ) by A1, XBOOLE_0:def_4;
then ((1 - a) * x) + (a * y) in M by Def4;
hence ((1 - a) * x) + (a * y) in M /\ N by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
hence M /\ N is Affine by Def4; ::_thesis: verum
end;
theorem :: RUSUB_4:36
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M, N being Affine Subset of V holds M + N is Affine
proof
let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for M, N being Affine Subset of V holds M + N is Affine
let M, N be Affine Subset of V; ::_thesis: M + N is Affine
for x, y being VECTOR of V
for a being Real st x in M + N & y in M + N holds
((1 - a) * x) + (a * y) in M + N
proof
let x, y be VECTOR of V; ::_thesis: for a being Real st x in M + N & y in M + N holds
((1 - a) * x) + (a * y) in M + N
let a be Real; ::_thesis: ( x in M + N & y in M + N implies ((1 - a) * x) + (a * y) in M + N )
assume that
A1: x in M + N and
A2: y in M + N ; ::_thesis: ((1 - a) * x) + (a * y) in M + N
consider u1, v1 being Element of V such that
A3: x = u1 + v1 and
A4: ( u1 in M & v1 in N ) by A1;
consider u2, v2 being Element of V such that
A5: y = u2 + v2 and
A6: ( u2 in M & v2 in N ) by A2;
A7: ((1 - a) * x) + (a * y) = (((1 - a) * u1) + ((1 - a) * v1)) + (a * (u2 + v2)) by A3, A5, RLVECT_1:def_5
.= (((1 - a) * u1) + ((1 - a) * v1)) + ((a * u2) + (a * v2)) by RLVECT_1:def_5
.= ((((1 - a) * u1) + ((1 - a) * v1)) + (a * u2)) + (a * v2) by RLVECT_1:def_3
.= (((1 - a) * v1) + (((1 - a) * u1) + (a * u2))) + (a * v2) by RLVECT_1:def_3
.= (((1 - a) * u1) + (a * u2)) + (((1 - a) * v1) + (a * v2)) by RLVECT_1:def_3 ;
( ((1 - a) * u1) + (a * u2) in M & ((1 - a) * v1) + (a * v2) in N ) by A4, A6, Def4;
hence ((1 - a) * x) + (a * y) in M + N by A7; ::_thesis: verum
end;
hence M + N is Affine by Def4; ::_thesis: verum
end;