let K be Ring; :: thesis: for V being LeftMod of K
for A, A1, A2 being Subset of V st A is base & A = A1 \/ A2 & A1 misses A2 holds
V is_the_direct_sum_of Lin A1, Lin A2
let V be LeftMod of K; :: thesis: for A, A1, A2 being Subset of V st A is base & A = A1 \/ A2 & A1 misses A2 holds
V is_the_direct_sum_of Lin A1, Lin A2
let A, A1, A2 be Subset of V; :: thesis: ( A is base & A = A1 \/ A2 & A1 misses A2 implies V is_the_direct_sum_of Lin A1, Lin A2 )
assume that
A1: A is base and
A2: A = A1 \/ A2 and
A3: A1 misses A2 ; :: thesis: V is_the_direct_sum_of Lin A1, Lin A2
set W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #);
A4: A is linearly-independent by A1, VECTSP_7:def 3;
Lin A = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by A1, VECTSP_7:def 3;
then A5: ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (Lin A1) + (Lin A2) by A2, MOD_3:12;
(Lin A1) /\ (Lin A2) = (0). V by A2, A3, A4, Th5;
hence V is_the_direct_sum_of Lin A1, Lin A2 by A5, VECTSP_5:def 4; :: thesis: verum