idlsrgval

	Ref	Expression
Hypotheses	idlsrgval.1	$⊢ I = LIdeal (R)$
	idlsrgval.2	$⊢ \underset{˙}{\oplus} = LSSum (R)$
	idlsrgval.3	$⊢ G = {mulGrp}_{R}$
	idlsrgval.4	$⊢ \underset{˙}{\otimes} = LSSum (G)$
Assertion	idlsrgval	$⊢ R \in V \to IDLsrg (R) = \{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i \underset{˙}{\otimes} 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)\}⟩\}$

Proof

Step	Hyp	Ref	Expression
1		idlsrgval.1	$⊢ I = LIdeal (R)$
2		idlsrgval.2	$⊢ \underset{˙}{\oplus} = LSSum (R)$
3		idlsrgval.3	$⊢ G = {mulGrp}_{R}$
4		idlsrgval.4	$⊢ \underset{˙}{\otimes} = LSSum (G)$
5		elex	$⊢ R \in V \to R \in V$
6		fvexd	$⊢ r = R \to LIdeal (r) \in V$
7		simpr	$⊢ (r = R \land b = LIdeal (r)) \to b = LIdeal (r)$
8		simpl	$⊢ (r = R \land b = LIdeal (r)) \to r = R$
9	8	fveq2d	$⊢ (r = R \land b = LIdeal (r)) \to LIdeal (r) = LIdeal (R)$
10	7 9	eqtrd	$⊢ (r = R \land b = LIdeal (r)) \to b = LIdeal (R)$
11	10 1	eqtr4di	$⊢ (r = R \land b = LIdeal (r)) \to b = I$
12	11	opeq2d	$⊢ (r = R \land b = LIdeal (r)) \to ⟨{Base}_{ndx}, b⟩ = ⟨{Base}_{ndx}, I⟩$
13	8	fveq2d	$⊢ (r = R \land b = LIdeal (r)) \to LSSum (r) = LSSum (R)$
14	13 2	eqtr4di	$⊢ (r = R \land b = LIdeal (r)) \to LSSum (r) = \underset{˙}{\oplus}$
15	14	opeq2d	$⊢ (r = R \land b = LIdeal (r)) \to ⟨+_{ndx}, LSSum (r)⟩ = ⟨+_{ndx}, \underset{˙}{\oplus}⟩$
16	8	fveq2d	$⊢ (r = R \land b = LIdeal (r)) \to RSpan (r) = RSpan (R)$
17	8	fveq2d	$⊢ (r = R \land b = LIdeal (r)) \to {mulGrp}_{r} = {mulGrp}_{R}$
18	17 3	eqtr4di	$⊢ (r = R \land b = LIdeal (r)) \to {mulGrp}_{r} = G$
19	18	fveq2d	$⊢ (r = R \land b = LIdeal (r)) \to LSSum ({mulGrp}_{r}) = LSSum (G)$
20	19 4	eqtr4di	$⊢ (r = R \land b = LIdeal (r)) \to LSSum ({mulGrp}_{r}) = \underset{˙}{\otimes}$
21	20	oveqd	$⊢ (r = R \land b = LIdeal (r)) \to i LSSum ({mulGrp}_{r}) j = i \underset{˙}{\otimes} j$
22	16 21	fveq12d	$⊢ (r = R \land b = LIdeal (r)) \to RSpan (r) (i LSSum ({mulGrp}_{r}) j) = RSpan (R) (i \underset{˙}{\otimes} j)$
23	11 11 22	mpoeq123dv	$⊢ (r = R \land b = LIdeal (r)) \to (i \in b, j \in b ⟼ RSpan (r) (i LSSum ({mulGrp}_{r}) j)) = (i \in I, j \in I ⟼ RSpan (R) (i \underset{˙}{\otimes} j))$
24	23	opeq2d	$⊢ (r = R \land b = LIdeal (r)) \to ⟨\cdot_{ndx}, (i \in b, j \in b ⟼ RSpan (r) (i LSSum ({mulGrp}_{r}) j))⟩ = ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i \underset{˙}{\otimes} j))⟩$
25	12 15 24	tpeq123d	$⊢ (r = R \land b = LIdeal (r)) \to \{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, LSSum (r)⟩, ⟨\cdot_{ndx}, (i \in b, j \in b ⟼ RSpan (r) (i LSSum ({mulGrp}_{r}) j))⟩\} = \{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i \underset{˙}{\otimes} j))⟩\}$
26	11	rabeqdv	$⊢ (r = R \land b = LIdeal (r)) \to \{j \in b \| \neg i \subseteq j\} = \{j \in I \| \neg i \subseteq j\}$
27	11 26	mpteq12dv	$⊢ (r = R \land b = LIdeal (r)) \to (i \in b ⟼ \{j \in b \| \neg i \subseteq j\}) = (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})$
28	27	rneqd	$⊢ (r = R \land b = LIdeal (r)) \to ran (i \in b ⟼ \{j \in b \| \neg i \subseteq j\}) = ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})$
29	28	opeq2d	$⊢ (r = R \land b = LIdeal (r)) \to ⟨TopSet (ndx), ran (i \in b ⟼ \{j \in b \| \neg i \subseteq j\})⟩ = ⟨TopSet (ndx), ran (i \in I ⟼ \{j \in I \| \neg i \subseteq j\})⟩$
30	11	sseq2d	$⊢ (r = R \land b = LIdeal (r)) \to (\{i, j\} \subseteq b \leftrightarrow \{i, j\} \subseteq I)$
31	30	anbi1d	$⊢ (r = R \land b = LIdeal (r)) \to ((\{i, j\} \subseteq b \land i \subseteq j) \leftrightarrow (\{i, j\} \subseteq I \land i \subseteq j))$
32	31	opabbidv	$⊢ (r = R \land b = LIdeal (r)) \to \{⟨i, j⟩ \| (\{i, j\} \subseteq b \land i \subseteq j)\} = \{⟨i, j⟩ \| (\{i, j\} \subseteq I \land i \subseteq j)\}$
33	32	opeq2d	$⊢ (r = R \land b = LIdeal (r)) \to ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq b \land i \subseteq j)\}⟩ = ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq I \land i \subseteq j)\}⟩$
34	29 33	preq12d	$⊢ (r = R \land b = LIdeal (r)) \to \{⟨TopSet (ndx), ran (i \in b ⟼ \{j \in b \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq b \land i \subseteq j)\}⟩\} = \{⟨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)\}⟩\}$
35	25 34	uneq12d	$⊢ (r = R \land b = LIdeal (r)) \to \{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, LSSum (r)⟩, ⟨\cdot_{ndx}, (i \in b, j \in b ⟼ RSpan (r) (i LSSum ({mulGrp}_{r}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in b ⟼ \{j \in b \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq b \land i \subseteq j)\}⟩\} = \{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i \underset{˙}{\otimes} 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)\}⟩\}$
36	6 35	csbied	$⊢ r = R \to ⦋ LIdeal (r) / b ⦌ (\{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, LSSum (r)⟩, ⟨\cdot_{ndx}, (i \in b, j \in b ⟼ RSpan (r) (i LSSum ({mulGrp}_{r}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in b ⟼ \{j \in b \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq b \land i \subseteq j)\}⟩\}) = \{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i \underset{˙}{\otimes} 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)\}⟩\}$
37		df-idlsrg	$⊢ IDLsrg = (r \in V ⟼ ⦋ LIdeal (r) / b ⦌ (\{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, LSSum (r)⟩, ⟨\cdot_{ndx}, (i \in b, j \in b ⟼ RSpan (r) (i LSSum ({mulGrp}_{r}) j))⟩\} \cup \{⟨TopSet (ndx), ran (i \in b ⟼ \{j \in b \| \neg i \subseteq j\})⟩, ⟨\leq_{ndx}, \{⟨i, j⟩ \| (\{i, j\} \subseteq b \land i \subseteq j)\}⟩\}))$
38		tpex	$⊢ \{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i \underset{˙}{\otimes} j))⟩\} \in V$
39		prex	$⊢ \{⟨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)\}⟩\} \in V$
40	38 39	unex	$⊢ \{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i \underset{˙}{\otimes} 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)\}⟩\} \in V$
41	36 37 40	fvmpt	$⊢ R \in V \to IDLsrg (R) = \{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i \underset{˙}{\otimes} 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)\}⟩\}$
42	5 41	syl	$⊢ R \in V \to IDLsrg (R) = \{⟨{Base}_{ndx}, I⟩, ⟨+_{ndx}, \underset{˙}{\oplus}⟩, ⟨\cdot_{ndx}, (i \in I, j \in I ⟼ RSpan (R) (i \underset{˙}{\otimes} 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)\}⟩\}$

Metamath Proof Explorer

Theorem idlsrgval

Proof