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 · ˙ = R
Assertion dvrcan5 R Ring X B Y U Z U X · ˙ Z × ˙ Y · ˙ 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 · ˙ = R
5 1 2 unitss U B
6 simpr3 R Ring X B Y U Z U Z U
7 5 6 sselid R Ring X B Y U Z U Z B
8 2 4 unitmulcl R Ring Y U Z U Y · ˙ Z U
9 8 3adant3r1 R Ring X B Y U Z U Y · ˙ Z U
10 eqid inv r R = inv r R
11 1 4 2 10 3 dvrval Z B Y · ˙ Z U Z × ˙ Y · ˙ Z = Z · ˙ inv r R Y · ˙ Z
12 7 9 11 syl2anc R Ring X B Y U Z U Z × ˙ Y · ˙ Z = Z · ˙ inv r R Y · ˙ Z
13 simpl R Ring X B Y U Z U R Ring
14 eqid mulGrp R 𝑠 U = mulGrp R 𝑠 U
15 2 14 unitgrp R Ring mulGrp R 𝑠 U Grp
16 13 15 syl R Ring X B Y U Z U mulGrp R 𝑠 U Grp
17 simpr2 R Ring X B Y U Z U Y U
18 2 14 unitgrpbas U = Base mulGrp R 𝑠 U
19 2 fvexi U V
20 eqid mulGrp R = mulGrp R
21 20 4 mgpplusg · ˙ = + mulGrp R
22 14 21 ressplusg U V · ˙ = + mulGrp R 𝑠 U
23 19 22 ax-mp · ˙ = + mulGrp R 𝑠 U
24 2 14 10 invrfval inv r R = inv g mulGrp R 𝑠 U
25 18 23 24 grpinvadd mulGrp R 𝑠 U Grp Y U Z U inv r R Y · ˙ Z = inv r R Z · ˙ inv r R Y
26 25 oveq2d mulGrp R 𝑠 U Grp Y U Z U Z · ˙ inv r R Y · ˙ Z = Z · ˙ inv r R Z · ˙ inv r R Y
27 16 17 6 26 syl3anc R Ring X B Y U Z U Z · ˙ inv r R Y · ˙ Z = Z · ˙ inv r R Z · ˙ inv r R Y
28 eqid 1 R = 1 R
29 2 10 4 28 unitrinv R Ring Z U Z · ˙ inv r R Z = 1 R
30 29 oveq1d R Ring Z U Z · ˙ inv r R Z · ˙ inv r R Y = 1 R · ˙ inv r R Y
31 30 3ad2antr3 R Ring X B Y U Z U Z · ˙ inv r R Z · ˙ inv r R Y = 1 R · ˙ inv r R Y
32 2 10 unitinvcl R Ring Z U inv r R Z U
33 32 3ad2antr3 R Ring X B Y U Z U inv r R Z U
34 5 33 sselid R Ring X B Y U Z U inv r R Z B
35 2 10 unitinvcl R Ring Y U inv r R Y U
36 35 3ad2antr2 R Ring X B Y U Z U inv r R Y U
37 5 36 sselid R Ring X B Y U Z U inv r R Y B
38 1 4 ringass R Ring Z B inv r R Z B inv r R Y B Z · ˙ inv r R Z · ˙ inv r R Y = Z · ˙ inv r R Z · ˙ inv r R Y
39 13 7 34 37 38 syl13anc R Ring X B Y U Z U Z · ˙ inv r R Z · ˙ inv r R Y = Z · ˙ inv r R Z · ˙ inv r R Y
40 1 4 28 ringlidm R Ring inv r R Y B 1 R · ˙ inv r R Y = inv r R Y
41 13 37 40 syl2anc R Ring X B Y U Z U 1 R · ˙ inv r R Y = inv r R Y
42 31 39 41 3eqtr3d R Ring X B Y U Z U Z · ˙ inv r R Z · ˙ inv r R Y = inv r R Y
43 12 27 42 3eqtrd R Ring X B Y U Z U Z × ˙ Y · ˙ Z = inv r R Y
44 43 oveq2d R Ring X B Y U Z U X · ˙ Z × ˙ Y · ˙ Z = X · ˙ inv r R Y
45 simpr1 R Ring X B Y U Z U X B
46 1 2 3 4 dvrass R Ring X B Z B Y · ˙ Z U X · ˙ Z × ˙ Y · ˙ Z = X · ˙ Z × ˙ Y · ˙ Z
47 13 45 7 9 46 syl13anc R Ring X B Y U Z U X · ˙ Z × ˙ Y · ˙ Z = X · ˙ Z × ˙ Y · ˙ Z
48 1 4 2 10 3 dvrval X B Y U X × ˙ Y = X · ˙ inv r R Y
49 45 17 48 syl2anc R Ring X B Y U Z U X × ˙ Y = X · ˙ inv r R Y
50 44 47 49 3eqtr4d R Ring X B Y U Z U X · ˙ Z × ˙ Y · ˙ Z = X × ˙ Y