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 
|- B = ( Base ` R )
dvdsrspss.k 
|- K = ( RSpan ` R )
dvdsrspss.d 
|- .|| = ( ||r ` R )
dvdsrspss.x 
|- ( ph -> X e. B )
dvdsrspss.y 
|- ( ph -> Y e. B )
dvdsrspss.r 
|- ( ph -> R e. Ring )
Assertion rspsnasso 
|- ( ph -> ( ( X .|| Y /\ Y .|| X ) <-> ( K ` { Y } ) = ( K ` { X } ) ) )

Proof

Step Hyp Ref Expression
1 dvdsrspss.b 
 |-  B = ( Base ` R )
2 dvdsrspss.k 
 |-  K = ( RSpan ` R )
3 dvdsrspss.d 
 |-  .|| = ( ||r ` R )
4 dvdsrspss.x 
 |-  ( ph -> X e. B )
5 dvdsrspss.y 
 |-  ( ph -> Y e. B )
6 dvdsrspss.r 
 |-  ( ph -> R e. Ring )
7 1 2 3 4 5 6 dvdsrspss 
 |-  ( ph -> ( X .|| Y <-> ( K ` { Y } ) C_ ( K ` { X } ) ) )
8 1 2 3 5 4 6 dvdsrspss 
 |-  ( ph -> ( Y .|| X <-> ( K ` { X } ) C_ ( K ` { Y } ) ) )
9 7 8 anbi12d 
 |-  ( ph -> ( ( X .|| Y /\ Y .|| X ) <-> ( ( K ` { Y } ) C_ ( K ` { X } ) /\ ( K ` { X } ) C_ ( K ` { Y } ) ) ) )
10 eqss 
 |-  ( ( K ` { Y } ) = ( K ` { X } ) <-> ( ( K ` { Y } ) C_ ( K ` { X } ) /\ ( K ` { X } ) C_ ( K ` { Y } ) ) )
11 9 10 bitr4di 
 |-  ( ph -> ( ( X .|| Y /\ Y .|| X ) <-> ( K ` { Y } ) = ( K ` { X } ) ) )