Metamath Proof Explorer


Theorem dvrcan3

Description: A cancellation law for division. ( divcan3 analog.) (Contributed by Mario Carneiro, 2-Jul-2014) (Revised by Mario Carneiro, 18-Jun-2015)

Ref Expression
Hypotheses dvrass.b B = Base R
dvrass.o U = Unit R
dvrass.d × ˙ = / r R
dvrass.t · ˙ = R
Assertion dvrcan3 R Ring X B Y U X · ˙ Y × ˙ Y = X

Proof

Step Hyp Ref Expression
1 dvrass.b B = Base R
2 dvrass.o U = Unit R
3 dvrass.d × ˙ = / r R
4 dvrass.t · ˙ = R
5 simp1 R Ring X B Y U R Ring
6 simp2 R Ring X B Y U X B
7 1 2 unitcl Y U Y B
8 7 3ad2ant3 R Ring X B Y U Y B
9 simp3 R Ring X B Y U Y U
10 1 2 3 4 dvrass R Ring X B Y B Y U X · ˙ Y × ˙ Y = X · ˙ Y × ˙ Y
11 5 6 8 9 10 syl13anc R Ring X B Y U X · ˙ Y × ˙ Y = X · ˙ Y × ˙ Y
12 eqid 1 R = 1 R
13 2 3 12 dvrid R Ring Y U Y × ˙ Y = 1 R
14 13 3adant2 R Ring X B Y U Y × ˙ Y = 1 R
15 14 oveq2d R Ring X B Y U X · ˙ Y × ˙ Y = X · ˙ 1 R
16 1 4 12 ringridm R Ring X B X · ˙ 1 R = X
17 16 3adant3 R Ring X B Y U X · ˙ 1 R = X
18 11 15 17 3eqtrd R Ring X B Y U X · ˙ Y × ˙ Y = X