Theorem dvreq1

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

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

Proof

Step	Hyp	Ref	Expression
1		dvreq1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		dvreq1.o	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		dvreq1.d	⊢ / = ( /r ‘ 𝑅 )
4		dvreq1.t	⊢ 1 = ( 1r ‘ 𝑅 )
5		oveq1	⊢ ( ( 𝑋 / 𝑌 ) = 1 → ( ( 𝑋 / 𝑌 ) ( .r ‘ 𝑅 ) 𝑌 ) = ( 1 ( .r ‘ 𝑅 ) 𝑌 ) )
6		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
7	1 2 3 6	dvrcan1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 / 𝑌 ) ( .r ‘ 𝑅 ) 𝑌 ) = 𝑋 )
8	1 2	unitcl	⊢ ( 𝑌 ∈ 𝑈 → 𝑌 ∈ 𝐵 )
9	1 6 4	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) → ( 1 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑌 )
10	8 9	sylan2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( 1 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑌 )
11	10	3adant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 1 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑌 )
12	7 11	eqeq12d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( ( 𝑋 / 𝑌 ) ( .r ‘ 𝑅 ) 𝑌 ) = ( 1 ( .r ‘ 𝑅 ) 𝑌 ) ↔ 𝑋 = 𝑌 ) )
13	5 12	syl5ib	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 / 𝑌 ) = 1 → 𝑋 = 𝑌 ) )
14	2 3 4	dvrid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( 𝑌 / 𝑌 ) = 1 )
15	14	3adant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑌 / 𝑌 ) = 1 )
16		oveq1	⊢ ( 𝑋 = 𝑌 → ( 𝑋 / 𝑌 ) = ( 𝑌 / 𝑌 ) )
17	16	eqeq1d	⊢ ( 𝑋 = 𝑌 → ( ( 𝑋 / 𝑌 ) = 1 ↔ ( 𝑌 / 𝑌 ) = 1 ) )
18	15 17	syl5ibrcom	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 = 𝑌 → ( 𝑋 / 𝑌 ) = 1 ) )
19	13 18	impbid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 / 𝑌 ) = 1 ↔ 𝑋 = 𝑌 ) )