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)

	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 (c H 2^{nd} (a)), 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 (c H 2^{nd} (a)), 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 (c h 2^{nd} (a)), 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 (c h 2^{nd} (a)), 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		ovex	$⊢ {⋃ ran ⋃ ran ⋃ ran r}^{dom r} \in V$
50		ovssunirn	$⊢ f (x) Hom (r (x)) g (x) \subseteq ⋃ ran Hom (r (x))$
51		df-hom	$⊢ Hom = Slot 14$
52	51	strfvss	$⊢ Hom (r (x)) \subseteq ⋃ ran r (x)$
53	52 28	sstri	$⊢ Hom (r (x)) \subseteq ⋃ ran ⋃ ran r$
54		rnss	$⊢ Hom (r (x)) \subseteq ⋃ ran ⋃ ran r \to ran Hom (r (x)) \subseteq ran ⋃ ran ⋃ ran r$
55		uniss	$⊢ ran Hom (r (x)) \subseteq ran ⋃ ran ⋃ ran r \to ⋃ ran Hom (r (x)) \subseteq ⋃ ran ⋃ ran ⋃ ran r$
56	53 54 55	mp2b	$⊢ ⋃ ran Hom (r (x)) \subseteq ⋃ ran ⋃ ran ⋃ ran r$
57	50 56	sstri	$⊢ f (x) Hom (r (x)) g (x) \subseteq ⋃ ran ⋃ ran ⋃ ran r$
58	57	rgenw	$⊢ \forall x \in dom r f (x) Hom (r (x)) g (x) \subseteq ⋃ ran ⋃ ran ⋃ ran r$
59		ss2ixp	$⊢ \forall x \in dom r f (x) Hom (r (x)) g (x) \subseteq ⋃ ran ⋃ ran ⋃ ran r \to \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x)) \subseteq \underset{x \in dom r}{⨉} ⋃ ran ⋃ ran ⋃ ran r$
60	58 59	ax-mp	$⊢ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x)) \subseteq \underset{x \in dom r}{⨉} ⋃ ran ⋃ ran ⋃ ran r$
61	18	dmex	$⊢ dom r \in V$
62	22	rnex	$⊢ ran ⋃ ran ⋃ ran r \in V$
63	62	uniex	$⊢ ⋃ ran ⋃ ran ⋃ ran r \in V$
64	61 63	ixpconst	$⊢ \underset{x \in dom r}{⨉} ⋃ ran ⋃ ran ⋃ ran r = {⋃ ran ⋃ ran ⋃ ran r}^{dom r}$
65	60 64	sseqtri	$⊢ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x)) \subseteq {⋃ ran ⋃ ran ⋃ ran r}^{dom r}$
66	49 65	elpwi2	$⊢ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x)) \in 𝒫 ({⋃ ran ⋃ ran ⋃ ran r}^{dom r})$
67	66	rgen2w	$⊢ \forall f \in v \forall g \in v \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x)) \in 𝒫 ({⋃ ran ⋃ ran ⋃ ran r}^{dom r})$
68		eqid	$⊢ (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) = (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x)))$
69	68	fmpo	$⊢ \forall f \in v \forall g \in v \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x)) \in 𝒫 ({⋃ ran ⋃ ran ⋃ ran r}^{dom r}) \leftrightarrow (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) : v \times v ⟶ 𝒫 ({⋃ ran ⋃ ran ⋃ ran r}^{dom r})$
70	67 69	mpbi	$⊢ (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) : v \times v ⟶ 𝒫 ({⋃ ran ⋃ ran ⋃ ran r}^{dom r})$
71		vex	$⊢ v \in V$
72	71 71	xpex	$⊢ v \times v \in V$
73	49	pwex	$⊢ 𝒫 ({⋃ ran ⋃ ran ⋃ ran r}^{dom r}) \in V$
74		fex2	$⊢ ((f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) : v \times v ⟶ 𝒫 ({⋃ ran ⋃ ran ⋃ ran r}^{dom r}) \land v \times v \in V \land 𝒫 ({⋃ ran ⋃ ran ⋃ ran r}^{dom r}) \in V) \to (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) \in V$
75	70 72 73 74	mp3an	$⊢ (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) \in V$
76	75	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$
77		simpr	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to v = B$
78	45	adantr	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to dom r = I$
79	78	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))$
80	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to Hom (r (x)) = Hom (R (x))$
81	80	oveqd	$⊢ ((φ \land s = S) \land r = R) \to f (x) Hom (r (x)) g (x) = f (x) Hom (R (x)) g (x)$
82	81	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))$
83	82	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))$
84	79 83	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))$
85	77 77 84	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)))$
86	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)))$
87	85 86	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$
88		simplr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to v = B$
89	88	opeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to ⟨{Base}_{ndx}, v⟩ = ⟨{Base}_{ndx}, B⟩$
90	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to +_{r (x)} = +_{R (x)}$
91	90	oveqd	$⊢ ((φ \land s = S) \land r = R) \to f (x) +_{r (x)} g (x) = f (x) +_{R (x)} g (x)$
92	45 91	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))$
93	92	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))$
94	77 77 93	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)))$
95	94	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)))$
96	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)))$
97	95 96	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{˙}{+}$
98	97	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{˙}{+}⟩$
99	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to \cdot_{r (x)} = \cdot_{R (x)}$
100	99	oveqd	$⊢ ((φ \land s = S) \land r = R) \to f (x) \cdot_{r (x)} g (x) = f (x) \cdot_{R (x)} g (x)$
101	45 100	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))$
102	101	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))$
103	77 77 102	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)))$
104	103	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)))$
105	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)))$
106	104 105	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}$
107	106	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}⟩$
108	89 98 107	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}⟩\}$
109		simp-4r	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to s = S$
110	109	opeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to ⟨Scalar (ndx), s⟩ = ⟨Scalar (ndx), S⟩$
111		simpllr	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to s = S$
112	111	fveq2d	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to {Base}_{s} = {Base}_{S}$
113	112 2	eqtr4di	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to {Base}_{s} = K$
114	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to \cdot_{r (x)} = \cdot_{R (x)}$
115	114	oveqd	$⊢ ((φ \land s = S) \land r = R) \to f \cdot_{r (x)} g (x) = f \cdot_{R (x)} g (x)$
116	45 115	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))$
117	116	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))$
118	113 77 117	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)))$
119	118	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)))$
120	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)))$
121	119 120	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}$
122	121	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}⟩$
123	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to \cdot_{𝑖} (r (x)) = \cdot_{𝑖} (R (x))$
124	123	oveqd	$⊢ ((φ \land s = S) \land r = R) \to f (x) \cdot_{𝑖} (r (x)) g (x) = f (x) \cdot_{𝑖} (R (x)) g (x)$
125	45 124	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))$
126	125	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))$
127	111 126	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))$
128	77 77 127	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)))$
129	128	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)))$
130	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)))$
131	129 130	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{˙}{,}$
132	131	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{˙}{,}⟩$
133	110 122 132	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{˙}{,}⟩\}$
134	108 133	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{˙}{,}⟩\}$
135		simpllr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to r = R$
136	135	coeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to TopOpen \circ r = TopOpen \circ R$
137	136	fveq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \prod_{𝑡} (TopOpen \circ r) = \prod_{𝑡} (TopOpen \circ R)$
138	9	ad4antr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to O = \prod_{𝑡} (TopOpen \circ R)$
139	137 138	eqtr4d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to \prod_{𝑡} (TopOpen \circ r) = O$
140	139	opeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to ⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ r)⟩ = ⟨TopSet (ndx), O⟩$
141	77	sseq2d	$⊢ (((φ \land s = S) \land r = R) \land v = B) \to (\{f, g\} \subseteq v \leftrightarrow \{f, g\} \subseteq B)$
142	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to \leq_{r (x)} = \leq_{R (x)}$
143	142	breqd	$⊢ ((φ \land s = S) \land r = R) \to (f (x) \leq_{r (x)} g (x) \leftrightarrow f (x) \leq_{R (x)} g (x))$
144	45 143	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))$
145	144	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))$
146	141 145	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)))$
147	146	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))\}$
148	147	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))\}$
149	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))\}$
150	148 149	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}$
151	150	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}⟩$
152	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to dist (r (x)) = dist (R (x))$
153	152	oveqd	$⊢ ((φ \land s = S) \land r = R) \to f (x) dist (r (x)) g (x) = f (x) dist (R (x)) g (x)$
154	45 153	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))$
155	154	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))$
156	155	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))$
157	156	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\}$
158	157	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\} ℝ^{} <)$
159	77 77 158	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\} ℝ^{} <))$
160	159	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\} ℝ^{} <))$
161	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\} ℝ^{*} <))$
162	160 161	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$
163	162	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⟩$
164	140 151 163	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⟩\}$
165		simpr	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to h = H$
166	165	opeq2d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to ⟨Hom (ndx), h⟩ = ⟨Hom (ndx), H⟩$
167	88	sqxpeqd	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to v \times v = B \times B$
168	165	oveqd	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to c h 2^{nd} (a) = c H 2^{nd} (a)$
169	165	fveq1d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to h (a) = H (a)$
170	40	fveq2d	$⊢ ((φ \land s = S) \land r = R) \to comp (r (x)) = comp (R (x))$
171	170	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)$
172	171	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)$
173	45 172	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))$
174	173	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))$
175	168 169 174	mpoeq123dv	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (d \in (c h 2^{nd} (a)), 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 (c H 2^{nd} (a)), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x)))$
176	167 88 175	mpoeq123dv	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (a \in (v \times v), c \in v ⟼ (d \in (c h 2^{nd} (a)), 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 (c H 2^{nd} (a)), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))$
177	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 (c H 2^{nd} (a)), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))$
178	176 177	eqtr4d	$⊢ ((((φ \land s = S) \land r = R) \land v = B) \land h = H) \to (a \in (v \times v), c \in v ⟼ (d \in (c h 2^{nd} (a)), 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{˙}{∙}$
179	178	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 (c h 2^{nd} (a)), 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{˙}{∙}⟩$
180	166 179	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 (c h 2^{nd} (a)), 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{˙}{∙}⟩\}$
181	164 180	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 (c h 2^{nd} (a)), 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{˙}{∙}⟩\}$
182	134 181	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 (c h 2^{nd} (a)), 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{˙}{∙}⟩\})$
183	76 87 182	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 (c h 2^{nd} (a)), 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{˙}{∙}⟩\})$
184	38 48 183	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 (c h 2^{nd} (a)), 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{˙}{∙}⟩\})$
185	184	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 (c h 2^{nd} (a)), 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{˙}{∙}⟩\})$
186	14	elexd	$⊢ φ \to S \in V$
187	15	elexd	$⊢ φ \to R \in V$
188		tpex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \in V$
189		tpex	$⊢ \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\} \in V$
190	188 189	unex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\} \in V$
191		tpex	$⊢ \{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \in V$
192		prex	$⊢ \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\} \in V$
193	191 192	unex	$⊢ \{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\} \in V$
194	190 193	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$
195	194	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$
196	17 185 186 187 195	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{˙}{∙}⟩\})$
197	1 196	syl5eq	$⊢ φ \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