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:25;
assume A5:
(Omega). V <> (Omega). W
;
contradictionthen
dim W <> dim V
by VECTSP_9:28;
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;
then consider x being
object such that A10:
x in the
carrier of
V
and A11:
not
x in the
carrier of
W
;
reconsider x =
x as
Vector of
V by A10;
0. V in W
by VECTSP_4:17;
then
x <> 0. V
by A11;
then
{x} is
linearly-independent
by VECTSP_7:3;
then consider I being
Basis of
V such that A12:
{x} c= I
by VECTSP_7:19;
reconsider J =
I as
finite Subset of
V by VECTSP_9:20;
card J = dim V
by VECTSP_9:def 1;
then consider K being
Subset of
J such that A13:
card K = m
by A7, Lm1;
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
object such that A17:
y in K
by A1, A13, CARD_1:27, 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:1;
then reconsider LL1 =
L9 as
linearly-independent Subset of
(Lin L) by VECTSP_9:12;
Lin LL1 = ModuleStr(# the
carrier of
(Lin L), the
U5 of
(Lin L), the
ZeroF of
(Lin L), the
lmult of
(Lin L) #)
by VECTSP_9:17;
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:41
.=
((card K) - (card {y})) + 1
by A17, EULER_1:4
.=
((card K) - 1) + 1
by CARD_1:30
.=
m
by A13
;
then
dim (Lin L) = m
by A18, VECTSP_9:def 1;
then
Lin L in m Subspaces_of V
by VECTSP_9:def 2;
then A19:
ex
M being
strict Subspace of
W st
(
M = Lin L &
dim M = m )
by A3, VECTSP_9:def 2;
x in {x}
by TARSKI:def 1;
then
x in L
by XBOOLE_0:def 3;
then
x in W
by A19, VECTSP_4:9, VECTSP_7:8;
hence
contradiction
by A11;
verum end;
end;