Metamath Proof Explorer


Theorem zlm1

Description: Unit 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𝑊 )