let F be Field; :: thesis: 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; :: thesis: 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; :: thesis: ( 1 <= m & m < n & n <= dim V implies GrassmannSpace V,m,n is with_non_trivial_blocks )
assume A1:
( 1 <= m & m < n & n <= dim V )
; :: thesis: GrassmannSpace V,m,n is with_non_trivial_blocks
set S = GrassmannSpace V,m,n;
let B be Block of (GrassmannSpace V,m,n); :: according to PENCIL_1:def 6 :: thesis: 2 c= card B
not the topology of (GrassmannSpace V,m,n) is empty
by A1, Th24;
then consider W being Subspace of V such that
A2:
( dim W = n & B = m Subspaces_of W )
by Def6;
m + 1 <= n
by A1, NAT_1:13;
then consider U being strict Subspace of W such that
A3:
dim U = m + 1
by A2, VECTSP_9:39;
consider I being Basis of U;
reconsider I' = I as finite Subset of U by VECTSP_9:24;
A4:
( I is linearly-independent & Lin I = VectSpStr(# the carrier of U,the U5 of U,the U2 of U,the lmult of U #) )
by VECTSP_7:def 3;
A5:
card I = m + 1
by A3, VECTSP_9:def 2;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
1 + 1 <= m + 1
by A1, XREAL_1:9;
then
2 c= card I
by A5, NAT_1:40;
then consider i, j being set such that
A6:
( i in I & j in I & i <> j )
by PENCIL_1:2;
reconsider I1 = I' \ {i} as finite Subset of U ;
reconsider I2 = I' \ {j} as finite Subset of U ;
A7:
I1 is linearly-independent
by A4, VECTSP_7:2, XBOOLE_1:36;
I1 c= the carrier of (Lin I1)
then reconsider I1' = I1 as Subset of (Lin I1) ;
reconsider II1 = I1' as linearly-independent Subset of (Lin I1) by A7, VECTSP_9:16;
Lin II1 = VectSpStr(# the carrier of (Lin I1),the U5 of (Lin I1),the U2 of (Lin I1),the lmult of (Lin I1) #)
by VECTSP_9:21;
then A8:
I1 is Basis of Lin I1
by VECTSP_7:def 3;
card I1 =
(card I') - (card {i})
by A6, EULER_1:5
.=
(m + 1) - 1
by A5, CARD_1:50
;
then A9:
dim (Lin I1) = m
by A8, VECTSP_9:def 2;
Lin I1 is strict Subspace of W
by VECTSP_4:34;
then A10:
Lin I1 in B
by A2, A9, VECTSP_9:def 3;
A11:
I2 is linearly-independent
by A4, VECTSP_7:2, XBOOLE_1:36;
I2 c= the carrier of (Lin I2)
then reconsider I2' = I2 as Subset of (Lin I2) ;
reconsider II2 = I2' as linearly-independent Subset of (Lin I2) by A11, VECTSP_9:16;
Lin II2 = VectSpStr(# the carrier of (Lin I2),the U5 of (Lin I2),the U2 of (Lin I2),the lmult of (Lin I2) #)
by VECTSP_9:21;
then A12:
I2 is Basis of Lin I2
by VECTSP_7:def 3;
card I2 =
(card I') - (card {j})
by A6, EULER_1:5
.=
(m + 1) - 1
by A5, CARD_1:50
;
then A13:
dim (Lin I2) = m
by A12, VECTSP_9:def 2;
Lin I2 is strict Subspace of W
by VECTSP_4:34;
then A14:
Lin I2 in B
by A2, A13, VECTSP_9:def 3;
not j in {i}
by A6, TARSKI:def 1;
then
j in I1
by A6, XBOOLE_0:def 5;
then A15:
j in Lin I1
by VECTSP_7:13;
not j in Lin I2
by A4, A6, VECTSP_9:18;
hence
2 c= card B
by A10, A14, A15, PENCIL_1:2; :: thesis: verum