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	$⊢ B = {Base}_{R}$
	isdrng2.z	$⊢ \underset{˙}{0} = 0_{R}$
	isdrng2.g	$⊢ G = {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\})$
Assertion	isdrng2	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land G \in Grp)$

Proof

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

Metamath Proof Explorer

Theorem isdrng2

Proof