dvdsrspss

Description: In a ring, an element X divides Y iff the ideal generated by Y is a subset of the ideal generated by X (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	dvdsrspss	$⊢ φ \to (X \underset{˙}{∥} Y \leftrightarrow K (\{Y\}) \subseteq 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		eqid	$⊢ \cdot_{R} = \cdot_{R}$
8	1 3 7	dvdsr	$⊢ X \underset{˙}{∥} Y \leftrightarrow (X \in B \land \exists t \in B t \cdot_{R} X = Y)$
9	4	biantrurd	$⊢ φ \to (\exists t \in B t \cdot_{R} X = Y \leftrightarrow (X \in B \land \exists t \in B t \cdot_{R} X = Y))$
10	8 9	bitr4id	$⊢ φ \to (X \underset{˙}{∥} Y \leftrightarrow \exists t \in B t \cdot_{R} X = Y)$
11	1 7 2	elrspsn	$⊢ (R \in Ring \land X \in B) \to (Y \in K (\{X\}) \leftrightarrow \exists t \in B Y = t \cdot_{R} X)$
12	6 4 11	syl2anc	$⊢ φ \to (Y \in K (\{X\}) \leftrightarrow \exists t \in B Y = t \cdot_{R} X)$
13		eqcom	$⊢ t \cdot_{R} X = Y \leftrightarrow Y = t \cdot_{R} X$
14	13	rexbii	$⊢ \exists t \in B t \cdot_{R} X = Y \leftrightarrow \exists t \in B Y = t \cdot_{R} X$
15	12 14	bitr4di	$⊢ φ \to (Y \in K (\{X\}) \leftrightarrow \exists t \in B t \cdot_{R} X = Y)$
16	6	adantr	$⊢ (φ \land Y \in K (\{X\})) \to R \in Ring$
17	4	snssd	$⊢ φ \to \{X\} \subseteq B$
18		eqid	$⊢ LIdeal (R) = LIdeal (R)$
19	2 1 18	rspcl	$⊢ (R \in Ring \land \{X\} \subseteq B) \to K (\{X\}) \in LIdeal (R)$
20	6 17 19	syl2anc	$⊢ φ \to K (\{X\}) \in LIdeal (R)$
21	20	adantr	$⊢ (φ \land Y \in K (\{X\})) \to K (\{X\}) \in LIdeal (R)$
22		simpr	$⊢ (φ \land Y \in K (\{X\})) \to Y \in K (\{X\})$
23	22	snssd	$⊢ (φ \land Y \in K (\{X\})) \to \{Y\} \subseteq K (\{X\})$
24	2 18	rspssp	$⊢ (R \in Ring \land K (\{X\}) \in LIdeal (R) \land \{Y\} \subseteq K (\{X\})) \to K (\{Y\}) \subseteq K (\{X\})$
25	16 21 23 24	syl3anc	$⊢ (φ \land Y \in K (\{X\})) \to K (\{Y\}) \subseteq K (\{X\})$
26		simpr	$⊢ (φ \land K (\{Y\}) \subseteq K (\{X\})) \to K (\{Y\}) \subseteq K (\{X\})$
27	5	snssd	$⊢ φ \to \{Y\} \subseteq B$
28	2 1	rspssid	$⊢ (R \in Ring \land \{Y\} \subseteq B) \to \{Y\} \subseteq K (\{Y\})$
29	6 27 28	syl2anc	$⊢ φ \to \{Y\} \subseteq K (\{Y\})$
30		snssg	$⊢ Y \in B \to (Y \in K (\{Y\}) \leftrightarrow \{Y\} \subseteq K (\{Y\}))$
31	30	biimpar	$⊢ (Y \in B \land \{Y\} \subseteq K (\{Y\})) \to Y \in K (\{Y\})$
32	5 29 31	syl2anc	$⊢ φ \to Y \in K (\{Y\})$
33	32	adantr	$⊢ (φ \land K (\{Y\}) \subseteq K (\{X\})) \to Y \in K (\{Y\})$
34	26 33	sseldd	$⊢ (φ \land K (\{Y\}) \subseteq K (\{X\})) \to Y \in K (\{X\})$
35	25 34	impbida	$⊢ φ \to (Y \in K (\{X\}) \leftrightarrow K (\{Y\}) \subseteq K (\{X\}))$
36	10 15 35	3bitr2d	$⊢ φ \to (X \underset{˙}{∥} Y \leftrightarrow K (\{Y\}) \subseteq K (\{X\}))$

Metamath Proof Explorer

Theorem dvdsrspss

Proof