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	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ 𝑋 ∥ 𝑌 ) )