let F be Field; for V being finite-dimensional VectSp of F
for W being Subspace of V
for v, u being Vector of V st v <> u & {v,u} is linearly-independent & W /\ (Lin {v,u}) = (0). V holds
dim (W + (Lin {v,u})) = (dim W) + 2
let V be finite-dimensional VectSp of F; for W being Subspace of V
for v, u being Vector of V st v <> u & {v,u} is linearly-independent & W /\ (Lin {v,u}) = (0). V holds
dim (W + (Lin {v,u})) = (dim W) + 2
let W be Subspace of V; for v, u being Vector of V st v <> u & {v,u} is linearly-independent & W /\ (Lin {v,u}) = (0). V holds
dim (W + (Lin {v,u})) = (dim W) + 2
let v, u be Vector of V; ( v <> u & {v,u} is linearly-independent & W /\ (Lin {v,u}) = (0). V implies dim (W + (Lin {v,u})) = (dim W) + 2 )
assume that
A1:
v <> u
and
A2:
{v,u} is linearly-independent
and
A3:
W /\ (Lin {v,u}) = (0). V
; dim (W + (Lin {v,u})) = (dim W) + 2
u in {v,u}
by TARSKI:def 2;
then A4:
u in Lin {v,u}
by VECTSP_7:8;
v in {v,u}
by TARSKI:def 2;
then
v in Lin {v,u}
by VECTSP_7:8;
then reconsider v1 = v, u1 = u as Vector of (Lin {v,u}) by A4;
reconsider L = {v1,u1} as linearly-independent Subset of (Lin {v,u}) by A2, VECTSP_9:12;
(Omega). (Lin {v,u}) = Lin L
by VECTSP_9:17;
then A5:
dim (Lin {v,u}) = 2
by A1, VECTSP_9:31;
(Omega). (W /\ (Lin {v,u})) = (0). (W /\ (Lin {v,u}))
by A3, VECTSP_4:36;
then
dim (W /\ (Lin {v,u})) = 0
by VECTSP_9:29;
hence dim (W + (Lin {v,u})) =
(dim (W + (Lin {v,u}))) + (dim (W /\ (Lin {v,u})))
.=
(dim W) + 2
by A5, VECTSP_9:32
;
verum