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 } ) ) )