Theorem prdsval 17375

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	⊢ 𝑃 = (𝑆Xs𝑅)
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	⊢ (𝜑 → ∙ = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(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 ⊢ 𝑃 = (𝑆Xs𝑅)
2		df-prds 17367	. . . 4 ⊢ Xs = (𝑠 ∈ 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), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})))
3	2	a1i 11	. . 3 ⊢ (𝜑 → Xs = (𝑠 ∈ 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), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩}))))
4		vex 3444	. . . . . . . . . . . 12 ⊢ 𝑟 ∈ V
5	4	rnex 7852	. . . . . . . . . . 11 ⊢ ran 𝑟 ∈ V
6	5	uniex 7686	. . . . . . . . . 10 ⊢ ∪ ran 𝑟 ∈ V
7	6	rnex 7852	. . . . . . . . 9 ⊢ ran ∪ ran 𝑟 ∈ V
8	7	uniex 7686	. . . . . . . 8 ⊢ ∪ ran ∪ ran 𝑟 ∈ V
9		baseid 17139	. . . . . . . . . . . 12 ⊢ Base = Slot (Base‘ndx)
10	9	strfvss 17114	. . . . . . . . . . 11 ⊢ (Base‘(𝑟‘𝑥)) ⊆ ∪ ran (𝑟‘𝑥)
11		fvssunirn 6865	. . . . . . . . . . . 12 ⊢ (𝑟‘𝑥) ⊆ ∪ ran 𝑟
12		rnss 5888	. . . . . . . . . . . 12 ⊢ ((𝑟‘𝑥) ⊆ ∪ ran 𝑟 → ran (𝑟‘𝑥) ⊆ ran ∪ ran 𝑟)
13		uniss 4871	. . . . . . . . . . . 12 ⊢ (ran (𝑟‘𝑥) ⊆ ran ∪ ran 𝑟 → ∪ ran (𝑟‘𝑥) ⊆ ∪ ran ∪ ran 𝑟)
14	11, 12, 13	mp2b 10	. . . . . . . . . . 11 ⊢ ∪ ran (𝑟‘𝑥) ⊆ ∪ ran ∪ ran 𝑟
15	10, 14	sstri 3943	. . . . . . . . . 10 ⊢ (Base‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran 𝑟
16	15	rgenw 3055	. . . . . . . . 9 ⊢ ∀𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran 𝑟
17		iunss 5000	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran 𝑟 ↔ ∀𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran 𝑟)
18	16, 17	mpbir 231	. . . . . . . 8 ⊢ ∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran 𝑟
19	8, 18	ssexi 5267	. . . . . . 7 ⊢ ∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ∈ V
20		ixpssmap2g 8865	. . . . . . 7 ⊢ (∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ∈ V → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ (∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ↑m dom 𝑟))
21	19, 20	ax-mp 5	. . . . . 6 ⊢ X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ (∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ↑m dom 𝑟)
22		ovex 7391	. . . . . . 7 ⊢ (∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ↑m dom 𝑟) ∈ V
23	22	ssex 5266	. . . . . 6 ⊢ (X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ (∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ↑m dom 𝑟) → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ∈ V)
24	21, 23	mp1i 13	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ∈ V)
25		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → 𝑟 = 𝑅)
26	25	fveq1d 6836	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑟‘𝑥) = (𝑅‘𝑥))
27	26	fveq2d 6838	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (Base‘(𝑟‘𝑥)) = (Base‘(𝑅‘𝑥)))
28	27	ixpeq2dv 8851	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ 𝐼 (Base‘(𝑟‘𝑥)) = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
29	25	dmeqd 5854	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑟 = dom 𝑅)
30		prdsval.i	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑅 = 𝐼)
31	30	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑅 = 𝐼)
32	29, 31	eqtrd 2771	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑟 = 𝐼)
33	32	ixpeq1d 8847	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) = X𝑥 ∈ 𝐼 (Base‘(𝑟‘𝑥)))
34		prdsval.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
35	34	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
36	28, 33, 35	3eqtr4d 2781	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) = 𝐵)
37		prdsvallem 17374	. . . . . . 7 ⊢ (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) ∈ V
38	37	a1i 11	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) ∈ V)
39		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝑣 = 𝐵)
40	32	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → dom 𝑟 = 𝐼)
41	40	ixpeq1d 8847	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)))
42	26	fveq2d 6838	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (Hom ‘(𝑟‘𝑥)) = (Hom ‘(𝑅‘𝑥)))
43	42	oveqd 7375	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))
44	43	ixpeq2dv 8851	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))
45	44	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))
46	41, 45	eqtrd 2771	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))
47	39, 39, 46	mpoeq123dv 7433	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))))
48		prdsval.h	. . . . . . . 8 ⊢ (𝜑 → 𝐻 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))))
49	48	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝐻 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))))
50	47, 49	eqtr4d 2774	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) = 𝐻)
51		simplr 768	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → 𝑣 = 𝐵)
52	51	opeq2d 4836	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(Base‘ndx), 𝑣⟩ = ⟨(Base‘ndx), 𝐵⟩)
53	26	fveq2d 6838	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (+g‘(𝑟‘𝑥)) = (+g‘(𝑅‘𝑥)))
54	53	oveqd 7375	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))
55	32, 54	mpteq12dv 5185	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))
56	55	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))
57	39, 39, 56	mpoeq123dv 7433	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
58	57	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
59		prdsval.a	. . . . . . . . . . . 12 ⊢ (𝜑 → + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
60	59	ad4antr 732	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
61	58, 60	eqtr4d 2774	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥)))) = + )
62	61	opeq2d 4836	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩ = ⟨(+g‘ndx), + ⟩)
63	26	fveq2d 6838	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (.r‘(𝑟‘𝑥)) = (.r‘(𝑅‘𝑥)))
64	63	oveqd 7375	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))
65	32, 64	mpteq12dv 5185	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))
66	65	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))
67	39, 39, 66	mpoeq123dv 7433	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
68	67	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
69		prdsval.t	. . . . . . . . . . . 12 ⊢ (𝜑 → × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
70	69	ad4antr 732	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
71	68, 70	eqtr4d 2774	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥)))) = × )
72	71	opeq2d 4836	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩ = ⟨(.r‘ndx), × ⟩)
73	52, 62, 72	tpeq123d 4705	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩})
74		simp-4r 783	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → 𝑠 = 𝑆)
75	74	opeq2d 4836	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(Scalar‘ndx), 𝑠⟩ = ⟨(Scalar‘ndx), 𝑆⟩)
76		simpllr 775	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝑠 = 𝑆)
77	76	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (Base‘𝑠) = (Base‘𝑆))
78		prdsval.k	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (Base‘𝑆)
79	77, 78	eqtr4di 2789	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (Base‘𝑠) = 𝐾)
80	26	fveq2d 6838	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ( ·𝑠 ‘(𝑟‘𝑥)) = ( ·𝑠 ‘(𝑅‘𝑥)))
81	80	oveqd 7375	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥)) = (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))
82	32, 81	mpteq12dv 5185	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))
83	82	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))
84	79, 39, 83	mpoeq123dv 7433	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))
85	84	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))
86		prdsval.m	. . . . . . . . . . . 12 ⊢ (𝜑 → · = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))
87	86	ad4antr 732	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → · = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))
88	85, 87	eqtr4d 2774	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥)))) = · )
89	88	opeq2d 4836	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩ = ⟨( ·𝑠 ‘ndx), · ⟩)
90	26	fveq2d 6838	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (·𝑖‘(𝑟‘𝑥)) = (·𝑖‘(𝑅‘𝑥)))
91	90	oveqd 7375	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))
92	32, 91	mpteq12dv 5185	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))
93	92	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))
94	76, 93	oveq12d 7376	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))
95	39, 39, 94	mpoeq123dv 7433	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))
96	95	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))
97		prdsval.j	. . . . . . . . . . . 12 ⊢ (𝜑 → , = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))
98	97	ad4antr 732	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → , = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))
99	96, 98	eqtr4d 2774	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))))) = , )
100	99	opeq2d 4836	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩ = ⟨(·𝑖‘ndx), , ⟩)
101	75, 89, 100	tpeq123d 4705	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩} = {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩})
102	73, 101	uneq12d 4121	. . . . . . 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), , ⟩}))
103		simpllr 775	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → 𝑟 = 𝑅)
104	103	coeq2d 5811	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (TopOpen ∘ 𝑟) = (TopOpen ∘ 𝑅))
105	104	fveq2d 6838	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (∏t‘(TopOpen ∘ 𝑟)) = (∏t‘(TopOpen ∘ 𝑅)))
106		prdsval.o	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑂 = (∏t‘(TopOpen ∘ 𝑅)))
107	106	ad4antr 732	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → 𝑂 = (∏t‘(TopOpen ∘ 𝑅)))
108	105, 107	eqtr4d 2774	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (∏t‘(TopOpen ∘ 𝑟)) = 𝑂)
109	108	opeq2d 4836	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩ = ⟨(TopSet‘ndx), 𝑂⟩)
110	39	sseq2d 3966	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → ({𝑓, 𝑔} ⊆ 𝑣 ↔ {𝑓, 𝑔} ⊆ 𝐵))
111	26	fveq2d 6838	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (le‘(𝑟‘𝑥)) = (le‘(𝑅‘𝑥)))
112	111	breqd 5109	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥) ↔ (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥)))
113	32, 112	raleqbidv 3316	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥) ↔ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥)))
114	113	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥) ↔ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥)))
115	110, 114	anbi12d 632	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥)) ↔ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))))
116	115	opabbidv 5164	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))} = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})
117	116	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))} = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})
118		prdsval.l	. . . . . . . . . . . 12 ⊢ (𝜑 → ≤ = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})
119	118	ad4antr 732	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ≤ = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})
120	117, 119	eqtr4d 2774	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))} = ≤ )
121	120	opeq2d 4836	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩ = ⟨(le‘ndx), ≤ ⟩)
122	26	fveq2d 6838	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (dist‘(𝑟‘𝑥)) = (dist‘(𝑅‘𝑥)))
123	122	oveqd 7375	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥)))
124	32, 123	mpteq12dv 5185	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))))
125	124	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))))
126	125	rneqd 5887	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) = ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))))
127	126	uneq1d 4119	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}) = (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}))
128	127	supeq1d 9349	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ) = sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))
129	39, 39, 128	mpoeq123dv 7433	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )))
130	129	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )))
131		prdsval.d	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )))
132	131	ad4antr 732	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )))
133	130, 132	eqtr4d 2774	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )) = 𝐷)
134	133	opeq2d 4836	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩ = ⟨(dist‘ndx), 𝐷⟩)
135	109, 121, 134	tpeq123d 4705	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} = {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩})
136		simpr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ℎ = 𝐻)
137	136	opeq2d 4836	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(Hom ‘ndx), ℎ⟩ = ⟨(Hom ‘ndx), 𝐻⟩)
138	51	sqxpeqd 5656	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑣 × 𝑣) = (𝐵 × 𝐵))
139	136	oveqd 7375	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ((2nd ‘𝑎)ℎ𝑐) = ((2nd ‘𝑎)𝐻𝑐))
140	136	fveq1d 6836	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (ℎ‘𝑎) = (𝐻‘𝑎))
141	26	fveq2d 6838	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (comp‘(𝑟‘𝑥)) = (comp‘(𝑅‘𝑥)))
142	141	oveqd 7375	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥)) = (⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥)))
143	142	oveqd 7375	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)) = ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))
144	32, 143	mpteq12dv 5185	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))
145	144	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))
146	139, 140, 145	mpoeq123dv 7433	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))) = (𝑑 ∈ ((2nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))
147	138, 51, 146	mpoeq123dv 7433	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))) = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))))
148		prdsval.x	. . . . . . . . . . . 12 ⊢ (𝜑 → ∙ = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))))
149	148	ad4antr 732	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ∙ = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))))
150	147, 149	eqtr4d 2774	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))) = ∙ )
151	150	opeq2d 4836	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩ = ⟨(comp‘ndx), ∙ ⟩)
152	137, 151	preq12d 4698	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩} = {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})
153	135, 152	uneq12d 4121	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩}) = ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩}))
154	102, 153	uneq12d 4121	. . . . . 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), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))
155	38, 50, 154	csbied2 3886	. . . . 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), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))
156	24, 36, 155	csbied2 3886	. . . 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), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))
157	156	anasss 466	. . 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), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))
158		prdsval.s	. . . 4 ⊢ (𝜑 → 𝑆 ∈ 𝑊)
159	158	elexd 3464	. . 3 ⊢ (𝜑 → 𝑆 ∈ V)
160		prdsval.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑍)
161	160	elexd 3464	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
162		tpex 7691	. . . . . 6 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∈ V
163		tpex 7691	. . . . . 6 ⊢ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩} ∈ V
164	162, 163	unex 7689	. . . . 5 ⊢ ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∈ V
165		tpex 7691	. . . . . 6 ⊢ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∈ V
166		prex 5382	. . . . . 6 ⊢ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩} ∈ V
167	165, 166	unex 7689	. . . . 5 ⊢ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩}) ∈ V
168	164, 167	unex 7689	. . . 4 ⊢ (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})) ∈ V
169	168	a1i 11	. . 3 ⊢ (𝜑 → (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})) ∈ V)
170	3, 157, 159, 161, 169	ovmpod 7510	. 2 ⊢ (𝜑 → (𝑆Xs𝑅) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))
171	1, 170	eqtrid 2783	1 ⊢ (𝜑 → 𝑃 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3051  Vcvv 3440  ⦋csb 3849   ∪ cun 3899   ⊆ wss 3901  {csn 4580  {cpr 4582  {ctp 4584  ⟨cop 4586  ∪ cuni 4863  ∪ ciun 4946   class class class wbr 5098  {copab 5160   ↦ cmpt 5179   × cxp 5622  dom cdm 5624  ran crn 5625   ∘ ccom 5628  ‘cfv 6492  (class class class)co 7358   ∈ cmpo 7360  1^st c1st 7931  2^nd c2nd 7932   ↑_m cmap 8763  Xcixp 8835  supcsup 9343  0cc0 11026  ℝ^*cxr 11165   < clt 11166  ndxcnx 17120  Basecbs 17136  +_gcplusg 17177  ._rcmulr 17178  Scalarcsca 17180   ·_𝑠 cvsca 17181  ·_𝑖cip 17182  TopSetcts 17183  lecple 17184  distcds 17186  Hom chom 17188  compcco 17189  TopOpenctopn 17341  ∏_tcpt 17358   Σ_g cgsu 17360  X_scprds 17365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-tp 4585  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-er 8635  df-map 8765  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-sup 9345  df-pnf 11168  df-mnf 11169  df-ltxr 11171  df-nn 12146  df-2 12208  df-3 12209  df-4 12210  df-5 12211  df-6 12212  df-7 12213  df-8 12214  df-9 12215  df-n0 12402  df-dec 12608  df-slot 17109  df-ndx 17121  df-base 17137  df-hom 17201  df-prds 17367

This theorem is referenced by:  prdssca  17376  prdsbas  17377  prdsplusg  17378  prdsmulr  17379  prdsvsca  17380  prdsip  17381  prdsle  17382  prdsds  17384  prdstset  17386  prdshom  17387  prdsco  17388