lincsumcl - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > lincsumcl		Structured version Visualization version GIF version

Theorem lincsumcl 44840

Description: The sum of two linear combinations is a linear combination, see also the proof in [Lang] p. 129. (Contributed by AV, 4-Apr-2019.) (Proof shortened by AV, 28-Jul-2019.)

**Hypothesis**
Ref	Expression
lincsumcl.b	⊢ + = (+_g‘𝑀)

**Assertion**
Ref	Expression
lincsumcl	⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐶 ∈ (𝑀 LinCo 𝑉) ∧ 𝐷 ∈ (𝑀 LinCo 𝑉))) → (𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉))

Proof of Theorem lincsumcl Dummy variables 𝑠 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2798	. . . . 5 ⊢ (Base‘𝑀) = (Base‘𝑀)
2		eqid 2798	. . . . 5 ⊢ (Scalar‘𝑀) = (Scalar‘𝑀)
3		eqid 2798	. . . . 5 ⊢ (Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀))
4	1, 2, 3	lcoval 44821	. . . 4 ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐶 ∈ (𝑀 LinCo 𝑉) ↔ (𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉)))))
5	1, 2, 3	lcoval 44821	. . . 4 ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝐷 ∈ (𝑀 LinCo 𝑉) ↔ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))))
6	4, 5	anbi12d 633	. . 3 ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ((𝐶 ∈ (𝑀 LinCo 𝑉) ∧ 𝐷 ∈ (𝑀 LinCo 𝑉)) ↔ ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))))
7		simpll 766	. . . . . 6 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → 𝑀 ∈ LMod)
8		simpll 766	. . . . . . 7 ⊢ (((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → 𝐶 ∈ (Base‘𝑀))
9	8	adantl 485	. . . . . 6 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → 𝐶 ∈ (Base‘𝑀))
10		simprl 770	. . . . . . 7 ⊢ (((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → 𝐷 ∈ (Base‘𝑀))
11	10	adantl 485	. . . . . 6 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → 𝐷 ∈ (Base‘𝑀))
12		lincsumcl.b	. . . . . . 7 ⊢ + = (+_g‘𝑀)
13	1, 12	lmodvacl 19641	. . . . . 6 ⊢ ((𝑀 ∈ LMod ∧ 𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀)) → (𝐶 + 𝐷) ∈ (Base‘𝑀))
14	7, 9, 11, 13	syl3anc 1368	. . . . 5 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → (𝐶 + 𝐷) ∈ (Base‘𝑀))
15	2	lmodfgrp 19636	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ LMod → (Scalar‘𝑀) ∈ Grp)
16		grpmnd 18102	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Scalar‘𝑀) ∈ Grp → (Scalar‘𝑀) ∈ Mnd)
17	15, 16	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ LMod → (Scalar‘𝑀) ∈ Mnd)
18	17	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (Scalar‘𝑀) ∈ Mnd)
19	18	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (Scalar‘𝑀) ∈ Mnd)
20		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → 𝑉 ∈ 𝒫 (Base‘𝑀))
21	20	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → 𝑉 ∈ 𝒫 (Base‘𝑀))
22		simpll 766	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) → 𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉))
23		simpl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉))
24	22, 23	anim12i 615	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → (𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)))
25	24	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)))
26		eqid 2798	. . . . . . . . . . . . . . . . 17 ⊢ (+_g‘(Scalar‘𝑀)) = (+_g‘(Scalar‘𝑀))
27	3, 26	ofaddmndmap 44745	. . . . . . . . . . . . . . . 16 ⊢ (((Scalar‘𝑀) ∈ Mnd ∧ 𝑉 ∈ 𝒫 (Base‘𝑀) ∧ (𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉))) → (𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥) ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉))
28	19, 21, 25, 27	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥) ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉))
29	17	anim1i 617	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ((Scalar‘𝑀) ∈ Mnd ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)))
30	29	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → ((Scalar‘𝑀) ∈ Mnd ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)))
31		simprl 770	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → 𝑦 finSupp (0_g‘(Scalar‘𝑀)))
32	31	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) → 𝑦 finSupp (0_g‘(Scalar‘𝑀)))
33		simprl 770	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → 𝑥 finSupp (0_g‘(Scalar‘𝑀)))
34	32, 33	anim12i 615	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝑥 finSupp (0_g‘(Scalar‘𝑀))))
35	34	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝑥 finSupp (0_g‘(Scalar‘𝑀))))
36	3	mndpfsupp 44778	. . . . . . . . . . . . . . . 16 ⊢ ((((Scalar‘𝑀) ∈ Mnd ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝑥 finSupp (0_g‘(Scalar‘𝑀)))) → (𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥) finSupp (0_g‘(Scalar‘𝑀)))
37	30, 25, 35, 36	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥) finSupp (0_g‘(Scalar‘𝑀)))
38		oveq12 7144	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐶 = (𝑦( linC ‘𝑀)𝑉) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))
39	38	expcom 417	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐷 = (𝑥( linC ‘𝑀)𝑉) → (𝐶 = (𝑦( linC ‘𝑀)𝑉) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉))))
40	39	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)) → (𝐶 = (𝑦( linC ‘𝑀)𝑉) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉))))
41	40	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 = (𝑦( linC ‘𝑀)𝑉) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉))))
42	41	com12 32	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐶 = (𝑦( linC ‘𝑀)𝑉) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉))))
43	42	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉)) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉))))
44	43	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉))))
45	44	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉))))
46	45	imp 410	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))
47	46	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝐶 + 𝐷) = ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)))
48		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)))
49		eqid 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦( linC ‘𝑀)𝑉) = (𝑦( linC ‘𝑀)𝑉)
50		eqid 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥( linC ‘𝑀)𝑉) = (𝑥( linC ‘𝑀)𝑉)
51	12, 49, 50, 2, 3, 26	lincsum 44838	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ 𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝑥 finSupp (0_g‘(Scalar‘𝑀)))) → ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)) = ((𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉))
52	48, 25, 35, 51	syl3anc 1368	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → ((𝑦( linC ‘𝑀)𝑉) + (𝑥( linC ‘𝑀)𝑉)) = ((𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉))
53	47, 52	eqtrd 2833	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → (𝐶 + 𝐷) = ((𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉))
54		breq1 5033	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥) → (𝑠 finSupp (0_g‘(Scalar‘𝑀)) ↔ (𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥) finSupp (0_g‘(Scalar‘𝑀))))
55		oveq1 7142	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = (𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥) → (𝑠( linC ‘𝑀)𝑉) = ((𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉))
56	55	eqeq2d 2809	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = (𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥) → ((𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉) ↔ (𝐶 + 𝐷) = ((𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉)))
57	54, 56	anbi12d 633	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = (𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥) → ((𝑠 finSupp (0_g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)) ↔ ((𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥) finSupp (0_g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = ((𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉))))
58	57	rspcev 3571	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥) ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ ((𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥) finSupp (0_g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = ((𝑦 ∘_f (+_g‘(Scalar‘𝑀))𝑥)( linC ‘𝑀)𝑉))) → ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑠 finSupp (0_g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))
59	28, 37, 53, 58	syl12anc 835	. . . . . . . . . . . . . 14 ⊢ (((((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀))) ∧ (𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) ∧ (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) → ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑠 finSupp (0_g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))
60	59	exp41 438	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → ((𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀)) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑠 finSupp (0_g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))))))
61	60	rexlimiva 3240	. . . . . . . . . . . 12 ⊢ (∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉)) → ((𝐶 ∈ (Base‘𝑀) ∧ 𝐷 ∈ (Base‘𝑀)) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑠 finSupp (0_g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))))))
62	61	expd 419	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉)) → (𝐶 ∈ (Base‘𝑀) → (𝐷 ∈ (Base‘𝑀) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑠 finSupp (0_g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))))))
63	62	impcom 411	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → (𝐷 ∈ (Base‘𝑀) → ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑠 finSupp (0_g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))))))
64	63	com13 88	. . . . . . . . 9 ⊢ ((𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉) ∧ (𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → (𝐷 ∈ (Base‘𝑀) → ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑠 finSupp (0_g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))))))
65	64	rexlimiva 3240	. . . . . . . 8 ⊢ (∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)) → (𝐷 ∈ (Base‘𝑀) → ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑠 finSupp (0_g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))))))
66	65	impcom 411	. . . . . . 7 ⊢ ((𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))) → ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑠 finSupp (0_g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))))
67	66	impcom 411	. . . . . 6 ⊢ (((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑠 finSupp (0_g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉))))
68	67	impcom 411	. . . . 5 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑠 finSupp (0_g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))
69	1, 2, 3	lcoval 44821	. . . . . 6 ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ((𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉) ↔ ((𝐶 + 𝐷) ∈ (Base‘𝑀) ∧ ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑠 finSupp (0_g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))))
70	69	adantr 484	. . . . 5 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → ((𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉) ↔ ((𝐶 + 𝐷) ∈ (Base‘𝑀) ∧ ∃𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑠 finSupp (0_g‘(Scalar‘𝑀)) ∧ (𝐶 + 𝐷) = (𝑠( linC ‘𝑀)𝑉)))))
71	14, 68, 70	mpbir2and 712	. . . 4 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ ((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉))))) → (𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉))
72	71	ex 416	. . 3 ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (((𝐶 ∈ (Base‘𝑀) ∧ ∃𝑦 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑦 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐶 = (𝑦( linC ‘𝑀)𝑉))) ∧ (𝐷 ∈ (Base‘𝑀) ∧ ∃𝑥 ∈ ((Base‘(Scalar‘𝑀)) ↑_m 𝑉)(𝑥 finSupp (0_g‘(Scalar‘𝑀)) ∧ 𝐷 = (𝑥( linC ‘𝑀)𝑉)))) → (𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉)))
73	6, 72	sylbid 243	. 2 ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ((𝐶 ∈ (𝑀 LinCo 𝑉) ∧ 𝐷 ∈ (𝑀 LinCo 𝑉)) → (𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉)))
74	73	imp 410	1 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) ∧ (𝐶 ∈ (𝑀 LinCo 𝑉) ∧ 𝐷 ∈ (𝑀 LinCo 𝑉))) → (𝐶 + 𝐷) ∈ (𝑀 LinCo 𝑉))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ∃wrex 3107 𝒫 cpw 4497 class class class wbr 5030 ‘cfv 6324 (class class class)co 7135 ∘_f cof 7387 ↑_m cmap 8389 finSupp cfsupp 8817 Basecbs 16475 +_gcplusg 16557 Scalarcsca 16560 0_gc0g 16705 Mndcmnd 17903 Grpcgrp 18095 LModclmod 19627 linC clinc 44813 LinCo clinco 44814

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-se 5479 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-isom 6333 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-of 7389 df-om 7561 df-1st 7671 df-2nd 7672 df-supp 7814 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-oadd 8089 df-er 8272 df-map 8391 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-fsupp 8818 df-oi 8958 df-card 9352 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-nn 11626 df-2 11688 df-n0 11886 df-z 11970 df-uz 12232 df-fz 12886 df-fzo 13029 df-seq 13365 df-hash 13687 df-ndx 16478 df-slot 16479 df-base 16481 df-sets 16482 df-ress 16483 df-plusg 16570 df-0g 16707 df-gsum 16708 df-mgm 17844 df-sgrp 17893 df-mnd 17904 df-submnd 17949 df-grp 18098 df-minusg 18099 df-cntz 18439 df-cmn 18900 df-abl 18901 df-mgp 19233 df-ur 19245 df-ring 19292 df-lmod 19629 df-linc 44815 df-lco 44816

This theorem is referenced by: lincsumscmcl 44842

W3C validator