ringinvdv

Description: Write the inverse function in terms of division. (Contributed by Mario Carneiro, 2-Jul-2014)

	Ref	Expression
Hypotheses	ringinvdv.b	$⊢ B = {Base}_{R}$
	ringinvdv.u	$⊢ U = Unit (R)$
	ringinvdv.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
	ringinvdv.o	$⊢ \underset{˙}{1} = 1_{R}$
	ringinvdv.i	$⊢ I = {inv}_{r} (R)$
Assertion	ringinvdv	$⊢ (R \in Ring \land X \in U) \to I (X) = \underset{˙}{1} \underset{˙}{\times} X$

Step	Hyp	Ref	Expression
1		ringinvdv.b	$⊢ B = {Base}_{R}$
2		ringinvdv.u	$⊢ U = Unit (R)$
3		ringinvdv.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
4		ringinvdv.o	$⊢ \underset{˙}{1} = 1_{R}$
5		ringinvdv.i	$⊢ I = {inv}_{r} (R)$
6	1 4	ringidcl	$⊢ R \in Ring \to \underset{˙}{1} \in B$
7		eqid	$⊢ \cdot_{R} = \cdot_{R}$
8	1 7 2 5 3	dvrval	$⊢ (\underset{˙}{1} \in B \land X \in U) \to \underset{˙}{1} \underset{˙}{\times} X = \underset{˙}{1} \cdot_{R} I (X)$
9	6 8	sylan	$⊢ (R \in Ring \land X \in U) \to \underset{˙}{1} \underset{˙}{\times} X = \underset{˙}{1} \cdot_{R} I (X)$
10	2 5 1	ringinvcl	$⊢ (R \in Ring \land X \in U) \to I (X) \in B$
11	1 7 4	ringlidm	$⊢ (R \in Ring \land I (X) \in B) \to \underset{˙}{1} \cdot_{R} I (X) = I (X)$
12	10 11	syldan	$⊢ (R \in Ring \land X \in U) \to \underset{˙}{1} \cdot_{R} I (X) = I (X)$
13	9 12	eqtr2d	$⊢ (R \in Ring \land X \in U) \to I (X) = \underset{˙}{1} \underset{˙}{\times} X$

Metamath Proof Explorer