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	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
	isdrngd.t	⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
	isdrngd.z	⊢ ( 𝜑 → 0 = ( 0g ‘ 𝑅 ) )
	isdrngd.u	⊢ ( 𝜑 → 1 = ( 1r ‘ 𝑅 ) )
	isdrngd.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	isdrngd.n	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
	isdrngd.o	⊢ ( 𝜑 → 1 ≠ 0 )
	isdrngd.i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 𝐼 ∈ 𝐵 )
	isdrngrd.k	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑥 · 𝐼 ) = 1 )
Assertion	isdrngrd	⊢ ( 𝜑 → 𝑅 ∈ DivRing )

Proof

Step	Hyp	Ref	Expression
1		isdrngd.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
2		isdrngd.t	⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
3		isdrngd.z	⊢ ( 𝜑 → 0 = ( 0g ‘ 𝑅 ) )
4		isdrngd.u	⊢ ( 𝜑 → 1 = ( 1r ‘ 𝑅 ) )
5		isdrngd.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		isdrngd.n	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
7		isdrngd.o	⊢ ( 𝜑 → 1 ≠ 0 )
8		isdrngd.i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 𝐼 ∈ 𝐵 )
9		isdrngrd.k	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑥 · 𝐼 ) = 1 )
10		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
11		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12	10 11	opprbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑅 ) )
13	1 12	eqtrdi	⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( oppr ‘ 𝑅 ) ) )
14		eqidd	⊢ ( 𝜑 → ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) ) )
15		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
16	10 15	oppr0	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ ( oppr ‘ 𝑅 ) )
17	3 16	eqtrdi	⊢ ( 𝜑 → 0 = ( 0g ‘ ( oppr ‘ 𝑅 ) ) )
18		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
19	10 18	oppr1	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ ( oppr ‘ 𝑅 ) )
20	4 19	eqtrdi	⊢ ( 𝜑 → 1 = ( 1r ‘ ( oppr ‘ 𝑅 ) ) )
21	10	opprring	⊢ ( 𝑅 ∈ Ring → ( oppr ‘ 𝑅 ) ∈ Ring )
22	5 21	syl	⊢ ( 𝜑 → ( oppr ‘ 𝑅 ) ∈ Ring )
23		eleq1w	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) )
24		neeq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≠ 0 ↔ 𝑥 ≠ 0 ) )
25	23 24	anbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) )
26	25	3anbi2d	⊢ ( 𝑦 = 𝑥 → ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) ↔ ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) ) )
27		oveq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) = ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) )
28	27	neeq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ↔ ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) )
29	26 28	imbi12d	⊢ ( 𝑦 = 𝑥 → ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) ↔ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) ) )
30		eleq1w	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵 ) )
31		neeq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≠ 0 ↔ 𝑧 ≠ 0 ) )
32	30 31	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ↔ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) )
33	32	3anbi3d	⊢ ( 𝑥 = 𝑧 → ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) ↔ ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) ) )
34		oveq2	⊢ ( 𝑥 = 𝑧 → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) )
35	34	neeq1d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) ≠ 0 ↔ ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) )
36	33 35	imbi12d	⊢ ( 𝑥 = 𝑧 → ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) ≠ 0 ) ↔ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) ) )
37	2	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → · = ( .r ‘ 𝑅 ) )
38	37	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) )
39		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
40		eqid	⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
41	11 39 10 40	opprmul	⊢ ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 )
42	38 41	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) = ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) )
43	42 6	eqnetrrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) ≠ 0 )
44	43	3com23	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) ≠ 0 )
45	36 44	chvarvv	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 )
46	29 45	chvarvv	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 )
47	11 39 10 40	opprmul	⊢ ( 𝐼 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝐼 )
48	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → · = ( .r ‘ 𝑅 ) )
49	48	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑥 · 𝐼 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝐼 ) )
50	49 9	eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝐼 ) = 1 )
51	47 50	eqtrid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝐼 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = 1 )
52	13 14 17 20 22 46 7 8 51	isdrngd	⊢ ( 𝜑 → ( oppr ‘ 𝑅 ) ∈ DivRing )
53	10	opprdrng	⊢ ( 𝑅 ∈ DivRing ↔ ( oppr ‘ 𝑅 ) ∈ DivRing )
54	52 53	sylibr	⊢ ( 𝜑 → 𝑅 ∈ DivRing )