Theorem 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	|- .x. = ( .r ` R )
	dvrval.u	|- U = ( Unit ` R )
	dvrval.i	|- I = ( invr ` R )
	dvrval.d	|- ./ = ( /r ` R )
Assertion	dvrval	|- ( ( X e. B /\ Y e. U ) -> ( X ./ Y ) = ( X .x. ( I ` Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvrval.b	|- B = ( Base ` R )
2		dvrval.t	|- .x. = ( .r ` R )
3		dvrval.u	|- U = ( Unit ` R )
4		dvrval.i	|- I = ( invr ` R )
5		dvrval.d	|- ./ = ( /r ` R )
6		oveq1	|- ( x = X -> ( x .x. ( I ` y ) ) = ( X .x. ( I ` y ) ) )
7		fveq2	|- ( y = Y -> ( I ` y ) = ( I ` Y ) )
8	7	oveq2d	|- ( y = Y -> ( X .x. ( I ` y ) ) = ( X .x. ( I ` Y ) ) )
9	1 2 3 4 5	dvrfval	|- ./ = ( x e. B , y e. U |-> ( x .x. ( I ` y ) ) )
10		ovex	|- ( X .x. ( I ` Y ) ) e. _V
11	6 8 9 10	ovmpo	|- ( ( X e. B /\ Y e. U ) -> ( X ./ Y ) = ( X .x. ( I ` Y ) ) )