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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
ellpi.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
ellpi.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
ellpi.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
ellpi.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion ellpi ( 𝜑 → ( 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ 𝑋 ∥ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 ellpi.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ellpi.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
3 ellpi.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
4 ellpi.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 ellpi.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 elex ⊢ ( 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) → 𝑌 ∈ V )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) ) → 𝑌 ∈ V )
8 3 reldvdsr ⊢ Rel ∥
9 8 brrelex2i ⊢ ( 𝑋 ∥ 𝑌 → 𝑌 ∈ V )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∥ 𝑌 ) → 𝑌 ∈ V )
11 1 2 3 rspsn ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝑋 } ) = { 𝑦 ∣ 𝑋 ∥ 𝑦 } )
12 4 5 11 syl2anc ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) = { 𝑦 ∣ 𝑋 ∥ 𝑦 } )
13 12 eleq2d ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ 𝑌 ∈ { 𝑦 ∣ 𝑋 ∥ 𝑦 } ) )
14 breq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 ∥ 𝑦 ↔ 𝑋 ∥ 𝑌 ) )
15 14 elabg ⊢ ( 𝑌 ∈ V → ( 𝑌 ∈ { 𝑦 ∣ 𝑋 ∥ 𝑦 } ↔ 𝑋 ∥ 𝑌 ) )
16 13 15 sylan9bb ⊢ ( ( 𝜑 ∧ 𝑌 ∈ V ) → ( 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ 𝑋 ∥ 𝑌 ) )
17 7 10 16 bibiad ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ 𝑋 ∥ 𝑌 ) )