Theorem ringidmlem

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

	Ref	Expression
Hypotheses	rngidm.b	$$⊢B={\mathrm{Base}}_R$$
	rngidm.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rngidm.u	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	ringidmlem	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}X=X\wedge X\underset{\dot{}}{·}\underset{\dot{}}{1}=X\right)$$

Proof

Step	Hyp	Ref	Expression
1		rngidm.b	$$⊢B={\mathrm{Base}}_R$$
2		rngidm.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		rngidm.u	$$⊢\underset{\dot{}}{1}=1_R$$
4		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
5	4	ringmgp	$$⊢R\in \mathrm{Ring}\to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
6	4 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
7	4 2	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_R}$$
8	4 3	ringidval	$$⊢\underset{\dot{}}{1}=0_{{\mathrm{mulGrp}}_R}$$
9	6 7 8	mndlrid	$$⊢\left({\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge X\in B\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}X=X\wedge X\underset{\dot{}}{·}\underset{\dot{}}{1}=X\right)$$
10	5 9	sylan	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}X=X\wedge X\underset{\dot{}}{·}\underset{\dot{}}{1}=X\right)$$