let GF be Field; :: thesis: for V being finite-dimensional VectSp of GF
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
dim V = (dim W1) + (dim W2)
let V be finite-dimensional VectSp of GF; :: thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
dim V = (dim W1) + (dim W2)
let W1, W2 be Subspace of V; :: thesis: ( V is_the_direct_sum_of W1,W2 implies dim V = (dim W1) + (dim W2) )
assume V is_the_direct_sum_of W1,W2 ; :: thesis: dim V = (dim W1) + (dim W2)
then A1: ( VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult of V #) = W1 + W2 & W1 /\ W2 = (0). V ) by VECTSP_5:def 4;
then (Omega). (W1 /\ W2) = (0). V by VECTSP_4:def 4
.= (0). (W1 /\ W2) by VECTSP_4:47 ;
then dim (W1 /\ W2) = 0 by Th33;
then (dim W1) + (dim W2) = (dim (W1 + W2)) + 0 by Th36
.= dim ((Omega). V) by A1, VECTSP_4:def 4
.= dim V by Th31 ;
hence dim V = (dim W1) + (dim W2) ; :: thesis: verum