let K be Ring; 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; 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; ( 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
; 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; verum