let F be Field; for V being finite-dimensional VectSp of F
for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil (W1,W2,k) is trivial
let V be finite-dimensional VectSp of F; for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil (W1,W2,k) is trivial
let W1, W2 be Subspace of V; ( W1 is Subspace of W2 implies for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil (W1,W2,k) is trivial )
assume
W1 is Subspace of W2
; for k being Nat st (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil (W1,W2,k) is trivial
then reconsider U = W1 as Subspace of W2 ;
let k be Nat; ( (dim W1) + 1 = k & dim W2 = k + 1 implies not pencil (W1,W2,k) is trivial )
assume A1:
( (dim W1) + 1 = k & dim W2 = k + 1 )
; not pencil (W1,W2,k) is trivial
set W = the Linear_Compl of U;
A2:
W2 is_the_direct_sum_of the Linear_Compl of U,U
by VECTSP_5:def 5;
then A3:
the Linear_Compl of U /\ U = (0). W2
by VECTSP_5:def 4;
dim W2 = (dim U) + (dim the Linear_Compl of U)
by A2, VECTSP_9:34;
then consider u, v being Vector of the Linear_Compl of U such that
A4:
u <> v
and
A5:
{u,v} is linearly-independent
and
(Omega). the Linear_Compl of U = Lin {u,v}
by A1, VECTSP_9:31;
reconsider u = u, v = v as Vector of W2 by VECTSP_4:10;
reconsider u1 = u, v1 = v as Vector of V by VECTSP_4:10;
A7:
v in the Linear_Compl of U
;
A9:
u in the Linear_Compl of U
;
v in {v1}
by TARSKI:def 1;
then
v in Lin {v1}
by VECTSP_7:8;
then A11:
v in W1 + (Lin {v1})
by VECTSP_5:2;
A12:
not v in Lin {u}
by A6, VECTSP10:13;
A13:
now not W1 + (Lin {v1}) = W1 + (Lin {u1})reconsider Wx = the
Linear_Compl of
U as
Subspace of
V by VECTSP_4:26;
assume
W1 + (Lin {v1}) = W1 + (Lin {u1})
;
contradictionthen consider h,
j being
Vector of
V such that A14:
h in W1
and A15:
j in Lin {u1}
and A16:
v1 = h + j
by A11, VECTSP_5:1;
consider a being
Element of
F such that A17:
j = a * u1
by A15, VECTSP10:3;
v1 - (a * u1) = h + ((a * u1) - (a * u1))
by A16, A17, RLVECT_1:def 3;
then
v1 - (a * u1) = h + (0. V)
by RLVECT_1:15;
then A18:
v1 - (a * u1) = h
by RLVECT_1:4;
a * u = a * u1
by VECTSP_4:14;
then A19:
v1 - (a * u1) = v - (a * u)
by VECTSP_4:16;
a * u in Wx
by A9, VECTSP_4:21;
then
v - (a * u) in Wx
by A7, VECTSP_4:23;
then
v - (a * u) in the
Linear_Compl of
U /\ U
by A14, A18, A19, VECTSP_5:3;
then
v - (a * u) = 0. W2
by A3, VECTSP_4:35;
then
h = 0. V
by A18, A19, VECTSP_4:11;
then
v1 = j
by A16, RLVECT_1:4;
hence
contradiction
by A12, A15, VECTSP10:13;
verum end;
v in W2
;
then A20:
W1 + (Lin {v1}) in pencil (W1,W2,k)
by A1, A8, Th15;
u in W2
;
then
W1 + (Lin {u1}) in pencil (W1,W2,k)
by A1, A10, Th15;
then
2 c= card (pencil (W1,W2,k))
by A13, A20, PENCIL_1:2;
hence
not pencil (W1,W2,k) is trivial
by PENCIL_1:4; verum