Metamath Proof Explorer

Theorem rdivmuldivd

Description: Multiplication of two ratios. Theorem I.14 of Apostol p. 18. (Contributed by Thierry Arnoux, 30-Oct-2017)

Ref Expression
Hypotheses dvrdir.b 
|- B = ( Base ` R )
dvrdir.u 
|- U = ( Unit ` R )
dvrdir.p 
|- .+ = ( +g ` R )
dvrdir.t 
|- ./ = ( /r ` R )
rdivmuldivd.p 
|- .x. = ( .r ` R )
rdivmuldivd.r 
|- ( ph -> R e. CRing )
rdivmuldivd.a 
|- ( ph -> X e. B )
rdivmuldivd.b 
|- ( ph -> Y e. U )
rdivmuldivd.c 
|- ( ph -> Z e. B )
rdivmuldivd.d 
|- ( ph -> W e. U )
Assertion rdivmuldivd 
|- ( ph -> ( ( X ./ Y ) .x. ( Z ./ W ) ) = ( ( X .x. Z ) ./ ( Y .x. W ) ) )

Proof

Step Hyp Ref Expression
1 dvrdir.b 
 |-  B = ( Base ` R )
2 dvrdir.u 
 |-  U = ( Unit ` R )
3 dvrdir.p 
 |-  .+ = ( +g ` R )
4 dvrdir.t 
 |-  ./ = ( /r ` R )
5 rdivmuldivd.p 
 |-  .x. = ( .r ` R )
6 rdivmuldivd.r 
 |-  ( ph -> R e. CRing )
7 rdivmuldivd.a 
 |-  ( ph -> X e. B )
8 rdivmuldivd.b 
 |-  ( ph -> Y e. U )
9 rdivmuldivd.c 
 |-  ( ph -> Z e. B )
10 rdivmuldivd.d 
 |-  ( ph -> W e. U )
11 eqid 
 |-  ( invr ` R ) = ( invr ` R )
