isdrng5

Description: A division ring is a ring in which 1 =/= 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by AV, 23-Jul-2026)

	Ref	Expression
Hypotheses	isdrng3.b	$⊢ B = {Base}_{R}$
	isdrng3.0	$⊢ \underset{˙}{0} = 0_{R}$
	isdrng3.1	$⊢ \underset{˙}{1} = 1_{R}$
	isdrng3.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	isdrng5	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1})$

Proof

Step	Hyp	Ref	Expression
1		isdrng3.b	$⊢ B = {Base}_{R}$
2		isdrng3.0	$⊢ \underset{˙}{0} = 0_{R}$
3		isdrng3.1	$⊢ \underset{˙}{1} = 1_{R}$
4		isdrng3.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5	1 2 3 4	isdrng3	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1})$
6		eldifi	$⊢ x \in (B ∖ \{\underset{˙}{0}\}) \to x \in B$
7		difss	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq B$
8		ssrexv	$⊢ B ∖ \{\underset{˙}{0}\} \subseteq B \to (\exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1} \to \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1})$
9	7 8	ax-mp	$⊢ \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1} \to \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1}$
10	1 4 2	ringlz	$⊢ (R \in Ring \land x \in B) \to \underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0}$
11		oveq1	$⊢ y = \underset{˙}{0} \to y \underset{˙}{\cdot} x = \underset{˙}{0} \underset{˙}{\cdot} x$
12	11	eqeq1d	$⊢ y = \underset{˙}{0} \to (y \underset{˙}{\cdot} x = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0})$
13	10 12	syl5ibrcom	$⊢ (R \in Ring \land x \in B) \to (y = \underset{˙}{0} \to y \underset{˙}{\cdot} x = \underset{˙}{0})$
14	13	necon3d	$⊢ (R \in Ring \land x \in B) \to (y \underset{˙}{\cdot} x \neq \underset{˙}{0} \to y \neq \underset{˙}{0})$
15		neeq1	$⊢ y \underset{˙}{\cdot} x = \underset{˙}{1} \to (y \underset{˙}{\cdot} x \neq \underset{˙}{0} \leftrightarrow \underset{˙}{1} \neq \underset{˙}{0})$
16	15	biimparc	$⊢ (\underset{˙}{1} \neq \underset{˙}{0} \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to y \underset{˙}{\cdot} x \neq \underset{˙}{0}$
17	14 16	impel	$⊢ ((R \in Ring \land x \in B) \land (\underset{˙}{1} \neq \underset{˙}{0} \land y \underset{˙}{\cdot} x = \underset{˙}{1})) \to y \neq \underset{˙}{0}$
18	17	an4s	$⊢ ((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \land (x \in B \land y \underset{˙}{\cdot} x = \underset{˙}{1})) \to y \neq \underset{˙}{0}$
19	18	anassrs	$⊢ (((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to y \neq \underset{˙}{0}$
20		pm3.2	$⊢ y \in B \to (y \neq \underset{˙}{0} \to (y \in B \land y \neq \underset{˙}{0}))$
21	19 20	syl5com	$⊢ (((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to (y \in B \to (y \in B \land y \neq \underset{˙}{0}))$
22		eldifsn	$⊢ y \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (y \in B \land y \neq \underset{˙}{0})$
23	21 22	imbitrrdi	$⊢ (((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in B) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to (y \in B \to y \in (B ∖ \{\underset{˙}{0}\}))$
24	23	imdistanda	$⊢ ((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in B) \to ((y \underset{˙}{\cdot} x = \underset{˙}{1} \land y \in B) \to (y \underset{˙}{\cdot} x = \underset{˙}{1} \land y \in (B ∖ \{\underset{˙}{0}\})))$
25		ancom	$⊢ (y \in B \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \leftrightarrow (y \underset{˙}{\cdot} x = \underset{˙}{1} \land y \in B)$
26		ancom	$⊢ (y \in (B ∖ \{\underset{˙}{0}\}) \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \leftrightarrow (y \underset{˙}{\cdot} x = \underset{˙}{1} \land y \in (B ∖ \{\underset{˙}{0}\}))$
27	24 25 26	3imtr4g	$⊢ ((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in B) \to ((y \in B \land y \underset{˙}{\cdot} x = \underset{˙}{1}) \to (y \in (B ∖ \{\underset{˙}{0}\}) \land y \underset{˙}{\cdot} x = \underset{˙}{1}))$
28	27	reximdv2	$⊢ ((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in B) \to (\exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1} \to \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1})$
29	9 28	impbid2	$⊢ ((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in B) \to (\exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1} \leftrightarrow \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1})$
30	6 29	sylan2	$⊢ ((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \land x \in (B ∖ \{\underset{˙}{0}\})) \to (\exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1} \leftrightarrow \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1})$
31	30	ralbidva	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \to (\forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1} \leftrightarrow \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1})$
32	31	pm5.32i	$⊢ ((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \leftrightarrow ((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1})$
33		df-3an	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \leftrightarrow ((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1})$
34		df-3an	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1}) \leftrightarrow ((R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0}) \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1})$
35	32 33 34	3bitr4i	$⊢ (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}) \leftrightarrow (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1})$
36	5 35	bitri	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in B y \underset{˙}{\cdot} x = \underset{˙}{1})$

Metamath Proof Explorer

Theorem isdrng5

Proof