idlsrgtset

Description: Topology component of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024)

	Ref	Expression
Hypotheses	idlsrgtset.1	$⊢ S = IDLsrg (R)$
	idlsrgtset.2	$⊢ I = LIdeal (R)$
	idlsrgtset.3	$⊢ J = ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})$
Assertion	idlsrgtset	$⊢ R \in V \to J = TopSet (S)$

Proof

Step	Hyp	Ref	Expression
1		idlsrgtset.1	$⊢ S = IDLsrg (R)$
2		idlsrgtset.2	$⊢ I = LIdeal (R)$
3		idlsrgtset.3	$⊢ J = ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})$
4	2	fvexi	$⊢ I \in V$
5	4	mptex	$⊢ (i \in I ⟼ \{j \in I \| \neg i \subseteq j\}) \in V$
6	5	rnex	$⊢ ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\}) \in V$
7		eqid	$⊢ \{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, LSSum (R)⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq I \land i \subseteq j)\}⟩\} = \{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, LSSum (R)⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq I \land i \subseteq j)\}⟩\}$
8	7	idlsrgstr	$⊢ (\{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, LSSum (R)⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq I \land i \subseteq j)\}⟩\}) Struct ⟨1, 10⟩$
9		tsetid	$⊢ TopSet = Slot TopSet (ndx)$
10		snsspr1	$⊢ \{⟨TopSet (ndx), ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})⟩\} \subseteq \{⟨TopSet (ndx), ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq I \land i \subseteq j)\}⟩\}$
11		ssun2	$⊢ \{⟨TopSet (ndx), ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq I \land i \subseteq j)\}⟩\} \subseteq \{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, LSSum (R)⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq I \land i \subseteq j)\}⟩\}$
12	10 11	sstri	$⊢ \{⟨TopSet (ndx), ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})⟩\} \subseteq \{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, LSSum (R)⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq I \land i \subseteq j)\}⟩\}$
13	8 9 12	strfv	$⊢ ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\}) \in V \to ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\}) = TopSet (\{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, LSSum (R)⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq I \land i \subseteq j)\}⟩\})$
14	6 13	ax-mp	$⊢ ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\}) = TopSet (\{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, LSSum (R)⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq I \land i \subseteq j)\}⟩\})$
15		eqid	$⊢ LSSum (R) = LSSum (R)$
16		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
17		eqid	$⊢ LSSum ({mulGrp}_{R}) = LSSum ({mulGrp}_{R})$
18	2 15 16 17	idlsrgval	$⊢ R \in V \to IDLsrg (R) = \{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, LSSum (R)⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq I \land i \subseteq j)\}⟩\}$
19	1 18	eqtrid	$⊢ R \in V \to S = \{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, LSSum (R)⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq I \land i \subseteq j)\}⟩\}$
20	19	fveq2d	$⊢ R \in V \to TopSet (S) = TopSet (\{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, LSSum (R)⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq I \land i \subseteq j)\}⟩\})$
21	14 20	eqtr4id	$⊢ R \in V \to ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\}) = TopSet (S)$
22	3 21	eqtrid	$⊢ R \in V \to J = TopSet (S)$

Metamath Proof Explorer

Theorem idlsrgtset

Proof