This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
dvrass.o ⊢ 𝑈 = ( Unit ‘ 𝑅 )
dvrass.d ⊢ / = ( /r ‘ 𝑅 )
dvrass.t ⊢ · = ( .r ‘ 𝑅 )
Assertion dvrcan3 ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 · 𝑌 ) / 𝑌 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 dvrass.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 dvrass.o ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 dvrass.d ⊢ / = ( /r ‘ 𝑅 )
4 dvrass.t ⊢ · = ( .r ‘ 𝑅 )
5 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → 𝑅 ∈ Ring )
6 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ∈ 𝐵 )
7 1 2 unitcl ⊢ ( 𝑌 ∈ 𝑈 → 𝑌 ∈ 𝐵 )
8 7 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ∈ 𝐵 )
9 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ∈ 𝑈 )
10 1 2 3 4 dvrass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑌 ) / 𝑌 ) = ( 𝑋 · ( 𝑌 / 𝑌 ) ) )
11 5 6 8 9 10 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 · 𝑌 ) / 𝑌 ) = ( 𝑋 · ( 𝑌 / 𝑌 ) ) )
12 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
13 2 3 12 dvrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( 𝑌 / 𝑌 ) = ( 1r ‘ 𝑅 ) )
14 13 3adant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑌 / 𝑌 ) = ( 1r ‘ 𝑅 ) )
15 14 oveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · ( 𝑌 / 𝑌 ) ) = ( 𝑋 · ( 1r ‘ 𝑅 ) ) )
16 1 4 12 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · ( 1r ‘ 𝑅 ) ) = 𝑋 )
17 16 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · ( 1r ‘ 𝑅 ) ) = 𝑋 )
18 11 15 17 3eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 · 𝑌 ) / 𝑌 ) = 𝑋 )