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 sselid โŠข ( ( ๐‘… โˆˆ 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 sselid โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘ˆ โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ( ( invr โ€˜ ๐‘… ) โ€˜ ๐‘ ) โˆˆ ๐ต )
35 2 10 unitinvcl โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘Œ โˆˆ ๐‘ˆ ) โ†’ ( ( invr โ€˜ ๐‘… ) โ€˜ ๐‘Œ ) โˆˆ ๐‘ˆ )
36 35 3ad2antr2 โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘ˆ โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ( ( invr โ€˜ ๐‘… ) โ€˜ ๐‘Œ ) โˆˆ ๐‘ˆ )
37 5 36 sselid โŠข ( ( ๐‘… โˆˆ 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 โˆง ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐‘ˆ โˆง ๐‘ โˆˆ ๐‘ˆ ) ) โ†’ ( ( ๐‘‹ ยท ๐‘ ) / ( ๐‘Œ ยท ๐‘ ) ) = ( ๐‘‹ / ๐‘Œ ) )