clmzlmvsca

Description: The scalar product of a subcomplex module matches the scalar product of the derived ZZ -module, which implies, together with zlmbas and zlmplusg , that any module over ZZ is structure-equivalent to the canonical ZZ -module ZModG . (Contributed by Mario Carneiro, 30-Oct-2015)

	Ref	Expression
Hypotheses	zlmclm.w	$⊢ W = ℤMod (G)$
	clmzlmvsca.x	$⊢ X = {Base}_{G}$
Assertion	clmzlmvsca	$⊢ (G \in CMod \land (A \in ℤ \land B \in X)) \to A \cdot_{G} B = A \cdot_{W} B$

Proof

Step	Hyp	Ref	Expression
1		zlmclm.w	$⊢ W = ℤMod (G)$
2		clmzlmvsca.x	$⊢ X = {Base}_{G}$
3		eqid	$⊢ \cdot_{G} = \cdot_{G}$
4	1 3	zlmvsca	$⊢ \cdot_{G} = \cdot_{W}$
5	4	eqcomi	$⊢ \cdot_{W} = \cdot_{G}$
6		eqid	$⊢ \cdot_{G} = \cdot_{G}$
7	2 5 6	clmmulg	$⊢ (G \in CMod \land A \in ℤ \land B \in X) \to A \cdot_{W} B = A \cdot_{G} B$
8	7	eqcomd	$⊢ (G \in CMod \land A \in ℤ \land B \in X) \to A \cdot_{G} B = A \cdot_{W} B$
9	8	3expb	$⊢ (G \in CMod \land (A \in ℤ \land B \in X)) \to A \cdot_{G} B = A \cdot_{W} B$

Metamath Proof Explorer

Theorem clmzlmvsca

Proof