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

Metamath Proof Explorer

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