lincsumcl

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)

		Ref	Expression
	Hypothesis	lincsumcl.b	$⊢ \underset{˙}{+} = +_{M}$
	Assertion	lincsumcl	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (C \in (M LinCo V) \land D \in (M LinCo V))) \to C \underset{˙}{+} D \in (M LinCo V)$

Proof

Step	Hyp	Ref	Expression
1		lincsumcl.b	$⊢ \underset{˙}{+} = +_{M}$
2		eqid	$⊢ {Base}_{M} = {Base}_{M}$
3		eqid	$⊢ Scalar (M) = Scalar (M)$
4		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
5	2 3 4	lcoval	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to (C \in (M LinCo V) \leftrightarrow (C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)))$
6	2 3 4	lcoval	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to (D \in (M LinCo V) \leftrightarrow (D \in {Base}_{M} \land \exists x \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)))$
7	5 6	anbi12d	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to ((C \in (M LinCo V) \land D \in (M LinCo V)) \leftrightarrow ((C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (D \in {Base}_{M} \land \exists x \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))))$
8		simpll	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land ((C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (D \in {Base}_{M} \land \exists x \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)))) \to M \in LMod$
9		simpll	$⊢ ((C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (D \in {Base}_{M} \land \exists x \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \to C \in {Base}_{M}$
10	9	adantl	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land ((C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (D \in {Base}_{M} \land \exists x \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)))) \to C \in {Base}_{M}$
11		simprl	$⊢ ((C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (D \in {Base}_{M} \land \exists x \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \to D \in {Base}_{M}$
12	11	adantl	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land ((C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (D \in {Base}_{M} \land \exists x \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)))) \to D \in {Base}_{M}$
13	2 1	lmodvacl	$⊢ (M \in LMod \land C \in {Base}_{M} \land D \in {Base}_{M}) \to C \underset{˙}{+} D \in {Base}_{M}$
14	8 10 12 13	syl3anc	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land ((C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (D \in {Base}_{M} \land \exists x \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)))) \to C \underset{˙}{+} D \in {Base}_{M}$
15	3	lmodfgrp	$⊢ M \in LMod \to Scalar (M) \in Grp$
16	15	grpmndd	$⊢ M \in LMod \to Scalar (M) \in Mnd$
17	16	adantr	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to Scalar (M) \in Mnd$
18	17	adantl	$⊢ ((((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \land (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to Scalar (M) \in Mnd$
19		simpr	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to V \in 𝒫 {Base}_{M}$
20	19	adantl	$⊢ ((((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \land (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to V \in 𝒫 {Base}_{M}$
21		simpll	$⊢ ((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \to y \in ({Base}_{Scalar (M)}^{V})$
22		simpl	$⊢ (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to x \in ({Base}_{Scalar (M)}^{V})$
23	21 22	anim12i	$⊢ (((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \land (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \to (y \in ({Base}_{Scalar (M)}^{V}) \land x \in ({Base}_{Scalar (M)}^{V}))$
24	23	adantr	$⊢ ((((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \land (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to (y \in ({Base}_{Scalar (M)}^{V}) \land x \in ({Base}_{Scalar (M)}^{V}))$
25		eqid	$⊢ +_{Scalar (M)} = +_{Scalar (M)}$
26	4 25	ofaddmndmap	$⊢ (Scalar (M) \in Mnd \land V \in 𝒫 {Base}_{M} \land (y \in ({Base}_{Scalar (M)}^{V}) \land x \in ({Base}_{Scalar (M)}^{V}))) \to y {+_{Scalar (M)}}_{f} x \in ({Base}_{Scalar (M)}^{V})$
27	18 20 24 26	syl3anc	$⊢ ((((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \land (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to y {+_{Scalar (M)}}_{f} x \in ({Base}_{Scalar (M)}^{V})$
28	16	anim1i	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to (Scalar (M) \in Mnd \land V \in 𝒫 {Base}_{M})$
29	28	adantl	$⊢ ((((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \land (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to (Scalar (M) \in Mnd \land V \in 𝒫 {Base}_{M})$
30		simprl	$⊢ (y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \to {finSupp}_{0_{Scalar (M)}} (y)$
31	30	adantr	$⊢ ((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \to {finSupp}_{0_{Scalar (M)}} (y)$
32		simprl	$⊢ (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to {finSupp}_{0_{Scalar (M)}} (x)$
33	31 32	anim12i	$⊢ (((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \land (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \to ({finSupp}_{0_{Scalar (M)}} (y) \land {finSupp}_{0_{Scalar (M)}} (x))$
34	33	adantr	$⊢ ((((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \land (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to ({finSupp}_{0_{Scalar (M)}} (y) \land {finSupp}_{0_{Scalar (M)}} (x))$
35	4	mndpfsupp	$⊢ ((Scalar (M) \in Mnd \land V \in 𝒫 {Base}_{M}) \land (y \in ({Base}_{Scalar (M)}^{V}) \land x \in ({Base}_{Scalar (M)}^{V})) \land ({finSupp}_{0_{Scalar (M)}} (y) \land {finSupp}_{0_{Scalar (M)}} (x))) \to {finSupp}_{0_{Scalar (M)}} ((y {+_{Scalar (M)}}_{f} x))$
36	29 24 34 35	syl3anc	$⊢ ((((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \land (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to {finSupp}_{0_{Scalar (M)}} ((y {+_{Scalar (M)}}_{f} x))$
37		oveq12	$⊢ (C = y linC (M) V \land D = x linC (M) V) \to C \underset{˙}{+} D = (y linC (M) V) \underset{˙}{+} (x linC (M) V)$
38	37	expcom	$⊢ D = x linC (M) V \to (C = y linC (M) V \to C \underset{˙}{+} D = (y linC (M) V) \underset{˙}{+} (x linC (M) V))$
39	38	adantl	$⊢ ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V) \to (C = y linC (M) V \to C \underset{˙}{+} D = (y linC (M) V) \underset{˙}{+} (x linC (M) V))$
40	39	adantl	$⊢ (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to (C = y linC (M) V \to C \underset{˙}{+} D = (y linC (M) V) \underset{˙}{+} (x linC (M) V))$
41	40	com12	$⊢ C = y linC (M) V \to ((x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to C \underset{˙}{+} D = (y linC (M) V) \underset{˙}{+} (x linC (M) V))$
42	41	adantl	$⊢ ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V) \to ((x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to C \underset{˙}{+} D = (y linC (M) V) \underset{˙}{+} (x linC (M) V))$
43	42	adantl	$⊢ (y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \to ((x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to C \underset{˙}{+} D = (y linC (M) V) \underset{˙}{+} (x linC (M) V))$
44	43	adantr	$⊢ ((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \to ((x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to C \underset{˙}{+} D = (y linC (M) V) \underset{˙}{+} (x linC (M) V))$
45	44	imp	$⊢ (((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \land (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \to C \underset{˙}{+} D = (y linC (M) V) \underset{˙}{+} (x linC (M) V)$
46	45	adantr	$⊢ ((((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \land (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to C \underset{˙}{+} D = (y linC (M) V) \underset{˙}{+} (x linC (M) V)$
47		simpr	$⊢ ((((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \land (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to (M \in LMod \land V \in 𝒫 {Base}_{M})$
48		eqid	$⊢ y linC (M) V = y linC (M) V$
49		eqid	$⊢ x linC (M) V = x linC (M) V$
50	1 48 49 3 4 25	lincsum	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (y \in ({Base}_{Scalar (M)}^{V}) \land x \in ({Base}_{Scalar (M)}^{V})) \land ({finSupp}_{0_{Scalar (M)}} (y) \land {finSupp}_{0_{Scalar (M)}} (x))) \to (y linC (M) V) \underset{˙}{+} (x linC (M) V) = (y {+_{Scalar (M)}}_{f} x) linC (M) V$
51	47 24 34 50	syl3anc	$⊢ ((((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \land (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to (y linC (M) V) \underset{˙}{+} (x linC (M) V) = (y {+_{Scalar (M)}}_{f} x) linC (M) V$
52	46 51	eqtrd	$⊢ ((((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \land (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to C \underset{˙}{+} D = (y {+_{Scalar (M)}}_{f} x) linC (M) V$
53		breq1	$⊢ s = y {+_{Scalar (M)}}_{f} x \to ({finSupp}_{0_{Scalar (M)}} (s) \leftrightarrow {finSupp}_{0_{Scalar (M)}} ((y {+_{Scalar (M)}}_{f} x)))$
54		oveq1	$⊢ s = y {+_{Scalar (M)}}_{f} x \to s linC (M) V = (y {+_{Scalar (M)}}_{f} x) linC (M) V$
55	54	eqeq2d	$⊢ s = y {+_{Scalar (M)}}_{f} x \to (C \underset{˙}{+} D = s linC (M) V \leftrightarrow C \underset{˙}{+} D = (y {+_{Scalar (M)}}_{f} x) linC (M) V)$
56	53 55	anbi12d	$⊢ s = y {+_{Scalar (M)}}_{f} x \to (({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{+} D = s linC (M) V) \leftrightarrow ({finSupp}_{0_{Scalar (M)}} ((y {+_{Scalar (M)}}_{f} x)) \land C \underset{˙}{+} D = (y {+_{Scalar (M)}}_{f} x) linC (M) V))$
57	56	rspcev	$⊢ (y {+_{Scalar (M)}}_{f} x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} ((y {+_{Scalar (M)}}_{f} x)) \land C \underset{˙}{+} D = (y {+_{Scalar (M)}}_{f} x) linC (M) V)) \to \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{+} D = s linC (M) V)$
58	27 36 52 57	syl12anc	$⊢ ((((y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (C \in {Base}_{M} \land D \in {Base}_{M})) \land (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \land (M \in LMod \land V \in 𝒫 {Base}_{M})) \to \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{+} D = s linC (M) V)$
59	58	exp41	$⊢ (y \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \to ((C \in {Base}_{M} \land D \in {Base}_{M}) \to ((x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to ((M \in LMod \land V \in 𝒫 {Base}_{M}) \to \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{+} D = s linC (M) V))))$
60	59	rexlimiva	$⊢ \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V) \to ((C \in {Base}_{M} \land D \in {Base}_{M}) \to ((x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to ((M \in LMod \land V \in 𝒫 {Base}_{M}) \to \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{+} D = s linC (M) V))))$
61	60	expd	$⊢ \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V) \to (C \in {Base}_{M} \to (D \in {Base}_{M} \to ((x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to ((M \in LMod \land V \in 𝒫 {Base}_{M}) \to \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{+} D = s linC (M) V)))))$
62	61	impcom	$⊢ (C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \to (D \in {Base}_{M} \to ((x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to ((M \in LMod \land V \in 𝒫 {Base}_{M}) \to \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{+} D = s linC (M) V))))$
63	62	com13	$⊢ (x \in ({Base}_{Scalar (M)}^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to (D \in {Base}_{M} \to ((C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \to ((M \in LMod \land V \in 𝒫 {Base}_{M}) \to \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{+} D = s linC (M) V))))$
64	63	rexlimiva	$⊢ \exists x \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V) \to (D \in {Base}_{M} \to ((C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \to ((M \in LMod \land V \in 𝒫 {Base}_{M}) \to \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{+} D = s linC (M) V))))$
65	64	impcom	$⊢ (D \in {Base}_{M} \land \exists x \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to ((C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \to ((M \in LMod \land V \in 𝒫 {Base}_{M}) \to \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{+} D = s linC (M) V)))$
66	65	impcom	$⊢ ((C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (D \in {Base}_{M} \land \exists x \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \to ((M \in LMod \land V \in 𝒫 {Base}_{M}) \to \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{+} D = s linC (M) V))$
67	66	impcom	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land ((C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (D \in {Base}_{M} \land \exists x \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)))) \to \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{+} D = s linC (M) V)$
68	2 3 4	lcoval	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to (C \underset{˙}{+} D \in (M LinCo V) \leftrightarrow (C \underset{˙}{+} D \in {Base}_{M} \land \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{+} D = s linC (M) V)))$
69	68	adantr	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land ((C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (D \in {Base}_{M} \land \exists x \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)))) \to (C \underset{˙}{+} D \in (M LinCo V) \leftrightarrow (C \underset{˙}{+} D \in {Base}_{M} \land \exists s \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{+} D = s linC (M) V)))$
70	14 67 69	mpbir2and	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land ((C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (D \in {Base}_{M} \land \exists x \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)))) \to C \underset{˙}{+} D \in (M LinCo V)$
71	70	ex	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to (((C \in {Base}_{M} \land \exists y \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (y) \land C = y linC (M) V)) \land (D \in {Base}_{M} \land \exists x \in ({Base}_{Scalar (M)}^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \to C \underset{˙}{+} D \in (M LinCo V))$
72	7 71	sylbid	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to ((C \in (M LinCo V) \land D \in (M LinCo V)) \to C \underset{˙}{+} D \in (M LinCo V))$
73	72	imp	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (C \in (M LinCo V) \land D \in (M LinCo V))) \to C \underset{˙}{+} D \in (M LinCo V)$

Metamath Proof Explorer

Theorem lincsumcl

Proof