Metamath Proof Explorer

Theorem dvrcan1

Description: A cancellation law for division. ( divcan1 analog.) (Contributed by Mario Carneiro, 2-Jul-2014) (Revised by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypotheses dvrass.b 
|- B = ( Base ` R )
dvrass.o 
|- U = ( Unit ` R )
dvrass.d 
|- ./ = ( /r ` R )
dvrass.t 
|- .x. = ( .r ` R )
Assertion dvrcan1 
|- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X ./ Y ) .x. Y ) = X )

Proof

Step Hyp Ref Expression
1 dvrass.b 
 |-  B = ( Base ` R )
2 dvrass.o 
 |-  U = ( Unit ` R )
3 dvrass.d 
 |-  ./ = ( /r ` R )
4 dvrass.t 
 |-  .x. = ( .r ` R )
5 eqid 
 |-  ( invr ` R ) = ( invr ` R )
6 1 4 2 5 3 dvrval 
 |-  ( ( X e. B /\ Y e. U ) -> ( X ./ Y ) = ( X .x. ( ( invr ` R ) ` Y ) ) )
7 6 3adant1 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X ./ Y ) = ( X .x. ( ( invr ` R ) ` Y ) ) )
8 7 oveq1d 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X ./ Y ) .x. Y ) = ( ( X .x. ( ( invr ` R ) ` Y ) ) .x. Y ) )
9 simp1 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> R e. Ring )
10 simp2 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> X e. B )
11 2 5 1 ringinvcl 
 |-  ( ( R e. Ring /\ Y e. U ) -> ( ( invr ` R ) ` Y ) e. B )
12 11 3adant2 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( invr ` R ) ` Y ) e. B )
13 1 2 unitcl 
 |-  ( Y e. U -> Y e. B )
14 13 3ad2ant3 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> Y e. B )
15 1 4 ringass 
 |-  ( ( R e. Ring /\ ( X e. B /\ ( ( invr ` R ) ` Y ) e. B /\ Y e. B ) ) -> ( ( X .x. ( ( invr ` R ) ` Y ) ) .x. Y ) = ( X .x. ( ( ( invr ` R ) ` Y ) .x. Y ) ) )
16 9 10 12 14 15 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X .x. ( ( invr ` R ) ` Y ) ) .x. Y ) = ( X .x. ( ( ( invr ` R ) ` Y ) .x. Y ) ) )
17 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
18 2 5 4 17 unitlinv 
 |-  ( ( R e. Ring /\ Y e. U ) -> ( ( ( invr ` R ) ` Y ) .x. Y ) = ( 1r ` R ) )
19 18 3adant2 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( ( invr ` R ) ` Y ) .x. Y ) = ( 1r ` R ) )
20 19 oveq2d 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X .x. ( ( ( invr ` R ) ` Y ) .x. Y ) ) = ( X .x. ( 1r ` R ) ) )
21 1 4 17 ringridm 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X .x. ( 1r ` R ) ) = X )
22 21 3adant3 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X .x. ( 1r ` R ) ) = X )
23 20 22 eqtrd 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X .x. ( ( ( invr ` R ) ` Y ) .x. Y ) ) = X )
24 16 23 eqtrd 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X .x. ( ( invr ` R ) ` Y ) ) .x. Y ) = X )
25 8 24 eqtrd 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X ./ Y ) .x. Y ) = X )