Theorem idomcanr

Description: Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011) (Revised by AV, 13-Jul-2026)

	Ref	Expression
Hypotheses	isidom3.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	isidom3.t	⊢ · = ( .r ‘ 𝑅 )
	isidom3.0	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	idomcanr	⊢ ( ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≠ 0 ) → ( ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) → 𝑋 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		isidom3.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		isidom3.t	⊢ · = ( .r ‘ 𝑅 )
3		isidom3.0	⊢ 0 = ( 0g ‘ 𝑅 )
4		isidom	⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
5	4	simplbi	⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ CRing )
6	1 2	crngcom	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 · 𝑍 ) = ( 𝑍 · 𝑋 ) )
7	6	3adant3r2	⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 · 𝑍 ) = ( 𝑍 · 𝑋 ) )
8	1 2	crngcom	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 · 𝑍 ) = ( 𝑍 · 𝑌 ) )
9	8	3adant3r1	⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 · 𝑍 ) = ( 𝑍 · 𝑌 ) )
10	7 9	eqeq12d	⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) ↔ ( 𝑍 · 𝑋 ) = ( 𝑍 · 𝑌 ) ) )
11	5 10	sylan	⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) ↔ ( 𝑍 · 𝑋 ) = ( 𝑍 · 𝑌 ) ) )
12	11	adantr	⊢ ( ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≠ 0 ) → ( ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) ↔ ( 𝑍 · 𝑋 ) = ( 𝑍 · 𝑌 ) ) )
13		3anrot	⊢ ( ( 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) )
14	13	biimpri	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
15	1 2 3	idomcanl	⊢ ( ( ( 𝑅 ∈ IDomn ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑍 ≠ 0 ) → ( ( 𝑍 · 𝑋 ) = ( 𝑍 · 𝑌 ) → 𝑋 = 𝑌 ) )
16	14 15	sylanl2	⊢ ( ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≠ 0 ) → ( ( 𝑍 · 𝑋 ) = ( 𝑍 · 𝑌 ) → 𝑋 = 𝑌 ) )
17	12 16	sylbid	⊢ ( ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≠ 0 ) → ( ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) → 𝑋 = 𝑌 ) )