prdsval - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > prdsval		GIF version

Theorem prdsval 13149

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.)

**Hypotheses**
Ref	Expression
prdsval.p	⊢ 𝑃 = (𝑆X_s𝑅)
prdsval.k	⊢ 𝐾 = (Base‘𝑆)
prdsval.i	⊢ (𝜑 → dom 𝑅 = 𝐼)
prdsval.b	⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
prdsval.a	⊢ (𝜑 → + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+_g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
prdsval.t	⊢ (𝜑 → × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(._r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
prdsval.m	⊢ (𝜑 → · = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·_𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))
prdsval.j	⊢ (𝜑 → , = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σ_g (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))
prdsval.o	⊢ (𝜑 → 𝑂 = (∏_t‘(TopOpen ∘ 𝑅)))
prdsval.l	⊢ (𝜑 → ≤ = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})
prdsval.d	⊢ (𝜑 → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < )))
prdsval.h	⊢ (𝜑 → 𝐻 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))))
prdsval.x	⊢ (𝜑 → ∙ = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2^nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))))
prdsval.s	⊢ (𝜑 → 𝑆 ∈ 𝑊)
prdsval.r	⊢ (𝜑 → 𝑅 ∈ 𝑍)

**Assertion**
Ref	Expression
prdsval	⊢ (𝜑 → 𝑃 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))

Distinct variable groups: 𝑎,𝑐,𝑑,𝑒,𝑓,𝑔,𝐵 𝐻,𝑎,𝑐,𝑑,𝑒 𝑥,𝑎,𝜑,𝑐,𝑑,𝑒,𝑓,𝑔 𝑥,𝐼 𝑅,𝑎,𝑐,𝑑,𝑒,𝑓,𝑔,𝑥 𝑆,𝑎,𝑐,𝑑,𝑒,𝑓,𝑔,𝑥 𝑓,𝐾,𝑔 Allowed substitution hints: 𝐵(𝑥) 𝐷(𝑥,𝑒,𝑓,𝑔,𝑎,𝑐,𝑑) 𝑃(𝑥,𝑒,𝑓,𝑔,𝑎,𝑐,𝑑) + (𝑥,𝑒,𝑓,𝑔,𝑎,𝑐,𝑑) ∙ (𝑥,𝑒,𝑓,𝑔,𝑎,𝑐,𝑑) · (𝑥,𝑒,𝑓,𝑔,𝑎,𝑐,𝑑) × (𝑥,𝑒,𝑓,𝑔,𝑎,𝑐,𝑑) 𝐻(𝑥,𝑓,𝑔) , (𝑥,𝑒,𝑓,𝑔,𝑎,𝑐,𝑑) 𝐼(𝑒,𝑓,𝑔,𝑎,𝑐,𝑑) 𝐾(𝑥,𝑒,𝑎,𝑐,𝑑) ≤ (𝑥,𝑒,𝑓,𝑔,𝑎,𝑐,𝑑) 𝑂(𝑥,𝑒,𝑓,𝑔,𝑎,𝑐,𝑑) 𝑊(𝑥,𝑒,𝑓,𝑔,𝑎,𝑐,𝑑) 𝑍(𝑥,𝑒,𝑓,𝑔,𝑎,𝑐,𝑑)

