Metamath Proof Explorer

Theorem dvrcan5

Description: Cancellation law for common factor in ratio. ( divcan5 analog.) (Contributed by Thierry Arnoux, 26-Oct-2016)

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

Proof

Step Hyp Ref Expression
1 dvrcan5.b 
 |-  B = ( Base ` R )
2 dvrcan5.o 
 |-  U = ( Unit ` R )
3 dvrcan5.d 
 |-  ./ = ( /r ` R )
4 dvrcan5.t 
 |-  .x. = ( .r ` R )
5 1 2 unitss 
 |-  U C_ B
6 simpr3 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> Z e. U )
7 5 6 sselid 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> Z e. B )
8 2 4 unitmulcl 
 |-  ( ( R e. Ring /\ Y e. U /\ Z e. U ) -> ( Y .x. Z ) e. U )
9 8 3adant3r1 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( Y .x. Z ) e. U )
10 eqid 
 |-  ( invr ` R ) = ( invr ` R )
11 1 4 2 10 3 dvrval 
 |-  ( ( Z e. B /\ ( Y .x. Z ) e. U ) -> ( Z ./ ( Y .x. Z ) ) = ( Z .x. ( ( invr ` R ) ` ( Y .x. Z ) ) ) )
12 7 9 11 syl2anc 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( Z ./ ( Y .x. Z ) ) = ( Z .x. ( ( invr ` R ) ` ( Y .x. Z ) ) ) )
13 simpl 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> R e. Ring )
14 eqid 
 |-  ( ( mulGrp ` R ) |`s U ) = ( ( mulGrp ` R ) |`s U )
15 2 14 unitgrp 
 |-  ( R e. Ring -> ( ( mulGrp ` R ) |`s U ) e. Grp )
16 13 15 syl 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( ( mulGrp ` R ) |`s U ) e. Grp )
17 simpr2 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> Y e. U )
18 2 14 unitgrpbas 
 |-  U = ( Base ` ( ( mulGrp ` R ) |`s U ) )
19 2 fvexi 
 |-  U e. _V
20 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
21 20 4 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` R ) )
22 14 21 ressplusg 
 |-  ( U e. _V -> .x. = ( +g ` ( ( mulGrp ` R ) |`s U ) ) )
23 19 22 ax-mp 
 |-  .x. = ( +g ` ( ( mulGrp ` R ) |`s U ) )
24 2 14 10 invrfval 
 |-  ( invr ` R ) = ( invg ` ( ( mulGrp ` R ) |`s U ) )
25 18 23 24 grpinvadd 
 |-  ( ( ( ( mulGrp ` R ) |`s U ) e. Grp /\ Y e. U /\ Z e. U ) -> ( ( invr ` R ) ` ( Y .x. Z ) ) = ( ( ( invr ` R ) ` Z ) .x. ( ( invr ` R ) ` Y ) ) )
26 25 oveq2d 
 |-  ( ( ( ( mulGrp ` R ) |`s U ) e. Grp /\ Y e. U /\ Z e. U ) -> ( Z .x. ( ( invr ` R ) ` ( Y .x. Z ) ) ) = ( Z .x. ( ( ( invr ` R ) ` Z ) .x. ( ( invr ` R ) ` Y ) ) ) )
27 16 17 6 26 syl3anc 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( Z .x. ( ( invr ` R ) ` ( Y .x. Z ) ) ) = ( Z .x. ( ( ( invr ` R ) ` Z ) .x. ( ( invr ` R ) ` Y ) ) ) )
28 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
29 2 10 4 28 unitrinv 
 |-  ( ( R e. Ring /\ Z e. U ) -> ( Z .x. ( ( invr ` R ) ` Z ) ) = ( 1r ` R ) )
30 29 oveq1d 
 |-  ( ( R e. Ring /\ Z e. U ) -> ( ( Z .x. ( ( invr ` R ) ` Z ) ) .x. ( ( invr ` R ) ` Y ) ) = ( ( 1r ` R ) .x. ( ( invr ` R ) ` Y ) ) )
31 30 3ad2antr3 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( ( Z .x. ( ( invr ` R ) ` Z ) ) .x. ( ( invr ` R ) ` Y ) ) = ( ( 1r ` R ) .x. ( ( invr ` R ) ` Y ) ) )
32 2 10 unitinvcl 
 |-  ( ( R e. Ring /\ Z e. U ) -> ( ( invr ` R ) ` Z ) e. U )
33 32 3ad2antr3 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( ( invr ` R ) ` Z ) e. U )
34 5 33 sselid 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( ( invr ` R ) ` Z ) e. B )
35 2 10 unitinvcl 
 |-  ( ( R e. Ring /\ Y e. U ) -> ( ( invr ` R ) ` Y ) e. U )
36 35 3ad2antr2 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( ( invr ` R ) ` Y ) e. U )
37 5 36 sselid 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( ( invr ` R ) ` Y ) e. B )
38 1 4 ringass 
 |-  ( ( R e. Ring /\ ( Z e. B /\ ( ( invr ` R ) ` Z ) e. B /\ ( ( invr ` R ) ` Y ) e. B ) ) -> ( ( Z .x. ( ( invr ` R ) ` Z ) ) .x. ( ( invr ` R ) ` Y ) ) = ( Z .x. ( ( ( invr ` R ) ` Z ) .x. ( ( invr ` R ) ` Y ) ) ) )
39 13 7 34 37 38 syl13anc 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( ( Z .x. ( ( invr ` R ) ` Z ) ) .x. ( ( invr ` R ) ` Y ) ) = ( Z .x. ( ( ( invr ` R ) ` Z ) .x. ( ( invr ` R ) ` Y ) ) ) )
40 1 4 28 ringlidm 
 |-  ( ( R e. Ring /\ ( ( invr ` R ) ` Y ) e. B ) -> ( ( 1r ` R ) .x. ( ( invr ` R ) ` Y ) ) = ( ( invr ` R ) ` Y ) )
