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)

	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$$
	isdrngd.j	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)\to I\ne \underset{\dot{}}{0}$$
	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		isdrngd.j	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)\to I\ne \underset{\dot{}}{0}$$
10		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}$$
11		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
12		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
13	11 12	opprbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{opp}_r\left(R\right)}$$
14	1 13	eqtrdi	$$⊢\phi \to B={\mathrm{Base}}_{{opp}_r\left(R\right)}$$
15		eqidd	$$⊢\phi \to {\cdot }_{{opp}_r\left(R\right)}={\cdot }_{{opp}_r\left(R\right)}$$
16		eqid	$$⊢0_R=0_R$$
17	11 16	oppr0	$$⊢0_R=0_{{opp}_r\left(R\right)}$$
18	3 17	eqtrdi	$$⊢\phi \to \underset{\dot{}}{0}=0_{{opp}_r\left(R\right)}$$
19		eqid	$$⊢1_R=1_R$$
20	11 19	oppr1	$$⊢1_R=1_{{opp}_r\left(R\right)}$$
21	4 20	eqtrdi	$$⊢\phi \to \underset{\dot{}}{1}=1_{{opp}_r\left(R\right)}$$
22	11	opprring	$$⊢R\in \mathrm{Ring}\to {opp}_r\left(R\right)\in \mathrm{Ring}$$
23	5 22	syl	$$⊢\phi \to {opp}_r\left(R\right)\in \mathrm{Ring}$$
24		eleq1w	$$⊢y=x\to \left(y\in B\leftrightarrow x\in B\right)$$
25		neeq1	$$⊢y=x\to \left(y\ne \underset{\dot{}}{0}\leftrightarrow x\ne \underset{\dot{}}{0}\right)$$
26	24 25	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)$$
27	26	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)$$
28		oveq1	$$⊢y=x\to y{\cdot }_{{opp}_r\left(R\right)}z=x{\cdot }_{{opp}_r\left(R\right)}z$$
29	28	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)$$
30	27 29	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)$$
31		eleq1w	$$⊢x=z\to \left(x\in B\leftrightarrow z\in B\right)$$
32		neeq1	$$⊢x=z\to \left(x\ne \underset{\dot{}}{0}\leftrightarrow z\ne \underset{\dot{}}{0}\right)$$
33	31 32	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)$$
34	33	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)$$
35		oveq2	$$⊢x=z\to y{\cdot }_{{opp}_r\left(R\right)}x=y{\cdot }_{{opp}_r\left(R\right)}z$$
36	35	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)$$
37	34 36	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)$$
38	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$$
39	38	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$$
40		eqid	$$⊢{\cdot }_R={\cdot }_R$$
41		eqid	$$⊢{\cdot }_{{opp}_r\left(R\right)}={\cdot }_{{opp}_r\left(R\right)}$$
42	12 40 11 41	opprmul	$$⊢y{\cdot }_{{opp}_r\left(R\right)}x=x{\cdot }_{R}y$$
43	39 42	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$$
44	43 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}$$
45	44	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}$$
46	37 45	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}$$
47	30 46	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}$$
48	12 40 11 41	opprmul	$$⊢I{\cdot }_{{opp}_r\left(R\right)}x=x{\cdot }_{R}I$$
49	2	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)\to \underset{\dot{}}{·}={\cdot }_R$$
50	49	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$$
51	50 10	eqtr3d	$$⊢\left(\phi \wedge \left(x\in B\wedge x\ne \underset{\dot{}}{0}\right)\right)\to x{\cdot }_{R}I=\underset{\dot{}}{1}$$
52	48 51	syl5eq	$$⊢\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}$$
53	14 15 18 21 23 47 7 8 9 52	isdrngd	$$⊢\phi \to {opp}_r\left(R\right)\in \mathrm{DivRing}$$
54	11	opprdrng	$$⊢R\in \mathrm{DivRing}\leftrightarrow {opp}_r\left(R\right)\in \mathrm{DivRing}$$
55	53 54	sylibr	$$⊢\phi \to R\in \mathrm{DivRing}$$