Theorem zlm0

Description: Zero of a ZZ -module. (Contributed by Thierry Arnoux, 8-Nov-2017)

	Ref	Expression
Hypotheses	zlmlem2.1	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
	zlm0.1	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	zlm0	⊢ 0 = ( 0g ‘ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		zlmlem2.1	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
2		zlm0.1	⊢ 0 = ( 0g ‘ 𝐺 )
3		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4	3	a1i	⊢ ( ⊤ → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
5	1 3	zlmbas	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝑊 )
6	5	a1i	⊢ ( ⊤ → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑊 ) )
7		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
8	1 7	zlmplusg	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝑊 )
9	8	a1i	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝑊 ) )
10	9	oveqd	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) )
11	4 6 10	grpidpropd	⊢ ( ⊤ → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝑊 ) )
12	11	mptru	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝑊 )
13	2 12	eqtri	⊢ 0 = ( 0g ‘ 𝑊 )