Metamath Proof Explorer

Theorem idlsrgplusg

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

		Ref	Expression
	Hypotheses	idlsrgplusg.1	$⊢ S = IDLsrg (R)$
		idlsrgplusg.2	$⊢ \underset{˙}{\oplus} = LSSum (R)$
	Assertion	idlsrgplusg	$⊢ R \in V \to \underset{˙}{\oplus} = +_{S}$

Proof

Step	Hyp	Ref	Expression
1		idlsrgplusg.1	$⊢ S = IDLsrg (R)$
2		idlsrgplusg.2	$⊢ \underset{˙}{\oplus} = LSSum (R)$
3	2	fvexi	$⊢ \underset{˙}{\oplus} \in V$
4		eqid	$⊢ \{⟨{Base}_{ndx}, LIdeal (R)⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in LIdeal (R), j \in LIdeal (R) ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in LIdeal (R) ⟼ \{j \in LIdeal (R) \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq LIdeal (R) \land i \subseteq j)\}⟩\} = \{⟨{Base}_{ndx}, LIdeal (R)⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in LIdeal (R), j \in LIdeal (R) ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in LIdeal (R) ⟼ \{j \in LIdeal (R) \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq LIdeal (R) \land i \subseteq j)\}⟩\}$
5	4	idlsrgstr	$⊢ (\{⟨{Base}_{ndx}, LIdeal (R)⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in LIdeal (R), j \in LIdeal (R) ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in LIdeal (R) ⟼ \{j \in LIdeal (R) \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq LIdeal (R) \land i \subseteq j)\}⟩\}) Struct ⟨1, 10⟩$
6		plusgid	$⊢ +_{𝑔} = Slot +_{ndx}$
7		snsstp2	$⊢ \{⟨+_{ndx}, \underset{˙}{\oplus}⟩\} \subseteq \{⟨{Base}_{ndx}, LIdeal (R)⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in LIdeal (R), j \in LIdeal (R) ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\}$
8		ssun1	$⊢ \{⟨{Base}_{ndx}, LIdeal (R)⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in LIdeal (R), j \in LIdeal (R) ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \subseteq \{⟨{Base}_{ndx}, LIdeal (R)⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in LIdeal (R), j \in LIdeal (R) ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in LIdeal (R) ⟼ \{j \in LIdeal (R) \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq LIdeal (R) \land i \subseteq j)\}⟩\}$
9	7 8	sstri	$⊢ \{⟨+_{ndx}, \underset{˙}{\oplus}⟩\} \subseteq \{⟨{Base}_{ndx}, LIdeal (R)⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in LIdeal (R), j \in LIdeal (R) ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in LIdeal (R) ⟼ \{j \in LIdeal (R) \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq LIdeal (R) \land i \subseteq j)\}⟩\}$
10	5 6 9	strfv	$⊢ \underset{˙}{\oplus} \in V \to \underset{˙}{\oplus} = +_{(\{⟨{Base}_{ndx}, LIdeal (R)⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in LIdeal (R), j \in LIdeal (R) ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in LIdeal (R) ⟼ \{j \in LIdeal (R) \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq LIdeal (R) \land i \subseteq j)\}⟩\})}$
11	3 10	ax-mp	$⊢ \underset{˙}{\oplus} = +_{(\{⟨{Base}_{ndx}, LIdeal (R)⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in LIdeal (R), j \in LIdeal (R) ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in LIdeal (R) ⟼ \{j \in LIdeal (R) \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq LIdeal (R) \land i \subseteq j)\}⟩\})}$
12		eqid	$⊢ LIdeal (R) = LIdeal (R)$
13		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
14		eqid	$⊢ LSSum ({mulGrp}_{R}) = LSSum ({mulGrp}_{R})$
15	12 2 13 14	idlsrgval	$⊢ R \in V \to IDLsrg (R) = \{⟨{Base}_{ndx}, LIdeal (R)⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in LIdeal (R), j \in LIdeal (R) ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in LIdeal (R) ⟼ \{j \in LIdeal (R) \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq LIdeal (R) \land i \subseteq j)\}⟩\}$
16	1 15	eqtrid	$⊢ R \in V \to S = \{⟨{Base}_{ndx}, LIdeal (R)⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in LIdeal (R), j \in LIdeal (R) ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in LIdeal (R) ⟼ \{j \in LIdeal (R) \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq LIdeal (R) \land i \subseteq j)\}⟩\}$
17	16	fveq2d	$⊢ R \in V \to +_{S} = +_{(\{⟨{Base}_{ndx}, LIdeal (R)⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in LIdeal (R), j \in LIdeal (R) ⟼ RSpan (R) (i LSSum ({mulGrp}_{R}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in LIdeal (R) ⟼ \{j \in LIdeal (R) \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq LIdeal (R) \land i \subseteq j)\}⟩\})}$
18	11 17	eqtr4id	$⊢ R \in V \to \underset{˙}{\oplus} = +_{S}$