let F be Field; :: thesis: for V being finite-dimensional VectSp of F
for W being Subspace of V
for m being Nat st 1 <= m & m <= dim V & m Subspaces_of V c= m Subspaces_of W holds
(Omega). V = (Omega). W
let V be finite-dimensional VectSp of F; :: thesis: for W being Subspace of V
for m being Nat st 1 <= m & m <= dim V & m Subspaces_of V c= m Subspaces_of W holds
(Omega). V = (Omega). W
let W be Subspace of V; :: thesis: for m being Nat st 1 <= m & m <= dim V & m Subspaces_of V c= m Subspaces_of W holds
(Omega). V = (Omega). W
let m be Nat; :: thesis: ( 1 <= m & m <= dim V & m Subspaces_of V c= m Subspaces_of W implies (Omega). V = (Omega). W )
assume A1:
( 1 <= m & m <= dim V & m Subspaces_of V c= m Subspaces_of W )
; :: thesis: (Omega). V = (Omega). W
hereby :: thesis: verum
assume A2:
(Omega). V <> (Omega). W
;
:: thesis: contradictionthen A3:
dim W <> dim V
by VECTSP_9:32;
dim W <= dim V
by VECTSP_9:29;
then A4:
dim W < dim V
by A3, XXREAL_0:1;
per cases
( m = dim V or m < dim V )
by A1, XXREAL_0:1;
suppose A7:
m < dim V
;
:: thesis: contradictionA8:
the
carrier of
W c= the
carrier of
V
by VECTSP_4:def 2;
then
not the
carrier of
V c= the
carrier of
W
by A8, XBOOLE_0:def 10;
then consider x being
set such that A10:
(
x in the
carrier of
V & not
x in the
carrier of
W )
by TARSKI:def 3;
reconsider x =
x as
Vector of
V by A10;
0. V in W
by VECTSP_4:25;
then
x <> 0. V
by A10, STRUCT_0:def 5;
then
{x} is
linearly-independent
by VECTSP_7:5;
then consider I being
Basis of
V such that A11:
{x} c= I
by VECTSP_7:27;
A12:
(
I is
linearly-independent &
Lin I = VectSpStr(# the
carrier of
V,the
U5 of
V,the
U2 of
V,the
lmult of
V #) )
by VECTSP_7:def 3;
reconsider J =
I as
finite Subset of
V by VECTSP_9:24;
card J = dim V
by VECTSP_9:def 2;
then consider K being
Subset of
J such that A13:
card K = m
by A7, Th2;
per cases
( x in K or not x in K )
;
suppose A14:
x in K
;
:: thesis: contradictionreconsider L =
K as
finite Subset of
V by XBOOLE_1:1;
A15:
L is
linearly-independent
by A12, VECTSP_7:2;
L c= the
carrier of
(Lin L)
then reconsider L' =
L as
Subset of
(Lin L) ;
reconsider LL1 =
L' as
linearly-independent Subset of
(Lin L) by A15, VECTSP_9:16;
Lin LL1 = VectSpStr(# the
carrier of
(Lin L),the
U5 of
(Lin L),the
U2 of
(Lin L),the
lmult of
(Lin L) #)
by VECTSP_9:21;
then
L is
Basis of
Lin L
by VECTSP_7:def 3;
then
dim (Lin L) = m
by A13, VECTSP_9:def 2;
then
Lin L in m Subspaces_of V
by VECTSP_9:def 3;
then consider M being
strict Subspace of
W such that A16:
(
M = Lin L &
dim M = m )
by A1, VECTSP_9:def 3;
x in W
by A14, A16, VECTSP_4:17, VECTSP_7:13;
hence
contradiction
by A10, STRUCT_0:def 5;
:: thesis: verum end; suppose A17:
not
x in K
;
:: thesis: contradictionconsider y being
set such that A18:
y in K
by A1, A13, CARD_1:47, XBOOLE_0:def 1;
(K \ {y}) \/ {x} c= the
carrier of
V
then reconsider L =
(K \ {y}) \/ {x} as
finite Subset of
V ;
x in {x}
by TARSKI:def 1;
then A19:
x in L
by XBOOLE_0:def 3;
not
x in K \ {y}
by A17, XBOOLE_0:def 5;
then A20:
card L =
(card (K \ {y})) + 1
by CARD_2:54
.=
((card K) - (card {y})) + 1
by A18, EULER_1:5
.=
((card K) - 1) + 1
by CARD_1:50
.=
m
by A13
;
L c= I
then A21:
L is
linearly-independent
by A12, VECTSP_7:2;
L c= the
carrier of
(Lin L)
then reconsider L' =
L as
Subset of
(Lin L) ;
reconsider LL1 =
L' as
linearly-independent Subset of
(Lin L) by A21, VECTSP_9:16;
Lin LL1 = VectSpStr(# the
carrier of
(Lin L),the
U5 of
(Lin L),the
U2 of
(Lin L),the
lmult of
(Lin L) #)
by VECTSP_9:21;
then
L is
Basis of
Lin L
by VECTSP_7:def 3;
then
dim (Lin L) = m
by A20, VECTSP_9:def 2;
then
Lin L in m Subspaces_of V
by VECTSP_9:def 3;
then consider M being
strict Subspace of
W such that A22:
(
M = Lin L &
dim M = m )
by A1, VECTSP_9:def 3;
x in W
by A19, A22, VECTSP_4:17, VECTSP_7:13;
hence
contradiction
by A10, STRUCT_0:def 5;
:: thesis: verum end; end;
end;