let F be Field; 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; for k being Nat st 1 <= k & k < dim V holds
PencilSpace (V,k) is identifying_close_blocks
let k be Nat; ( 1 <= k & k < dim V implies PencilSpace (V,k) is identifying_close_blocks )
assume that
A1:
1 <= k
and
A2:
k < dim V
; PencilSpace (V,k) is identifying_close_blocks
set S = PencilSpace (V,k);
thus
PencilSpace (V,k) is identifying_close_blocks
verumproof
let X,
Y be
Block of
(PencilSpace (V,k));
PENCIL_1:def 7 ( not 2 c= card (X /\ Y) or X = Y )
assume
2
c= card (X /\ Y)
;
X = Y
then consider P,
Q being
object such that A3:
(
P in X /\ Y &
Q in X /\ Y )
and A4:
P <> Q
by PENCIL_1:2;
A5:
(
P in X &
Q in X )
by A3, XBOOLE_0:def 4;
A6:
(
P in Y &
Q in Y )
by A3, XBOOLE_0:def 4;
A7:
not
PencilSpace (
V,
k) is
void
by A1, A2, Th17;
then consider W1,
W2 being
Subspace of
V such that A8:
W1 is
Subspace of
W2
and A9:
(
(dim W1) + 1
= k &
dim W2 = k + 1 )
and A10:
X = pencil (
W1,
W2,
k)
by Def4;
not the
topology of
(PencilSpace (V,k)) is
empty
by A7;
then
X in the
topology of
(PencilSpace (V,k))
;
then reconsider P =
P,
Q =
Q as
Point of
(PencilSpace (V,k)) by A5;
A11:
not
PencilSpace (
V,
k) is
empty
by A2, VECTSP_9:36;
then
ex
P1 being
strict Subspace of
V st
(
P1 = P &
dim P1 = k )
by VECTSP_9:def 2;
then reconsider P =
P as
strict Subspace of
V ;
ex
Q1 being
strict Subspace of
V st
(
Q1 = Q &
dim Q1 = k )
by A11, VECTSP_9:def 2;
then reconsider Q =
Q as
strict Subspace of
V ;
consider U1,
U2 being
Subspace of
V such that A12:
U1 is
Subspace of
U2
and A13:
(
(dim U1) + 1
= k &
dim U2 = k + 1 )
and A14:
Y = pencil (
U1,
U2,
k)
by A7, Def4;
A15:
(Omega). W2 =
P + Q
by A4, A5, A9, A10, Th11
.=
(Omega). U2
by A4, A6, A13, A14, Th11
;
(Omega). W1 =
P /\ Q
by A4, A5, A9, A10, Th11
.=
(Omega). U1
by A4, A6, A13, A14, Th11
;
hence
X = Y
by A8, A10, A12, A14, A15, Th6;
verum
end;