This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) ↔ ( 𝐾 ‘ { 𝑌 } ) = ( 𝐾 ‘ { 𝑋 } ) ) )