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 let 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, Th11;
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) <> b1consider I being
Basis of
W1;
reconsider I1 =
I as
finite Subset of
W1 by VECTSP_9:24;
2
- 1
<= ((dim W1) + 1) - 1
by A5, A16, XREAL_1:11;
then
1
<= card I1
by VECTSP_9:def 2;
then
not
I1 is
empty
;
then consider i being
set such that A17:
i in I
by XBOOLE_0:def 1;
reconsider i =
i as
Vector of
W1 by A17;
reconsider J =
I1 \ {i} as
finite Subset of
V by A8, XBOOLE_1:1;
I is
linearly-independent
by VECTSP_7:def 3;
then
I \ {i} is
linearly-independent
by VECTSP_7:2, XBOOLE_1:36;
then reconsider JJ =
I \ {i} as
linearly-independent Subset of
V by VECTSP_9:15;
J c= the
carrier of
(Lin J)
then reconsider JJJ =
JJ as
linearly-independent Subset of
(Lin J) by VECTSP_9:16;
Lin JJJ = Lin J
by VECTSP_9:21;
then A18:
J is
Basis of
Lin J
by VECTSP_7:def 3;
A19:
card I = dim W1
by VECTSP_9:def 2;
consider T being
Linear_Compl of
W1;
A20:
V is_the_direct_sum_of W1,
T
by VECTSP_5:48;
then A21:
W1 /\ T = (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 T)) - ((dim W1) + 1)
by A20, VECTSP_9:38;
then consider u,
v being
Vector of
T such that A22:
u <> v
and A23:
{u,v} is
linearly-independent
and A24:
(Omega). T = Lin {u,v}
by A5, VECTSP_9:35;
A25:
v in the
carrier of
T
;
( the
carrier of
T c= the
carrier of
V &
u in the
carrier of
T )
by VECTSP_4:def 2;
then reconsider u1 =
u,
v1 =
v as
Vector of
V by A25;
reconsider Y =
{u,v} as
linearly-independent Subset of
V by A23, VECTSP_9:15;
A26:
Y = {u,v}
;
Lin (I \ {i}) is
Subspace of
Lin I
by VECTSP_7:18, XBOOLE_1:36;
then A27:
Lin J is
Subspace of
W1
by VECTSP_9:21;
the
carrier of
((Lin J) /\ (Lin {u1,v1})) c= the
carrier of
((0). V)
proof
let a be
set ;
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 A28:
a in (Lin J) /\ (Lin {u1,v1})
by STRUCT_0:def 5;
then
a in Lin {u1,v1}
by VECTSP_5:7;
then
a in Lin {u,v}
by VECTSP_9:21;
then
a in the
carrier of
VectSpStr(# the
carrier of
T,the
U5 of
T,the
ZeroF of
T,the
lmult of
T #)
by A24, STRUCT_0:def 5;
then A29:
a in T
by STRUCT_0:def 5;
a in Lin J
by A28, VECTSP_5:7;
then
a in W1
by A27, VECTSP_4:16;
then
a in W1 /\ T
by A29, VECTSP_5:7;
hence
a in the
carrier of
((0). V)
by A21, STRUCT_0:def 5;
verum
end; then A30:
(
(0). V is
Subspace of
(Lin J) /\ (Lin {u1,v1}) &
(Lin J) /\ (Lin {u1,v1}) is
Subspace of
(0). V )
by VECTSP_4:35, VECTSP_4:50;
card J =
(card I1) - (card {i})
by A17, EULER_1:5
.=
(dim W1) - 1
by A19, CARD_1:50
;
then
dim (Lin J) = (dim W1) - 1
by A18, VECTSP_9:def 2;
then A31:
dim ((Lin J) + (Lin {u1,v1})) = ((dim W1) - 1) + 2
by A22, A26, A30, Th15, VECTSP_4:33;
A32:
Lin I = (Omega). W1
by VECTSP_7:def 3;
A33:
i in W1
by STRUCT_0:def 5;
now A34:
now reconsider IV =
I as
Subset of
V by A8, XBOOLE_1:1;
assume A35:
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:20;
then
Lin I is
Subspace of
(Lin J) + (Lin {u1,v1})
by VECTSP_9:21;
then A39:
W1 is
Subspace of
(Lin J) + (Lin {u1,v1})
by A32, Th6;
the
carrier of
(W1 /\ (Lin {u1,v1})) c= the
carrier of
((0). V)
proof
let a be
set ;
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 A40:
a in W1 /\ (Lin {u1,v1})
by STRUCT_0:def 5;
then
a in Lin {u1,v1}
by VECTSP_5:7;
then
a in Lin {u,v}
by VECTSP_9:21;
then
a in the
carrier of
VectSpStr(# the
carrier of
T,the
U5 of
T,the
ZeroF of
T,the
lmult of
T #)
by A24, STRUCT_0:def 5;
then A41:
a in T
by STRUCT_0:def 5;
a in W1
by A40, VECTSP_5:7;
then
a in W1 /\ T
by A41, VECTSP_5:7;
hence
a in the
carrier of
((0). V)
by A21, STRUCT_0:def 5;
verum
end; then
(
(0). V is
Subspace of
W1 /\ (Lin {u1,v1}) &
W1 /\ (Lin {u1,v1}) is
Subspace of
(0). V )
by VECTSP_4:35, VECTSP_4:50;
then A42:
dim (W1 + (Lin {u1,v1})) = (dim W1) + 2
by A22, A26, Th15, VECTSP_4:33;
Lin {u1,v1} is
Subspace of
(Lin J) + (Lin {u1,v1})
by VECTSP_5:11;
then
W1 + (Lin {u1,v1}) is
Subspace of
(Lin J) + (Lin {u1,v1})
by A39, VECTSP_5:40;
then
((dim W1) + 1) + 1
<= (dim W1) + 1
by A31, A42, VECTSP_9:29;
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, Th9;
hence
contradiction
by A33, A34, VECTSP_4:16;
verum hence
the
carrier of
(PencilSpace V,k) <> B
by A5, A31, VECTSP_9:def 3;
verum end; end;
then
the carrier of (PencilSpace V,k) is not Block of (PencilSpace V,k)
;
hence
not PencilSpace V,k is degenerated
by PENCIL_1:def 5; verum