Theorem ellpi

Description: Elementhood in a left principal ideal in terms of the "divides" relation. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	ellpi.b	|- B = ( Base ` R )
	ellpi.k	|- K = ( RSpan ` R )
	ellpi.d	|- .|| = ( ||r ` R )
	ellpi.r	|- ( ph -> R e. Ring )
	ellpi.x	|- ( ph -> X e. B )
Assertion	ellpi	|- ( ph -> ( Y e. ( K ` { X } ) <-> X .|| Y ) )

Proof

Step	Hyp	Ref	Expression
1		ellpi.b	|- B = ( Base ` R )
2		ellpi.k	|- K = ( RSpan ` R )
3		ellpi.d	|- .|| = ( ||r ` R )
4		ellpi.r	|- ( ph -> R e. Ring )
5		ellpi.x	|- ( ph -> X e. B )
6		elex	|- ( Y e. ( K ` { X } ) -> Y e. _V )
7	6	adantl	|- ( ( ph /\ Y e. ( K ` { X } ) ) -> Y e. _V )
8	3	reldvdsr	|- Rel .||
9	8	brrelex2i	|- ( X .|| Y -> Y e. _V )
10	9	adantl	|- ( ( ph /\ X .|| Y ) -> Y e. _V )
11	1 2 3	rspsn	|- ( ( R e. Ring /\ X e. B ) -> ( K ` { X } ) = { y | X .|| y } )
12	4 5 11	syl2anc	|- ( ph -> ( K ` { X } ) = { y | X .|| y } )
13	12	eleq2d	|- ( ph -> ( Y e. ( K ` { X } ) <-> Y e. { y | X .|| y } ) )
14		breq2	|- ( y = Y -> ( X .|| y <-> X .|| Y ) )
15	14	elabg	|- ( Y e. _V -> ( Y e. { y | X .|| y } <-> X .|| Y ) )
16	13 15	sylan9bb	|- ( ( ph /\ Y e. _V ) -> ( Y e. ( K ` { X } ) <-> X .|| Y ) )
17	7 10 16	bibiad	|- ( ph -> ( Y e. ( K ` { X } ) <-> X .|| Y ) )