41 13 37 40 syl2anc 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( ( 1r ` R ) .x. ( ( invr ` R ) ` Y ) ) = ( ( invr ` R ) ` Y ) )
42 31 39 41 3eqtr3d 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( Z .x. ( ( ( invr ` R ) ` Z ) .x. ( ( invr ` R ) ` Y ) ) ) = ( ( invr ` R ) ` Y ) )
43 12 27 42 3eqtrd 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( Z ./ ( Y .x. Z ) ) = ( ( invr ` R ) ` Y ) )
44 43 oveq2d 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( X .x. ( Z ./ ( Y .x. Z ) ) ) = ( X .x. ( ( invr ` R ) ` Y ) ) )
45 simpr1 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> X e. B )
46 1 2 3 4 dvrass 
 |-  ( ( R e. Ring /\ ( X e. B /\ Z e. B /\ ( Y .x. Z ) e. U ) ) -> ( ( X .x. Z ) ./ ( Y .x. Z ) ) = ( X .x. ( Z ./ ( Y .x. Z ) ) ) )
47 13 45 7 9 46 syl13anc 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( ( X .x. Z ) ./ ( Y .x. Z ) ) = ( X .x. ( Z ./ ( Y .x. Z ) ) ) )
48 1 4 2 10 3 dvrval 
 |-  ( ( X e. B /\ Y e. U ) -> ( X ./ Y ) = ( X .x. ( ( invr ` R ) ` Y ) ) )
49 45 17 48 syl2anc 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( X ./ Y ) = ( X .x. ( ( invr ` R ) ` Y ) ) )
50 44 47 49 3eqtr4d 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. U /\ Z e. U ) ) -> ( ( X .x. Z ) ./ ( Y .x. Z ) ) = ( X ./ Y ) )