lincscmcl

Description: The multiplication of a linear combination with a scalar is a linear combination, see also the proof in Lang p. 129. (Contributed by AV, 11-Apr-2019) (Proof shortened by AV, 28-Jul-2019)

	Ref	Expression
Hypotheses	lincscmcl.s	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
	lincscmcl.r	$⊢ R = {Base}_{Scalar (M)}$
Assertion	lincscmcl	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R \land D \in (M LinCo V)) \to C \underset{˙}{\cdot} D \in (M LinCo V)$

Proof

Step	Hyp	Ref	Expression
1		lincscmcl.s	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
2		lincscmcl.r	$⊢ R = {Base}_{Scalar (M)}$
3		eqid	$⊢ {Base}_{M} = {Base}_{M}$
4		eqid	$⊢ Scalar (M) = Scalar (M)$
5	3 4 2	lcoval	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to (D \in (M LinCo V) \leftrightarrow (D \in {Base}_{M} \land \exists x \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)))$
6	5	adantr	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \to (D \in (M LinCo V) \leftrightarrow (D \in {Base}_{M} \land \exists x \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)))$
7		simpl	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to M \in LMod$
8	7	ad2antrr	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \land (D \in {Base}_{M} \land \exists x \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \to M \in LMod$
9		simpr	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \to C \in R$
10	9	adantr	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \land (D \in {Base}_{M} \land \exists x \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \to C \in R$
11		simprl	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \land (D \in {Base}_{M} \land \exists x \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \to D \in {Base}_{M}$
12	3 4 1 2	lmodvscl	$⊢ (M \in LMod \land C \in R \land D \in {Base}_{M}) \to C \underset{˙}{\cdot} D \in {Base}_{M}$
13	8 10 11 12	syl3anc	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \land (D \in {Base}_{M} \land \exists x \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \to C \underset{˙}{\cdot} D \in {Base}_{M}$
14	4	lmodring	$⊢ M \in LMod \to Scalar (M) \in Ring$
15	14	ad2antrr	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \to Scalar (M) \in Ring$
16	15	adantl	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to Scalar (M) \in Ring$
17	16	adantr	$⊢ ((((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \land v \in V) \to Scalar (M) \in Ring$
18	9	adantl	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to C \in R$
19	18	adantr	$⊢ ((((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \land v \in V) \to C \in R$
20		elmapi	$⊢ x \in (R^{V}) \to x : V ⟶ R$
21		ffvelrn	$⊢ (x : V ⟶ R \land v \in V) \to x (v) \in R$
22	21	ex	$⊢ x : V ⟶ R \to (v \in V \to x (v) \in R)$
23	20 22	syl	$⊢ x \in (R^{V}) \to (v \in V \to x (v) \in R)$
24	23	adantr	$⊢ (x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to (v \in V \to x (v) \in R)$
25	24	ad2antrr	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to (v \in V \to x (v) \in R)$
26	25	imp	$⊢ ((((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \land v \in V) \to x (v) \in R$
27		eqid	$⊢ \cdot_{Scalar (M)} = \cdot_{Scalar (M)}$
28	2 27	ringcl	$⊢ (Scalar (M) \in Ring \land C \in R \land x (v) \in R) \to C \cdot_{Scalar (M)} x (v) \in R$
29	17 19 26 28	syl3anc	$⊢ ((((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \land v \in V) \to C \cdot_{Scalar (M)} x (v) \in R$
30	29	fmpttd	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to (v \in V ⟼ C \cdot_{Scalar (M)} x (v)) : V ⟶ R$
31	2	fvexi	$⊢ R \in V$
32		simpr	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to V \in 𝒫 {Base}_{M}$
33	32	adantr	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \to V \in 𝒫 {Base}_{M}$
34	33	adantl	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to V \in 𝒫 {Base}_{M}$
35		elmapg	$⊢ (R \in V \land V \in 𝒫 {Base}_{M}) \to ((v \in V ⟼ C \cdot_{Scalar (M)} x (v)) \in (R^{V}) \leftrightarrow (v \in V ⟼ C \cdot_{Scalar (M)} x (v)) : V ⟶ R)$
36	31 34 35	sylancr	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to ((v \in V ⟼ C \cdot_{Scalar (M)} x (v)) \in (R^{V}) \leftrightarrow (v \in V ⟼ C \cdot_{Scalar (M)} x (v)) : V ⟶ R)$
37	30 36	mpbird	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to (v \in V ⟼ C \cdot_{Scalar (M)} x (v)) \in (R^{V})$
38	15 33 9	3jca	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \to (Scalar (M) \in Ring \land V \in 𝒫 {Base}_{M} \land C \in R)$
39	38	adantl	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to (Scalar (M) \in Ring \land V \in 𝒫 {Base}_{M} \land C \in R)$
40		simpl	$⊢ (x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to x \in (R^{V})$
41	40	ad2antrr	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to x \in (R^{V})$
42		simprl	$⊢ (x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to {finSupp}_{0_{Scalar (M)}} (x)$
43	42	ad2antrr	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to {finSupp}_{0_{Scalar (M)}} (x)$
44	2	rmfsupp	$⊢ ((Scalar (M) \in Ring \land V \in 𝒫 {Base}_{M} \land C \in R) \land x \in (R^{V}) \land {finSupp}_{0_{Scalar (M)}} (x)) \to {finSupp}_{0_{Scalar (M)}} ((v \in V ⟼ C \cdot_{Scalar (M)} x (v)))$
45	39 41 43 44	syl3anc	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to {finSupp}_{0_{Scalar (M)}} ((v \in V ⟼ C \cdot_{Scalar (M)} x (v)))$
46		oveq2	$⊢ D = x linC (M) V \to C \underset{˙}{\cdot} D = C \underset{˙}{\cdot} (x linC (M) V)$
47	46	adantl	$⊢ ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V) \to C \underset{˙}{\cdot} D = C \underset{˙}{\cdot} (x linC (M) V)$
48	47	adantl	$⊢ (x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to C \underset{˙}{\cdot} D = C \underset{˙}{\cdot} (x linC (M) V)$
49	48	ad2antrr	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to C \underset{˙}{\cdot} D = C \underset{˙}{\cdot} (x linC (M) V)$
50		simprl	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to (M \in LMod \land V \in 𝒫 {Base}_{M})$
51	40	adantr	$⊢ ((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \to x \in (R^{V})$
52	51 9	anim12i	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to (x \in (R^{V}) \land C \in R)$
53		eqid	$⊢ x linC (M) V = x linC (M) V$
54		eqid	$⊢ (v \in V ⟼ C \cdot_{Scalar (M)} x (v)) = (v \in V ⟼ C \cdot_{Scalar (M)} x (v))$
55	1 27 53 2 54	lincscm	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land (x \in (R^{V}) \land C \in R) \land {finSupp}_{0_{Scalar (M)}} (x)) \to C \underset{˙}{\cdot} (x linC (M) V) = (v \in V ⟼ C \cdot_{Scalar (M)} x (v)) linC (M) V$
56	50 52 43 55	syl3anc	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to C \underset{˙}{\cdot} (x linC (M) V) = (v \in V ⟼ C \cdot_{Scalar (M)} x (v)) linC (M) V$
57	49 56	eqtrd	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to C \underset{˙}{\cdot} D = (v \in V ⟼ C \cdot_{Scalar (M)} x (v)) linC (M) V$
58		breq1	$⊢ s = (v \in V ⟼ C \cdot_{Scalar (M)} x (v)) \to ({finSupp}_{0_{Scalar (M)}} (s) \leftrightarrow {finSupp}_{0_{Scalar (M)}} ((v \in V ⟼ C \cdot_{Scalar (M)} x (v))))$
59		oveq1	$⊢ s = (v \in V ⟼ C \cdot_{Scalar (M)} x (v)) \to s linC (M) V = (v \in V ⟼ C \cdot_{Scalar (M)} x (v)) linC (M) V$
60	59	eqeq2d	$⊢ s = (v \in V ⟼ C \cdot_{Scalar (M)} x (v)) \to (C \underset{˙}{\cdot} D = s linC (M) V \leftrightarrow C \underset{˙}{\cdot} D = (v \in V ⟼ C \cdot_{Scalar (M)} x (v)) linC (M) V)$
61	58 60	anbi12d	$⊢ s = (v \in V ⟼ C \cdot_{Scalar (M)} x (v)) \to (({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{\cdot} D = s linC (M) V) \leftrightarrow ({finSupp}_{0_{Scalar (M)}} ((v \in V ⟼ C \cdot_{Scalar (M)} x (v))) \land C \underset{˙}{\cdot} D = (v \in V ⟼ C \cdot_{Scalar (M)} x (v)) linC (M) V))$
62	61	rspcev	$⊢ ((v \in V ⟼ C \cdot_{Scalar (M)} x (v)) \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} ((v \in V ⟼ C \cdot_{Scalar (M)} x (v))) \land C \underset{˙}{\cdot} D = (v \in V ⟼ C \cdot_{Scalar (M)} x (v)) linC (M) V)) \to \exists s \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{\cdot} D = s linC (M) V)$
63	37 45 57 62	syl12anc	$⊢ (((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \land ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R)) \to \exists s \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{\cdot} D = s linC (M) V)$
64	63	ex	$⊢ ((x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \land D \in {Base}_{M}) \to (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \to \exists s \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{\cdot} D = s linC (M) V))$
65	64	ex	$⊢ (x \in (R^{V}) \land ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to (D \in {Base}_{M} \to (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \to \exists s \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{\cdot} D = s linC (M) V)))$
66	65	rexlimiva	$⊢ \exists x \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V) \to (D \in {Base}_{M} \to (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \to \exists s \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{\cdot} D = s linC (M) V)))$
67	66	impcom	$⊢ (D \in {Base}_{M} \land \exists x \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \to \exists s \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{\cdot} D = s linC (M) V))$
68	67	impcom	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \land (D \in {Base}_{M} \land \exists x \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \to \exists s \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{\cdot} D = s linC (M) V)$
69	3 4 2	lcoval	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M}) \to (C \underset{˙}{\cdot} D \in (M LinCo V) \leftrightarrow (C \underset{˙}{\cdot} D \in {Base}_{M} \land \exists s \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{\cdot} D = s linC (M) V)))$
70	69	ad2antrr	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \land (D \in {Base}_{M} \land \exists x \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \to (C \underset{˙}{\cdot} D \in (M LinCo V) \leftrightarrow (C \underset{˙}{\cdot} D \in {Base}_{M} \land \exists s \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (s) \land C \underset{˙}{\cdot} D = s linC (M) V)))$
71	13 68 70	mpbir2and	$⊢ (((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \land (D \in {Base}_{M} \land \exists x \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V))) \to C \underset{˙}{\cdot} D \in (M LinCo V)$
72	71	ex	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \to ((D \in {Base}_{M} \land \exists x \in (R^{V}) ({finSupp}_{0_{Scalar (M)}} (x) \land D = x linC (M) V)) \to C \underset{˙}{\cdot} D \in (M LinCo V))$
73	6 72	sylbid	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R) \to (D \in (M LinCo V) \to C \underset{˙}{\cdot} D \in (M LinCo V))$
74	73	3impia	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land C \in R \land D \in (M LinCo V)) \to C \underset{˙}{\cdot} D \in (M LinCo V)$

Metamath Proof Explorer

Theorem lincscmcl

Proof