drnginvrcl

Description: Closure of the multiplicative inverse in a division ring. ( reccl 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	drnginvrcl	$⊢ (R \in DivRing \land X \in B \land X \neq \underset{˙}{0}) \to I (X) \in B$

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		eqid	$⊢ Unit (R) = Unit (R)$
5	1 4 2	drngunit	$⊢ R \in DivRing \to (X \in Unit (R) \leftrightarrow (X \in B \land X \neq \underset{˙}{0}))$
6		drngring	$⊢ R \in DivRing \to R \in Ring$
7	4 3 1	ringinvcl	$⊢ (R \in Ring \land X \in Unit (R)) \to I (X) \in B$
8	7	ex	$⊢ R \in Ring \to (X \in Unit (R) \to I (X) \in B)$
9	6 8	syl	$⊢ R \in DivRing \to (X \in Unit (R) \to I (X) \in B)$
10	5 9	sylbird	$⊢ R \in DivRing \to ((X \in B \land X \neq \underset{˙}{0}) \to I (X) \in B)$
11	10	3impib	$⊢ (R \in DivRing \land X \in B \land X \neq \underset{˙}{0}) \to I (X) \in B$

Metamath Proof Explorer