let F be Field; 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; 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; 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; ( 1 <= m & m <= dim V & m Subspaces_of V c= m Subspaces_of W implies (Omega). V = (Omega). W )
assume that
A1:
1 <= m
and
A2:
m <= dim V
and
A3:
m Subspaces_of V c= m Subspaces_of W
; (Omega). V = (Omega). W
hereby verum
A4:
dim W <= dim V
by VECTSP_9:29;
assume A5:
(Omega). V <> (Omega). W
;
contradictionthen
dim W <> dim V
by VECTSP_9:32;
then A6:
dim W < dim V
by A4, XXREAL_0:1;
per cases
( m = dim V or m < dim V )
by A2, XXREAL_0:1;
suppose A7:
m < dim V
;
contradiction
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
and A11:
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 A11, STRUCT_0:def 5;
then
{x} is
linearly-independent
by VECTSP_7:5;
then consider I being
Basis of
V such that A12:
{x} c= I
by VECTSP_7:27;
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;
A14:
I is
linearly-independent
by VECTSP_7:def 3;
per cases
( x in K or not x in K )
;
suppose A16:
not
x in K
;
contradictionconsider y being
set such that A17:
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 ;
L c= the
carrier of
(Lin L)
then reconsider L9 =
L as
Subset of
(Lin L) ;
L c= I
then
L is
linearly-independent
by A14, VECTSP_7:2;
then reconsider LL1 =
L9 as
linearly-independent Subset of
(Lin L) by VECTSP_9:16;
Lin LL1 = VectSpStr(# the
carrier of
(Lin L),the
U5 of
(Lin L),the
ZeroF of
(Lin L),the
lmult of
(Lin L) #)
by VECTSP_9:21;
then A18:
L is
Basis of
Lin L
by VECTSP_7:def 3;
not
x in K \ {y}
by A16, XBOOLE_0:def 5;
then card L =
(card (K \ {y})) + 1
by CARD_2:54
.=
((card K) - (card {y})) + 1
by A17, EULER_1:5
.=
((card K) - 1) + 1
by CARD_1:50
.=
m
by A13
;
then
dim (Lin L) = m
by A18, VECTSP_9:def 2;
then
Lin L in m Subspaces_of V
by VECTSP_9:def 3;
then A19:
ex
M being
strict Subspace of
W st
(
M = Lin L &
dim M = m )
by A3, VECTSP_9:def 3;
x in {x}
by TARSKI:def 1;
then
x in L
by XBOOLE_0:def 3;
then
x in W
by A19, VECTSP_4:17, VECTSP_7:13;
hence
contradiction
by A11, STRUCT_0:def 5;
verum end;
end;