Metamath Proof Explorer


Theorem dvreq1

Description: A cancellation law for division. ( diveq1 analog.) (Contributed by Mario Carneiro, 28-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 dvreq1.b B = Base R
2 dvreq1.o U = Unit R
3 dvreq1.d × ˙ = / r R
4 dvreq1.t 1 ˙ = 1 R
5 oveq1 X × ˙ Y = 1 ˙ X × ˙ Y R Y = 1 ˙ R Y
6 eqid R = R
7 1 2 3 6 dvrcan1 R Ring X B Y U X × ˙ Y R Y = X
8 1 2 unitcl Y U Y B
9 1 6 4 ringlidm R Ring Y B 1 ˙ R Y = Y
10 8 9 sylan2 R Ring Y U 1 ˙ R Y = Y
11 10 3adant2 R Ring X B Y U 1 ˙ R Y = Y
12 7 11 eqeq12d R Ring X B Y U X × ˙ Y R Y = 1 ˙ R Y X = Y
13 5 12 syl5ib R Ring X B Y U X × ˙ Y = 1 ˙ X = Y
14 2 3 4 dvrid R Ring Y U Y × ˙ Y = 1 ˙
15 14 3adant2 R Ring X B Y U Y × ˙ Y = 1 ˙
16 oveq1 X = Y X × ˙ Y = Y × ˙ Y
17 16 eqeq1d X = Y X × ˙ Y = 1 ˙ Y × ˙ Y = 1 ˙
18 15 17 syl5ibrcom R Ring X B Y U X = Y X × ˙ Y = 1 ˙
19 13 18 impbid R Ring X B Y U X × ˙ Y = 1 ˙ X = Y