Theorem idomrcanOLD

Description: Obsolete version of idomrcan as of 21-Jun-2025. (Contributed by Thierry Arnoux, 22-Mar-2025) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		domncanOLD.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		domncanOLD.1	⊢ 0 = ( 0g ‘ 𝑅 )
3		domncanOLD.m	⊢ · = ( .r ‘ 𝑅 )
4		domncanOLD.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ { 0 } ) )
5		domncanOLD.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		domncanOLD.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
7		idomrcanOLD.r	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
8		idomrcanOLD.2	⊢ ( 𝜑 → ( 𝑌 · 𝑋 ) = ( 𝑍 · 𝑋 ) )
9	7	idomdomd	⊢ ( 𝜑 → 𝑅 ∈ Domn )
10		df-idom	⊢ IDomn = ( CRing ∩ Domn )
11	7 10	eleqtrdi	⊢ ( 𝜑 → 𝑅 ∈ ( CRing ∩ Domn ) )
12	11	elin1d	⊢ ( 𝜑 → 𝑅 ∈ CRing )
13	4	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
14	1 3	crngcom	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) = ( 𝑌 · 𝑋 ) )
15	12 13 5 14	syl3anc	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) = ( 𝑌 · 𝑋 ) )
16	1 3	crngcom	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 · 𝑍 ) = ( 𝑍 · 𝑋 ) )
17	12 13 6 16	syl3anc	⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) = ( 𝑍 · 𝑋 ) )
18	8 15 17	3eqtr4d	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) )
19	1 2 3 4 5 6 9 18	domnlcan	⊢ ( 𝜑 → 𝑌 = 𝑍 )