dvrval

Description: Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014) (Revised by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	dvrval.b	$⊢ B = {Base}_{R}$
	dvrval.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	dvrval.u	$⊢ U = Unit (R)$
	dvrval.i	$⊢ I = {inv}_{r} (R)$
	dvrval.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
Assertion	dvrval	$⊢ (X \in B \land Y \in U) \to X \underset{˙}{\times} Y = X \underset{˙}{\cdot} I (Y)$

Step	Hyp	Ref	Expression
1		dvrval.b	$⊢ B = {Base}_{R}$
2		dvrval.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		dvrval.u	$⊢ U = Unit (R)$
4		dvrval.i	$⊢ I = {inv}_{r} (R)$
5		dvrval.d	$⊢ \underset{˙}{\times} = /_{r} (R)$
6		oveq1	$⊢ x = X \to x \underset{˙}{\cdot} I (y) = X \underset{˙}{\cdot} I (y)$
7		fveq2	$⊢ y = Y \to I (y) = I (Y)$
8	7	oveq2d	$⊢ y = Y \to X \underset{˙}{\cdot} I (y) = X \underset{˙}{\cdot} I (Y)$
9	1 2 3 4 5	dvrfval	$⊢ \underset{˙}{\times} = (x \in B, y \in U ⟼ x \underset{˙}{\cdot} I (y))$
10		ovex	$⊢ X \underset{˙}{\cdot} I (Y) \in V$
11	6 8 9 10	ovmpo	$⊢ (X \in B \land Y \in U) \to X \underset{˙}{\times} Y = X \underset{˙}{\cdot} I (Y)$

Metamath Proof Explorer