rspprop

Description: Properties of a class to be the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 30-Jun-2026)

	Ref	Expression
Hypotheses	rspvalint.v	$⊢ B = {Base}_{R}$
	rspvalint.i	$⊢ I = LIdeal (R)$
	rspvalint.k	$⊢ K = RSpan (R)$
Assertion	rspprop	$⊢ (R \in Ring \land S \subseteq B) \to (K (S) = X \leftrightarrow (X \in I \land S \subseteq X \land \forall i \in I (S \subseteq i \to X \subseteq i)))$

Proof

Step	Hyp	Ref	Expression
1		rspvalint.v	$⊢ B = {Base}_{R}$
2		rspvalint.i	$⊢ I = LIdeal (R)$
3		rspvalint.k	$⊢ K = RSpan (R)$
4	3 1 2	rspcl	$⊢ (R \in Ring \land S \subseteq B) \to K (S) \in I$
5	3 1	rspssid	$⊢ (R \in Ring \land S \subseteq B) \to S \subseteq K (S)$
6	3 2	rspssp	$⊢ (R \in Ring \land i \in I \land S \subseteq i) \to K (S) \subseteq i$
7	6	3expia	$⊢ (R \in Ring \land i \in I) \to (S \subseteq i \to K (S) \subseteq i)$
8	7	ralrimiva	$⊢ R \in Ring \to \forall i \in I (S \subseteq i \to K (S) \subseteq i)$
9	8	adantr	$⊢ (R \in Ring \land S \subseteq B) \to \forall i \in I (S \subseteq i \to K (S) \subseteq i)$
10	4 5 9	3jca	$⊢ (R \in Ring \land S \subseteq B) \to (K (S) \in I \land S \subseteq K (S) \land \forall i \in I (S \subseteq i \to K (S) \subseteq i))$
11		eleq1	$⊢ K (S) = X \to (K (S) \in I \leftrightarrow X \in I)$
12		sseq2	$⊢ K (S) = X \to (S \subseteq K (S) \leftrightarrow S \subseteq X)$
13		sseq1	$⊢ K (S) = X \to (K (S) \subseteq i \leftrightarrow X \subseteq i)$
14	13	imbi2d	$⊢ K (S) = X \to ((S \subseteq i \to K (S) \subseteq i) \leftrightarrow (S \subseteq i \to X \subseteq i))$
15	14	ralbidv	$⊢ K (S) = X \to (\forall i \in I (S \subseteq i \to K (S) \subseteq i) \leftrightarrow \forall i \in I (S \subseteq i \to X \subseteq i))$
16	11 12 15	3anbi123d	$⊢ K (S) = X \to ((K (S) \in I \land S \subseteq K (S) \land \forall i \in I (S \subseteq i \to K (S) \subseteq i)) \leftrightarrow (X \in I \land S \subseteq X \land \forall i \in I (S \subseteq i \to X \subseteq i)))$
17	10 16	syl5ibcom	$⊢ (R \in Ring \land S \subseteq B) \to (K (S) = X \to (X \in I \land S \subseteq X \land \forall i \in I (S \subseteq i \to X \subseteq i)))$
18	3 2	rspssp	$⊢ (R \in Ring \land X \in I \land S \subseteq X) \to K (S) \subseteq X$
19	18	3adant3r3	$⊢ (R \in Ring \land (X \in I \land S \subseteq X \land \forall i \in I (S \subseteq i \to X \subseteq i))) \to K (S) \subseteq X$
20	19	adantlr	$⊢ ((R \in Ring \land S \subseteq B) \land (X \in I \land S \subseteq X \land \forall i \in I (S \subseteq i \to X \subseteq i))) \to K (S) \subseteq X$
21		ssint	$⊢ X \subseteq ⋂ \{j \in I \| S \subseteq j\} \leftrightarrow \forall i \in \{j \in I \| S \subseteq j\} X \subseteq i$
22		sseq2	$⊢ j = i \to (S \subseteq j \leftrightarrow S \subseteq i)$
23	22	ralrab	$⊢ \forall i \in \{j \in I \| S \subseteq j\} X \subseteq i \leftrightarrow \forall i \in I (S \subseteq i \to X \subseteq i)$
24	21 23	sylbbr	$⊢ \forall i \in I (S \subseteq i \to X \subseteq i) \to X \subseteq ⋂ \{j \in I \| S \subseteq j\}$
25	24	3ad2ant3	$⊢ (X \in I \land S \subseteq X \land \forall i \in I (S \subseteq i \to X \subseteq i)) \to X \subseteq ⋂ \{j \in I \| S \subseteq j\}$
26	25	adantl	$⊢ ((R \in Ring \land S \subseteq B) \land (X \in I \land S \subseteq X \land \forall i \in I (S \subseteq i \to X \subseteq i))) \to X \subseteq ⋂ \{j \in I \| S \subseteq j\}$
27	1 2 3	rspvalint	$⊢ (R \in Ring \land S \subseteq B) \to K (S) = ⋂ \{j \in I \| S \subseteq j\}$
28	27	adantr	$⊢ ((R \in Ring \land S \subseteq B) \land (X \in I \land S \subseteq X \land \forall i \in I (S \subseteq i \to X \subseteq i))) \to K (S) = ⋂ \{j \in I \| S \subseteq j\}$
29	26 28	sseqtrrd	$⊢ ((R \in Ring \land S \subseteq B) \land (X \in I \land S \subseteq X \land \forall i \in I (S \subseteq i \to X \subseteq i))) \to X \subseteq K (S)$
30	20 29	eqssd	$⊢ ((R \in Ring \land S \subseteq B) \land (X \in I \land S \subseteq X \land \forall i \in I (S \subseteq i \to X \subseteq i))) \to K (S) = X$
31	30	ex	$⊢ (R \in Ring \land S \subseteq B) \to ((X \in I \land S \subseteq X \land \forall i \in I (S \subseteq i \to X \subseteq i)) \to K (S) = X)$
32	17 31	impbid	$⊢ (R \in Ring \land S \subseteq B) \to (K (S) = X \leftrightarrow (X \in I \land S \subseteq X \land \forall i \in I (S \subseteq i \to X \subseteq i)))$

Metamath Proof Explorer

Theorem rspprop

Proof