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={\mathrm{Base}}_R$$
	ellpi.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
	ellpi.d	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
	ellpi.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	ellpi.x	$$⊢\phi \to X\in B$$
Assertion	ellpi	$$⊢\phi \to \left(Y\in K\left(\left\{X\right\}\right)\leftrightarrow X\underset{\dot{}}{\parallel }Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		ellpi.b	$$⊢B={\mathrm{Base}}_R$$
2		ellpi.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
3		ellpi.d	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
4		ellpi.r	$$⊢\phi \to R\in \mathrm{Ring}$$
5		ellpi.x	$$⊢\phi \to X\in B$$
6		elex	$$⊢Y\in K\left(\left\{X\right\}\right)\to Y\in \mathrm{V}$$
7	6	adantl	$$⊢\left(\phi \wedge Y\in K\left(\left\{X\right\}\right)\right)\to Y\in \mathrm{V}$$
8	3	reldvdsr	$$⊢\mathrm{Rel}\underset{\dot{}}{\parallel }$$
9	8	brrelex2i	$$⊢X\underset{\dot{}}{\parallel }Y\to Y\in \mathrm{V}$$
10	9	adantl	$$⊢\left(\phi \wedge X\underset{\dot{}}{\parallel }Y\right)\to Y\in \mathrm{V}$$
11	1 2 3	rspsn	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to K\left(\left\{X\right\}\right)=\left\{y|X\underset{\dot{}}{\parallel }y\right\}$$
12	4 5 11	syl2anc	$$⊢\phi \to K\left(\left\{X\right\}\right)=\left\{y|X\underset{\dot{}}{\parallel }y\right\}$$
13	12	eleq2d	$$⊢\phi \to \left(Y\in K\left(\left\{X\right\}\right)\leftrightarrow Y\in \left\{y|X\underset{\dot{}}{\parallel }y\right\}\right)$$
14		breq2	$$⊢y=Y\to \left(X\underset{\dot{}}{\parallel }y\leftrightarrow X\underset{\dot{}}{\parallel }Y\right)$$
15	14	elabg	$$⊢Y\in \mathrm{V}\to \left(Y\in \left\{y|X\underset{\dot{}}{\parallel }y\right\}\leftrightarrow X\underset{\dot{}}{\parallel }Y\right)$$
16	13 15	sylan9bb	$$⊢\left(\phi \wedge Y\in \mathrm{V}\right)\to \left(Y\in K\left(\left\{X\right\}\right)\leftrightarrow X\underset{\dot{}}{\parallel }Y\right)$$
17	7 10 16	bibiad	$$⊢\phi \to \left(Y\in K\left(\left\{X\right\}\right)\leftrightarrow X\underset{\dot{}}{\parallel }Y\right)$$