Theorem isdrng2

Description: A division ring can equivalently be defined as a ring such that the nonzero elements form a group under multiplication (from which it follows that this is the same group as the group of units). (Contributed by Mario Carneiro, 2-Dec-2014) (Proof shortened by AV, 12-Sep-2026)

	Ref	Expression
Hypotheses	isdrng2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	isdrng2.z	⊢ 0 = ( 0g ‘ 𝑅 )
	isdrng2.g	⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
Assertion	isdrng2	⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) )

Proof

Step	Hyp	Ref	Expression
1		isdrng2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		isdrng2.z	⊢ 0 = ( 0g ‘ 𝑅 )
3		isdrng2.g	⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
4	1 2 3	drngprops	⊢ ( 𝑅 ∈ DivRing → ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) )
5		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) → 𝑅 ∈ Ring )
6		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
7	1 6	unitcl	⊢ ( 𝑥 ∈ ( Unit ‘ 𝑅 ) → 𝑥 ∈ 𝐵 )
8	7	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) → 𝑥 ∈ 𝐵 )
9		difss	⊢ ( 𝐵 ∖ { 0 } ) ⊆ 𝐵
10		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
11	10 1	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
12	3 11	ressbas2	⊢ ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 → ( 𝐵 ∖ { 0 } ) = ( Base ‘ 𝐺 ) )
13	9 12	ax-mp	⊢ ( 𝐵 ∖ { 0 } ) = ( Base ‘ 𝐺 )
14		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
15	13 14	grpidcl	⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ ( 𝐵 ∖ { 0 } ) )
16	15	ad2antlr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) → ( 0g ‘ 𝐺 ) ∈ ( 𝐵 ∖ { 0 } ) )
17	16	eldifsnbd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) → ( 0g ‘ 𝐺 ) ≠ 0 )
18		simpll	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
19	16	eldifad	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
20		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) → 𝑥 ∈ ( Unit ‘ 𝑅 ) )
21		eqid	⊢ ( /r ‘ 𝑅 ) = ( /r ‘ 𝑅 )
22		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
23	1 6 21 22	dvrcan1	⊢ ( ( 𝑅 ∈ Ring ∧ ( 0g ‘ 𝐺 ) ∈ 𝐵 ∧ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( 0g ‘ 𝐺 ) ( /r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝐺 ) )
24	18 19 20 23	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( 0g ‘ 𝐺 ) ( /r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝐺 ) )
25	1 6 21	dvrcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 0g ‘ 𝐺 ) ∈ 𝐵 ∧ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) → ( ( 0g ‘ 𝐺 ) ( /r ‘ 𝑅 ) 𝑥 ) ∈ 𝐵 )
26	18 19 20 25	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) → ( ( 0g ‘ 𝐺 ) ( /r ‘ 𝑅 ) 𝑥 ) ∈ 𝐵 )
27	1 22 2 18 26	ringrzd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( 0g ‘ 𝐺 ) ( /r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
28	17 24 27	3netr4d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( 0g ‘ 𝐺 ) ( /r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) ≠ ( ( ( 0g ‘ 𝐺 ) ( /r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 0 ) )
29		oveq2	⊢ ( 𝑥 = 0 → ( ( ( 0g ‘ 𝐺 ) ( /r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( ( ( 0g ‘ 𝐺 ) ( /r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 0 ) )
30	29	necon3i	⊢ ( ( ( ( 0g ‘ 𝐺 ) ( /r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) ≠ ( ( ( 0g ‘ 𝐺 ) ( /r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑅 ) 0 ) → 𝑥 ≠ 0 )
31	28 30	syl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) → 𝑥 ≠ 0 )
32	8 31	eldifsnd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( Unit ‘ 𝑅 ) ) → 𝑥 ∈ ( 𝐵 ∖ { 0 } ) )
33	32	ex	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) → ( 𝑥 ∈ ( Unit ‘ 𝑅 ) → 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) )
34	33	ssrdv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) → ( Unit ‘ 𝑅 ) ⊆ ( 𝐵 ∖ { 0 } ) )
35		eldifi	⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) → 𝑥 ∈ 𝐵 )
36	35	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑥 ∈ 𝐵 )
37		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
38	13 37	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝐵 ∖ { 0 } ) )
39	38	adantll	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝐵 ∖ { 0 } ) )
40	39	eldifad	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 )
41		eqid	⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
42	1 41 22	dvdsrmul	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 ) → 𝑥 ( ∥r ‘ 𝑅 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) )
43	36 40 42	syl2anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑥 ( ∥r ‘ 𝑅 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) )
44	1	fvexi	⊢ 𝐵 ∈ V
45		difexg	⊢ ( 𝐵 ∈ V → ( 𝐵 ∖ { 0 } ) ∈ V )
46	10 22	mgpplusg	⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
47	3 46	ressplusg	⊢ ( ( 𝐵 ∖ { 0 } ) ∈ V → ( .r ‘ 𝑅 ) = ( +g ‘ 𝐺 ) )
48	44 45 47	mp2b	⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝐺 )
49	13 48 14 37	grplinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝐺 ) )
50	49	adantll	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝐺 ) )
51		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
52	1 51	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
53	1 22 51	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
54	52 53	mpdan	⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
55	54	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
56		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) → 𝐺 ∈ Grp )
57	6 51	1unit	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
58	57	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
59	34 58	sseldd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) → ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ { 0 } ) )
60	13 48 14	grpid	⊢ ( ( 𝐺 ∈ Grp ∧ ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) ↔ ( 0g ‘ 𝐺 ) = ( 1r ‘ 𝑅 ) ) )
61	56 59 60	syl2anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) → ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) ↔ ( 0g ‘ 𝐺 ) = ( 1r ‘ 𝑅 ) ) )
62	55 61	mpbid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) → ( 0g ‘ 𝐺 ) = ( 1r ‘ 𝑅 ) )
63	62	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 0g ‘ 𝐺 ) = ( 1r ‘ 𝑅 ) )
64	50 63	eqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
65	43 64	breqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
66		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
67	66 1	opprbas	⊢ 𝐵 = ( Base ‘ ( oppr ‘ 𝑅 ) )
68		eqid	⊢ ( ∥r ‘ ( oppr ‘ 𝑅 ) ) = ( ∥r ‘ ( oppr ‘ 𝑅 ) )
69		eqid	⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
70	67 68 69	dvdsrmul	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 ) → 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) )
71	36 40 70	syl2anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) )
72	1 22 66 69	opprmul	⊢ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) )
73	13 48 14 37	grprinv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 ( .r ‘ 𝑅 ) ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) = ( 0g ‘ 𝐺 ) )
74	73	adantll	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 ( .r ‘ 𝑅 ) ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) = ( 0g ‘ 𝐺 ) )
75	74 63	eqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 ( .r ‘ 𝑅 ) ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) = ( 1r ‘ 𝑅 ) )
76	72 75	eqtrid	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
77	71 76	breqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) )
78	6 51 41 66 68	isunit	⊢ ( 𝑥 ∈ ( Unit ‘ 𝑅 ) ↔ ( 𝑥 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
79	65 77 78	sylanbrc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑥 ∈ ( Unit ‘ 𝑅 ) )
80	34 79	eqelssd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) → ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) )
81	1 6 2	isdrng	⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) ) )
82	5 80 81	sylanbrc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) → 𝑅 ∈ DivRing )
83	4 82	impbii	⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) )