prdsval

Description: Value of the structure product. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Mario Carneiro, 7-Jan-2017) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)

	Ref	Expression
Hypotheses	prdsval.p	$⊢ P = S ⨉_{𝑠} R$
	prdsval.k	$⊢ K = {Base}_{S}$
	prdsval.i	$⊢ φ \to dom R = I$
	prdsval.b	$⊢ φ \to B = \underset{x \in I}{⨉} {Base}_{R (x)}$
	prdsval.a	$⊢ φ \to \underset{˙}{+} = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))$
	prdsval.t	$⊢ φ \to \underset{˙}{\times} = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))$
	prdsval.m	$⊢ φ \to \underset{˙}{\cdot} = (f \in K, g \in B ⟼ (x \in I ⟼ f \cdot_{R (x)} g (x)))$
	prdsval.j	$⊢ φ \to \underset{˙}{,} = (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))$
	prdsval.o	$⊢ φ \to O = \prod_{𝑡} (TopOpen \circ R)$
	prdsval.l	$⊢ φ \to \underset{˙}{\leq} = \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\}$
	prdsval.d	$⊢ φ \to D = (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <))$
	prdsval.h	$⊢ φ \to H = (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))$
	prdsval.x	$⊢ φ \to \underset{˙}{∙} = (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))$
	prdsval.s	$⊢ φ \to S \in W$
	prdsval.r	$⊢ φ \to R \in Z$
Assertion	prdsval	$⊢ φ \to P = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}) \cup (\{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\})$

Proof

