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

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