Theorem zlm1

Description: Unity element of a ZZ -module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017)

	Ref	Expression
Hypotheses	zlmlem2.1	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
	zlm1.1	⊢ 1 = ( 1r ‘ 𝐺 )
Assertion	zlm1	⊢ 1 = ( 1r ‘ 𝑊 )

Proof

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