Metamath Proof Explorer


Theorem dvrid

Description: A cancellation law for division. ( divid analog.) (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Hypotheses unitdvcl.o U=UnitR
unitdvcl.d ×˙=/rR
dvrid.o 1˙=1R
Assertion dvrid RRingXUX×˙X=1˙

Proof

Step Hyp Ref Expression
1 unitdvcl.o U=UnitR
2 unitdvcl.d ×˙=/rR
3 dvrid.o 1˙=1R
4 eqid BaseR=BaseR
5 4 1 unitcl XUXBaseR
6 5 adantl RRingXUXBaseR
7 eqid R=R
8 eqid invrR=invrR
9 4 7 1 8 2 dvrval XBaseRXUX×˙X=XRinvrRX
10 6 9 sylancom RRingXUX×˙X=XRinvrRX
11 1 8 7 3 unitrinv RRingXUXRinvrRX=1˙
12 10 11 eqtrd RRingXUX×˙X=1˙