Theorem idomrcan

Description: Right-cancellation law for integral domains. (Contributed by Thierry Arnoux, 22-Mar-2025) (Proof shortened by SN, 21-Jun-2025)

	Ref	Expression
Hypotheses	idomrcan.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	idomrcan.0	⊢ 0 = ( 0g ‘ 𝑅 )
	idomrcan.m	⊢ · = ( .r ‘ 𝑅 )
	idomrcan.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	idomrcan.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	idomrcan.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝐵 ∖ { 0 } ) )
	idomrcan.r	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
	idomrcan.1	⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) )
Assertion	idomrcan	⊢ ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		idomrcan.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		idomrcan.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		idomrcan.m	⊢ · = ( .r ‘ 𝑅 )
4		idomrcan.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		idomrcan.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		idomrcan.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝐵 ∖ { 0 } ) )
7		idomrcan.r	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
8		idomrcan.1	⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) )
9	7	idomdomd	⊢ ( 𝜑 → 𝑅 ∈ Domn )
10	1 2 3 4 5 6 9 8	domnrcan	⊢ ( 𝜑 → 𝑋 = 𝑌 )