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	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
	ellpi.r	$⊢ φ \to R \in Ring$
	ellpi.x	$⊢ φ \to X \in B$
Assertion	ellpi	$⊢ φ \to (Y \in K (\{X\}) \leftrightarrow X \underset{˙}{∥} Y)$

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

Metamath Proof Explorer