Theorem domnlcanbOLD

Description: Obsolete version of domnlcanb as of 21-Jun-2025. (Contributed by Thierry Arnoux, 8-Jun-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	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	domnlcanbOLD.r	⊢ ( 𝜑 → 𝑅 ∈ Domn )
Assertion	domnlcanbOLD	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) ↔ 𝑌 = 𝑍 ) )

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		domnlcanbOLD.r	⊢ ( 𝜑 → 𝑅 ∈ Domn )
8	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) ) → 𝑋 ∈ ( 𝐵 ∖ { 0 } ) )
9	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) ) → 𝑌 ∈ 𝐵 )
10	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) ) → 𝑍 ∈ 𝐵 )
11	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) ) → 𝑅 ∈ Domn )
12		simpr	⊢ ( ( 𝜑 ∧ ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) ) → ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) )
13	1 2 3 8 9 10 11 12	domnlcan	⊢ ( ( 𝜑 ∧ ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) ) → 𝑌 = 𝑍 )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → 𝑌 = 𝑍 )
15	14	oveq2d	⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) )
16	13 15	impbida	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) ↔ 𝑌 = 𝑍 ) )