let F be Field; for V being finite-dimensional VectSp of F
for m, n being Nat st 1 <= m & m < n & n <= dim V holds
GrassmannSpace (V,m,n) is with_non_trivial_blocks
let V be finite-dimensional VectSp of F; for m, n being Nat st 1 <= m & m < n & n <= dim V holds
GrassmannSpace (V,m,n) is with_non_trivial_blocks
let m, n be Nat; ( 1 <= m & m < n & n <= dim V implies GrassmannSpace (V,m,n) is with_non_trivial_blocks )
assume that
A1:
1 <= m
and
A2:
m < n
and
A3:
n <= dim V
; GrassmannSpace (V,m,n) is with_non_trivial_blocks
set S = GrassmannSpace (V,m,n);
let B be Block of (GrassmannSpace (V,m,n)); PENCIL_1:def 6 2 c= card B
not the topology of (GrassmannSpace (V,m,n)) is empty
by A3, Th22;
then consider W being Subspace of V such that
A4:
dim W = n
and
A5:
B = m Subspaces_of W
by Def6;
m + 1 <= n
by A2, NAT_1:13;
then consider U being strict Subspace of W such that
A6:
dim U = m + 1
by A4, VECTSP_9:35;
set I = the Basis of U;
A7:
card the Basis of U = m + 1
by A6, VECTSP_9:def 1;
reconsider I9 = the Basis of U as finite Subset of U ;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
1 + 1 <= m + 1
by A1, XREAL_1:7;
then
Segm 2 c= Segm (m + 1)
by NAT_1:39;
then consider i, j being object such that
A8:
i in the Basis of U
and
A9:
j in the Basis of U
and
A10:
i <> j
by PENCIL_1:2, A7;
reconsider I1 = I9 \ {i} as finite Subset of U ;
I1 c= the carrier of (Lin I1)
then reconsider I19 = I1 as Subset of (Lin I1) ;
A11:
the Basis of U is linearly-independent
by VECTSP_7:def 3;
then
I1 is linearly-independent
by VECTSP_7:1, XBOOLE_1:36;
then reconsider II1 = I19 as linearly-independent Subset of (Lin I1) by VECTSP_9:12;
Lin II1 = ModuleStr(# the carrier of (Lin I1), the U5 of (Lin I1), the ZeroF of (Lin I1), the lmult of (Lin I1) #)
by VECTSP_9:17;
then A12:
I1 is Basis of (Lin I1)
by VECTSP_7:def 3;
reconsider I2 = I9 \ {j} as finite Subset of U ;
I2 c= the carrier of (Lin I2)
then reconsider I29 = I2 as Subset of (Lin I2) ;
I2 is linearly-independent
by A11, VECTSP_7:1, XBOOLE_1:36;
then reconsider II2 = I29 as linearly-independent Subset of (Lin I2) by VECTSP_9:12;
Lin II2 = ModuleStr(# the carrier of (Lin I2), the U5 of (Lin I2), the ZeroF of (Lin I2), the lmult of (Lin I2) #)
by VECTSP_9:17;
then A13:
I2 is Basis of (Lin I2)
by VECTSP_7:def 3;
card I2 =
(card I9) - (card {j})
by A9, EULER_1:4
.=
(m + 1) - 1
by A7, CARD_1:30
;
then A14:
dim (Lin I2) = m
by A13, VECTSP_9:def 1;
Lin I2 is strict Subspace of W
by VECTSP_4:26;
then A15:
Lin I2 in B
by A5, A14, VECTSP_9:def 2;
card I1 =
(card I9) - (card {i})
by A8, EULER_1:4
.=
(m + 1) - 1
by A7, CARD_1:30
;
then A16:
dim (Lin I1) = m
by A12, VECTSP_9:def 1;
Lin I1 is strict Subspace of W
by VECTSP_4:26;
then A17:
Lin I1 in B
by A5, A16, VECTSP_9:def 2;
not j in {i}
by A10, TARSKI:def 1;
then
j in I1
by A9, XBOOLE_0:def 5;
then A18:
j in Lin I1
by VECTSP_7:8;
not j in Lin I2
by A11, A9, VECTSP_9:14;
hence
2 c= card B
by A17, A15, A18, PENCIL_1:2; verum