Proof of Theorem prdsval Dummy variables ℎ 𝑟 𝑠 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prdsval.p	. 2 ⊢ 𝑃 = (𝑆X_s𝑅)
2		df-prds 13143	. . . 4 ⊢ X_s = (𝑠 ∈ V, 𝑟 ∈ V ↦ ⦋X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+_g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+_g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(._r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(._r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·_𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·_𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·_𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σ_g (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2^nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})))
3	2	a1i 9	. . 3 ⊢ (𝜑 → X_s = (𝑠 ∈ V, 𝑟 ∈ V ↦ ⦋X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+_g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+_g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(._r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(._r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·_𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·_𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·_𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σ_g (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2^nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩}))))
4		vex 2776	. . . . . . . . . . . 12 ⊢ 𝑟 ∈ V
5	4	rnex 4951	. . . . . . . . . . 11 ⊢ ran 𝑟 ∈ V
6	5	uniex 4488	. . . . . . . . . 10 ⊢ ∪ ran 𝑟 ∈ V
7	6	rnex 4951	. . . . . . . . 9 ⊢ ran ∪ ran 𝑟 ∈ V
8	7	uniex 4488	. . . . . . . 8 ⊢ ∪ ran ∪ ran 𝑟 ∈ V
9		baseid 12930	. . . . . . . . . . . . 13 ⊢ Base = Slot (Base‘ndx)
10		vex 2776	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
11	4, 10	fvex 5603	. . . . . . . . . . . . . 14 ⊢ (𝑟‘𝑥) ∈ V
12	11	a1i 9	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑟‘𝑥) ∈ V)
13		basendxnn 12932	. . . . . . . . . . . . . 14 ⊢ (Base‘ndx) ∈ ℕ
14	13	a1i 9	. . . . . . . . . . . . 13 ⊢ (⊤ → (Base‘ndx) ∈ ℕ)
15	9, 12, 14	strfvssn 12898	. . . . . . . . . . . 12 ⊢ (⊤ → (Base‘(𝑟‘𝑥)) ⊆ ∪ ran (𝑟‘𝑥))
16	15	mptru 1382	. . . . . . . . . . 11 ⊢ (Base‘(𝑟‘𝑥)) ⊆ ∪ ran (𝑟‘𝑥)
17		fvssunirng 5598	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ V → (𝑟‘𝑥) ⊆ ∪ ran 𝑟)
18	17	elv 2777	. . . . . . . . . . . 12 ⊢ (𝑟‘𝑥) ⊆ ∪ ran 𝑟
19		rnss 4913	. . . . . . . . . . . 12 ⊢ ((𝑟‘𝑥) ⊆ ∪ ran 𝑟 → ran (𝑟‘𝑥) ⊆ ran ∪ ran 𝑟)
20		uniss 3873	. . . . . . . . . . . 12 ⊢ (ran (𝑟‘𝑥) ⊆ ran ∪ ran 𝑟 → ∪ ran (𝑟‘𝑥) ⊆ ∪ ran ∪ ran 𝑟)
21	18, 19, 20	mp2b 8	. . . . . . . . . . 11 ⊢ ∪ ran (𝑟‘𝑥) ⊆ ∪ ran ∪ ran 𝑟
22	16, 21	sstri 3203	. . . . . . . . . 10 ⊢ (Base‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran 𝑟
23	22	rgenw 2562	. . . . . . . . 9 ⊢ ∀𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran 𝑟
24		iunss 3970	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran 𝑟 ↔ ∀𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran 𝑟)
25	23, 24	mpbir 146	. . . . . . . 8 ⊢ ∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran 𝑟
26	8, 25	ssexi 4186	. . . . . . 7 ⊢ ∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ∈ V
27		ixpssmap2g 6821	. . . . . . 7 ⊢ (∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ∈ V → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ (∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ↑_𝑚 dom 𝑟))
28	26, 27	ax-mp 5	. . . . . 6 ⊢ X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ (∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ↑_𝑚 dom 𝑟)
29		fnmap 6749	. . . . . . . 8 ⊢ ↑_𝑚 Fn (V × V)
30	4	dmex 4950	. . . . . . . 8 ⊢ dom 𝑟 ∈ V
31		fnovex 5984	. . . . . . . 8 ⊢ (( ↑_𝑚 Fn (V × V) ∧ ∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ∈ V ∧ dom 𝑟 ∈ V) → (∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ↑_𝑚 dom 𝑟) ∈ V)
32	29, 26, 30, 31	mp3an 1350	. . . . . . 7 ⊢ (∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ↑_𝑚 dom 𝑟) ∈ V
33	32	ssex 4185	. . . . . 6 ⊢ (X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ (∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ↑_𝑚 dom 𝑟) → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ∈ V)
34	28, 33	mp1i 10	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ∈ V)
35		simpr 110	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → 𝑟 = 𝑅)
36	35	fveq1d 5585	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑟‘𝑥) = (𝑅‘𝑥))
37	36	fveq2d 5587	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (Base‘(𝑟‘𝑥)) = (Base‘(𝑅‘𝑥)))
38	37	ixpeq2dv 6808	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ 𝐼 (Base‘(𝑟‘𝑥)) = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
39	35	dmeqd 4885	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑟 = dom 𝑅)
40		prdsval.i	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑅 = 𝐼)
41	40	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑅 = 𝐼)
42	39, 41	eqtrd 2239	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑟 = 𝐼)
43	42	ixpeq1d 6804	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) = X𝑥 ∈ 𝐼 (Base‘(𝑟‘𝑥)))
44		prdsval.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
45	44	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
46	38, 43, 45	3eqtr4d 2249	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) = 𝐵)
47		prdsvallem 13148	. . . . . . 7 ⊢ (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) ∈ V
48	47	a1i 9	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) ∈ V)
49		simpr 110	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝑣 = 𝐵)
50	42	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → dom 𝑟 = 𝐼)
51	50	ixpeq1d 6804	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)))
52	36	fveq2d 5587	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (Hom ‘(𝑟‘𝑥)) = (Hom ‘(𝑅‘𝑥)))
53	52	oveqd 5968	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))
54	53	ixpeq2dv 6808	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))
55	54	adantr 276	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))
56	51, 55	eqtrd 2239	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))
57	49, 49, 56	mpoeq123dv 6014	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))))
58		prdsval.h	. . . . . . . 8 ⊢ (𝜑 → 𝐻 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))))
59	58	ad3antrrr 492	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝐻 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))))
60	57, 59	eqtr4d 2242	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) = 𝐻)
61		simplr 528	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → 𝑣 = 𝐵)
62	61	opeq2d 3828	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(Base‘ndx), 𝑣⟩ = ⟨(Base‘ndx), 𝐵⟩)
63	36	fveq2d 5587	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (+_g‘(𝑟‘𝑥)) = (+_g‘(𝑅‘𝑥)))
64	63	oveqd 5968	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(+_g‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(+_g‘(𝑅‘𝑥))(𝑔‘𝑥)))
65	42, 64	mpteq12dv 4130	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+_g‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+_g‘(𝑅‘𝑥))(𝑔‘𝑥))))
66	65	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+_g‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+_g‘(𝑅‘𝑥))(𝑔‘𝑥))))
67	49, 49, 66	mpoeq123dv 6014	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+_g‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+_g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
68	67	adantr 276	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+_g‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+_g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
69		prdsval.a	. . . . . . . . . . . 12 ⊢ (𝜑 → + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+_g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
70	69	ad4antr 494	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+_g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
71	68, 70	eqtr4d 2242	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+_g‘(𝑟‘𝑥))(𝑔‘𝑥)))) = + )
72	71	opeq2d 3828	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(+_g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+_g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩ = ⟨(+_g‘ndx), + ⟩)
73	36	fveq2d 5587	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (._r‘(𝑟‘𝑥)) = (._r‘(𝑅‘𝑥)))
74	73	oveqd 5968	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(._r‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(._r‘(𝑅‘𝑥))(𝑔‘𝑥)))
75	42, 74	mpteq12dv 4130	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(._r‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(._r‘(𝑅‘𝑥))(𝑔‘𝑥))))
76	75	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(._r‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(._r‘(𝑅‘𝑥))(𝑔‘𝑥))))
77	49, 49, 76	mpoeq123dv 6014	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(._r‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(._r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
78	77	adantr 276	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(._r‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(._r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
79		prdsval.t	. . . . . . . . . . . 12 ⊢ (𝜑 → × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(._r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
80	79	ad4antr 494	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(._r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
81	78, 80	eqtr4d 2242	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(._r‘(𝑟‘𝑥))(𝑔‘𝑥)))) = × )
82	81	opeq2d 3828	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(._r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(._r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩ = ⟨(._r‘ndx), × ⟩)
83	62, 72, 82	tpeq123d 3726	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨(Base‘ndx), 𝑣⟩, ⟨(+_g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+_g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(._r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(._r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩})
84		simp-4r 542	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → 𝑠 = 𝑆)
85	84	opeq2d 3828	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(Scalar‘ndx), 𝑠⟩ = ⟨(Scalar‘ndx), 𝑆⟩)
86		simpllr 534	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝑠 = 𝑆)
87	86	fveq2d 5587	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (Base‘𝑠) = (Base‘𝑆))
88		prdsval.k	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (Base‘𝑆)
89	87, 88	eqtr4di 2257	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (Base‘𝑠) = 𝐾)
90	36	fveq2d 5587	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ( ·_𝑠 ‘(𝑟‘𝑥)) = ( ·_𝑠 ‘(𝑅‘𝑥)))
91	90	oveqd 5968	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑓( ·_𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥)) = (𝑓( ·_𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))
92	42, 91	mpteq12dv 4130	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·_𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑓( ·_𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))
93	92	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·_𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑓( ·_𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))
94	89, 49, 93	mpoeq123dv 6014	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·_𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·_𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))
95	94	adantr 276	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·_𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·_𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))
96		prdsval.m	. . . . . . . . . . . 12 ⊢ (𝜑 → · = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·_𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))
97	96	ad4antr 494	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → · = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·_𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))
98	95, 97	eqtr4d 2242	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·_𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥)))) = · )
99	98	opeq2d 3828	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨( ·_𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·_𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩ = ⟨( ·_𝑠 ‘ndx), · ⟩)
100	36	fveq2d 5587	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (·_𝑖‘(𝑟‘𝑥)) = (·_𝑖‘(𝑅‘𝑥)))
101	100	oveqd 5968	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(·_𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(·_𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))
102	42, 101	mpteq12dv 4130	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))
103	102	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))
104	86, 103	oveq12d 5969	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑠 Σ_g (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑆 Σ_g (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))
105	49, 49, 104	mpoeq123dv 6014	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σ_g (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σ_g (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))
106	105	adantr 276	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σ_g (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σ_g (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))
107		prdsval.j	. . . . . . . . . . . 12 ⊢ (𝜑 → , = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σ_g (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))
108	107	ad4antr 494	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → , = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σ_g (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))
109	106, 108	eqtr4d 2242	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σ_g (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))))) = , )
110	109	opeq2d 3828	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(·_𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σ_g (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩ = ⟨(·_𝑖‘ndx), , ⟩)
111	85, 99, 110	tpeq123d 3726	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·_𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·_𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·_𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σ_g (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩} = {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩})
112	83, 111	uneq12d 3329	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ({⟨(Base‘ndx), 𝑣⟩, ⟨(+_g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+_g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(._r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(._r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·_𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·_𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·_𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σ_g (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩}))
113		simpllr 534	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → 𝑟 = 𝑅)
114	113	coeq2d 4844	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (TopOpen ∘ 𝑟) = (TopOpen ∘ 𝑅))
115	114	fveq2d 5587	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (∏_t‘(TopOpen ∘ 𝑟)) = (∏_t‘(TopOpen ∘ 𝑅)))
116		prdsval.o	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑂 = (∏_t‘(TopOpen ∘ 𝑅)))
117	116	ad4antr 494	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → 𝑂 = (∏_t‘(TopOpen ∘ 𝑅)))
118	115, 117	eqtr4d 2242	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (∏_t‘(TopOpen ∘ 𝑟)) = 𝑂)
119	118	opeq2d 3828	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑟))⟩ = ⟨(TopSet‘ndx), 𝑂⟩)
120	49	sseq2d 3224	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → ({𝑓, 𝑔} ⊆ 𝑣 ↔ {𝑓, 𝑔} ⊆ 𝐵))
121	36	fveq2d 5587	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (le‘(𝑟‘𝑥)) = (le‘(𝑅‘𝑥)))
122	121	breqd 4058	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥) ↔ (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥)))
123	42, 122	raleqbidv 2719	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥) ↔ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥)))
124	123	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥) ↔ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥)))
125	120, 124	anbi12d 473	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥)) ↔ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))))
126	125	opabbidv 4114	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))} = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})
127	126	adantr 276	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))} = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})
128		prdsval.l	. . . . . . . . . . . 12 ⊢ (𝜑 → ≤ = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})
129	128	ad4antr 494	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ≤ = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})
130	127, 129	eqtr4d 2242	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))} = ≤ )
131	130	opeq2d 3828	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩ = ⟨(le‘ndx), ≤ ⟩)
132	36	fveq2d 5587	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (dist‘(𝑟‘𝑥)) = (dist‘(𝑅‘𝑥)))
133	132	oveqd 5968	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥)))
134	42, 133	mpteq12dv 4130	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))))
135	134	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))))
136	135	rneqd 4912	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) = ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))))
137	136	uneq1d 3327	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}) = (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}))
138	137	supeq1d 7096	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ) = sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ))
139	49, 49, 138	mpoeq123dv 6014	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < )) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < )))
140	139	adantr 276	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < )) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < )))
141		prdsval.d	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < )))
142	141	ad4antr 494	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < )))
143	140, 142	eqtr4d 2242	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < )) = 𝐷)
144	143	opeq2d 3828	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < ))⟩ = ⟨(dist‘ndx), 𝐷⟩)
145	119, 131, 144	tpeq123d 3726	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < ))⟩} = {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩})
146		simpr 110	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ℎ = 𝐻)
147	146	opeq2d 3828	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(Hom ‘ndx), ℎ⟩ = ⟨(Hom ‘ndx), 𝐻⟩)
148	61	sqxpeqd 4705	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑣 × 𝑣) = (𝐵 × 𝐵))
149	146	oveqd 5968	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ((2^nd ‘𝑎)ℎ𝑐) = ((2^nd ‘𝑎)𝐻𝑐))
150	146	fveq1d 5585	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (ℎ‘𝑎) = (𝐻‘𝑎))
151	36	fveq2d 5587	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (comp‘(𝑟‘𝑥)) = (comp‘(𝑅‘𝑥)))
152	151	oveqd 5968	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥)) = (⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥)))
153	152	oveqd 5968	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)) = ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))
154	42, 153	mpteq12dv 4130	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))
155	154	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))
156	149, 150, 155	mpoeq123dv 6014	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑑 ∈ ((2^nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))) = (𝑑 ∈ ((2^nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))
157	148, 61, 156	mpoeq123dv 6014	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2^nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))) = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2^nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))))
158		prdsval.x	. . . . . . . . . . . 12 ⊢ (𝜑 → ∙ = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2^nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))))
159	158	ad4antr 494	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ∙ = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2^nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))))
160	157, 159	eqtr4d 2242	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2^nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))) = ∙ )
161	160	opeq2d 3828	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2^nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩ = ⟨(comp‘ndx), ∙ ⟩)
162	147, 161	preq12d 3719	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2^nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩} = {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})
163	145, 162	uneq12d 3329	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ({⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2^nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩}) = ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩}))
164	112, 163	uneq12d 3329	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (({⟨(Base‘ndx), 𝑣⟩, ⟨(+_g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+_g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(._r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(._r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·_𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·_𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·_𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σ_g (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2^nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))
165	48, 60, 164	csbied2 3142	. . . . 5 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → ⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+_g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+_g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(._r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(._r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·_𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·_𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·_𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σ_g (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2^nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))
166	34, 46, 165	csbied2 3142	. . . 4 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ⦋X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+_g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+_g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(._r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(._r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·_𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·_𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·_𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σ_g (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2^nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))
167	166	anasss 399	. . 3 ⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑟 = 𝑅)) → ⦋X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+_g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+_g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(._r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(._r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·_𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·_𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·_𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σ_g (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2^nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))
168		prdsval.s	. . . 4 ⊢ (𝜑 → 𝑆 ∈ 𝑊)
169	168	elexd 2786	. . 3 ⊢ (𝜑 → 𝑆 ∈ V)
170		prdsval.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑍)
171	170	elexd 2786	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
172		dmexg 4947	. . . . . . . . . . 11 ⊢ (𝑅 ∈ 𝑍 → dom 𝑅 ∈ V)
173	170, 172	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → dom 𝑅 ∈ V)
174	40, 173	eqeltrrd 2284	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ V)
175		basfn 12934	. . . . . . . . . . 11 ⊢ Base Fn V
176		fvexg 5602	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ 𝑍 ∧ 𝑥 ∈ V) → (𝑅‘𝑥) ∈ V)
177	170, 10, 176	sylancl 413	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑅‘𝑥) ∈ V)
178		funfvex 5600	. . . . . . . . . . . 12 ⊢ ((Fun Base ∧ (𝑅‘𝑥) ∈ dom Base) → (Base‘(𝑅‘𝑥)) ∈ V)
179	178	funfni 5381	. . . . . . . . . . 11 ⊢ ((Base Fn V ∧ (𝑅‘𝑥) ∈ V) → (Base‘(𝑅‘𝑥)) ∈ V)
180	175, 177, 179	sylancr 414	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘(𝑅‘𝑥)) ∈ V)
181	180	ralrimivw 2581	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)) ∈ V)
182		ixpexgg 6816	. . . . . . . . 9 ⊢ ((𝐼 ∈ V ∧ ∀𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)) ∈ V) → X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)) ∈ V)
183	174, 181, 182	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)) ∈ V)
184	44, 183	eqeltrd 2283	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ V)
185		opexg 4276	. . . . . . 7 ⊢ (((Base‘ndx) ∈ ℕ ∧ 𝐵 ∈ V) → ⟨(Base‘ndx), 𝐵⟩ ∈ V)
186	13, 184, 185	sylancr 414	. . . . . 6 ⊢ (𝜑 → ⟨(Base‘ndx), 𝐵⟩ ∈ V)
187		plusgndxnn 12987	. . . . . . 7 ⊢ (+_g‘ndx) ∈ ℕ
188		mpoexga 6305	. . . . . . . . 9 ⊢ ((𝐵 ∈ V ∧ 𝐵 ∈ V) → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+_g‘(𝑅‘𝑥))(𝑔‘𝑥)))) ∈ V)
189	184, 184, 188	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+_g‘(𝑅‘𝑥))(𝑔‘𝑥)))) ∈ V)
190	69, 189	eqeltrd 2283	. . . . . . 7 ⊢ (𝜑 → + ∈ V)
191		opexg 4276	. . . . . . 7 ⊢ (((+_g‘ndx) ∈ ℕ ∧ + ∈ V) → ⟨(+_g‘ndx), + ⟩ ∈ V)
192	187, 190, 191	sylancr 414	. . . . . 6 ⊢ (𝜑 → ⟨(+_g‘ndx), + ⟩ ∈ V)
193		mulrslid 13008	. . . . . . . 8 ⊢ (._r = Slot (._r‘ndx) ∧ (._r‘ndx) ∈ ℕ)
194	193	simpri 113	. . . . . . 7 ⊢ (._r‘ndx) ∈ ℕ
195		mpoexga 6305	. . . . . . . . 9 ⊢ ((𝐵 ∈ V ∧ 𝐵 ∈ V) → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(._r‘(𝑅‘𝑥))(𝑔‘𝑥)))) ∈ V)
196	184, 184, 195	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(._r‘(𝑅‘𝑥))(𝑔‘𝑥)))) ∈ V)
197	79, 196	eqeltrd 2283	. . . . . . 7 ⊢ (𝜑 → × ∈ V)
198		opexg 4276	. . . . . . 7 ⊢ (((._r‘ndx) ∈ ℕ ∧ × ∈ V) → ⟨(._r‘ndx), × ⟩ ∈ V)
199	194, 197, 198	sylancr 414	. . . . . 6 ⊢ (𝜑 → ⟨(._r‘ndx), × ⟩ ∈ V)
200		tpexg 4495	. . . . . 6 ⊢ ((⟨(Base‘ndx), 𝐵⟩ ∈ V ∧ ⟨(+_g‘ndx), + ⟩ ∈ V ∧ ⟨(._r‘ndx), × ⟩ ∈ V) → {⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩} ∈ V)
201	186, 192, 199, 200	syl3anc 1250	. . . . 5 ⊢ (𝜑 → {⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩} ∈ V)
202		scaslid 13029	. . . . . . . 8 ⊢ (Scalar = Slot (Scalar‘ndx) ∧ (Scalar‘ndx) ∈ ℕ)
203	202	simpri 113	. . . . . . 7 ⊢ (Scalar‘ndx) ∈ ℕ
204		opexg 4276	. . . . . . 7 ⊢ (((Scalar‘ndx) ∈ ℕ ∧ 𝑆 ∈ 𝑊) → ⟨(Scalar‘ndx), 𝑆⟩ ∈ V)
205	203, 168, 204	sylancr 414	. . . . . 6 ⊢ (𝜑 → ⟨(Scalar‘ndx), 𝑆⟩ ∈ V)
206		vscaslid 13039	. . . . . . . 8 ⊢ ( ·_𝑠 = Slot ( ·_𝑠 ‘ndx) ∧ ( ·_𝑠 ‘ndx) ∈ ℕ)
207	206	simpri 113	. . . . . . 7 ⊢ ( ·_𝑠 ‘ndx) ∈ ℕ
208		funfvex 5600	. . . . . . . . . . . 12 ⊢ ((Fun Base ∧ 𝑆 ∈ dom Base) → (Base‘𝑆) ∈ V)
209	208	funfni 5381	. . . . . . . . . . 11 ⊢ ((Base Fn V ∧ 𝑆 ∈ V) → (Base‘𝑆) ∈ V)
210	175, 169, 209	sylancr 414	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝑆) ∈ V)
211	88, 210	eqeltrid 2293	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ V)
212		mpoexga 6305	. . . . . . . . 9 ⊢ ((𝐾 ∈ V ∧ 𝐵 ∈ V) → (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·_𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))) ∈ V)
213	211, 184, 212	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·_𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))) ∈ V)
214	96, 213	eqeltrd 2283	. . . . . . 7 ⊢ (𝜑 → · ∈ V)
215		opexg 4276	. . . . . . 7 ⊢ ((( ·_𝑠 ‘ndx) ∈ ℕ ∧ · ∈ V) → ⟨( ·_𝑠 ‘ndx), · ⟩ ∈ V)
216	207, 214, 215	sylancr 414	. . . . . 6 ⊢ (𝜑 → ⟨( ·_𝑠 ‘ndx), · ⟩ ∈ V)
217		ipslid 13047	. . . . . . . 8 ⊢ (·_𝑖 = Slot (·_𝑖‘ndx) ∧ (·_𝑖‘ndx) ∈ ℕ)
218	217	simpri 113	. . . . . . 7 ⊢ (·_𝑖‘ndx) ∈ ℕ
219		mpoexga 6305	. . . . . . . . 9 ⊢ ((𝐵 ∈ V ∧ 𝐵 ∈ V) → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σ_g (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))) ∈ V)
220	184, 184, 219	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σ_g (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))) ∈ V)
221	107, 220	eqeltrd 2283	. . . . . . 7 ⊢ (𝜑 → , ∈ V)
222		opexg 4276	. . . . . . 7 ⊢ (((·_𝑖‘ndx) ∈ ℕ ∧ , ∈ V) → ⟨(·_𝑖‘ndx), , ⟩ ∈ V)
223	218, 221, 222	sylancr 414	. . . . . 6 ⊢ (𝜑 → ⟨(·_𝑖‘ndx), , ⟩ ∈ V)
224		tpexg 4495	. . . . . 6 ⊢ ((⟨(Scalar‘ndx), 𝑆⟩ ∈ V ∧ ⟨( ·_𝑠 ‘ndx), · ⟩ ∈ V ∧ ⟨(·_𝑖‘ndx), , ⟩ ∈ V) → {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩} ∈ V)
225	205, 216, 223, 224	syl3anc 1250	. . . . 5 ⊢ (𝜑 → {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩} ∈ V)
226		unexg 4494	. . . . 5 ⊢ (({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩} ∈ V ∧ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩} ∈ V) → ({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩}) ∈ V)
227	201, 225, 226	syl2anc 411	. . . 4 ⊢ (𝜑 → ({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩}) ∈ V)
228		tsetndxnn 13065	. . . . . . 7 ⊢ (TopSet‘ndx) ∈ ℕ
229		topnfn 13120	. . . . . . . . . . 11 ⊢ TopOpen Fn V
230		fnfun 5376	. . . . . . . . . . 11 ⊢ (TopOpen Fn V → Fun TopOpen)
231	229, 230	ax-mp 5	. . . . . . . . . 10 ⊢ Fun TopOpen
232		cofunexg 6201	. . . . . . . . . 10 ⊢ ((Fun TopOpen ∧ 𝑅 ∈ 𝑍) → (TopOpen ∘ 𝑅) ∈ V)
233	231, 170, 232	sylancr 414	. . . . . . . . 9 ⊢ (𝜑 → (TopOpen ∘ 𝑅) ∈ V)
234		ptex 13140	. . . . . . . . 9 ⊢ ((TopOpen ∘ 𝑅) ∈ V → (∏_t‘(TopOpen ∘ 𝑅)) ∈ V)
235	233, 234	syl 14	. . . . . . . 8 ⊢ (𝜑 → (∏_t‘(TopOpen ∘ 𝑅)) ∈ V)
236	116, 235	eqeltrd 2283	. . . . . . 7 ⊢ (𝜑 → 𝑂 ∈ V)
237		opexg 4276	. . . . . . 7 ⊢ (((TopSet‘ndx) ∈ ℕ ∧ 𝑂 ∈ V) → ⟨(TopSet‘ndx), 𝑂⟩ ∈ V)
238	228, 236, 237	sylancr 414	. . . . . 6 ⊢ (𝜑 → ⟨(TopSet‘ndx), 𝑂⟩ ∈ V)
239		plendxnn 13079	. . . . . . 7 ⊢ (le‘ndx) ∈ ℕ
240		vex 2776	. . . . . . . . . . . 12 ⊢ 𝑓 ∈ V
241		vex 2776	. . . . . . . . . . . 12 ⊢ 𝑔 ∈ V
242	240, 241	prss 3791	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ↔ {𝑓, 𝑔} ⊆ 𝐵)
243	242	anbi1i 458	. . . . . . . . . 10 ⊢ (((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥)) ↔ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥)))
244	243	opabbii 4115	. . . . . . . . 9 ⊢ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))} = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))}
245		xpexg 4793	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ 𝐵 ∈ V) → (𝐵 × 𝐵) ∈ V)
246	184, 184, 245	syl2anc 411	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 × 𝐵) ∈ V)
247		opabssxp 4753	. . . . . . . . . . 11 ⊢ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))} ⊆ (𝐵 × 𝐵)
248	247	a1i 9	. . . . . . . . . 10 ⊢ (𝜑 → {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))} ⊆ (𝐵 × 𝐵))
249	246, 248	ssexd 4188	. . . . . . . . 9 ⊢ (𝜑 → {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))} ∈ V)
250	244, 249	eqeltrrid 2294	. . . . . . . 8 ⊢ (𝜑 → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))} ∈ V)
251	128, 250	eqeltrd 2283	. . . . . . 7 ⊢ (𝜑 → ≤ ∈ V)
252		opexg 4276	. . . . . . 7 ⊢ (((le‘ndx) ∈ ℕ ∧ ≤ ∈ V) → ⟨(le‘ndx), ≤ ⟩ ∈ V)
253	239, 251, 252	sylancr 414	. . . . . 6 ⊢ (𝜑 → ⟨(le‘ndx), ≤ ⟩ ∈ V)
254		dsndxnn 13094	. . . . . . 7 ⊢ (dist‘ndx) ∈ ℕ
255		mpoexga 6305	. . . . . . . . 9 ⊢ ((𝐵 ∈ V ∧ 𝐵 ∈ V) → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < )) ∈ V)
256	184, 184, 255	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < )) ∈ V)
257	141, 256	eqeltrd 2283	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ V)
258		opexg 4276	. . . . . . 7 ⊢ (((dist‘ndx) ∈ ℕ ∧ 𝐷 ∈ V) → ⟨(dist‘ndx), 𝐷⟩ ∈ V)
259	254, 257, 258	sylancr 414	. . . . . 6 ⊢ (𝜑 → ⟨(dist‘ndx), 𝐷⟩ ∈ V)
260		tpexg 4495	. . . . . 6 ⊢ ((⟨(TopSet‘ndx), 𝑂⟩ ∈ V ∧ ⟨(le‘ndx), ≤ ⟩ ∈ V ∧ ⟨(dist‘ndx), 𝐷⟩ ∈ V) → {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∈ V)
261	238, 253, 259, 260	syl3anc 1250	. . . . 5 ⊢ (𝜑 → {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∈ V)
262		homslid 13111	. . . . . . . 8 ⊢ (Hom = Slot (Hom ‘ndx) ∧ (Hom ‘ndx) ∈ ℕ)
263	262	simpri 113	. . . . . . 7 ⊢ (Hom ‘ndx) ∈ ℕ
264		mpoexga 6305	. . . . . . . . 9 ⊢ ((𝐵 ∈ V ∧ 𝐵 ∈ V) → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) ∈ V)
265	184, 184, 264	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) ∈ V)
266	58, 265	eqeltrd 2283	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ V)
267		opexg 4276	. . . . . . 7 ⊢ (((Hom ‘ndx) ∈ ℕ ∧ 𝐻 ∈ V) → ⟨(Hom ‘ndx), 𝐻⟩ ∈ V)
268	263, 266, 267	sylancr 414	. . . . . 6 ⊢ (𝜑 → ⟨(Hom ‘ndx), 𝐻⟩ ∈ V)
269		ccoslid 13114	. . . . . . . 8 ⊢ (comp = Slot (comp‘ndx) ∧ (comp‘ndx) ∈ ℕ)
270	269	simpri 113	. . . . . . 7 ⊢ (comp‘ndx) ∈ ℕ
271		mpoexga 6305	. . . . . . . . 9 ⊢ (((𝐵 × 𝐵) ∈ V ∧ 𝐵 ∈ V) → (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2^nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))) ∈ V)
272	246, 184, 271	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2^nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))) ∈ V)
273	158, 272	eqeltrd 2283	. . . . . . 7 ⊢ (𝜑 → ∙ ∈ V)
274		opexg 4276	. . . . . . 7 ⊢ (((comp‘ndx) ∈ ℕ ∧ ∙ ∈ V) → ⟨(comp‘ndx), ∙ ⟩ ∈ V)
275	270, 273, 274	sylancr 414	. . . . . 6 ⊢ (𝜑 → ⟨(comp‘ndx), ∙ ⟩ ∈ V)
276		prexg 4259	. . . . . 6 ⊢ ((⟨(Hom ‘ndx), 𝐻⟩ ∈ V ∧ ⟨(comp‘ndx), ∙ ⟩ ∈ V) → {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩} ∈ V)
277	268, 275, 276	syl2anc 411	. . . . 5 ⊢ (𝜑 → {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩} ∈ V)
278		unexg 4494	. . . . 5 ⊢ (({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∈ V ∧ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩} ∈ V) → ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩}) ∈ V)
279	261, 277, 278	syl2anc 411	. . . 4 ⊢ (𝜑 → ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩}) ∈ V)
280		unexg 4494	. . . 4 ⊢ ((({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩}) ∈ V ∧ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩}) ∈ V) → (({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})) ∈ V)
281	227, 279, 280	syl2anc 411	. . 3 ⊢ (𝜑 → (({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})) ∈ V)
282	3, 167, 169, 171, 281	ovmpod 6080	. 2 ⊢ (𝜑 → (𝑆X_s𝑅) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))
283	1, 282	eqtrid 2251	1 ⊢ (𝜑 → 𝑃 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩, ⟨(._r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), · ⟩, ⟨(·_𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1373 ⊤wtru 1374 ∈ wcel 2177 ∀wral 2485 Vcvv 2773 ⦋csb 3094 ∪ cun 3165 ⊆ wss 3167 {csn 3634 {cpr 3635 {ctp 3636 ⟨cop 3637 ∪ cuni 3852 ∪ ciun 3929 class class class wbr 4047 {copab 4108 ↦ cmpt 4109 × cxp 4677 dom cdm 4679 ran crn 4680 ∘ ccom 4683 Fun wfun 5270 Fn wfn 5271 ‘cfv 5276 (class class class)co 5951 ∈ cmpo 5953 1^st c1st 6231 2^nd c2nd 6232 ↑_𝑚 cmap 6742 Xcixp 6792 supcsup 7091 0cc0 7932 ℝ^*cxr 8113 < clt 8114 ℕcn 9043 ndxcnx 12873 Slot cslot 12875 Basecbs 12876 +_gcplusg 12953 ._rcmulr 12954 Scalarcsca 12956 ·_𝑠 cvsca 12957 ·_𝑖cip 12958 TopSetcts 12959 lecple 12960 distcds 12962 Hom chom 12964 compcco 12965 TopOpenctopn 13116 ∏_tcpt 13131 Σ_g cgsu 13133 X_scprds 13141

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4163 ax-sep 4166 ax-pow 4222 ax-pr 4257 ax-un 4484 ax-setind 4589 ax-cnex 8023 ax-resscn 8024 ax-1cn 8025 ax-1re 8026 ax-icn 8027 ax-addcl 8028 ax-addrcl 8029 ax-mulcl 8030 ax-addcom 8032 ax-mulcom 8033 ax-addass 8034 ax-mulass 8035 ax-distr 8036 ax-i2m1 8037 ax-1rid 8039 ax-0id 8040 ax-rnegex 8041 ax-cnre 8043

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-ral 2490 df-rex 2491 df-reu 2492 df-rab 2494 df-v 2775 df-sbc 3000 df-csb 3095 df-dif 3169 df-un 3171 df-in 3173 df-ss 3180 df-pw 3619 df-sn 3640 df-pr 3641 df-tp 3642 df-op 3643 df-uni 3853 df-int 3888 df-iun 3931 df-br 4048 df-opab 4110 df-mpt 4111 df-id 4344 df-xp 4685 df-rel 4686 df-cnv 4687 df-co 4688 df-dm 4689 df-rn 4690 df-res 4691 df-ima 4692 df-iota 5237 df-fun 5278 df-fn 5279 df-f 5280 df-f1 5281 df-fo 5282 df-f1o 5283 df-fv 5284 df-riota 5906 df-ov 5954 df-oprab 5955 df-mpo 5956 df-1st 6233 df-2nd 6234 df-map 6744 df-ixp 6793 df-sup 7093 df-sub 8252 df-inn 9044 df-2 9102 df-3 9103 df-4 9104 df-5 9105 df-6 9106 df-7 9107 df-8 9108 df-9 9109 df-n0 9303 df-dec 9512 df-ndx 12879 df-slot 12880 df-base 12882 df-plusg 12966 df-mulr 12967 df-sca 12969 df-vsca 12970 df-ip 12971 df-tset 12972 df-ple 12973 df-ds 12975 df-hom 12977 df-cco 12978 df-rest 13117 df-topn 13118 df-topgen 13136 df-pt 13137 df-prds 13143

This theorem is referenced by: prdsbaslemss 13150 prdssca 13151 prdsbas 13152 prdsplusg 13153 prdsmulr 13154

W3C validator