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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 · 𝑌 ) / 𝑌 ) = 𝑋 )