Theorem rspsnasso

Description: Two elements X and Y of a ring R are associates, i.e. each divides the other, iff the ideals they generate are equal. (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	dvdsrspss.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	dvdsrspss.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
	dvdsrspss.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
	dvdsrspss.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	dvdsrspss.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	dvdsrspss.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion	rspsnasso	⊢ ( 𝜑 → ( ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) ↔ ( 𝐾 ‘ { 𝑌 } ) = ( 𝐾 ‘ { 𝑋 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvdsrspss.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		dvdsrspss.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
3		dvdsrspss.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
4		dvdsrspss.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		dvdsrspss.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		dvdsrspss.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7	1 2 3 4 5 6	dvdsrspss	⊢ ( 𝜑 → ( 𝑋 ∥ 𝑌 ↔ ( 𝐾 ‘ { 𝑌 } ) ⊆ ( 𝐾 ‘ { 𝑋 } ) ) )
8	1 2 3 5 4 6	dvdsrspss	⊢ ( 𝜑 → ( 𝑌 ∥ 𝑋 ↔ ( 𝐾 ‘ { 𝑋 } ) ⊆ ( 𝐾 ‘ { 𝑌 } ) ) )
9	7 8	anbi12d	⊢ ( 𝜑 → ( ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) ↔ ( ( 𝐾 ‘ { 𝑌 } ) ⊆ ( 𝐾 ‘ { 𝑋 } ) ∧ ( 𝐾 ‘ { 𝑋 } ) ⊆ ( 𝐾 ‘ { 𝑌 } ) ) ) )
10		eqss	⊢ ( ( 𝐾 ‘ { 𝑌 } ) = ( 𝐾 ‘ { 𝑋 } ) ↔ ( ( 𝐾 ‘ { 𝑌 } ) ⊆ ( 𝐾 ‘ { 𝑋 } ) ∧ ( 𝐾 ‘ { 𝑋 } ) ⊆ ( 𝐾 ‘ { 𝑌 } ) ) )
11	9 10	bitr4di	⊢ ( 𝜑 → ( ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) ↔ ( 𝐾 ‘ { 𝑌 } ) = ( 𝐾 ‘ { 𝑋 } ) ) )