Metamath Proof Explorer

Theorem dvrcan1

Description: A cancellation law for division. ( divcan1 analog.) (Contributed by Mario Carneiro, 2-Jul-2014) (Revised by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypotheses dvrass.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
dvrass.o ⊢ 𝑈 = ( Unit ‘ 𝑅 )
dvrass.d ⊢ / = ( /r ‘ 𝑅 )
dvrass.t ⊢ · = ( .r ‘ 𝑅 )
Assertion dvrcan1 ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 / 𝑌 ) · 𝑌 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 dvrass.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 dvrass.o ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 dvrass.d ⊢ / = ( /r ‘ 𝑅 )
4 dvrass.t ⊢ · = ( .r ‘ 𝑅 )
5 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
6 1 4 2 5 3 dvrval ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 / 𝑌 ) = ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
7 6 3adant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 / 𝑌 ) = ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
8 7 oveq1d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 / 𝑌 ) · 𝑌 ) = ( ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) · 𝑌 ) )
9 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → 𝑅 ∈ Ring )
10 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ∈ 𝐵 )
11 2 5 1 ringinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 )
12 11 3adant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 )
13 1 2 unitcl ⊢ ( 𝑌 ∈ 𝑈 → 𝑌 ∈ 𝐵 )
14 13 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ∈ 𝐵 )
15 1 4 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) · 𝑌 ) = ( 𝑋 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) · 𝑌 ) ) )
16 9 10 12 14 15 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) · 𝑌 ) = ( 𝑋 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) · 𝑌 ) ) )
17 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
18 2 5 4 17 unitlinv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) · 𝑌 ) = ( 1r ‘ 𝑅 ) )
19 18 3adant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) · 𝑌 ) = ( 1r ‘ 𝑅 ) )
20 19 oveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) · 𝑌 ) ) = ( 𝑋 · ( 1r ‘ 𝑅 ) ) )
21 1 4 17 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · ( 1r ‘ 𝑅 ) ) = 𝑋 )
22 21 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · ( 1r ‘ 𝑅 ) ) = 𝑋 )
23 20 22 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · ( ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) · 𝑌 ) ) = 𝑋 )
24 16 23 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 · ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) · 𝑌 ) = 𝑋 )
25 8 24 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 / 𝑌 ) · 𝑌 ) = 𝑋 )