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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
dvrcan5.o ⊢ 𝑈 = ( Unit ‘ 𝑅 )
dvrcan5.d ⊢ / = ( /r ‘ 𝑅 )
dvrcan5.t ⊢ · = ( .r ‘ 𝑅 )
Assertion dvrcan5 ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑍 ) / ( 𝑌 · 𝑍 ) ) = ( 𝑋 / 𝑌 ) )

Proof

Step Hyp Ref Expression
1 dvrcan5.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 dvrcan5.o ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 dvrcan5.d ⊢ / = ( /r ‘ 𝑅 )
4 dvrcan5.t ⊢ · = ( .r ‘ 𝑅 )
5 1 2 unitss ⊢ 𝑈 ⊆ 𝐵
6 simpr3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑍 ∈ 𝑈 )
7 5 6 sseldi ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑍 ∈ 𝐵 )
8 2 4 unitmulcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) → ( 𝑌 · 𝑍 ) ∈ 𝑈 )
9 8 3adant3r1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑌 · 𝑍 ) ∈ 𝑈 )
10 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
11 1 4 2 10 3 dvrval ⊢ ( ( 𝑍 ∈ 𝐵 ∧ ( 𝑌 · 𝑍 ) ∈ 𝑈 ) → ( 𝑍 / ( 𝑌 · 𝑍 ) ) = ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) ) )
12 7 9 11 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑍 / ( 𝑌 · 𝑍 ) ) = ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) ) )
13 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑅 ∈ Ring )
14 eqid ⊢ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) = ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 )
15 2 14 unitgrp ⊢ ( 𝑅 ∈ Ring → ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ∈ Grp )
16 13 15 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ∈ Grp )
17 simpr2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑌 ∈ 𝑈 )
18 2 14 unitgrpbas ⊢ 𝑈 = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
19 2 fvexi ⊢ 𝑈 ∈ V
20 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
21 20 4 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
22 14 21 ressplusg ⊢ ( 𝑈 ∈ V → · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ) )
23 19 22 ax-mp ⊢ · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
24 2 14 10 invrfval ⊢ ( invr ‘ 𝑅 ) = ( invg ‘ ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) )
25 18 23 24 grpinvadd ⊢ ( ( ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ∈ Grp ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
26 25 oveq2d ⊢ ( ( ( ( mulGrp ‘ 𝑅 ) ↾s 𝑈 ) ∈ Grp ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) → ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) ) = ( 𝑍 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) ) )
27 16 17 6 26 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ ( 𝑌 · 𝑍 ) ) ) = ( 𝑍 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) ) )
28 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
29 2 10 4 28 unitrinv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝑈 ) → ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) )
30 29 oveq1d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝑈 ) → ( ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) = ( ( 1r ‘ 𝑅 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
31 30 3ad2antr3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) = ( ( 1r ‘ 𝑅 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
32 2 10 unitinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑍 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝑈 )
33 32 3ad2antr3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝑈 )
34 5 33 sseldi ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 )
35 2 10 unitinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝑈 )
36 35 3ad2antr2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝑈 )
37 5 36 sseldi ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 )
38 1 4 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑍 ∈ 𝐵 ∧ ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ∈ 𝐵 ∧ ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 ) ) → ( ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) = ( 𝑍 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) ) )
39 13 7 34 37 38 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑍 · ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) = ( 𝑍 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) ) )
40 1 4 28 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) = ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) )
41 13 37 40 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 1r ‘ 𝑅 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) = ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) )
42 31 39 41 3eqtr3d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑍 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑍 ) · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) ) = ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) )
43 12 27 42 3eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑍 / ( 𝑌 · 𝑍 ) ) = ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) )
44 43 oveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑋 · ( 𝑍 / ( 𝑌 · 𝑍 ) ) ) = ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
45 simpr1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → 𝑋 ∈ 𝐵 )
46 1 2 3 4 dvrass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ ( 𝑌 · 𝑍 ) ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑍 ) / ( 𝑌 · 𝑍 ) ) = ( 𝑋 · ( 𝑍 / ( 𝑌 · 𝑍 ) ) ) )
47 13 45 7 9 46 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑍 ) / ( 𝑌 · 𝑍 ) ) = ( 𝑋 · ( 𝑍 / ( 𝑌 · 𝑍 ) ) ) )
48 1 4 2 10 3 dvrval ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 / 𝑌 ) = ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
49 45 17 48 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( 𝑋 / 𝑌 ) = ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
50 44 47 49 3eqtr4d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ 𝑍 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑍 ) / ( 𝑌 · 𝑍 ) ) = ( 𝑋 / 𝑌 ) )