Metamath Proof Explorer

Theorem idlsrgbas

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

		Ref	Expression
	Hypotheses	idlsrgbas.1	$⊢ S = IDLsrg (R)$
		idlsrgbas.2	$⊢ I = LIdeal (R)$
	Assertion	idlsrgbas	$⊢ R \in V \to I = {Base}_{S}$

Proof

Step	Hyp	Ref	Expression
1		idlsrgbas.1	$⊢ S = IDLsrg (R)$
2		idlsrgbas.2	$⊢ I = LIdeal (R)$
3	2	fvexi	$⊢ I \in V$
4		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)\}⟩\}$
5	4	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⟩$
6		baseid	$⊢ Base = Slot {Base}_{ndx}$
7		snsstp1	$⊢ \{⟨{Base}_{ndx}, I⟩\} \subseteq \{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, LSSum (R)⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\}$
8		ssun1	$⊢ \{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, LSSum (R)⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) 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)\}⟩\}$
9	7 8	sstri	$⊢ \{⟨{Base}_{ndx}, I⟩\} \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)\}⟩\}$
10	5 6 9	strfv	$⊢ I \in V \to I = {Base}_{(\{⟨{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)\}⟩\})}$
11	3 10	ax-mp	$⊢ I = {Base}_{(\{⟨{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		eqid	$⊢ LSSum (R) = LSSum (R)$
13		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
14		eqid	$⊢ LSSum ({mulGrp}_{R}) = LSSum ({mulGrp}_{R})$
15	2 12 13 14	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)\}⟩\}$
16	1 15	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)\}⟩\}$
17	16	fveq2d	$⊢ R \in V \to {Base}_{S} = {Base}_{(\{⟨{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)\}⟩\})}$
18	11 17	eqtr4id	$⊢ R \in V \to I = {Base}_{S}$