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)

	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		eqid	$⊢ Unit (R) = Unit (R)$
5	1 4 2	isdrng	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land Unit (R) = B ∖ \{\underset{˙}{0}\})$
6		oveq2	$⊢ Unit (R) = B ∖ \{\underset{˙}{0}\} \to {mulGrp}_{R} ↾_{𝑠} Unit (R) = {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\})$
7	6	adantl	$⊢ (R \in Ring \land Unit (R) = B ∖ \{\underset{˙}{0}\}) \to {mulGrp}_{R} ↾_{𝑠} Unit (R) = {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\})$
8	7 3	eqtr4di	$⊢ (R \in Ring \land Unit (R) = B ∖ \{\underset{˙}{0}\}) \to {mulGrp}_{R} ↾_{𝑠} Unit (R) = G$
9		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} Unit (R) = {mulGrp}_{R} ↾_{𝑠} Unit (R)$
10	4 9	unitgrp	$⊢ R \in Ring \to {mulGrp}_{R} ↾_{𝑠} Unit (R) \in Grp$
11	10	adantr	$⊢ (R \in Ring \land Unit (R) = B ∖ \{\underset{˙}{0}\}) \to {mulGrp}_{R} ↾_{𝑠} Unit (R) \in Grp$
12	8 11	eqeltrrd	$⊢ (R \in Ring \land Unit (R) = B ∖ \{\underset{˙}{0}\}) \to G \in Grp$
13	1 4	unitcl	$⊢ x \in Unit (R) \to x \in B$
14	13	adantl	$⊢ ((R \in Ring \land G \in Grp) \land x \in Unit (R)) \to x \in B$
15		difss	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq B$
16		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
17	16 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
18	3 17	ressbas2	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq B \to B ∖ \{\underset{˙}{0}\} = {Base}_{G}$
19	15 18	ax-mp	$⊢ B ∖ \{\underset{˙}{0}\} = {Base}_{G}$
20		eqid	$⊢ 0_{G} = 0_{G}$
21	19 20	grpidcl	$⊢ G \in Grp \to 0_{G} \in (B ∖ \{\underset{˙}{0}\})$
22	21	ad2antlr	$⊢ ((R \in Ring \land G \in Grp) \land x \in Unit (R)) \to 0_{G} \in (B ∖ \{\underset{˙}{0}\})$
23		eldifsn	$⊢ 0_{G} \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (0_{G} \in B \land 0_{G} \neq \underset{˙}{0})$
24	22 23	sylib	$⊢ ((R \in Ring \land G \in Grp) \land x \in Unit (R)) \to (0_{G} \in B \land 0_{G} \neq \underset{˙}{0})$
25	24	simprd	$⊢ ((R \in Ring \land G \in Grp) \land x \in Unit (R)) \to 0_{G} \neq \underset{˙}{0}$
26		simpll	$⊢ ((R \in Ring \land G \in Grp) \land x \in Unit (R)) \to R \in Ring$
27	22	eldifad	$⊢ ((R \in Ring \land G \in Grp) \land x \in Unit (R)) \to 0_{G} \in B$
28		simpr	$⊢ ((R \in Ring \land G \in Grp) \land x \in Unit (R)) \to x \in Unit (R)$
29		eqid	$⊢ /_{r} (R) = /_{r} (R)$
30		eqid	$⊢ \cdot_{R} = \cdot_{R}$
31	1 4 29 30	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}$
32	26 27 28 31	syl3anc	$⊢ ((R \in Ring \land G \in Grp) \land x \in Unit (R)) \to (0_{G} /_{r} (R) x) \cdot_{R} x = 0_{G}$
33	1 4 29	dvrcl	$⊢ (R \in Ring \land 0_{G} \in B \land x \in Unit (R)) \to 0_{G} /_{r} (R) x \in B$
34	26 27 28 33	syl3anc	$⊢ ((R \in Ring \land G \in Grp) \land x \in Unit (R)) \to 0_{G} /_{r} (R) x \in B$
35	1 30 2	ringrz	$⊢ (R \in Ring \land 0_{G} /_{r} (R) x \in B) \to (0_{G} /_{r} (R) x) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
36	26 34 35	syl2anc	$⊢ ((R \in Ring \land G \in Grp) \land x \in Unit (R)) \to (0_{G} /_{r} (R) x) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
37	25 32 36	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}$
38		oveq2	$⊢ x = \underset{˙}{0} \to (0_{G} /_{r} (R) x) \cdot_{R} x = (0_{G} /_{r} (R) x) \cdot_{R} \underset{˙}{0}$
39	38	necon3i	$⊢ (0_{G} /_{r} (R) x) \cdot_{R} x \neq (0_{G} /_{r} (R) x) \cdot_{R} \underset{˙}{0} \to x \neq \underset{˙}{0}$
40	37 39	syl	$⊢ ((R \in Ring \land G \in Grp) \land x \in Unit (R)) \to x \neq \underset{˙}{0}$
41		eldifsn	$⊢ x \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (x \in B \land x \neq \underset{˙}{0})$
42	14 40 41	sylanbrc	$⊢ ((R \in Ring \land G \in Grp) \land x \in Unit (R)) \to x \in (B ∖ \{\underset{˙}{0}\})$
43	42	ex	$⊢ (R \in Ring \land G \in Grp) \to (x \in Unit (R) \to x \in (B ∖ \{\underset{˙}{0}\}))$
44	43	ssrdv	$⊢ (R \in Ring \land G \in Grp) \to Unit (R) \subseteq B ∖ \{\underset{˙}{0}\}$
45		eldifi	$⊢ x \in (B ∖ \{\underset{˙}{0}\}) \to x \in B$
46	45	adantl	$⊢ ((R \in Ring \land G \in Grp) \land x \in (B ∖ \{\underset{˙}{0}\})) \to x \in B$
47		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
48	19 47	grpinvcl	$⊢ (G \in Grp \land x \in (B ∖ \{\underset{˙}{0}\})) \to {inv}_{g} (G) (x) \in (B ∖ \{\underset{˙}{0}\})$
49	48	adantll	$⊢ ((R \in Ring \land G \in Grp) \land x \in (B ∖ \{\underset{˙}{0}\})) \to {inv}_{g} (G) (x) \in (B ∖ \{\underset{˙}{0}\})$
50	49	eldifad	$⊢ ((R \in Ring \land G \in Grp) \land x \in (B ∖ \{\underset{˙}{0}\})) \to {inv}_{g} (G) (x) \in B$
51		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
52	1 51 30	dvdsrmul	$⊢ (x \in B \land {inv}_{g} (G) (x) \in B) \to x ∥_{r} (R) ({inv}_{g} (G) (x) \cdot_{R} x)$
53	46 50 52	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)$
54	1	fvexi	$⊢ B \in V$
55		difexg	$⊢ B \in V \to B ∖ \{\underset{˙}{0}\} \in V$
56	16 30	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
57	3 56	ressplusg	$⊢ B ∖ \{\underset{˙}{0}\} \in V \to \cdot_{R} = +_{G}$
58	54 55 57	mp2b	$⊢ \cdot_{R} = +_{G}$
59	19 58 20 47	grplinv	$⊢ (G \in Grp \land x \in (B ∖ \{\underset{˙}{0}\})) \to {inv}_{g} (G) (x) \cdot_{R} x = 0_{G}$
60	59	adantll	$⊢ ((R \in Ring \land G \in Grp) \land x \in (B ∖ \{\underset{˙}{0}\})) \to {inv}_{g} (G) (x) \cdot_{R} x = 0_{G}$
61		eqid	$⊢ 1_{R} = 1_{R}$
62	1 61	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
63	1 30 61	ringlidm	$⊢ (R \in Ring \land 1_{R} \in B) \to 1_{R} \cdot_{R} 1_{R} = 1_{R}$
64	62 63	mpdan	$⊢ R \in Ring \to 1_{R} \cdot_{R} 1_{R} = 1_{R}$
65	64	adantr	$⊢ (R \in Ring \land G \in Grp) \to 1_{R} \cdot_{R} 1_{R} = 1_{R}$
66		simpr	$⊢ (R \in Ring \land G \in Grp) \to G \in Grp$
67	4 61	1unit	$⊢ R \in Ring \to 1_{R} \in Unit (R)$
68	67	adantr	$⊢ (R \in Ring \land G \in Grp) \to 1_{R} \in Unit (R)$
69	44 68	sseldd	$⊢ (R \in Ring \land G \in Grp) \to 1_{R} \in (B ∖ \{\underset{˙}{0}\})$
70	19 58 20	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})$
71	66 69 70	syl2anc	$⊢ (R \in Ring \land G \in Grp) \to (1_{R} \cdot_{R} 1_{R} = 1_{R} \leftrightarrow 0_{G} = 1_{R})$
72	65 71	mpbid	$⊢ (R \in Ring \land G \in Grp) \to 0_{G} = 1_{R}$
73	72	adantr	$⊢ ((R \in Ring \land G \in Grp) \land x \in (B ∖ \{\underset{˙}{0}\})) \to 0_{G} = 1_{R}$
74	60 73	eqtrd	$⊢ ((R \in Ring \land G \in Grp) \land x \in (B ∖ \{\underset{˙}{0}\})) \to {inv}_{g} (G) (x) \cdot_{R} x = 1_{R}$
75	53 74	breqtrd	$⊢ ((R \in Ring \land G \in Grp) \land x \in (B ∖ \{\underset{˙}{0}\})) \to x ∥_{r} (R) 1_{R}$
76		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
77	76 1	opprbas	$⊢ B = {Base}_{{opp}_{r} (R)}$
78		eqid	$⊢ ∥_{r} ({opp}_{r} (R)) = ∥_{r} ({opp}_{r} (R))$
79		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
80	77 78 79	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)$
81	46 50 80	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)$
82	1 30 76 79	opprmul	$⊢ {inv}_{g} (G) (x) \cdot_{{opp}_{r} (R)} x = x \cdot_{R} {inv}_{g} (G) (x)$
83	19 58 20 47	grprinv	$⊢ (G \in Grp \land x \in (B ∖ \{\underset{˙}{0}\})) \to x \cdot_{R} {inv}_{g} (G) (x) = 0_{G}$
84	83	adantll	$⊢ ((R \in Ring \land G \in Grp) \land x \in (B ∖ \{\underset{˙}{0}\})) \to x \cdot_{R} {inv}_{g} (G) (x) = 0_{G}$
85	84 73	eqtrd	$⊢ ((R \in Ring \land G \in Grp) \land x \in (B ∖ \{\underset{˙}{0}\})) \to x \cdot_{R} {inv}_{g} (G) (x) = 1_{R}$
86	82 85	syl5eq	$⊢ ((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}$
87	81 86	breqtrd	$⊢ ((R \in Ring \land G \in Grp) \land x \in (B ∖ \{\underset{˙}{0}\})) \to x ∥_{r} ({opp}_{r} (R)) 1_{R}$
88	4 61 51 76 78	isunit	$⊢ x \in Unit (R) \leftrightarrow (x ∥_{r} (R) 1_{R} \land x ∥_{r} ({opp}_{r} (R)) 1_{R})$
89	75 87 88	sylanbrc	$⊢ ((R \in Ring \land G \in Grp) \land x \in (B ∖ \{\underset{˙}{0}\})) \to x \in Unit (R)$
90	44 89	eqelssd	$⊢ (R \in Ring \land G \in Grp) \to Unit (R) = B ∖ \{\underset{˙}{0}\}$
91	12 90	impbida	$⊢ R \in Ring \to (Unit (R) = B ∖ \{\underset{˙}{0}\} \leftrightarrow G \in Grp)$
92	91	pm5.32i	$⊢ (R \in Ring \land Unit (R) = B ∖ \{\underset{˙}{0}\}) \leftrightarrow (R \in Ring \land G \in Grp)$
93	5 92	bitri	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land G \in Grp)$

Metamath Proof Explorer

Theorem isdrng2

Proof