lincscm

Description: A linear combinations multiplied with a scalar is a linear combination, see also the proof in Lang p. 129. (Contributed by AV, 9-Apr-2019) (Revised by AV, 28-Jul-2019)

	Ref	Expression
Hypotheses	lincscm.s	$⊢ \underset{˙}{∙} = \cdot_{M}$
	lincscm.t	$⊢ \underset{˙}{\cdot} = \cdot_{Scalar (M)}$
	lincscm.x	$⊢ X = A linC (M) V$
	lincscm.r	$⊢ R = {Base}_{Scalar (M)}$
	lincscm.f	$⊢ F = (x \in V ⟼ S \underset{˙}{\cdot} A (x))$
Assertion	lincscm	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to S \underset{˙}{∙} X = F linC (M) V$

Proof

Step	Hyp	Ref	Expression
1		lincscm.s	$⊢ \underset{˙}{∙} = \cdot_{M}$
2		lincscm.t	$⊢ \underset{˙}{\cdot} = \cdot_{Scalar (M)}$
3		lincscm.x	$⊢ X = A linC (M) V$
4		lincscm.r	$⊢ R = {Base}_{Scalar (M)}$
5		lincscm.f	$⊢ F = (x \in V ⟼ S \underset{˙}{\cdot} A (x))$
6		eqid	$⊢ {Base}_{M} = {Base}_{M}$
7		eqid	$⊢ Scalar (M) = Scalar (M)$
8		eqid	$⊢ 0_{M} = 0_{M}$
9		eqid	$⊢ +_{M} = +_{M}$
10		simp1l	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to M \in LMod$
11		simpr	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to V \in 𝒫 {Base}_{M}$
12	11	3ad2ant1	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to V \in 𝒫 {Base}_{M}$
13		simpr	$⊢ (A \in (R^{V}) \land S \in R) \to S \in R$
14	13	3ad2ant2	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to S \in R$
15	10	adantr	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land v \in V) \to M \in LMod$
16		elmapi	$⊢ A \in (R^{V}) \to A : V ⟶ R$
17		ffvelcdm	$⊢ (A : V ⟶ R \land v \in V) \to A (v) \in R$
18	17	ex	$⊢ A : V ⟶ R \to (v \in V \to A (v) \in R)$
19	16 18	syl	$⊢ A \in (R^{V}) \to (v \in V \to A (v) \in R)$
20	19	adantr	$⊢ (A \in (R^{V}) \land S \in R) \to (v \in V \to A (v) \in R)$
21	20	3ad2ant2	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to (v \in V \to A (v) \in R)$
22	21	imp	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land v \in V) \to A (v) \in R$
23		elelpwi	$⊢ (v \in V \land V \in 𝒫 {Base}_{M}) \to v \in {Base}_{M}$
24	23	expcom	$⊢ V \in 𝒫 {Base}_{M} \to (v \in V \to v \in {Base}_{M})$
25	24	adantl	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to (v \in V \to v \in {Base}_{M})$
26	25	3ad2ant1	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to (v \in V \to v \in {Base}_{M})$
27	26	imp	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land v \in V) \to v \in {Base}_{M}$
28		eqid	$⊢ \cdot_{M} = \cdot_{M}$
29	6 7 28 4	lmodvscl	$⊢ (M \in LMod \land A (v) \in R \land v \in {Base}_{M}) \to A (v) \cdot_{M} v \in {Base}_{M}$
30	15 22 27 29	syl3anc	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land v \in V) \to A (v) \cdot_{M} v \in {Base}_{M}$
31	7 4	scmfsupp	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land A \in (R^{V}) \land {finSupp}_{0_{Scalar (M)}} (A)) \to {finSupp}_{0_{M}} ((v \in V ⟼ A (v) \cdot_{M} v))$
32	31	3adant2r	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to {finSupp}_{0_{M}} ((v \in V ⟼ A (v) \cdot_{M} v))$
33	6 7 4 8 9 1 10 12 14 30 32	gsumvsmul	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to \underset{v \in V}{\sum_{M}} (S \underset{˙}{∙} (A (v) \cdot_{M} v)) = S \underset{˙}{∙} (\underset{v \in V}{\sum_{M}}, (A (v) \cdot_{M} v))$
34	7	lmodring	$⊢ M \in LMod \to Scalar (M) \in Ring$
35	34	adantr	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to Scalar (M) \in Ring$
36	35	3ad2ant1	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to Scalar (M) \in Ring$
37	36	adantr	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land x \in V) \to Scalar (M) \in Ring$
38	4	eleq2i	$⊢ S \in R \leftrightarrow S \in {Base}_{Scalar (M)}$
39	38	biimpi	$⊢ S \in R \to S \in {Base}_{Scalar (M)}$
40	39	adantl	$⊢ (A \in (R^{V}) \land S \in R) \to S \in {Base}_{Scalar (M)}$
41	40	3ad2ant2	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to S \in {Base}_{Scalar (M)}$
42	41	adantr	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land x \in V) \to S \in {Base}_{Scalar (M)}$
43		ffvelcdm	$⊢ (A : V ⟶ R \land x \in V) \to A (x) \in R$
44	43 4	eleqtrdi	$⊢ (A : V ⟶ R \land x \in V) \to A (x) \in {Base}_{Scalar (M)}$
45	44	ex	$⊢ A : V ⟶ R \to (x \in V \to A (x) \in {Base}_{Scalar (M)})$
46	16 45	syl	$⊢ A \in (R^{V}) \to (x \in V \to A (x) \in {Base}_{Scalar (M)})$
47	46	adantr	$⊢ (A \in (R^{V}) \land S \in R) \to (x \in V \to A (x) \in {Base}_{Scalar (M)})$
48	47	3ad2ant2	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to (x \in V \to A (x) \in {Base}_{Scalar (M)})$
49	48	imp	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land x \in V) \to A (x) \in {Base}_{Scalar (M)}$
50		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
51	50 2	ringcl	$⊢ (Scalar (M) \in Ring \land S \in {Base}_{Scalar (M)} \land A (x) \in {Base}_{Scalar (M)}) \to S \underset{˙}{\cdot} A (x) \in {Base}_{Scalar (M)}$
52	37 42 49 51	syl3anc	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land x \in V) \to S \underset{˙}{\cdot} A (x) \in {Base}_{Scalar (M)}$
53	52 5	fmptd	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to F : V ⟶ {Base}_{Scalar (M)}$
54		fvex	$⊢ {Base}_{Scalar (M)} \in V$
55		elmapg	$⊢ ({Base}_{Scalar (M)} \in V \land V \in 𝒫 {Base}_{M}) \to (F \in ({Base}_{Scalar (M)}^{V}) \leftrightarrow F : V ⟶ {Base}_{Scalar (M)})$
56	54 12 55	sylancr	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to (F \in ({Base}_{Scalar (M)}^{V}) \leftrightarrow F : V ⟶ {Base}_{Scalar (M)})$
57	53 56	mpbird	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to F \in ({Base}_{Scalar (M)}^{V})$
58		lincval	$⊢ (M \in LMod \land F \in ({Base}_{Scalar (M)}^{V}) \land V \in 𝒫 {Base}_{M}) \to F linC (M) V = \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v)$
59	10 57 12 58	syl3anc	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to F linC (M) V = \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v)$
60		simpr	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land v \in V) \to v \in V$
61		ovex	$⊢ S \underset{˙}{\cdot} A (v) \in V$
62		fveq2	$⊢ x = v \to A (x) = A (v)$
63	62	oveq2d	$⊢ x = v \to S \underset{˙}{\cdot} A (x) = S \underset{˙}{\cdot} A (v)$
64	63 5	fvmptg	$⊢ (v \in V \land S \underset{˙}{\cdot} A (v) \in V) \to F (v) = S \underset{˙}{\cdot} A (v)$
65	60 61 64	sylancl	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land v \in V) \to F (v) = S \underset{˙}{\cdot} A (v)$
66	65	oveq1d	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land v \in V) \to F (v) \cdot_{M} v = (S \underset{˙}{\cdot} A (v)) \cdot_{M} v$
67	14	adantr	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land v \in V) \to S \in R$
68	6 7 28 4 2	lmodvsass	$⊢ (M \in LMod \land (S \in R \land A (v) \in R \land v \in {Base}_{M})) \to (S \underset{˙}{\cdot} A (v)) \cdot_{M} v = S \cdot_{M} (A (v) \cdot_{M} v)$
69	15 67 22 27 68	syl13anc	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land v \in V) \to (S \underset{˙}{\cdot} A (v)) \cdot_{M} v = S \cdot_{M} (A (v) \cdot_{M} v)$
70	1	eqcomi	$⊢ \cdot_{M} = \underset{˙}{∙}$
71	70	a1i	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land v \in V) \to \cdot_{M} = \underset{˙}{∙}$
72	71	oveqd	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land v \in V) \to S \cdot_{M} (A (v) \cdot_{M} v) = S \underset{˙}{∙} (A (v) \cdot_{M} v)$
73	69 72	eqtrd	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land v \in V) \to (S \underset{˙}{\cdot} A (v)) \cdot_{M} v = S \underset{˙}{∙} (A (v) \cdot_{M} v)$
74	66 73	eqtrd	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \land v \in V) \to F (v) \cdot_{M} v = S \underset{˙}{∙} (A (v) \cdot_{M} v)$
75	74	mpteq2dva	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to (v \in V ⟼ F (v) \cdot_{M} v) = (v \in V ⟼ S \underset{˙}{∙} (A (v) \cdot_{M} v))$
76	75	oveq2d	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to \underset{v \in V}{\sum_{M}} (F (v) \cdot_{M} v) = \underset{v \in V}{\sum_{M}} (S \underset{˙}{∙} (A (v) \cdot_{M} v))$
77	59 76	eqtrd	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to F linC (M) V = \underset{v \in V}{\sum_{M}} (S \underset{˙}{∙} (A (v) \cdot_{M} v))$
78	3	a1i	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to X = A linC (M) V$
79	4	oveq1i	$⊢ R^{V} = {Base}_{Scalar (M)}^{V}$
80	79	eleq2i	$⊢ A \in (R^{V}) \leftrightarrow A \in ({Base}_{Scalar (M)}^{V})$
81	80	biimpi	$⊢ A \in (R^{V}) \to A \in ({Base}_{Scalar (M)}^{V})$
82	81	adantr	$⊢ (A \in (R^{V}) \land S \in R) \to A \in ({Base}_{Scalar (M)}^{V})$
83	82	3ad2ant2	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to A \in ({Base}_{Scalar (M)}^{V})$
84		lincval	$⊢ (M \in LMod \land A \in ({Base}_{Scalar (M)}^{V}) \land V \in 𝒫 {Base}_{M}) \to A linC (M) V = \underset{v \in V}{\sum_{M}} (A (v) \cdot_{M} v)$
85	10 83 12 84	syl3anc	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to A linC (M) V = \underset{v \in V}{\sum_{M}} (A (v) \cdot_{M} v)$
86	78 85	eqtrd	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to X = \underset{v \in V}{\sum_{M}} (A (v) \cdot_{M} v)$
87	86	oveq2d	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to S \underset{˙}{∙} X = S \underset{˙}{∙} (\underset{v \in V}{\sum_{M}}, (A (v) \cdot_{M} v))$
88	33 77 87	3eqtr4rd	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (A \in (R^{V}) \land S \in R) \land {finSupp}_{0_{Scalar (M)}} (A)) \to S \underset{˙}{∙} X = F linC (M) V$

Metamath Proof Explorer

Theorem lincscm

Proof