drnginvrl

Description: Property of the multiplicative inverse in a division ring. ( recid2 analog). (Contributed by NM, 19-Apr-2014)

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

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

Metamath Proof Explorer