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 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 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 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: ( 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 ; :: thesis: 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 ;
:: thesis: verum