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		grpmnd	$⊢ Scalar (M) \in Grp \to Scalar (M) \in Mnd$
17	15 16	syl	$⊢ M \in LMod \to Scalar (M) \in Mnd$
18	17	adantr	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to Scalar (M) \in Mnd$
19	18	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$
20		simpr	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to V \in 𝒫 {Base}_{M}$
21	20	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}$
22		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})$
23		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})$
24	22 23	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}))$
25	24	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}))$
26		eqid	$⊢ +_{Scalar (M)} = +_{Scalar (M)}$
27	4 26	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})$
28	19 21 25 27	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})$
29	17	anim1i	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to (Scalar (M) \in Mnd \land V \in 𝒫 {Base}_{M})$
30	29	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})$
31		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)$
32	31	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)$
33		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)$
34	32 33	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))$
35	34	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))$
36	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))$
37	30 25 35 36	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))$
38		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)$
39	38	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))$
40	39	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))$
41	40	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))$
42	41	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))$
43	42	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))$
44	43	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))$
45	44	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))$
46	45	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)$
47	46	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)$
48		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})$
49		eqid	$⊢ y linC (M) V = y linC (M) V$
50		eqid	$⊢ x linC (M) V = x linC (M) V$
51	1 49 50 3 4 26	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$
52	48 25 35 51	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$
53	47 52	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$
54		breq1	$⊢ s = y {+_{Scalar (M)}}_{f} x \to ({finSupp}_{0_{Scalar (M)}} (s) \leftrightarrow {finSupp}_{0_{Scalar (M)}} ((y {+_{Scalar (M)}}_{f} x)))$
55		oveq1	$⊢ s = y {+_{Scalar (M)}}_{f} x \to s linC (M) V = (y {+_{Scalar (M)}}_{f} x) linC (M) V$
56	55	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)$
57	54 56	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))$
58	57	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)$
59	28 37 53 58	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)$
60	59	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))))$
61	60	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))))$
62	61	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)))))$
63	62	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))))$
64	63	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))))$
65	64	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))))$
66	65	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)))$
67	66	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))$
68	67	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)$
69	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)))$
70	69	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)))$
71	14 68 70	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)$
72	71	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))$
73	7 72	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))$
74	73	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