Theorem 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=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
	clmzlmvsca.x	$$⊢X={\mathrm{Base}}_G$$
Assertion	clmzlmvsca	$$⊢\left(G\in \mathrm{CMod}\wedge \left(A\in \mathbb{Z}\wedge B\in X\right)\right)\to A{\cdot }_{G}B=A{\cdot }_{W}B$$

Proof

Step	Hyp	Ref	Expression
1		zlmclm.w	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
2		clmzlmvsca.x	$$⊢X={\mathrm{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	$$⊢\left(G\in \mathrm{CMod}\wedge A\in \mathbb{Z}\wedge B\in X\right)\to A{\cdot }_{W}B=A{\cdot }_{G}B$$
8	7	eqcomd	$$⊢\left(G\in \mathrm{CMod}\wedge A\in \mathbb{Z}\wedge B\in X\right)\to A{\cdot }_{G}B=A{\cdot }_{W}B$$
9	8	3expb	$$⊢\left(G\in \mathrm{CMod}\wedge \left(A\in \mathbb{Z}\wedge B\in X\right)\right)\to A{\cdot }_{G}B=A{\cdot }_{W}B$$