Theorem drngid

Description: A division ring's unit is the identity element of its multiplicative group. (Contributed by NM, 7-Sep-2011)

	Ref	Expression
Hypotheses	drngid.b	$$⊢B={\mathrm{Base}}_R$$
	drngid.z	$$⊢\underset{\dot{}}{0}=0_R$$
	drngid.u	$$⊢\underset{\dot{}}{1}=1_R$$
	drngid.g	$$⊢G={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	drngid	$$⊢R\in \mathrm{DivRing}\to \underset{\dot{}}{1}=0_G$$

Proof

Step	Hyp	Ref	Expression
1		drngid.b	$$⊢B={\mathrm{Base}}_R$$
2		drngid.z	$$⊢\underset{\dot{}}{0}=0_R$$
3		drngid.u	$$⊢\underset{\dot{}}{1}=1_R$$
4		drngid.g	$$⊢G={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
5		drngring	$$⊢R\in \mathrm{DivRing}\to R\in \mathrm{Ring}$$
6		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
7		eqid	$$⊢{\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\mathrm{Unit}\left(R\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\mathrm{Unit}\left(R\right)$$
8	6 7 3	unitgrpid	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\mathrm{Unit}\left(R\right)\right)}$$
9	5 8	syl	$$⊢R\in \mathrm{DivRing}\to \underset{\dot{}}{1}=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\mathrm{Unit}\left(R\right)\right)}$$
10	1 6 2	isdrng	$$⊢R\in \mathrm{DivRing}\leftrightarrow \left(R\in \mathrm{Ring}\wedge \mathrm{Unit}\left(R\right)=B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
11	10	simprbi	$$⊢R\in \mathrm{DivRing}\to \mathrm{Unit}\left(R\right)=B\setminus \left\{\underset{\dot{}}{0}\right\}$$
12	11	oveq2d	$$⊢R\in \mathrm{DivRing}\to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\mathrm{Unit}\left(R\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
13	12 4	eqtr4di	$$⊢R\in \mathrm{DivRing}\to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\mathrm{Unit}\left(R\right)=G$$
14	13	fveq2d	$$⊢R\in \mathrm{DivRing}\to 0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\mathrm{Unit}\left(R\right)\right)}=0_G$$
15	9 14	eqtrd	$$⊢R\in \mathrm{DivRing}\to \underset{\dot{}}{1}=0_G$$