let F be Field; for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V & 3 <= dim V holds
not PencilSpace (V,k) is degenerated
let V be finite-dimensional VectSp of F; for k being Nat st 1 <= k & k < dim V & 3 <= dim V holds
not PencilSpace (V,k) is degenerated
let k be Nat; ( 1 <= k & k < dim V & 3 <= dim V implies not PencilSpace (V,k) is degenerated )
assume that
A1:
1 <= k
and
A2:
k < dim V
and
A3:
3 <= dim V
; not PencilSpace (V,k) is degenerated
set S = PencilSpace (V,k);
now for B being Block of (PencilSpace (V,k)) holds the carrier of (PencilSpace (V,k)) <> Blet B be
Block of
(PencilSpace (V,k));
the carrier of (PencilSpace (V,k)) <> b1
not the
topology of
(PencilSpace (V,k)) is
empty
by A1, A2, Th10;
then consider W1,
W2 being
Subspace of
V such that A4:
W1 is
Subspace of
W2
and A5:
(dim W1) + 1
= k
and A6:
dim W2 = k + 1
and A7:
B = pencil (
W1,
W2,
k)
by Def4;
A8:
the
carrier of
W1 c= the
carrier of
V
by VECTSP_4:def 2;
per cases
( k + 1 < dim V or ( 2 <= k & k + 1 >= dim V ) )
by A2, A3, Th1;
suppose A16:
( 2
<= k &
k + 1
>= dim V )
;
the carrier of (PencilSpace (V,k)) <> b1set I = the
Basis of
W1;
reconsider I1 = the
Basis of
W1 as
finite Subset of
W1 ;
2
- 1
<= ((dim W1) + 1) - 1
by A5, A16, XREAL_1:9;
then
1
<= card I1
by VECTSP_9:def 1;
then
not
I1 is
empty
;
then consider i being
object such that A17:
i in the
Basis of
W1
;
reconsider i =
i as
Vector of
W1 by A17;
reconsider J =
I1 \ {i} as
finite Subset of
V by A8, XBOOLE_1:1;
the
Basis of
W1 is
linearly-independent
by VECTSP_7:def 3;
then
the
Basis of
W1 \ {i} is
linearly-independent
by VECTSP_7:1, XBOOLE_1:36;
then reconsider JJ = the
Basis of
W1 \ {i} as
linearly-independent Subset of
V by VECTSP_9:11;
J c= the
carrier of
(Lin J)
then reconsider JJJ =
JJ as
linearly-independent Subset of
(Lin J) by VECTSP_9:12;
Lin JJJ = Lin J
by VECTSP_9:17;
then A18:
J is
Basis of
(Lin J)
by VECTSP_7:def 3;
A19:
card the
Basis of
W1 = dim W1
by VECTSP_9:def 1;
set T = the
Linear_Compl of
W1;
A20:
V is_the_direct_sum_of W1, the
Linear_Compl of
W1
by VECTSP_5:38;
then A21:
W1 /\ the
Linear_Compl of
W1 = (0). V
by VECTSP_5:def 4;
k + 1
<= dim V
by A2, NAT_1:13;
then
dim V = k + 1
by A16, XXREAL_0:1;
then
(k + 1) - ((dim W1) + 1) = ((dim W1) + (dim the Linear_Compl of W1)) - ((dim W1) + 1)
by A20, VECTSP_9:34;
then consider u,
v being
Vector of the
Linear_Compl of
W1 such that A22:
u <> v
and A23:
{u,v} is
linearly-independent
and A24:
(Omega). the
Linear_Compl of
W1 = Lin {u,v}
by A5, VECTSP_9:31;
( the
carrier of the
Linear_Compl of
W1 c= the
carrier of
V &
u in the
carrier of the
Linear_Compl of
W1 )
by VECTSP_4:def 2;
then reconsider u1 =
u,
v1 =
v as
Vector of
V ;
reconsider Y =
{u,v} as
linearly-independent Subset of
V by A23, VECTSP_9:11;
A25:
Y = {u,v}
;
Lin ( the Basis of W1 \ {i}) is
Subspace of
Lin the
Basis of
W1
by VECTSP_7:13, XBOOLE_1:36;
then A26:
Lin J is
Subspace of
W1
by VECTSP_9:17;
the
carrier of
((Lin J) /\ (Lin {u1,v1})) c= the
carrier of
((0). V)
proof
let a be
object ;
TARSKI:def 3 ( not a in the carrier of ((Lin J) /\ (Lin {u1,v1})) or a in the carrier of ((0). V) )
assume
a in the
carrier of
((Lin J) /\ (Lin {u1,v1}))
;
a in the carrier of ((0). V)
then A27:
a in (Lin J) /\ (Lin {u1,v1})
;
then
a in Lin {u1,v1}
by VECTSP_5:3;
then
a in Lin {u,v}
by VECTSP_9:17;
then
a in the
carrier of
ModuleStr(# the
carrier of the
Linear_Compl of
W1, the
U5 of the
Linear_Compl of
W1, the
ZeroF of the
Linear_Compl of
W1, the
lmult of the
Linear_Compl of
W1 #)
by A24;
then A28:
a in the
Linear_Compl of
W1
;
a in Lin J
by A27, VECTSP_5:3;
then
a in W1
by A26, VECTSP_4:8;
then
a in W1 /\ the
Linear_Compl of
W1
by A28, VECTSP_5:3;
hence
a in the
carrier of
((0). V)
by A21;
verum
end; then A29:
(
(0). V is
Subspace of
(Lin J) /\ (Lin {u1,v1}) &
(Lin J) /\ (Lin {u1,v1}) is
Subspace of
(0). V )
by VECTSP_4:27, VECTSP_4:39;
card J =
(card I1) - (card {i})
by A17, EULER_1:4
.=
(dim W1) - 1
by A19, CARD_1:30
;
then
dim (Lin J) = (dim W1) - 1
by A18, VECTSP_9:def 1;
then A30:
dim ((Lin J) + (Lin {u1,v1})) = ((dim W1) - 1) + 2
by A22, A25, A29, Th14, VECTSP_4:25;
A31:
Lin the
Basis of
W1 = (Omega). W1
by VECTSP_7:def 3;
A32:
i in W1
;
now not (Lin J) + (Lin {u1,v1}) in BA33:
now not i in (Lin J) + (Lin {u1,v1})reconsider IV = the
Basis of
W1 as
Subset of
V by A8, XBOOLE_1:1;
assume A34:
i in (Lin J) + (Lin {u1,v1})
;
contradiction
IV c= the
carrier of
((Lin J) + (Lin {u1,v1}))
then
Lin IV is
Subspace of
(Lin J) + (Lin {u1,v1})
by VECTSP_9:16;
then
Lin the
Basis of
W1 is
Subspace of
(Lin J) + (Lin {u1,v1})
by VECTSP_9:17;
then A38:
W1 is
Subspace of
(Lin J) + (Lin {u1,v1})
by A31, Th5;
the
carrier of
(W1 /\ (Lin {u1,v1})) c= the
carrier of
((0). V)
proof
let a be
object ;
TARSKI:def 3 ( not a in the carrier of (W1 /\ (Lin {u1,v1})) or a in the carrier of ((0). V) )
assume
a in the
carrier of
(W1 /\ (Lin {u1,v1}))
;
a in the carrier of ((0). V)
then A39:
a in W1 /\ (Lin {u1,v1})
;
then
a in Lin {u1,v1}
by VECTSP_5:3;
then
a in Lin {u,v}
by VECTSP_9:17;
then
a in the
carrier of
ModuleStr(# the
carrier of the
Linear_Compl of
W1, the
U5 of the
Linear_Compl of
W1, the
ZeroF of the
Linear_Compl of
W1, the
lmult of the
Linear_Compl of
W1 #)
by A24;
then A40:
a in the
Linear_Compl of
W1
;
a in W1
by A39, VECTSP_5:3;
then
a in W1 /\ the
Linear_Compl of
W1
by A40, VECTSP_5:3;
hence
a in the
carrier of
((0). V)
by A21;
verum
end; then
(
(0). V is
Subspace of
W1 /\ (Lin {u1,v1}) &
W1 /\ (Lin {u1,v1}) is
Subspace of
(0). V )
by VECTSP_4:27, VECTSP_4:39;
then A41:
dim (W1 + (Lin {u1,v1})) = (dim W1) + 2
by A22, A25, Th14, VECTSP_4:25;
Lin {u1,v1} is
Subspace of
(Lin J) + (Lin {u1,v1})
by VECTSP_5:7;
then
W1 + (Lin {u1,v1}) is
Subspace of
(Lin J) + (Lin {u1,v1})
by A38, VECTSP_5:34;
then
((dim W1) + 1) + 1
<= (dim W1) + 1
by A30, A41, VECTSP_9:25;
hence
contradiction
by NAT_1:13;
verum end; assume
(Lin J) + (Lin {u1,v1}) in B
;
contradictionthen
W1 is
Subspace of
(Lin J) + (Lin {u1,v1})
by A7, Th8;
hence
contradiction
by A32, A33, VECTSP_4:8;
verum hence
the
carrier of
(PencilSpace (V,k)) <> B
by A5, A30, VECTSP_9:def 2;
verum end; end;
then
the carrier of (PencilSpace (V,k)) is not Block of (PencilSpace (V,k))
;
hence
not PencilSpace (V,k) is degenerated
; verum