let F be Field; :: thesis: for V being finite-dimensional VectSp of F
for W being Subspace of V
for v, u being Vector of V st not v in W & not u in W & 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; :: thesis: for W being Subspace of V
for v, u being Vector of V st not v in W & not u in W & 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; :: thesis: for v, u being Vector of V st not v in W & not u in W & 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; :: thesis: ( not v in W & not u in W & v <> u & {v,u} is linearly-independent & W /\ (Lin {v,u}) = (0). V implies dim (W + (Lin {v,u})) = (dim W) + 2 )
assume A1: ( not v in W & not u in W & v <> u & {v,u} is linearly-independent & W /\ (Lin {v,u}) = (0). V ) ; :: thesis: dim (W + (Lin {v,u})) = (dim W) + 2
( v in {v,u} & u in {v,u} ) by TARSKI:def 2;
then ( v in Lin {v,u} & u in Lin {v,u} ) by VECTSP_7:13;
then reconsider v1 = v, u1 = u as Vector of (Lin {v,u}) by STRUCT_0:def 5;
reconsider L = {v1,u1} as linearly-independent Subset of (Lin {v,u}) by A1, VECTSP_9:16;
(Omega). (Lin {v,u}) = Lin L by VECTSP_9:21;
then A2: dim (Lin {v,u}) = 2 by A1, VECTSP_9:35;
(Omega). (W /\ (Lin {v,u})) = (0). (W /\ (Lin {v,u})) by A1, VECTSP_4:47;
then dim (W /\ (Lin {v,u})) = 0 by VECTSP_9:33;
hence dim (W + (Lin {v,u})) = (dim (W + (Lin {v,u}))) + (dim (W /\ (Lin {v,u})))
.= (dim W) + 2 by A2, VECTSP_9:36 ;
:: thesis: verum