let F be Field; for V being finite-dimensional VectSp of F
for m being Nat st m + 1 <= dim V holds
GrassmannSpace (V,m,(m + 1)) is identifying_close_blocks
let V be finite-dimensional VectSp of F; for m being Nat st m + 1 <= dim V holds
GrassmannSpace (V,m,(m + 1)) is identifying_close_blocks
let m be Nat; ( m + 1 <= dim V implies GrassmannSpace (V,m,(m + 1)) is identifying_close_blocks )
assume A1:
m + 1 <= dim V
; GrassmannSpace (V,m,(m + 1)) is identifying_close_blocks
set S = GrassmannSpace (V,m,(m + 1));
let K, L be Block of (GrassmannSpace (V,m,(m + 1))); PENCIL_1:def 7 ( not 2 c= card (K /\ L) or K = L )
A2:
not the topology of (GrassmannSpace (V,m,(m + 1))) is empty
by A1, Th22;
then consider W1 being Subspace of V such that
A3:
dim W1 = m + 1
and
A4:
K = m Subspaces_of W1
by Def6;
assume
2 c= card (K /\ L)
; K = L
then consider x, y being object such that
A5:
x in K /\ L
and
A6:
y in K /\ L
and
A7:
x <> y
by PENCIL_1:2;
y in K
by A6, XBOOLE_0:def 4;
then consider Y being strict Subspace of W1 such that
A8:
y = Y
and
A9:
dim Y = m
by A4, VECTSP_9:def 2;
consider W2 being Subspace of V such that
A10:
dim W2 = m + 1
and
A11:
L = m Subspaces_of W2
by A2, Def6;
y in L
by A6, XBOOLE_0:def 4;
then consider Y9 being strict Subspace of W2 such that
A12:
y = Y9
and
dim Y9 = m
by A11, VECTSP_9:def 2;
x in L
by A5, XBOOLE_0:def 4;
then consider X9 being strict Subspace of W2 such that
A13:
x = X9
and
dim X9 = m
by A11, VECTSP_9:def 2;
x in K
by A5, XBOOLE_0:def 4;
then consider X being strict Subspace of W1 such that
A14:
x = X
and
A15:
dim X = m
by A4, VECTSP_9:def 2;
reconsider x = x, y = y as strict Subspace of V by A14, A8, VECTSP_4:26;
x + y is Subspace of W1
by A14, A8, VECTSP_5:34;
then
( x is Subspace of x + y & dim (x + y) <= m + 1 )
by A3, VECTSP_5:7, VECTSP_9:25;
then A19:
dim (x + y) = m + 1
by A14, A15, A16, NAT_1:9, VECTSP_9:25;
X9 + Y9 = x + y
by A13, A12, VECTSP10:12;
then A20:
(Omega). (X9 + Y9) = (Omega). W2
by A10, A19, VECTSP_9:28;
A21:
X + Y = x + y
by A14, A8, VECTSP10:12;
then
(Omega). (X + Y) = (Omega). W1
by A3, A19, VECTSP_9:28;
hence
K = L
by A4, A11, A13, A12, A21, A20, Th23, VECTSP10:12; verum