isdrng4

Description: A division ring is a ring in which 1 =/= 0 and every nonzero element has a left and right inverse. (Contributed by Thierry Arnoux, 2-Mar-2025)

	Ref	Expression
Hypotheses	isdrng4.b	$⊢ B = {Base}_{R}$
	isdrng4.0	$⊢ \underset{˙}{0} = 0_{R}$
	isdrng4.1	$⊢ \underset{˙}{1} = 1_{R}$
	isdrng4.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	isdrng4.u	$⊢ U = Unit (R)$
	isdrng4.r	$⊢ φ \to R \in Ring$
Assertion	isdrng4	$⊢ φ \to (R \in DivRing \leftrightarrow (\underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1})))$

Proof

Step	Hyp	Ref	Expression
1		isdrng4.b	$⊢ B = {Base}_{R}$
2		isdrng4.0	$⊢ \underset{˙}{0} = 0_{R}$
3		isdrng4.1	$⊢ \underset{˙}{1} = 1_{R}$
4		isdrng4.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		isdrng4.u	$⊢ U = Unit (R)$
6		isdrng4.r	$⊢ φ \to R \in Ring$
7	1 5 2	isdrng	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land U = B ∖ \{\underset{˙}{0}\})$
8	6	biantrurd	$⊢ φ \to (U = B ∖ \{\underset{˙}{0}\} \leftrightarrow (R \in Ring \land U = B ∖ \{\underset{˙}{0}\}))$
9	7 8	bitr4id	$⊢ φ \to (R \in DivRing \leftrightarrow U = B ∖ \{\underset{˙}{0}\})$
10	5 3	1unit	$⊢ R \in Ring \to \underset{˙}{1} \in U$
11	6 10	syl	$⊢ φ \to \underset{˙}{1} \in U$
12	11	adantr	$⊢ (φ \land U = B ∖ \{\underset{˙}{0}\}) \to \underset{˙}{1} \in U$
13		simpr	$⊢ (φ \land U = B ∖ \{\underset{˙}{0}\}) \to U = B ∖ \{\underset{˙}{0}\}$
14	12 13	eleqtrd	$⊢ (φ \land U = B ∖ \{\underset{˙}{0}\}) \to \underset{˙}{1} \in (B ∖ \{\underset{˙}{0}\})$
15		eldifsni	$⊢ \underset{˙}{1} \in (B ∖ \{\underset{˙}{0}\}) \to \underset{˙}{1} \neq \underset{˙}{0}$
16	14 15	syl	$⊢ (φ \land U = B ∖ \{\underset{˙}{0}\}) \to \underset{˙}{1} \neq \underset{˙}{0}$
17		simpll	$⊢ ((φ \land U = B ∖ \{\underset{˙}{0}\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to φ$
18	13	eleq2d	$⊢ (φ \land U = B ∖ \{\underset{˙}{0}\}) \to (x \in U \leftrightarrow x \in (B ∖ \{\underset{˙}{0}\}))$
19	18	biimpar	$⊢ ((φ \land U = B ∖ \{\underset{˙}{0}\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to x \in U$
20	6	ad5antr	$⊢ (((((φ \land x \in U) \land y \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \land z \in B) \land x \underset{˙}{\cdot} z = \underset{˙}{1}) \to R \in Ring$
21	1 5	unitcl	$⊢ x \in U \to x \in B$
22	21	ad5antlr	$⊢ (((((φ \land x \in U) \land y \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \land z \in B) \land x \underset{˙}{\cdot} z = \underset{˙}{1}) \to x \in B$
23		simp-4r	$⊢ (((((φ \land x \in U) \land y \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \land z \in B) \land x \underset{˙}{\cdot} z = \underset{˙}{1}) \to y \in B$
24		simplr	$⊢ (((((φ \land x \in U) \land y \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \land z \in B) \land x \underset{˙}{\cdot} z = \underset{˙}{1}) \to z \in B$
25		simpllr	$⊢ (((((φ \land x \in U) \land y \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \land z \in B) \land x \underset{˙}{\cdot} z = \underset{˙}{1}) \to y \underset{˙}{\cdot} x = \underset{˙}{1}$
26		simpr	$⊢ (((((φ \land x \in U) \land y \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \land z \in B) \land x \underset{˙}{\cdot} z = \underset{˙}{1}) \to x \underset{˙}{\cdot} z = \underset{˙}{1}$
27	1 2 3 4 5 20 22 23 24 25 26	ringinveu	$⊢ (((((φ \land x \in U) \land y \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \land z \in B) \land x \underset{˙}{\cdot} z = \underset{˙}{1}) \to z = y$
28	27	oveq2d	$⊢ (((((φ \land x \in U) \land y \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \land z \in B) \land x \underset{˙}{\cdot} z = \underset{˙}{1}) \to x \underset{˙}{\cdot} z = x \underset{˙}{\cdot} y$
29	28 26	eqtr3d	$⊢ (((((φ \land x \in U) \land y \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \land z \in B) \land x \underset{˙}{\cdot} z = \underset{˙}{1}) \to x \underset{˙}{\cdot} y = \underset{˙}{1}$
30	21	ad3antlr	$⊢ (((φ \land x \in U) \land y \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to x \in B$
31		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
32		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
33		eqid	$⊢ ∥_{r} ({opp}_{r} (R)) = ∥_{r} ({opp}_{r} (R))$
34	5 3 31 32 33	isunit	$⊢ x \in U \leftrightarrow (x ∥_{r} (R) \underset{˙}{1} \land x ∥_{r} ({opp}_{r} (R)) \underset{˙}{1})$
35	34	simprbi	$⊢ x \in U \to x ∥_{r} ({opp}_{r} (R)) \underset{˙}{1}$
36	35	ad3antlr	$⊢ (((φ \land x \in U) \land y \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to x ∥_{r} ({opp}_{r} (R)) \underset{˙}{1}$
37	32 1	opprbas	$⊢ B = {Base}_{{opp}_{r} (R)}$
38		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
39	37 33 38	dvdsr2	$⊢ x \in B \to (x ∥_{r} ({opp}_{r} (R)) \underset{˙}{1} \leftrightarrow \exists y \in B y \cdot_{{opp}_{r} (R)} x = \underset{˙}{1})$
40	39	biimpa	$⊢ (x \in B \land x ∥_{r} ({opp}_{r} (R)) \underset{˙}{1}) \to \exists y \in B y \cdot_{{opp}_{r} (R)} x = \underset{˙}{1}$
41	1 4 32 38	opprmul	$⊢ y \cdot_{{opp}_{r} (R)} x = x \underset{˙}{\cdot} y$
42	41	eqeq1i	$⊢ y \cdot_{{opp}_{r} (R)} x = \underset{˙}{1} \leftrightarrow x \underset{˙}{\cdot} y = \underset{˙}{1}$
43	42	rexbii	$⊢ \exists y \in B y \cdot_{{opp}_{r} (R)} x = \underset{˙}{1} \leftrightarrow \exists y \in B x \underset{˙}{\cdot} y = \underset{˙}{1}$
44	40 43	sylib	$⊢ (x \in B \land x ∥_{r} ({opp}_{r} (R)) \underset{˙}{1}) \to \exists y \in B x \underset{˙}{\cdot} y = \underset{˙}{1}$
45		oveq2	$⊢ y = z \to x \underset{˙}{\cdot} y = x \underset{˙}{\cdot} z$
46	45	eqeq1d	$⊢ y = z \to (x \underset{˙}{\cdot} y = \underset{˙}{1} \leftrightarrow x \underset{˙}{\cdot} z = \underset{˙}{1})$
47	46	cbvrexvw	$⊢ \exists y \in B x \underset{˙}{\cdot} y = \underset{˙}{1} \leftrightarrow \exists z \in B x \underset{˙}{\cdot} z = \underset{˙}{1}$
48	44 47	sylib	$⊢ (x \in B \land x ∥_{r} ({opp}_{r} (R)) \underset{˙}{1}) \to \exists z \in B x \underset{˙}{\cdot} z = \underset{˙}{1}$
49	30 36 48	syl2anc	$⊢ (((φ \land x \in U) \land y \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to \exists z \in B x \underset{˙}{\cdot} z = \underset{˙}{1}$
50	29 49	r19.29a	$⊢ (((φ \land x \in U) \land y \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to x \underset{˙}{\cdot} y = \underset{˙}{1}$
51		simpr	$⊢ (((φ \land x \in U) \land y \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to y \underset{˙}{\cdot} x = \underset{˙}{1}$
52	50 51	jca	$⊢ (((φ \land x \in U) \land y \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1})$
53	52	anasss	$⊢ ((φ \land x \in U) \land (y \in B \land y \underset{˙}{\cdot} x = \underset{˙}{1})) \to (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1})$
54	21	adantl	$⊢ (φ \land x \in U) \to x \in B$
55	34	simplbi	$⊢ x \in U \to x ∥_{r} (R) \underset{˙}{1}$
56	55	adantl	$⊢ (φ \land x \in U) \to x ∥_{r} (R) \underset{˙}{1}$
57	1 31 4	dvdsr2	$⊢ x \in B \to (x ∥_{r} (R) \underset{˙}{1} \leftrightarrow \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1})$
58	57	biimpa	$⊢ (x \in B \land x ∥_{r} (R) \underset{˙}{1}) \to \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1}$
59	54 56 58	syl2anc	$⊢ (φ \land x \in U) \to \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1}$
60	53 59	reximddv	$⊢ (φ \land x \in U) \to \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1})$
61	17 19 60	syl2anc	$⊢ ((φ \land U = B ∖ \{\underset{˙}{0}\}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1})$
62	61	ralrimiva	$⊢ (φ \land U = B ∖ \{\underset{˙}{0}\}) \to \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1})$
63	16 62	jca	$⊢ (φ \land U = B ∖ \{\underset{˙}{0}\}) \to (\underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1}))$
64	1 5	unitss	$⊢ U \subseteq B$
65	64	a1i	$⊢ (φ \land (\underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1}))) \to U \subseteq B$
66	6	adantr	$⊢ (φ \land (\underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1}))) \to R \in Ring$
67		simprl	$⊢ (φ \land (\underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1}))) \to \underset{˙}{1} \neq \underset{˙}{0}$
68	5 2 3	0unit	$⊢ R \in Ring \to (\underset{˙}{0} \in U \leftrightarrow \underset{˙}{1} = \underset{˙}{0})$
69	68	necon3bbid	$⊢ R \in Ring \to (\neg \underset{˙}{0} \in U \leftrightarrow \underset{˙}{1} \neq \underset{˙}{0})$
70	69	biimpar	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \to \neg \underset{˙}{0} \in U$
71	66 67 70	syl2anc	$⊢ (φ \land (\underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1}))) \to \neg \underset{˙}{0} \in U$
72		ssdifsn	$⊢ U \subseteq B ∖ \{\underset{˙}{0}\} \leftrightarrow (U \subseteq B \land \neg \underset{˙}{0} \in U)$
73	65 71 72	sylanbrc	$⊢ (φ \land (\underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1}))) \to U \subseteq B ∖ \{\underset{˙}{0}\}$
74		simplr	$⊢ (((φ \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1})) \to x \in (B ∖ \{\underset{˙}{0}\})$
75	74	eldifad	$⊢ (((φ \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1})) \to x \in B$
76		simpr	$⊢ (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to y \underset{˙}{\cdot} x = \underset{˙}{1}$
77	76	reximi	$⊢ \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1}$
78	77	adantl	$⊢ (((φ \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1})) \to \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1}$
79	57	biimpar	$⊢ (x \in B \land \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1}) \to x ∥_{r} (R) \underset{˙}{1}$
80	75 78 79	syl2anc	$⊢ (((φ \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1})) \to x ∥_{r} (R) \underset{˙}{1}$
81		simpl	$⊢ (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to x \underset{˙}{\cdot} y = \underset{˙}{1}$
82	81	reximi	$⊢ \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to \exists y \in B x \underset{˙}{\cdot} y = \underset{˙}{1}$
83	82	adantl	$⊢ (((φ \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1})) \to \exists y \in B x \underset{˙}{\cdot} y = \underset{˙}{1}$
84	83 43	sylibr	$⊢ (((φ \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1})) \to \exists y \in B y \cdot_{{opp}_{r} (R)} x = \underset{˙}{1}$
85	39	biimpar	$⊢ (x \in B \land \exists y \in B y \cdot_{{opp}_{r} (R)} x = \underset{˙}{1}) \to x ∥_{r} ({opp}_{r} (R)) \underset{˙}{1}$
86	75 84 85	syl2anc	$⊢ (((φ \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1})) \to x ∥_{r} ({opp}_{r} (R)) \underset{˙}{1}$
87	80 86 34	sylanbrc	$⊢ (((φ \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in (B ∖ \{\underset{˙}{0}\})) \land \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1})) \to x \in U$
88	87	ex	$⊢ ((φ \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to (\exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to x \in U)$
89	88	ralimdva	$⊢ (φ \land \underset{˙}{1} \neq \underset{˙}{0}) \to (\forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to \forall x \in (B ∖ \{\underset{˙}{0}\}) x \in U)$
90	89	impr	$⊢ (φ \land (\underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1}))) \to \forall x \in (B ∖ \{\underset{˙}{0}\}) x \in U$
91		dfss3	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq U \leftrightarrow \forall x \in (B ∖ \{\underset{˙}{0}\}) x \in U$
92	90 91	sylibr	$⊢ (φ \land (\underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1}))) \to B ∖ \{\underset{˙}{0}\} \subseteq U$
93	73 92	eqssd	$⊢ (φ \land (\underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1}))) \to U = B ∖ \{\underset{˙}{0}\}$
94	63 93	impbida	$⊢ φ \to (U = B ∖ \{\underset{˙}{0}\} \leftrightarrow (\underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1})))$
95	9 94	bitrd	$⊢ φ \to (R \in DivRing \leftrightarrow (\underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B (x \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} x = \underset{˙}{1})))$

Metamath Proof Explorer

Theorem isdrng4

Proof