Theorem drngid2

Description: Properties showing that an element I is the identity element of a division ring. (Contributed by Mario Carneiro, 11-Oct-2013)

	Ref	Expression
Hypotheses	drngid2.b	$$⊢B={\mathrm{Base}}_R$$
	drngid2.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	drngid2.o	$$⊢\underset{\dot{}}{0}=0_R$$
	drngid2.u	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	drngid2	$$⊢R\in \mathrm{DivRing}\to \left(\left(I\in B\wedge I\ne \underset{\dot{}}{0}\wedge I\underset{\dot{}}{·}I=I\right)\leftrightarrow \underset{\dot{}}{1}=I\right)$$

Proof

Step	Hyp	Ref	Expression
1		drngid2.b	$$⊢B={\mathrm{Base}}_R$$
2		drngid2.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		drngid2.o	$$⊢\underset{\dot{}}{0}=0_R$$
4		drngid2.u	$$⊢\underset{\dot{}}{1}=1_R$$
5		df-3an	$$⊢\left(I\in B\wedge I\ne \underset{\dot{}}{0}\wedge I\underset{\dot{}}{·}I=I\right)\leftrightarrow \left(\left(I\in B\wedge I\ne \underset{\dot{}}{0}\right)\wedge I\underset{\dot{}}{·}I=I\right)$$
6		eldifsn	$$⊢I\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(I\in B\wedge I\ne \underset{\dot{}}{0}\right)$$
7	6	anbi1i	$$⊢\left(I\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge I\underset{\dot{}}{·}I=I\right)\leftrightarrow \left(\left(I\in B\wedge I\ne \underset{\dot{}}{0}\right)\wedge I\underset{\dot{}}{·}I=I\right)$$
8	5 7	bitr4i	$$⊢\left(I\in B\wedge I\ne \underset{\dot{}}{0}\wedge I\underset{\dot{}}{·}I=I\right)\leftrightarrow \left(I\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge I\underset{\dot{}}{·}I=I\right)$$
9		eqid	$$⊢{\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
10	1 3 9	drngmgp	$$⊢R\in \mathrm{DivRing}\to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}$$
11		difss	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq B$$
12		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
13	12 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
14	9 13	ressbas2	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq B\to B\setminus \left\{\underset{\dot{}}{0}\right\}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
15	11 14	ax-mp	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
16	1	fvexi	$$⊢B\in \mathrm{V}$$
17		difexg	$$⊢B\in \mathrm{V}\to B\setminus \left\{\underset{\dot{}}{0}\right\}\in \mathrm{V}$$
18	12 2	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_R}$$
19	9 18	ressplusg	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}\in \mathrm{V}\to \underset{\dot{}}{·}={+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
20	16 17 19	mp2b	$$⊢\underset{\dot{}}{·}={+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
21		eqid	$$⊢0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
22	15 20 21	isgrpid2	$$⊢{\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\in \mathrm{Grp}\to \left(\left(I\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge I\underset{\dot{}}{·}I=I\right)\leftrightarrow 0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}=I\right)$$
23	10 22	syl	$$⊢R\in \mathrm{DivRing}\to \left(\left(I\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge I\underset{\dot{}}{·}I=I\right)\leftrightarrow 0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}=I\right)$$
24	8 23	syl5bb	$$⊢R\in \mathrm{DivRing}\to \left(\left(I\in B\wedge I\ne \underset{\dot{}}{0}\wedge I\underset{\dot{}}{·}I=I\right)\leftrightarrow 0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}=I\right)$$
25	1 3 4 9	drngid	$$⊢R\in \mathrm{DivRing}\to \underset{\dot{}}{1}=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}$$
26	25	eqeq1d	$$⊢R\in \mathrm{DivRing}\to \left(\underset{\dot{}}{1}=I\leftrightarrow 0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)}=I\right)$$
27	24 26	bitr4d	$$⊢R\in \mathrm{DivRing}\to \left(\left(I\in B\wedge I\ne \underset{\dot{}}{0}\wedge I\underset{\dot{}}{·}I=I\right)\leftrightarrow \underset{\dot{}}{1}=I\right)$$