isdrng

Description: The predicate "is a division ring". (Contributed by NM, 18-Oct-2012) (Revised by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	isdrng.b	$⊢ B = {Base}_{R}$
	isdrng.u	$⊢ U = Unit (R)$
	isdrng.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	isdrng	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land U = B ∖ \{\underset{˙}{0}\})$

Step	Hyp	Ref	Expression
1		isdrng.b	$⊢ B = {Base}_{R}$
2		isdrng.u	$⊢ U = Unit (R)$
3		isdrng.z	$⊢ \underset{˙}{0} = 0_{R}$
4		fveq2	$⊢ r = R \to Unit (r) = Unit (R)$
5	4 2	eqtr4di	$⊢ r = R \to Unit (r) = U$
6		fveq2	$⊢ r = R \to {Base}_{r} = {Base}_{R}$
7	6 1	eqtr4di	$⊢ r = R \to {Base}_{r} = B$
8		fveq2	$⊢ r = R \to 0_{r} = 0_{R}$
9	8 3	eqtr4di	$⊢ r = R \to 0_{r} = \underset{˙}{0}$
10	9	sneqd	$⊢ r = R \to \{0_{r}\} = \{\underset{˙}{0}\}$
11	7 10	difeq12d	$⊢ r = R \to {Base}_{r} ∖ \{0_{r}\} = B ∖ \{\underset{˙}{0}\}$
12	5 11	eqeq12d	$⊢ r = R \to (Unit (r) = {Base}_{r} ∖ \{0_{r}\} \leftrightarrow U = B ∖ \{\underset{˙}{0}\})$
13		df-drng	$⊢ DivRing = \{r \in Ring \| Unit (r) = {Base}_{r} ∖ \{0_{r}\}\}$
14	12 13	elrab2	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land U = B ∖ \{\underset{˙}{0}\})$

Metamath Proof Explorer