12 1 5 2 11 4 dvrval 
 |-  ( ( X e. B /\ Y e. U ) -> ( X ./ Y ) = ( X .x. ( ( invr ` R ) ` Y ) ) )
13 12 oveq1d 
 |-  ( ( X e. B /\ Y e. U ) -> ( ( X ./ Y ) .x. ( Z ./ W ) ) = ( ( X .x. ( ( invr ` R ) ` Y ) ) .x. ( Z ./ W ) ) )
14 7 8 13 syl2anc 
 |-  ( ph -> ( ( X ./ Y ) .x. ( Z ./ W ) ) = ( ( X .x. ( ( invr ` R ) ` Y ) ) .x. ( Z ./ W ) ) )
15 crngring 
 |-  ( R e. CRing -> R e. Ring )
16 6 15 syl 
 |-  ( ph -> R e. Ring )
17 1 2 unitss 
 |-  U C_ B
18 2 11 unitinvcl 
 |-  ( ( R e. Ring /\ Y e. U ) -> ( ( invr ` R ) ` Y ) e. U )
19 16 8 18 syl2anc 
 |-  ( ph -> ( ( invr ` R ) ` Y ) e. U )
20 17 19 sseldi 
 |-  ( ph -> ( ( invr ` R ) ` Y ) e. B )
21 1 2 4 dvrcl 
 |-  ( ( R e. Ring /\ Z e. B /\ W e. U ) -> ( Z ./ W ) e. B )
22 16 9 10 21 syl3anc 
 |-  ( ph -> ( Z ./ W ) e. B )
23 1 5 ringass 
 |-  ( ( R e. Ring /\ ( X e. B /\ ( ( invr ` R ) ` Y ) e. B /\ ( Z ./ W ) e. B ) ) -> ( ( X .x. ( ( invr ` R ) ` Y ) ) .x. ( Z ./ W ) ) = ( X .x. ( ( ( invr ` R ) ` Y ) .x. ( Z ./ W ) ) ) )
24 16 7 20 22 23 syl13anc 
 |-  ( ph -> ( ( X .x. ( ( invr ` R ) ` Y ) ) .x. ( Z ./ W ) ) = ( X .x. ( ( ( invr ` R ) ` Y ) .x. ( Z ./ W ) ) ) )
25 1 5 crngcom 
 |-  ( ( R e. CRing /\ ( ( invr ` R ) ` Y ) e. B /\ ( Z ./ W ) e. B ) -> ( ( ( invr ` R ) ` Y ) .x. ( Z ./ W ) ) = ( ( Z ./ W ) .x. ( ( invr ` R ) ` Y ) ) )
26 6 20 22 25 syl3anc 
 |-  ( ph -> ( ( ( invr ` R ) ` Y ) .x. ( Z ./ W ) ) = ( ( Z ./ W ) .x. ( ( invr ` R ) ` Y ) ) )
27 26 oveq2d 
 |-  ( ph -> ( X .x. ( ( ( invr ` R ) ` Y ) .x. ( Z ./ W ) ) ) = ( X .x. ( ( Z ./ W ) .x. ( ( invr ` R ) ` Y ) ) ) )
28 14 24 27 3eqtrd 
 |-  ( ph -> ( ( X ./ Y ) .x. ( Z ./ W ) ) = ( X .x. ( ( Z ./ W ) .x. ( ( invr ` R ) ` Y ) ) ) )
29 eqid 
 |-  ( ( mulGrp ` R ) |`s U ) = ( ( mulGrp ` R ) |`s U )
30 2 29 unitgrp 
 |-  ( R e. Ring -> ( ( mulGrp ` R ) |`s U ) e. Grp )
31 16 30 syl 
 |-  ( ph -> ( ( mulGrp ` R ) |`s U ) e. Grp )
32 2 29 unitgrpbas 
 |-  U = ( Base ` ( ( mulGrp ` R ) |`s U ) )
33 eqid 
 |-  ( +g ` ( ( mulGrp ` R ) |`s U ) ) = ( +g ` ( ( mulGrp ` R ) |`s U ) )
34 2 29 11 invrfval 
 |-  ( invr ` R ) = ( invg ` ( ( mulGrp ` R ) |`s U ) )
35 32 33 34 grpinvadd 
 |-  ( ( ( ( mulGrp ` R ) |`s U ) e. Grp /\ Y e. U /\ W e. U ) -> ( ( invr ` R ) ` ( Y ( +g ` ( ( mulGrp ` R ) |`s U ) ) W ) ) = ( ( ( invr ` R ) ` W ) ( +g ` ( ( mulGrp ` R ) |`s U ) ) ( ( invr ` R ) ` Y ) ) )
36 31 8 10 35 syl3anc 
 |-  ( ph -> ( ( invr ` R ) ` ( Y ( +g ` ( ( mulGrp ` R ) |`s U ) ) W ) ) = ( ( ( invr ` R ) ` W ) ( +g ` ( ( mulGrp ` R ) |`s U ) ) ( ( invr ` R ) ` Y ) ) )
37 eqid 
 |-  ( mulGrp ` ( R |`s U ) ) = ( mulGrp ` ( R |`s U ) )
38 2 fvexi 
 |-  U e. _V
39 eqid 
 |-  ( R |`s U ) = ( R |`s U )
40 39 5 ressmulr 
 |-  ( U e. _V -> .x. = ( .r ` ( R |`s U ) ) )
41 38 40 ax-mp 
 |-  .x. = ( .r ` ( R |`s U ) )
42 37 41 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` ( R |`s U ) ) )
43 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
44 39 43 mgpress 
 |-  ( ( R e. Ring /\ U e. _V ) -> ( ( mulGrp ` R ) |`s U ) = ( mulGrp ` ( R |`s U ) ) )
45 16 38 44 sylancl 
 |-  ( ph -> ( ( mulGrp ` R ) |`s U ) = ( mulGrp ` ( R |`s U ) ) )
46 45 fveq2d 
 |-  ( ph -> ( +g ` ( ( mulGrp ` R ) |`s U ) ) = ( +g ` ( mulGrp ` ( R |`s U ) ) ) )
47 42 46 eqtr4id 
 |-  ( ph -> .x. = ( +g ` ( ( mulGrp ` R ) |`s U ) ) )
48 47 oveqd 
 |-  ( ph -> ( Y .x. W ) = ( Y ( +g ` ( ( mulGrp ` R ) |`s U ) ) W ) )
49 48 fveq2d 
 |-  ( ph -> ( ( invr ` R ) ` ( Y .x. W ) ) = ( ( invr ` R ) ` ( Y ( +g ` ( ( mulGrp ` R ) |`s U ) ) W ) ) )
50 47 oveqd 
 |-  ( ph -> ( ( ( invr ` R ) ` W ) .x. ( ( invr ` R ) ` Y ) ) = ( ( ( invr ` R ) ` W ) ( +g ` ( ( mulGrp ` R ) |`s U ) ) ( ( invr ` R ) ` Y ) ) )
51 36 49 50 3eqtr4d 
 |-  ( ph -> ( ( invr ` R ) ` ( Y .x. W ) ) = ( ( ( invr ` R ) ` W ) .x. ( ( invr ` R ) ` Y ) ) )
52 51 oveq2d 
 |-  ( ph -> ( ( X .x. Z ) .x. ( ( invr ` R ) ` ( Y .x. W ) ) ) = ( ( X .x. Z ) .x. ( ( ( invr ` R ) ` W ) .x. ( ( invr ` R ) ` Y ) ) ) )
53 1 5 ringcl 
 |-  ( ( R e. Ring /\ X e. B /\ Z e. B ) -> ( X .x. Z ) e. B )
54 16 7 9 53 syl3anc 
 |-  ( ph -> ( X .x. Z ) e. B )
55 2 5 unitmulcl 
 |-  ( ( R e. Ring /\ Y e. U /\ W e. U ) -> ( Y .x. W ) e. U )
56 16 8 10 55 syl3anc 
 |-  ( ph -> ( Y .x. W ) e. U )
57 1 5 2 11 4 dvrval 
 |-  ( ( ( X .x. Z ) e. B /\ ( Y .x. W ) e. U ) -> ( ( X .x. Z ) ./ ( Y .x. W ) ) = ( ( X .x. Z ) .x. ( ( invr ` R ) ` ( Y .x. W ) ) ) )
58 54 56 57 syl2anc 
 |-  ( ph -> ( ( X .x. Z ) ./ ( Y .x. W ) ) = ( ( X .x. Z ) .x. ( ( invr ` R ) ` ( Y .x. W ) ) ) )
59 2 11 unitinvcl 
 |-  ( ( R e. Ring /\ W e. U ) -> ( ( invr ` R ) ` W ) e. U )
60 16 10 59 syl2anc 
 |-  ( ph -> ( ( invr ` R ) ` W ) e. U )
61 17 60 sseldi 
 |-  ( ph -> ( ( invr ` R ) ` W ) e. B )
62 1 5 ringass 
 |-  ( ( R e. Ring /\ ( X e. B /\ Z e. B /\ ( ( invr ` R ) ` W ) e. B ) ) -> ( ( X .x. Z ) .x. ( ( invr ` R ) ` W ) ) = ( X .x. ( Z .x. ( ( invr ` R ) ` W ) ) ) )
63 16 7 9 61 62 syl13anc 
 |-  ( ph -> ( ( X .x. Z ) .x. ( ( invr ` R ) ` W ) ) = ( X .x. ( Z .x. ( ( invr ` R ) ` W ) ) ) )
64 1 5 2 11 4 dvrval 
 |-  ( ( Z e. B /\ W e. U ) -> ( Z ./ W ) = ( Z .x. ( ( invr ` R ) ` W ) ) )
65 9 10 64 syl2anc 
 |-  ( ph -> ( Z ./ W ) = ( Z .x. ( ( invr ` R ) ` W ) ) )
66 65 oveq2d 
 |-  ( ph -> ( X .x. ( Z ./ W ) ) = ( X .x. ( Z .x. ( ( invr ` R ) ` W ) ) ) )
67 63 66 eqtr4d 
 |-  ( ph -> ( ( X .x. Z ) .x. ( ( invr ` R ) ` W ) ) = ( X .x. ( Z ./ W ) ) )
68 67 oveq1d 
 |-  ( ph -> ( ( ( X .x. Z ) .x. ( ( invr ` R ) ` W ) ) .x. ( ( invr ` R ) ` Y ) ) = ( ( X .x. ( Z ./ W ) ) .x. ( ( invr ` R ) ` Y ) ) )
69 1 5 ringass 
 |-  ( ( R e. Ring /\ ( ( X .x. Z ) e. B /\ ( ( invr ` R ) ` W ) e. B /\ ( ( invr ` R ) ` Y ) e. B ) ) -> ( ( ( X .x. Z ) .x. ( ( invr ` R ) ` W ) ) .x. ( ( invr ` R ) ` Y ) ) = ( ( X .x. Z ) .x. ( ( ( invr ` R ) ` W ) .x. ( ( invr ` R ) ` Y ) ) ) )
70 16 54 61 20 69 syl13anc 
 |-  ( ph -> ( ( ( X .x. Z ) .x. ( ( invr ` R ) ` W ) ) .x. ( ( invr ` R ) ` Y ) ) = ( ( X .x. Z ) .x. ( ( ( invr ` R ) ` W ) .x. ( ( invr ` R ) ` Y ) ) ) )
71 1 5 ringass 
 |-  ( ( R e. Ring /\ ( X e. B /\ ( Z ./ W ) e. B /\ ( ( invr ` R ) ` Y ) e. B ) ) -> ( ( X .x. ( Z ./ W ) ) .x. ( ( invr ` R ) ` Y ) ) = ( X .x. ( ( Z ./ W ) .x. ( ( invr ` R ) ` Y ) ) ) )
72 16 7 22 20 71 syl13anc 
 |-  ( ph -> ( ( X .x. ( Z ./ W ) ) .x. ( ( invr ` R ) ` Y ) ) = ( X .x. ( ( Z ./ W ) .x. ( ( invr ` R ) ` Y ) ) ) )
73 68 70 72 3eqtr3rd 
 |-  ( ph -> ( X .x. ( ( Z ./ W ) .x. ( ( invr ` R ) ` Y ) ) ) = ( ( X .x. Z ) .x. ( ( ( invr ` R ) ` W ) .x. ( ( invr ` R ) ` Y ) ) ) )
74 52 58 73 3eqtr4rd 
 |-  ( ph -> ( X .x. ( ( Z ./ W ) .x. ( ( invr ` R ) ` Y ) ) ) = ( ( X .x. Z ) ./ ( Y .x. W ) ) )
75 28 74 eqtrd 
 |-  ( ph -> ( ( X ./ Y ) .x. ( Z ./ W ) ) = ( ( X .x. Z ) ./ ( Y .x. W ) ) )