Theorem ringidmlem

Description: Lemma for ringlidm and ringridm . (Contributed by NM, 15-Sep-2011) (Revised by Mario Carneiro, 27-Dec-2014)

	Ref	Expression
Hypotheses	ringidm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ringidm.t	⊢ · = ( .r ‘ 𝑅 )
	ringidm.u	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	ringidmlem	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 1 · 𝑋 ) = 𝑋 ∧ ( 𝑋 · 1 ) = 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		ringidm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		ringidm.t	⊢ · = ( .r ‘ 𝑅 )
3		ringidm.u	⊢ 1 = ( 1r ‘ 𝑅 )
4		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
5	4	ringmgp	⊢ ( 𝑅 ∈ Ring → ( 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	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 1 · 𝑋 ) = 𝑋 ∧ ( 𝑋 · 1 ) = 𝑋 ) )