ringidmlem

	Ref	Expression
Hypotheses	ringidm.b	$⊢ B = {Base}_{R}$
	ringidm.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	ringidm.u	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	ringidmlem	$⊢ (R \in Ring \land X \in B) \to (\underset{˙}{1} \underset{˙}{\cdot} X = X \land X \underset{˙}{\cdot} \underset{˙}{1} = X)$

Step	Hyp	Ref	Expression
1		ringidm.b	$⊢ B = {Base}_{R}$
2		ringidm.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		ringidm.u	$⊢ \underset{˙}{1} = 1_{R}$
4		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
5	4	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
6	4 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
7	4 2	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
8	4 3	ringidval	$⊢ \underset{˙}{1} = 0_{{mulGrp}_{R}}$
9	6 7 8	mndlrid	$⊢ ({mulGrp}_{R} \in Mnd \land X \in B) \to (\underset{˙}{1} \underset{˙}{\cdot} X = X \land X \underset{˙}{\cdot} \underset{˙}{1} = X)$
10	5 9	sylan	$⊢ (R \in Ring \land X \in B) \to (\underset{˙}{1} \underset{˙}{\cdot} X = X \land X \underset{˙}{\cdot} \underset{˙}{1} = X)$

Metamath Proof Explorer