Metamath Proof Explorer

Theorem isdrng3

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, 22-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	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})$

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		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) = {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\})$
6	1 2 5	isdrng2	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp)$
7	2 3	drngunz	$⊢ R \in DivRing \to \underset{˙}{1} \neq \underset{˙}{0}$
8	6 7	sylbir	$⊢ (R \in Ring \land {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp) \to \underset{˙}{1} \neq \underset{˙}{0}$
9	1 2 3 4	isdrng3lem1	$⊢ (R \in Ring \land {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp) \to \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}$
10	8 9	jca	$⊢ (R \in Ring \land {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp) \to (\underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1})$
11		3anass	$⊢ (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}))$
12	1 2 3 4	isdrng3lem2	$⊢ (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}) \to {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp$
13	11 12	sylbir	$⊢ (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})) \to {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp$
14	10 13	impbida	$⊢ R \in Ring \to ({mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp \leftrightarrow (\underset{˙}{1} \neq \underset{˙}{0} \land \forall x \in (B ∖ \{\underset{˙}{0}\}) \exists y \in (B ∖ \{\underset{˙}{0}\}) y \underset{˙}{\cdot} x = \underset{˙}{1}))$
15	14	pm5.32i	$⊢ (R \in Ring \land {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\}) \in Grp) \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}))$
16	15 6 11	3bitr4i	$⊢ 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})$