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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
dvrdir.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
dvrdir.p ⊢ + = ( +g ‘ 𝑅 )
dvrdir.t ⊢ / = ( /r ‘ 𝑅 )
rdivmuldivd.p ⊢ · = ( .r ‘ 𝑅 )
rdivmuldivd.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
rdivmuldivd.a ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
rdivmuldivd.b ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
rdivmuldivd.c ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
rdivmuldivd.d ⊢ ( 𝜑 → 𝑊 ∈ 𝑈 )
Assertion rdivmuldivd ( 𝜑 → ( ( 𝑋 / 𝑌 ) · ( 𝑍 / 𝑊 ) ) = ( ( 𝑋 · 𝑍 ) / ( 𝑌 · 𝑊 ) ) )

Proof

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