srgidmlem

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

Step	Hyp	Ref	Expression
1		srgidm.b	$⊢ B = {Base}_{R}$
2		srgidm.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		srgidm.u	$⊢ \underset{˙}{1} = 1_{R}$
4		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
5	4	srgmgp	$⊢ R \in SRing \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 SRing \land X \in B) \to (\underset{˙}{1} \underset{˙}{\cdot} X = X \land X \underset{˙}{\cdot} \underset{˙}{1} = X)$

Metamath Proof Explorer