Theorem isdrngrd

Description: Properties that characterize a division ring among rings: it should be nonzero, have no nonzero zero-divisors, and every nonzero element x should have a right-inverse I ( x ) . See isdrngd for the characterization using left-inverses. (Contributed by NM, 10-Aug-2013) Remove hypothesis. (Revised by SN, 19-Feb-2025)

	Ref	Expression
Hypotheses	isdrngd.b	$$⊢\phi \to B={\mathrm{Base}}_R$$
	isdrngd.t	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_R$$
	isdrngd.z	$$⊢\phi \to \underset{\dot{}}{0}=0_R$$
	isdrngd.u	$$⊢\phi \to \underset{\dot{}}{1}=1_R$$
	isdrngd.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	isdrngd.n	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\right)\to x\underset{\dot{}}{·}y\ne \underset{\dot{}}{0}$$
	isdrngd.o	$$⊢\phi \to \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$
	isdrngd.i	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)\to I\in B$$
	isdrngrd.k	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)\to x\underset{\dot{}}{·}I=\underset{\dot{}}{1}$$
Assertion	isdrngrd	$$⊢\phi \to R\in \mathrm{DivRing}$$

Proof

Step	Hyp	Ref	Expression
1		isdrngd.b	$$⊢\phi \to B={\mathrm{Base}}_R$$
2		isdrngd.t	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_R$$
3		isdrngd.z	$$⊢\phi \to \underset{\dot{}}{0}=0_R$$
4		isdrngd.u	$$⊢\phi \to \underset{\dot{}}{1}=1_R$$
5		isdrngd.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		isdrngd.n	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\right)\to x\underset{\dot{}}{·}y\ne \underset{\dot{}}{0}$$
7		isdrngd.o	$$⊢\phi \to \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$
8		isdrngd.i	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)\to I\in B$$
9		isdrngrd.k	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)\to x\underset{\dot{}}{·}I=\underset{\dot{}}{1}$$
10		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
11		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
12	10 11	opprbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{opp}_r\left(R\right)}$$
13	1 12	eqtrdi	$$⊢\phi \to B={\mathrm{Base}}_{{opp}_r\left(R\right)}$$
14		eqidd	$$⊢\phi \to {\cdot }_{{opp}_r\left(R\right)}={\cdot }_{{opp}_r\left(R\right)}$$
15		eqid	$$⊢0_R=0_R$$
16	10 15	oppr0	$$⊢0_R=0_{{opp}_r\left(R\right)}$$
17	3 16	eqtrdi	$$⊢\phi \to \underset{\dot{}}{0}=0_{{opp}_r\left(R\right)}$$
18		eqid	$$⊢1_R=1_R$$
19	10 18	oppr1	$$⊢1_R=1_{{opp}_r\left(R\right)}$$
20	4 19	eqtrdi	$$⊢\phi \to \underset{\dot{}}{1}=1_{{opp}_r\left(R\right)}$$
21	10	opprring	$$⊢R\in \mathrm{Ring}\to {opp}_r\left(R\right)\in \mathrm{Ring}$$
22	5 21	syl	$$⊢\phi \to {opp}_r\left(R\right)\in \mathrm{Ring}$$
23		eleq1w	$$⊢y=x\to \left(y\in B\leftrightarrow x\in B\right)$$
24		neeq1	$$⊢y=x\to \left(y\ne \underset{\dot{}}{0}\leftrightarrow x\ne \underset{\dot{}}{0}\right)$$
25	23 24	anbi12d	$$⊢y=x\to \left(\left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\leftrightarrow \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)$$
26	25	3anbi2d	$$⊢y=x\to \left(\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\leftrightarrow \left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\right)$$
27		oveq1	$$⊢y=x\to y{\cdot }_{{opp}_r\left(R\right)}z=x{\cdot }_{{opp}_r\left(R\right)}z$$
28	27	neeq1d	$$⊢y=x\to \left(y{\cdot }_{{opp}_r\left(R\right)}z\ne \underset{\dot{}}{0}\leftrightarrow x{\cdot }_{{opp}_r\left(R\right)}z\ne \underset{\dot{}}{0}\right)$$
29	26 28	imbi12d	$$⊢y=x\to \left(\left(\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to y{\cdot }_{{opp}_r\left(R\right)}z\ne \underset{\dot{}}{0}\right)\leftrightarrow \left(\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to x{\cdot }_{{opp}_r\left(R\right)}z\ne \underset{\dot{}}{0}\right)\right)$$
30		eleq1w	$$⊢x=z\to \left(x\in B\leftrightarrow z\in B\right)$$
31		neeq1	$$⊢x=z\to \left(x\ne \underset{\dot{}}{0}\leftrightarrow z\ne \underset{\dot{}}{0}\right)$$
32	30 31	anbi12d	$$⊢x=z\to \left(\left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\leftrightarrow \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)$$
33	32	3anbi3d	$$⊢x=z\to \left(\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)\leftrightarrow \left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\right)$$
34		oveq2	$$⊢x=z\to y{\cdot }_{{opp}_r\left(R\right)}x=y{\cdot }_{{opp}_r\left(R\right)}z$$
35	34	neeq1d	$$⊢x=z\to \left(y{\cdot }_{{opp}_r\left(R\right)}x\ne \underset{\dot{}}{0}\leftrightarrow y{\cdot }_{{opp}_r\left(R\right)}z\ne \underset{\dot{}}{0}\right)$$
36	33 35	imbi12d	$$⊢x=z\to \left(\left(\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)\to y{\cdot }_{{opp}_r\left(R\right)}x\ne \underset{\dot{}}{0}\right)\leftrightarrow \left(\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to y{\cdot }_{{opp}_r\left(R\right)}z\ne \underset{\dot{}}{0}\right)\right)$$
37	2	3ad2ant1	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\right)\to \underset{\dot{}}{·}={\cdot }_R$$
38	37	oveqd	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\right)\to x\underset{\dot{}}{·}y=x{\cdot }_{R}y$$
39		eqid	$$⊢{\cdot }_R={\cdot }_R$$
40		eqid	$$⊢{\cdot }_{{opp}_r\left(R\right)}={\cdot }_{{opp}_r\left(R\right)}$$
41	11 39 10 40	opprmul	$$⊢y{\cdot }_{{opp}_r\left(R\right)}x=x{\cdot }_{R}y$$
42	38 41	eqtr4di	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\right)\to x\underset{\dot{}}{·}y=y{\cdot }_{{opp}_r\left(R\right)}x$$
43	42 6	eqnetrrd	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\right)\to y{\cdot }_{{opp}_r\left(R\right)}x\ne \underset{\dot{}}{0}$$
44	43	3com23	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)\to y{\cdot }_{{opp}_r\left(R\right)}x\ne \underset{\dot{}}{0}$$
45	36 44	chvarvv	$$⊢\left(\phi \wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to y{\cdot }_{{opp}_r\left(R\right)}z\ne \underset{\dot{}}{0}$$
46	29 45	chvarvv	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to x{\cdot }_{{opp}_r\left(R\right)}z\ne \underset{\dot{}}{0}$$
47	11 39 10 40	opprmul	$$⊢I{\cdot }_{{opp}_r\left(R\right)}x=x{\cdot }_{R}I$$
48	2	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)\to \underset{\dot{}}{·}={\cdot }_R$$
49	48	oveqd	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)\to x\underset{\dot{}}{·}I=x{\cdot }_{R}I$$
50	49 9	eqtr3d	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)\to x{\cdot }_{R}I=\underset{\dot{}}{1}$$
51	47 50	eqtrid	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)\to I{\cdot }_{{opp}_r\left(R\right)}x=\underset{\dot{}}{1}$$
52	13 14 17 20 22 46 7 8 51	isdrngd	$$⊢\phi \to {opp}_r\left(R\right)\in \mathrm{DivRing}$$
53	10	opprdrng	$$⊢R\in \mathrm{DivRing}\leftrightarrow {opp}_r\left(R\right)\in \mathrm{DivRing}$$
54	52 53	sylibr	$$⊢\phi \to R\in \mathrm{DivRing}$$