let F be Field; :: thesis: 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; :: thesis: for k being Nat st 1 <= k & k < dim V & 3 <= dim V holds
not PencilSpace V,k is degenerated
let k be Nat; :: thesis: ( 1 <= k & k < dim V & 3 <= dim V implies not PencilSpace V,k is degenerated )
assume A1:
( 1 <= k & k < dim V & 3 <= dim V )
; :: thesis: not PencilSpace V,k is degenerated
set S = PencilSpace V,k;
thus
not PencilSpace V,k is degenerated
:: thesis: verumproof
now let B be
Block of
(PencilSpace V,k);
:: thesis: the carrier of (PencilSpace V,k) <> b1
not the
topology of
(PencilSpace V,k) is
empty
by A1, Th11;
then consider W1,
W2 being
Subspace of
V such that A2:
(
W1 is
Subspace of
W2 &
(dim W1) + 1
= k &
dim W2 = k + 1 &
B = pencil W1,
W2,
k )
by Def4;
A3:
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 A1, Th1;
suppose A10:
( 2
<= k &
k + 1
>= dim V )
;
:: thesis: the carrier of (PencilSpace V,k) <> b1then
(
k + 1
<= dim V &
dim V <= k + 1 )
by A1, NAT_1:13;
then A11:
dim V = k + 1
by XXREAL_0:1;
consider T being
Linear_Compl of
W1;
A12:
the
carrier of
T c= the
carrier of
V
by VECTSP_4:def 2;
A13:
V is_the_direct_sum_of W1,
T
by VECTSP_5:48;
then
(k + 1) - ((dim W1) + 1) = ((dim W1) + (dim T)) - ((dim W1) + 1)
by A11, VECTSP_9:38;
then consider u,
v being
Vector of
T such that A14:
(
u <> v &
{u,v} is
linearly-independent &
(Omega). T = Lin {u,v} )
by A2, VECTSP_9:35;
A15:
(
u <> 0. T &
v <> 0. T )
by A14, VECTSP_7:6;
(
u in the
carrier of
T &
v in the
carrier of
T )
;
then reconsider u1 =
u,
v1 =
v as
Vector of
V by A12;
consider I being
Basis of
W1;
reconsider I1 =
I as
finite Subset of
W1 by VECTSP_9:24;
2
- 1
<= ((dim W1) + 1) - 1
by A2, A10, XREAL_1:11;
then
1
<= card I1
by VECTSP_9:def 2;
then
not
I1 is
empty
;
then consider i being
set such that A16:
i in I
by XBOOLE_0:def 1;
reconsider i =
i as
Vector of
W1 by A16;
reconsider J =
I1 \ {i} as
finite Subset of
V by A3, XBOOLE_1:1;
A17:
card I = dim W1
by VECTSP_9:def 2;
A18:
card J =
(card I1) - (card {i})
by A16, EULER_1:5
.=
(dim W1) - 1
by A17, CARD_1:50
;
A19:
J c= the
carrier of
(Lin J)
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;
reconsider JJJ =
JJ as
linearly-independent Subset of
(Lin J) by A19, VECTSP_9:16;
Lin JJJ = Lin J
by VECTSP_9:21;
then
J is
Basis of
Lin J
by VECTSP_7:def 3;
then A20:
dim (Lin J) = (dim W1) - 1
by A18, VECTSP_9:def 2;
A21:
W1 /\ T = (0). V
by A13, VECTSP_5:def 4;
A24:
Lin I = (Omega). W1
by VECTSP_7:def 3;
Lin (I \ {i}) is
Subspace of
Lin I
by VECTSP_7:18, XBOOLE_1:36;
then A25:
Lin J is
Subspace of
W1
by VECTSP_9:21;
then A26:
not
u1 in Lin J
by A22, VECTSP_4:16;
A27:
not
v1 in Lin J
by A23, A25, VECTSP_4:16;
reconsider Y =
{u,v} as
linearly-independent Subset of
V by A14, VECTSP_9:15;
A28:
Y = {u,v}
;
A29:
(0). V is
Subspace of
(Lin J) /\ (Lin {u1,v1})
by VECTSP_4:50;
the
carrier of
((Lin J) /\ (Lin {u1,v1})) c= the
carrier of
((0). V)
proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( 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}))
;
:: thesis: a in the carrier of ((0). V)
then
a in (Lin J) /\ (Lin {u1,v1})
by STRUCT_0:def 5;
then
(
a in Lin J &
a in Lin {u1,v1} )
by VECTSP_5:7;
then
(
a in W1 &
a in Lin {u,v} )
by A25, VECTSP_4:16, VECTSP_9:21;
then
(
a in W1 &
a in the
carrier of
VectSpStr(# the
carrier of
T,the
U5 of
T,the
U2 of
T,the
lmult of
T #) )
by A14, STRUCT_0:def 5;
then
(
a in W1 &
a in T )
by STRUCT_0:def 5;
then
a in W1 /\ T
by VECTSP_5:7;
hence
a in the
carrier of
((0). V)
by A21, STRUCT_0:def 5;
:: thesis: verum
end; then
(Lin J) /\ (Lin {u1,v1}) is
Subspace of
(0). V
by VECTSP_4:35;
then A30:
dim ((Lin J) + (Lin {u1,v1})) = ((dim W1) - 1) + 2
by A14, A20, A26, A27, A28, A29, Th15, VECTSP_4:33;
A31:
i in W1
by STRUCT_0:def 5;
now assume
(Lin J) + (Lin {u1,v1}) in B
;
:: thesis: contradictionthen A32:
W1 is
Subspace of
(Lin J) + (Lin {u1,v1})
by A2, Th9;
now assume A33:
i in (Lin J) + (Lin {u1,v1})
;
:: thesis: contradictionreconsider IV =
I as
Subset of
V by A3, XBOOLE_1:1;
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 A37:
W1 is
Subspace of
(Lin J) + (Lin {u1,v1})
by A24, Th6;
Lin {u1,v1} is
Subspace of
(Lin J) + (Lin {u1,v1})
by VECTSP_5:11;
then A38:
W1 + (Lin {u1,v1}) is
Subspace of
(Lin J) + (Lin {u1,v1})
by A37, VECTSP_5:40;
A39:
(0). V is
Subspace of
W1 /\ (Lin {u1,v1})
by VECTSP_4:50;
the
carrier of
(W1 /\ (Lin {u1,v1})) c= the
carrier of
((0). V)
proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( 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}))
;
:: thesis: a in the carrier of ((0). V)
then
a in W1 /\ (Lin {u1,v1})
by STRUCT_0:def 5;
then
(
a in W1 &
a in Lin {u1,v1} )
by VECTSP_5:7;
then
(
a in W1 &
a in Lin {u,v} )
by VECTSP_9:21;
then
(
a in W1 &
a in the
carrier of
VectSpStr(# the
carrier of
T,the
U5 of
T,the
U2 of
T,the
lmult of
T #) )
by A14, STRUCT_0:def 5;
then
(
a in W1 &
a in T )
by STRUCT_0:def 5;
then
a in W1 /\ T
by VECTSP_5:7;
hence
a in the
carrier of
((0). V)
by A21, STRUCT_0:def 5;
:: thesis: verum
end; then
W1 /\ (Lin {u1,v1}) is
Subspace of
(0). V
by VECTSP_4:35;
then
dim (W1 + (Lin {u1,v1})) = (dim W1) + 2
by A14, A22, A23, A28, A39, Th15, VECTSP_4:33;
then
((dim W1) + 1) + 1
<= (dim W1) + 1
by A30, A38, VECTSP_9:29;
hence
contradiction
by NAT_1:13;
:: thesis: verum end; hence
contradiction
by A31, A32, VECTSP_4:16;
:: thesis: verum end; hence
the
carrier of
(PencilSpace V,k) <> B
by A2, A30, VECTSP_9:def 3;
:: thesis: 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;
:: thesis: verum
end;