zlmvsca

Description: Scalar multiplication operation of a ZZ -module. (Contributed by Mario Carneiro, 2-Oct-2015)

Step	Hyp	Ref	Expression
1		zlmbas.w	$⊢ W = ℤMod (G)$
2		zlmvsca.2	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		ovex	$⊢ G sSet ⟨Scalar (ndx), ℤ_{ring}⟩ \in V$
4	2	fvexi	$⊢ \underset{˙}{\cdot} \in V$
5		vscaid	$⊢ \cdot_{𝑠} = Slot \cdot_{ndx}$
6	5	setsid	$⊢ (G sSet ⟨Scalar (ndx), ℤ_{ring}⟩ \in V \land \underset{˙}{\cdot} \in V) \to \underset{˙}{\cdot} = \cdot_{((G sSet ⟨Scalar (ndx), ℤ_{ring}⟩) sSet ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩)}$
7	3 4 6	mp2an	$⊢ \underset{˙}{\cdot} = \cdot_{((G sSet ⟨Scalar (ndx), ℤ_{ring}⟩) sSet ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩)}$
8	1 2	zlmval	$⊢ G \in V \to W = (G sSet ⟨Scalar (ndx), ℤ_{ring}⟩) sSet ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩$
9	8	fveq2d	$⊢ G \in V \to \cdot_{W} = \cdot_{((G sSet ⟨Scalar (ndx), ℤ_{ring}⟩) sSet ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩)}$
10	7 9	eqtr4id	$⊢ G \in V \to \underset{˙}{\cdot} = \cdot_{W}$
11	5	str0	$⊢ \emptyset = \cdot_{\emptyset}$
12		fvprc	$⊢ \neg G \in V \to \cdot_{G} = \emptyset$
13	2 12	eqtrid	$⊢ \neg G \in V \to \underset{˙}{\cdot} = \emptyset$
14		fvprc	$⊢ \neg G \in V \to ℤMod (G) = \emptyset$
15	1 14	eqtrid	$⊢ \neg G \in V \to W = \emptyset$
16	15	fveq2d	$⊢ \neg G \in V \to \cdot_{W} = \cdot_{\emptyset}$
17	11 13 16	3eqtr4a	$⊢ \neg G \in V \to \underset{˙}{\cdot} = \cdot_{W}$
18	10 17	pm2.61i	$⊢ \underset{˙}{\cdot} = \cdot_{W}$

Metamath Proof Explorer