This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem srgidmlem

Description: Lemma for srglidm and srgridm . (Contributed by NM, 15-Sep-2011) (Revised by Mario Carneiro, 27-Dec-2014) (Revised by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Hypotheses srgidm.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
srgidm.t ⊢ · = ( .r ‘ 𝑅 )
srgidm.u ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion srgidmlem ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) → ( ( 1 · 𝑋 ) = 𝑋 ∧ ( 𝑋 · 1 ) = 𝑋 ) )

Proof

Step Hyp Ref Expression
1 srgidm.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 srgidm.t ⊢ · = ( .r ‘ 𝑅 )
3 srgidm.u ⊢ 1 = ( 1r ‘ 𝑅 )
4 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
5 4 srgmgp ⊢ ( 𝑅 ∈ SRing → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
6 4 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
7 4 2 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
8 4 3 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
9 6 7 8 mndlrid ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝑋 ∈ 𝐵 ) → ( ( 1 · 𝑋 ) = 𝑋 ∧ ( 𝑋 · 1 ) = 𝑋 ) )
10 5 9 sylan ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) → ( ( 1 · 𝑋 ) = 𝑋 ∧ ( 𝑋 · 1 ) = 𝑋 ) )