Step	Hyp	Ref	Expression
1		prdsval.p	$⊢ P = S ⨉_{𝑠} R$
2		prdsval.k	$⊢ K = {Base}_{S}$
3		prdsval.i	$⊢ φ \to dom R = I$
4		prdsval.b	$⊢ φ \to B = \underset{x \in I}{⨉} {Base}_{R (x)}$
5		prdsval.a	$⊢ φ \to \underset{˙}{+} = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))$
6		prdsval.t	$⊢ φ \to \underset{˙}{\times} = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))$
7		prdsval.m	$⊢ φ \to \underset{˙}{\cdot} = (f \in K, g \in B ⟼ (x \in I ⟼ f \cdot_{R (x)} g (x)))$
8		prdsval.j	$⊢ φ \to \underset{˙}{,} = (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))$
9		prdsval.o	$⊢ φ \to O = \prod_{𝑡} (TopOpen \circ R)$
10		prdsval.l	$⊢ φ \to \underset{˙}{\leq} = \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\}$
11		prdsval.d	$⊢ φ \to D = (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <))$
12		prdsval.h	$⊢ φ \to H = (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))$
13		prdsval.x	$⊢ φ \to \underset{˙}{∙} = (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))$
14		prdsval.s	$⊢ φ \to S \in W$
15		prdsval.r	$⊢ φ \to R \in Z$
16		df-prds	$⊢ ⨉_{𝑠} = (s \in V, r \in V ⟼ ⦋ \underset{x \in dom r}{⨉} {Base}_{r (x)} / v ⦌ ⦋ (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) / h ⦌ ((\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) +_{r (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) \cdot_{r (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), s⟩, ⟨\cdot_{ndx}, (f \in {Base}_{s}, g \in v ⟼ (x \in dom r ⟼ f \cdot_{r (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in v, g \in v ⟼ \underset{x \in dom r}{\sum_{s}} (f (x) \cdot_{𝑖} (r (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ r)⟩, ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in dom r f (x) \leq_{r (x)} g (x))\}⟩, ⟨dist (ndx), (f \in v, g \in v ⟼ sup (ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} \cup \{⟨Hom (ndx), h⟩, ⟨comp (ndx), (a \in (v \times v), c \in v ⟼ (d \in (2^{nd} (a) h c), e \in h (a) ⟼ (x \in dom r ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x))))⟩\})))$
17	16	a1i	$⊢ φ \to ⨉_{𝑠} = (s \in V, r \in V ⟼ ⦋ \underset{x \in dom r}{⨉} {Base}_{r (x)} / v ⦌ ⦋ (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) / h ⦌ ((\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) +_{r (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) \cdot_{r (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), s⟩, ⟨\cdot_{ndx}, (f \in {Base}_{s}, g \in v ⟼ (x \in dom r ⟼ f \cdot_{r (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in v, g \in v ⟼ \underset{x \in dom r}{\sum_{s}} (f (x) \cdot_{𝑖} (r (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ r)⟩, ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in dom r f (x) \leq_{r (x)} g (x))\}⟩, ⟨dist (ndx), (f \in v, g \in v ⟼ sup (ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} \cup \{⟨Hom (ndx), h⟩, ⟨comp (ndx), (a \in (v \times v), c \in v ⟼ (d \in (2^{nd} (a) h c), e \in h (a) ⟼ (x \in dom r ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x))))⟩\})))$
18		vex	$⊢ r \in V$
19	18	rnex	$⊢ ran r \in V$
20	19	uniex	$⊢ ⋃ ran r \in V$
21	20	rnex	$⊢ ran ⋃ ran r \in V$
22	21	uniex	$⊢ ⋃ ran ⋃ ran r \in V$
23		baseid	$⊢ Base = Slot {Base}_{ndx}$
24	23	strfvss	$⊢ {Base}_{r (x)} \subseteq ⋃ ran r (x)$
25		fvssunirn	$⊢ r (x) \subseteq ⋃ ran r$
26		rnss	$⊢ r (x) \subseteq ⋃ ran r \to ran r (x) \subseteq ran ⋃ ran r$
27		uniss	$⊢ ran r (x) \subseteq ran ⋃ ran r \to ⋃ ran r (x) \subseteq ⋃ ran ⋃ ran r$
28	25 26 27	mp2b	$⊢ ⋃ ran r (x) \subseteq ⋃ ran ⋃ ran r$
29	24 28	sstri	$⊢ {Base}_{r (x)} \subseteq ⋃ ran ⋃ ran r$
30	29	rgenw	$⊢ \forall x \in dom r {Base}_{r (x)} \subseteq ⋃ ran ⋃ ran r$
31		iunss	$⊢ ⋃_{x \in dom r} {Base}_{r (x)} \subseteq ⋃ ran ⋃ ran r \leftrightarrow \forall x \in dom r {Base}_{r (x)} \subseteq ⋃ ran ⋃ ran r$
32	30 31	mpbir	$⊢ ⋃_{x \in dom r} {Base}_{r (x)} \subseteq ⋃ ran ⋃ ran r$
33	22 32	ssexi	$⊢ ⋃_{x \in dom r} {Base}_{r (x)} \in V$
34		ixpssmap2g	$⊢ ⋃_{x \in dom r} {Base}_{r (x)} \in V \to \underset{x \in dom r}{⨉} {Base}_{r (x)} \subseteq {⋃_{x \in dom r} {Base}_{r (x)}}^{dom r}$
35	33 34	ax-mp	$⊢ \underset{x \in dom r}{⨉} {Base}_{r (x)} \subseteq {⋃_{x \in dom r} {Base}_{r (x)}}^{dom r}$
36		ovex	$⊢ {⋃_{x \in dom r} {Base}_{r (x)}}^{dom r} \in V$
37	36	ssex	$⊢ \underset{x \in dom r}{⨉} {Base}_{r (x)} \subseteq {⋃_{x \in dom r} {Base}_{r (x)}}^{dom r} \to \underset{x \in dom r}{⨉} {Base}_{r (x)} \in V$
38	35 37	mp1i	$⊢ ((φ \land s = S) \land r = R) \to \underset{x \in dom r}{⨉} {Base}_{r (x)} \in V$
39		simpr	$⊢ ((φ \land s = S) \land r = R) \to r = R$
40	39	fveq1d	$⊢ ((φ \land s = S) \land r = R) \to r (x) = R (x)$
41	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to {Base}_{r (x)} = {Base}_{R (x)}$
42	41	ixpeq2dv	$⊢ ((φ \land s = S) \land r = R) \to \underset{x \in I}{⨉} {Base}_{r (x)} = \underset{x \in I}{⨉} {Base}_{R (x)}$
43	39	dmeqd	$⊢ ((φ \land s = S) \land r = R) \to dom r = dom R$
44	3	ad2antrr	$⊢ ((φ \land s = S) \land r = R) \to dom R = I$
45	43 44	eqtrd	$⊢ ((φ \land s = S) \land r = R) \to dom r = I$
46	45	ixpeq1d	$⊢ ((φ \land s = S) \land r = R) \to \underset{x \in dom r}{⨉} {Base}_{r (x)} = \underset{x \in I}{⨉} {Base}_{r (x)}$
47	4	ad2antrr	$⊢ ((φ \land s = S) \land r = R) \to B = \underset{x \in I}{⨉} {Base}_{R (x)}$
48	42 46 47	3eqtr4d	$⊢ ((φ \land s = S) \land r = R) \to \underset{x \in dom r}{⨉} {Base}_{r (x)} = B$
49		prdsvallem	$⊢ (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) \in V$
50	49	a1i	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) \in V$
51		simpr	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to v = B$
52	45	adantr	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to dom r = I$
53	52	ixpeq1d	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x)) = \underset{x \in I}{⨉} (f (x) Hom (r (x)) g (x))$
54	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to Hom (r (x)) = Hom (R (x))$
55	54	oveqd	$⊢ ((φ \land s = S) \land r = R) \to f (x) Hom (r (x)) g (x) = f (x) Hom (R (x)) g (x)$
56	55	ixpeq2dv	$⊢ ((φ \land s = S) \land r = R) \to \underset{x \in I}{⨉} (f (x) Hom (r (x)) g (x)) = \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))$
57	56	adantr	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to \underset{x \in I}{⨉} (f (x) Hom (r (x)) g (x)) = \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))$
58	53 57	eqtrd	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x)) = \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))$
59	51 51 58	mpoeq123dv	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) = (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))$
60	12	ad3antrrr	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to H = (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))$
61	59 60	eqtr4d	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) = H$
62		simplr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to v = B$
63	62	opeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to ⟨{Base}_{ndx}, v⟩ = ⟨{Base}_{ndx}, B⟩$
64	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to +_{r (x)} = +_{R (x)}$
65	64	oveqd	$⊢ ((φ \land s = S) \land r = R) \to f (x) +_{r (x)} g (x) = f (x) +_{R (x)} g (x)$
66	45 65	mpteq12dv	$⊢ ((φ \land s = S) \land r = R) \to (x \in dom r ⟼ f (x) +_{r (x)} g (x)) = (x \in I ⟼ f (x) +_{R (x)} g (x))$
67	66	adantr	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to (x \in dom r ⟼ f (x) +_{r (x)} g (x)) = (x \in I ⟼ f (x) +_{R (x)} g (x))$
68	51 51 67	mpoeq123dv	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) +_{r (x)} g (x))) = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))$
69	68	adantr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) +_{r (x)} g (x))) = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))$
70	5	ad4antr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \underset{˙}{+} = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))$
71	69 70	eqtr4d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) +_{r (x)} g (x))) = \underset{˙}{+}$
72	71	opeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to ⟨+_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) +_{r (x)} g (x)))⟩ = ⟨+_{ndx}, \underset{˙}{+}⟩$
73	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to \cdot_{r (x)} = \cdot_{R (x)}$
74	73	oveqd	$⊢ ((φ \land s = S) \land r = R) \to f (x) \cdot_{r (x)} g (x) = f (x) \cdot_{R (x)} g (x)$
75	45 74	mpteq12dv	$⊢ ((φ \land s = S) \land r = R) \to (x \in dom r ⟼ f (x) \cdot_{r (x)} g (x)) = (x \in I ⟼ f (x) \cdot_{R (x)} g (x))$
76	75	adantr	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to (x \in dom r ⟼ f (x) \cdot_{r (x)} g (x)) = (x \in I ⟼ f (x) \cdot_{R (x)} g (x))$
77	51 51 76	mpoeq123dv	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) \cdot_{r (x)} g (x))) = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))$
78	77	adantr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) \cdot_{r (x)} g (x))) = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))$
79	6	ad4antr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \underset{˙}{\times} = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))$
80	78 79	eqtr4d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) \cdot_{r (x)} g (x))) = \underset{˙}{\times}$
81	80	opeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to ⟨\cdot_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) \cdot_{r (x)} g (x)))⟩ = ⟨\cdot_{ndx}, \underset{˙}{\times}⟩$
82	63 72 81	tpeq123d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) +_{r (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) \cdot_{r (x)} g (x)))⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\}$
83		simp-4r	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to s = S$
84	83	opeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to ⟨Scalar (ndx), s⟩ = ⟨Scalar (ndx), S⟩$
85		simpllr	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to s = S$
86	85	fveq2d	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to {Base}_{s} = {Base}_{S}$
87	86 2	eqtr4di	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to {Base}_{s} = K$
88	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to \cdot_{r (x)} = \cdot_{R (x)}$
89	88	oveqd	$⊢ ((φ \land s = S) \land r = R) \to f \cdot_{r (x)} g (x) = f \cdot_{R (x)} g (x)$
90	45 89	mpteq12dv	$⊢ ((φ \land s = S) \land r = R) \to (x \in dom r ⟼ f \cdot_{r (x)} g (x)) = (x \in I ⟼ f \cdot_{R (x)} g (x))$
91	90	adantr	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to (x \in dom r ⟼ f \cdot_{r (x)} g (x)) = (x \in I ⟼ f \cdot_{R (x)} g (x))$
92	87 51 91	mpoeq123dv	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to (f \in {Base}_{s}, g \in v ⟼ (x \in dom r ⟼ f \cdot_{r (x)} g (x))) = (f \in K, g \in B ⟼ (x \in I ⟼ f \cdot_{R (x)} g (x)))$
93	92	adantr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (f \in {Base}_{s}, g \in v ⟼ (x \in dom r ⟼ f \cdot_{r (x)} g (x))) = (f \in K, g \in B ⟼ (x \in I ⟼ f \cdot_{R (x)} g (x)))$
94	7	ad4antr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \underset{˙}{\cdot} = (f \in K, g \in B ⟼ (x \in I ⟼ f \cdot_{R (x)} g (x)))$
95	93 94	eqtr4d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (f \in {Base}_{s}, g \in v ⟼ (x \in dom r ⟼ f \cdot_{r (x)} g (x))) = \underset{˙}{\cdot}$
96	95	opeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to ⟨\cdot_{ndx}, (f \in {Base}_{s}, g \in v ⟼ (x \in dom r ⟼ f \cdot_{r (x)} g (x)))⟩ = ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩$
97	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to \cdot_{𝑖} (r (x)) = \cdot_{𝑖} (R (x))$
98	97	oveqd	$⊢ ((φ \land s = S) \land r = R) \to f (x) \cdot_{𝑖} (r (x)) g (x) = f (x) \cdot_{𝑖} (R (x)) g (x)$
99	45 98	mpteq12dv	$⊢ ((φ \land s = S) \land r = R) \to (x \in dom r ⟼ f (x) \cdot_{𝑖} (r (x)) g (x)) = (x \in I ⟼ f (x) \cdot_{𝑖} (R (x)) g (x))$
100	99	adantr	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to (x \in dom r ⟼ f (x) \cdot_{𝑖} (r (x)) g (x)) = (x \in I ⟼ f (x) \cdot_{𝑖} (R (x)) g (x))$
101	85 100	oveq12d	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to \underset{x \in dom r}{\sum_{s}} (f (x) \cdot_{𝑖} (r (x)) g (x)) = \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x))$
102	51 51 101	mpoeq123dv	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to (f \in v, g \in v ⟼ \underset{x \in dom r}{\sum_{s}} (f (x) \cdot_{𝑖} (r (x)) g (x))) = (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))$
103	102	adantr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (f \in v, g \in v ⟼ \underset{x \in dom r}{\sum_{s}} (f (x) \cdot_{𝑖} (r (x)) g (x))) = (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))$
104	8	ad4antr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \underset{˙}{,} = (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))$
105	103 104	eqtr4d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (f \in v, g \in v ⟼ \underset{x \in dom r}{\sum_{s}} (f (x) \cdot_{𝑖} (r (x)) g (x))) = \underset{˙}{,}$
106	105	opeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to ⟨\cdot_{𝑖} (ndx), (f \in v, g \in v ⟼ \underset{x \in dom r}{\sum_{s}} (f (x) \cdot_{𝑖} (r (x)) g (x)))⟩ = ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩$
107	84 96 106	tpeq123d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \{⟨Scalar (ndx), s⟩, ⟨\cdot_{ndx}, (f \in {Base}_{s}, g \in v ⟼ (x \in dom r ⟼ f \cdot_{r (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in v, g \in v ⟼ \underset{x \in dom r}{\sum_{s}} (f (x) \cdot_{𝑖} (r (x)) g (x)))⟩\} = \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}$
108	82 107	uneq12d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) +_{r (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) \cdot_{r (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), s⟩, ⟨\cdot_{ndx}, (f \in {Base}_{s}, g \in v ⟼ (x \in dom r ⟼ f \cdot_{r (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in v, g \in v ⟼ \underset{x \in dom r}{\sum_{s}} (f (x) \cdot_{𝑖} (r (x)) g (x)))⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}$
109		simpllr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to r = R$
110	109	coeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to TopOpen \circ r = TopOpen \circ R$
111	110	fveq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \prod_{𝑡} (TopOpen \circ r) = \prod_{𝑡} (TopOpen \circ R)$
112	9	ad4antr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to O = \prod_{𝑡} (TopOpen \circ R)$
113	111 112	eqtr4d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \prod_{𝑡} (TopOpen \circ r) = O$
114	113	opeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to ⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ r)⟩ = ⟨TopSet (ndx), O⟩$
115	51	sseq2d	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to (\{f, g\} \subseteq v \leftrightarrow \{f, g\} \subseteq B)$
116	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to \leq_{r (x)} = \leq_{R (x)}$
117	116	breqd	$⊢ ((φ \land s = S) \land r = R) \to (f (x) \leq_{r (x)} g (x) \leftrightarrow f (x) \leq_{R (x)} g (x))$
118	45 117	raleqbidv	$⊢ ((φ \land s = S) \land r = R) \to (\forall x \in dom r f (x) \leq_{r (x)} g (x) \leftrightarrow \forall x \in I f (x) \leq_{R (x)} g (x))$
119	118	adantr	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to (\forall x \in dom r f (x) \leq_{r (x)} g (x) \leftrightarrow \forall x \in I f (x) \leq_{R (x)} g (x))$
120	115 119	anbi12d	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to ((\{f, g\} \subseteq v \land \forall x \in dom r f (x) \leq_{r (x)} g (x)) \leftrightarrow (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x)))$
121	120	opabbidv	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in dom r f (x) \leq_{r (x)} g (x))\} = \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\}$
122	121	adantr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in dom r f (x) \leq_{r (x)} g (x))\} = \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\}$
123	10	ad4antr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \underset{˙}{\leq} = \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\}$
124	122 123	eqtr4d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in dom r f (x) \leq_{r (x)} g (x))\} = \underset{˙}{\leq}$
125	124	opeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in dom r f (x) \leq_{r (x)} g (x))\}⟩ = ⟨\leq_{ndx}, \underset{˙}{\leq}⟩$
126	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to dist (r (x)) = dist (R (x))$
127	126	oveqd	$⊢ ((φ \land s = S) \land r = R) \to f (x) dist (r (x)) g (x) = f (x) dist (R (x)) g (x)$
128	45 127	mpteq12dv	$⊢ ((φ \land s = S) \land r = R) \to (x \in dom r ⟼ f (x) dist (r (x)) g (x)) = (x \in I ⟼ f (x) dist (R (x)) g (x))$
129	128	adantr	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to (x \in dom r ⟼ f (x) dist (r (x)) g (x)) = (x \in I ⟼ f (x) dist (R (x)) g (x))$
130	129	rneqd	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) = ran (x \in I ⟼ f (x) dist (R (x)) g (x))$
131	130	uneq1d	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) \cup \{0\} = ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\}$
132	131	supeq1d	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to sup (ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) \cup \{0\} ℝ^{} <) = sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <)$
133	51 51 132	mpoeq123dv	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to (f \in v, g \in v ⟼ sup (ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) \cup \{0\} ℝ^{} <)) = (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <))$
134	133	adantr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (f \in v, g \in v ⟼ sup (ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) \cup \{0\} ℝ^{} <)) = (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <))$
135	11	ad4antr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to D = (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <))$
136	134 135	eqtr4d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (f \in v, g \in v ⟼ sup (ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) \cup \{0\} ℝ^{*} <)) = D$
137	136	opeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to ⟨dist (ndx), (f \in v, g \in v ⟼ sup (ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩ = ⟨dist (ndx), D⟩$
138	114 125 137	tpeq123d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ r)⟩, ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in dom r f (x) \leq_{r (x)} g (x))\}⟩, ⟨dist (ndx), (f \in v, g \in v ⟼ sup (ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} = \{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\}$
139		simpr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to h = H$
140	139	opeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to ⟨Hom (ndx), h⟩ = ⟨Hom (ndx), H⟩$
141	62	sqxpeqd	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to v \times v = B \times B$
142	139	oveqd	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to 2^{nd} (a) h c = 2^{nd} (a) H c$
143	139	fveq1d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to h (a) = H (a)$
144	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to comp (r (x)) = comp (R (x))$
145	144	oveqd	$⊢ ((φ \land s = S) \land r = R) \to ⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x) = ⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)$
146	145	oveqd	$⊢ ((φ \land s = S) \land r = R) \to d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x) = d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x)$
147	45 146	mpteq12dv	$⊢ ((φ \land s = S) \land r = R) \to (x \in dom r ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x)) = (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))$
148	147	ad2antrr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (x \in dom r ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x)) = (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))$
149	142 143 148	mpoeq123dv	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (d \in (2^{nd} (a) h c), e \in h (a) ⟼ (x \in dom r ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x))) = (d \in (2^{nd} (a) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x)))$
150	141 62 149	mpoeq123dv	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (a \in (v \times v), c \in v ⟼ (d \in (2^{nd} (a) h c), e \in h (a) ⟼ (x \in dom r ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x)))) = (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))$
151	13	ad4antr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \underset{˙}{∙} = (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))$
152	150 151	eqtr4d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (a \in (v \times v), c \in v ⟼ (d \in (2^{nd} (a) h c), e \in h (a) ⟼ (x \in dom r ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x)))) = \underset{˙}{∙}$
153	152	opeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to ⟨comp (ndx), (a \in (v \times v), c \in v ⟼ (d \in (2^{nd} (a) h c), e \in h (a) ⟼ (x \in dom r ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x))))⟩ = ⟨comp (ndx), \underset{˙}{∙}⟩$
154	140 153	preq12d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \{⟨Hom (ndx), h⟩, ⟨comp (ndx), (a \in (v \times v), c \in v ⟼ (d \in (2^{nd} (a) h c), e \in h (a) ⟼ (x \in dom r ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x))))⟩\} = \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\}$
155	138 154	uneq12d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ r)⟩, ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in dom r f (x) \leq_{r (x)} g (x))\}⟩, ⟨dist (ndx), (f \in v, g \in v ⟼ sup (ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} \cup \{⟨Hom (ndx), h⟩, ⟨comp (ndx), (a \in (v \times v), c \in v ⟼ (d \in (2^{nd} (a) h c), e \in h (a) ⟼ (x \in dom r ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x))))⟩\} = \{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\}$
156	108 155	uneq12d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) +_{r (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) \cdot_{r (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), s⟩, ⟨\cdot_{ndx}, (f \in {Base}_{s}, g \in v ⟼ (x \in dom r ⟼ f \cdot_{r (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in v, g \in v ⟼ \underset{x \in dom r}{\sum_{s}} (f (x) \cdot_{𝑖} (r (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ r)⟩, ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in dom r f (x) \leq_{r (x)} g (x))\}⟩, ⟨dist (ndx), (f \in v, g \in v ⟼ sup (ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} \cup \{⟨Hom (ndx), h⟩, ⟨comp (ndx), (a \in (v \times v), c \in v ⟼ (d \in (2^{nd} (a) h c), e \in h (a) ⟼ (x \in dom r ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x))))⟩\}) = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}) \cup (\{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\})$
157	50 61 156	csbied2	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to ⦋ (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) / h ⦌ ((\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) +_{r (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) \cdot_{r (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), s⟩, ⟨\cdot_{ndx}, (f \in {Base}_{s}, g \in v ⟼ (x \in dom r ⟼ f \cdot_{r (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in v, g \in v ⟼ \underset{x \in dom r}{\sum_{s}} (f (x) \cdot_{𝑖} (r (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ r)⟩, ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in dom r f (x) \leq_{r (x)} g (x))\}⟩, ⟨dist (ndx), (f \in v, g \in v ⟼ sup (ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} \cup \{⟨Hom (ndx), h⟩, ⟨comp (ndx), (a \in (v \times v), c \in v ⟼ (d \in (2^{nd} (a) h c), e \in h (a) ⟼ (x \in dom r ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x))))⟩\})) = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}) \cup (\{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\})$
158	38 48 157	csbied2	$⊢ ((φ \land s = S) \land r = R) \to ⦋ \underset{x \in dom r}{⨉} {Base}_{r (x)} / v ⦌ ⦋ (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) / h ⦌ ((\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) +_{r (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) \cdot_{r (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), s⟩, ⟨\cdot_{ndx}, (f \in {Base}_{s}, g \in v ⟼ (x \in dom r ⟼ f \cdot_{r (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in v, g \in v ⟼ \underset{x \in dom r}{\sum_{s}} (f (x) \cdot_{𝑖} (r (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ r)⟩, ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in dom r f (x) \leq_{r (x)} g (x))\}⟩, ⟨dist (ndx), (f \in v, g \in v ⟼ sup (ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} \cup \{⟨Hom (ndx), h⟩, ⟨comp (ndx), (a \in (v \times v), c \in v ⟼ (d \in (2^{nd} (a) h c), e \in h (a) ⟼ (x \in dom r ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x))))⟩\})) = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}) \cup (\{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\})$
159	158	anasss	$⊢ (φ \land (s = S \land r = R)) \to ⦋ \underset{x \in dom r}{⨉} {Base}_{r (x)} / v ⦌ ⦋ (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) / h ⦌ ((\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) +_{r (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in v, g \in v ⟼ (x \in dom r ⟼ f (x) \cdot_{r (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), s⟩, ⟨\cdot_{ndx}, (f \in {Base}_{s}, g \in v ⟼ (x \in dom r ⟼ f \cdot_{r (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in v, g \in v ⟼ \underset{x \in dom r}{\sum_{s}} (f (x) \cdot_{𝑖} (r (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ r)⟩, ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in dom r f (x) \leq_{r (x)} g (x))\}⟩, ⟨dist (ndx), (f \in v, g \in v ⟼ sup (ran (x \in dom r ⟼ f (x) dist (r (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} \cup \{⟨Hom (ndx), h⟩, ⟨comp (ndx), (a \in (v \times v), c \in v ⟼ (d \in (2^{nd} (a) h c), e \in h (a) ⟼ (x \in dom r ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (r (x)) c (x)) e (x))))⟩\})) = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}) \cup (\{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\})$
160	14	elexd	$⊢ φ \to S \in V$
161	15	elexd	$⊢ φ \to R \in V$
162		tpex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \in V$
163		tpex	$⊢ \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\} \in V$
164	162 163	unex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\} \in V$
165		tpex	$⊢ \{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \in V$
166		prex	$⊢ \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\} \in V$
167	165 166	unex	$⊢ \{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\} \in V$
168	164 167	unex	$⊢ (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}) \cup (\{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\}) \in V$
169	168	a1i	$⊢ φ \to (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}) \cup (\{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\}) \in V$
170	17 159 160 161 169	ovmpod	$⊢ φ \to S ⨉_{𝑠} R = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}) \cup (\{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\})$
171	1 170	eqtrid	$⊢ φ \to P = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}) \cup (\{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\})$

Metamath Proof Explorer

Theorem prdsval

Proof