drnginvrn0

Description: The multiplicative inverse in a division ring is nonzero. ( recne0 analog). (Contributed by NM, 19-Apr-2014)

	Ref	Expression
Hypotheses	invrcl.b	$⊢ B = {Base}_{R}$
	invrcl.z	$⊢ \underset{˙}{0} = 0_{R}$
	invrcl.i	$⊢ I = {inv}_{r} (R)$
Assertion	drnginvrn0	$⊢ (R \in DivRing \land X \in B \land X \neq \underset{˙}{0}) \to I (X) \neq \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		invrcl.b	$⊢ B = {Base}_{R}$
2		invrcl.z	$⊢ \underset{˙}{0} = 0_{R}$
3		invrcl.i	$⊢ I = {inv}_{r} (R)$
4		drngring	$⊢ R \in DivRing \to R \in Ring$
5		eqid	$⊢ Unit (R) = Unit (R)$
6	5 3	unitinvcl	$⊢ (R \in Ring \land X \in Unit (R)) \to I (X) \in Unit (R)$
7	6	ex	$⊢ R \in Ring \to (X \in Unit (R) \to I (X) \in Unit (R))$
8	4 7	syl	$⊢ R \in DivRing \to (X \in Unit (R) \to I (X) \in Unit (R))$
9	1 5 2	drngunit	$⊢ R \in DivRing \to (X \in Unit (R) \leftrightarrow (X \in B \land X \neq \underset{˙}{0}))$
10	1 5 2	drngunit	$⊢ R \in DivRing \to (I (X) \in Unit (R) \leftrightarrow (I (X) \in B \land I (X) \neq \underset{˙}{0}))$
11	8 9 10	3imtr3d	$⊢ R \in DivRing \to ((X \in B \land X \neq \underset{˙}{0}) \to (I (X) \in B \land I (X) \neq \underset{˙}{0}))$
12	11	3impib	$⊢ (R \in DivRing \land X \in B \land X \neq \underset{˙}{0}) \to (I (X) \in B \land I (X) \neq \underset{˙}{0})$
13	12	simprd	$⊢ (R \in DivRing \land X \in B \land X \neq \underset{˙}{0}) \to I (X) \neq \underset{˙}{0}$

Metamath Proof Explorer