let F be Field; :: thesis: for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
PencilSpace V,k is identifying_close_blocks
let V be finite-dimensional VectSp of F; :: thesis: for k being Nat st 1 <= k & k < dim V holds
PencilSpace V,k is identifying_close_blocks
let k be Nat; :: thesis: ( 1 <= k & k < dim V implies PencilSpace V,k is identifying_close_blocks )
assume A1:
( 1 <= k & k < dim V )
; :: thesis: PencilSpace V,k is identifying_close_blocks
set S = PencilSpace V,k;
thus
PencilSpace V,k is identifying_close_blocks
:: thesis: verumproof
let X,
Y be
Block of
(PencilSpace V,k);
:: according to PENCIL_1:def 7 :: thesis: ( not 2 c= card (X /\ Y) or X = Y )
assume
2
c= card (X /\ Y)
;
:: thesis: X = Y
then consider P,
Q being
set such that A2:
(
P in X /\ Y &
Q in X /\ Y &
P <> Q )
by PENCIL_1:2;
A3:
(
P in X &
P in Y &
Q in X &
Q in Y )
by A2, XBOOLE_0:def 4;
A4:
not
PencilSpace V,
k is
empty
by A1, VECTSP_9:40;
B5:
not
PencilSpace V,
k is
void
by A1, Th19;
then
not the
topology of
(PencilSpace V,k) is
empty
;
then
(
X in the
topology of
(PencilSpace V,k) &
Y in the
topology of
(PencilSpace V,k) )
;
then reconsider P =
P,
Q =
Q as
Point of
(PencilSpace V,k) by A3;
consider P1 being
strict Subspace of
V such that A6:
(
P1 = P &
dim P1 = k )
by A4, VECTSP_9:def 3;
reconsider P =
P as
strict Subspace of
V by A6;
consider Q1 being
strict Subspace of
V such that A7:
(
Q1 = Q &
dim Q1 = k )
by A4, VECTSP_9:def 3;
reconsider Q =
Q as
strict Subspace of
V by A7;
consider W1,
W2 being
Subspace of
V such that A8:
(
W1 is
Subspace of
W2 &
(dim W1) + 1
= k &
dim W2 = k + 1 &
X = pencil W1,
W2,
k )
by B5, Def4;
consider U1,
U2 being
Subspace of
V such that A9:
(
U1 is
Subspace of
U2 &
(dim U1) + 1
= k &
dim U2 = k + 1 &
Y = pencil U1,
U2,
k )
by B5, Def4;
A10:
(Omega). W1 =
P /\ Q
by A1, A2, A3, A8, Th12
.=
(Omega). U1
by A1, A2, A3, A9, Th12
;
(Omega). W2 =
P + Q
by A1, A2, A3, A8, Th12
.=
(Omega). U2
by A1, A2, A3, A9, Th12
;
hence
X = Y
by A8, A9, A10, Th7;
:: thesis: verum
end;