drngprops

Description: Properties of a division ring. (Contributed by NM, 4-Apr-2009) (Revised by AV, 26-Aug-2026)

	Ref	Expression
Hypotheses	isdrng2.b	$⊢ B = {Base}_{R}$
	isdrng2.z	$⊢ \underset{˙}{0} = 0_{R}$
	isdrng2.g	$⊢ G = {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\})$
Assertion	drngprops	$⊢ R \in DivRing \to (R \in Ring \land G \in Grp)$

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		simpl	$⊢ (R \in Ring \land Unit (R) = B ∖ \{\underset{˙}{0}\}) \to R \in Ring$
7		oveq2	$⊢ Unit (R) = B ∖ \{\underset{˙}{0}\} \to {mulGrp}_{R} ↾_{𝑠} Unit (R) = {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\})$
8	7	adantl	$⊢ (R \in Ring \land Unit (R) = B ∖ \{\underset{˙}{0}\}) \to {mulGrp}_{R} ↾_{𝑠} Unit (R) = {mulGrp}_{R} ↾_{𝑠} (B ∖ \{\underset{˙}{0}\})$
9	8 3	eqtr4di	$⊢ (R \in Ring \land Unit (R) = B ∖ \{\underset{˙}{0}\}) \to {mulGrp}_{R} ↾_{𝑠} Unit (R) = G$
10		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} Unit (R) = {mulGrp}_{R} ↾_{𝑠} Unit (R)$
11	4 10	unitgrp	$⊢ R \in Ring \to {mulGrp}_{R} ↾_{𝑠} Unit (R) \in Grp$
12	11	adantr	$⊢ (R \in Ring \land Unit (R) = B ∖ \{\underset{˙}{0}\}) \to {mulGrp}_{R} ↾_{𝑠} Unit (R) \in Grp$
13	9 12	eqeltrrd	$⊢ (R \in Ring \land Unit (R) = B ∖ \{\underset{˙}{0}\}) \to G \in Grp$
14	6 13	jca	$⊢ (R \in Ring \land Unit (R) = B ∖ \{\underset{˙}{0}\}) \to (R \in Ring \land G \in Grp)$
15	5 14	sylbi	$⊢ R \in DivRing \to (R \in Ring \land G \in Grp)$

Metamath Proof Explorer