Metamath Proof Explorer

Theorem dvrcan3

Description: A cancellation law for division. ( divcan3 analog.) (Contributed by Mario Carneiro, 2-Jul-2014) (Revised by Mario Carneiro, 18-Jun-2015)

Ref Expression
Hypotheses dvrass.b 
|- B = ( Base ` R )
dvrass.o 
|- U = ( Unit ` R )
dvrass.d 
|- ./ = ( /r ` R )
dvrass.t 
|- .x. = ( .r ` R )
Assertion dvrcan3 
|- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X .x. Y ) ./ 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 simp1 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> R e. Ring )
6 simp2 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> X e. B )
7 1 2 unitcl 
 |-  ( Y e. U -> Y e. B )
8 7 3ad2ant3 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> Y e. B )
9 simp3 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> Y e. U )
10 1 2 3 4 dvrass 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Y e. U ) ) -> ( ( X .x. Y ) ./ Y ) = ( X .x. ( Y ./ Y ) ) )
11 5 6 8 9 10 syl13anc 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X .x. Y ) ./ Y ) = ( X .x. ( Y ./ Y ) ) )
12 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
13 2 3 12 dvrid 
 |-  ( ( R e. Ring /\ Y e. U ) -> ( Y ./ Y ) = ( 1r ` R ) )
14 13 3adant2 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( Y ./ Y ) = ( 1r ` R ) )
15 14 oveq2d 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X .x. ( Y ./ Y ) ) = ( X .x. ( 1r ` R ) ) )
16 1 4 12 ringridm 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X .x. ( 1r ` R ) ) = X )
17 16 3adant3 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X .x. ( 1r ` R ) ) = X )
18 11 15 17 3eqtrd 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X .x. Y ) ./ Y ) = X )