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

Metamath Proof Explorer

Theorem rspsnasso

Description: Two elements X and Y of a ring R are associates, i.e. each divides the other, iff the ideals they generate are equal. (Contributed by Thierry Arnoux, 22-Mar-2025)

		Ref	Expression
	Hypotheses	dvdsrspss.b	$⊢ B = {Base}_{R}$
		dvdsrspss.k	$⊢ K = RSpan (R)$
		dvdsrspss.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
		dvdsrspss.x	$⊢ φ \to X \in B$
		dvdsrspss.y	$⊢ φ \to Y \in B$
		dvdsrspss.r	$⊢ φ \to R \in Ring$
	Assertion	rspsnasso	$⊢ φ \to ((X \underset{˙}{∥} Y \land Y \underset{˙}{∥} X) \leftrightarrow K (\{Y\}) = K (\{X\}))$

Proof

Step	Hyp	Ref	Expression
1		dvdsrspss.b	$⊢ B = {Base}_{R}$
2		dvdsrspss.k	$⊢ K = RSpan (R)$
3		dvdsrspss.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
4		dvdsrspss.x	$⊢ φ \to X \in B$
5		dvdsrspss.y	$⊢ φ \to Y \in B$
6		dvdsrspss.r	$⊢ φ \to R \in Ring$
7	1 2 3 4 5 6	dvdsrspss	$⊢ φ \to (X \underset{˙}{∥} Y \leftrightarrow K (\{Y\}) \subseteq K (\{X\}))$
8	1 2 3 5 4 6	dvdsrspss	$⊢ φ \to (Y \underset{˙}{∥} X \leftrightarrow K (\{X\}) \subseteq K (\{Y\}))$
9	7 8	anbi12d	$⊢ φ \to ((X \underset{˙}{∥} Y \land Y \underset{˙}{∥} X) \leftrightarrow (K (\{Y\}) \subseteq K (\{X\}) \land K (\{X\}) \subseteq K (\{Y\})))$
10		eqss	$⊢ K (\{Y\}) = K (\{X\}) \leftrightarrow (K (\{Y\}) \subseteq K (\{X\}) \land K (\{X\}) \subseteq K (\{Y\}))$
11	9 10	bitr4di	$⊢ φ \to ((X \underset{˙}{∥} Y \land Y \underset{˙}{∥} X) \leftrightarrow K (\{Y\}) = K (\{X\}))$