Theorem prdsval 17546

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 17538	. . . 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 3457	. . . . . . . . . . . 12 ⊢ 𝑟 ∈ V
5	4	rnex 7911	. . . . . . . . . . 11 ⊢ ran 𝑟 ∈ V
6	5	uniex 7747	. . . . . . . . . 10 ⊢ ∪ ran 𝑟 ∈ V
7	6	rnex 7911	. . . . . . . . 9 ⊢ ran ∪ ran 𝑟 ∈ V
8	7	uniex 7747	. . . . . . . 8 ⊢ ∪ ran ∪ ran 𝑟 ∈ V
9		baseid 17310	. . . . . . . . . . . 12 ⊢ Base = Slot (Base‘ndx)
10	9	strfvss 17285	. . . . . . . . . . 11 ⊢ (Base‘(𝑟‘𝑥)) ⊆ ∪ ran (𝑟‘𝑥)
11		fvssunirn 6913	. . . . . . . . . . . 12 ⊢ (𝑟‘𝑥) ⊆ ∪ ran 𝑟
12		rnss 5927	. . . . . . . . . . . 12 ⊢ ((𝑟‘𝑥) ⊆ ∪ ran 𝑟 → ran (𝑟‘𝑥) ⊆ ran ∪ ran 𝑟)
13		uniss 4878	. . . . . . . . . . . 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 3082	. . . . . . . . 9 ⊢ ∀𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran 𝑟
17		iunss 5007	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran 𝑟 ↔ ∀𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran 𝑟)
18	16, 17	mpbir 234	. . . . . . . 8 ⊢ ∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ ∪ ran ∪ ran 𝑟
19	8, 18	ssexi 5291	. . . . . . 7 ⊢ ∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ∈ V
20		ixpssmap2g 8938	. . . . . . 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 7450	. . . . . . 7 ⊢ (∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ↑m dom 𝑟) ∈ V
23	22	ssex 5289	. . . . . 6 ⊢ (X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ⊆ (∪ 𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ↑m dom 𝑟) → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ∈ V)
24	21, 23	mp1i 14	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) ∈ V)
25		simpr 490	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → 𝑟 = 𝑅)
26	25	fveq1d 6884	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑟‘𝑥) = (𝑅‘𝑥))
27	26	fveq2d 6886	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (Base‘(𝑟‘𝑥)) = (Base‘(𝑅‘𝑥)))
28	27	ixpeq2dv 8924	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ 𝐼 (Base‘(𝑟‘𝑥)) = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
29	25	dmeqd 5893	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑟 = dom 𝑅)
30		prdsval.i	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑅 = 𝐼)
31	30	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑅 = 𝐼)
32	29, 31	eqtrd 2797	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑟 = 𝐼)
33	32	ixpeq1d 8920	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) = X𝑥 ∈ 𝐼 (Base‘(𝑟‘𝑥)))
34		prdsval.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
35	34	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
36	28, 33, 35	3eqtr4d 2807	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) = 𝐵)
37		prdsvallem 17545	. . . . . . 7 ⊢ (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) ∈ V
38	37	a1i 11	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) ∈ V)
39		simpr 490	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝑣 = 𝐵)
40	32	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → dom 𝑟 = 𝐼)
41	40	ixpeq1d 8920	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)))
42	26	fveq2d 6886	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (Hom ‘(𝑟‘𝑥)) = (Hom ‘(𝑅‘𝑥)))
43	42	oveqd 7434	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))
44	43	ixpeq2dv 8924	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))
45	44	adantr 486	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))
46	41, 45	eqtrd 2797	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥)) = X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))
47	39, 39, 46	mpoeq123dv 7492	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))))
48		prdsval.h	. . . . . . . 8 ⊢ (𝜑 → 𝐻 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))))
49	48	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝐻 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))))
50	47, 49	eqtr4d 2800	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) = 𝐻)
51		simplr 781	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → 𝑣 = 𝐵)
52	51	opeq2d 4843	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(Base‘ndx), 𝑣⟩ = ⟨(Base‘ndx), 𝐵⟩)
53	26	fveq2d 6886	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (+g‘(𝑟‘𝑥)) = (+g‘(𝑅‘𝑥)))
54	53	oveqd 7434	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))
55	32, 54	mpteq12dv 5196	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))
56	55	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥))))
57	39, 39, 56	mpoeq123dv 7492	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
58	57	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
59		prdsval.a	. . . . . . . . . . . 12 ⊢ (𝜑 → + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
60	59	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
61	58, 60	eqtr4d 2800	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥)))) = + )
62	61	opeq2d 4843	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩ = ⟨(+g‘ndx), + ⟩)
63	26	fveq2d 6886	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (.r‘(𝑟‘𝑥)) = (.r‘(𝑅‘𝑥)))
64	63	oveqd 7434	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))
65	32, 64	mpteq12dv 5196	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))
66	65	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥))))
67	39, 39, 66	mpoeq123dv 7492	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
68	67	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
69		prdsval.t	. . . . . . . . . . . 12 ⊢ (𝜑 → × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
70	69	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
71	68, 70	eqtr4d 2800	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥)))) = × )
72	71	opeq2d 4843	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩ = ⟨(.r‘ndx), × ⟩)
73	52, 62, 72	tpeq123d 4712	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩})
74		simp-4r 796	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → 𝑠 = 𝑆)
75	74	opeq2d 4843	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(Scalar‘ndx), 𝑠⟩ = ⟨(Scalar‘ndx), 𝑆⟩)
76		simpllr 788	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝑠 = 𝑆)
77	76	fveq2d 6886	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (Base‘𝑠) = (Base‘𝑆))
78		prdsval.k	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (Base‘𝑆)
79	77, 78	eqtr4di 2815	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (Base‘𝑠) = 𝐾)
80	26	fveq2d 6886	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ( ·𝑠 ‘(𝑟‘𝑥)) = ( ·𝑠 ‘(𝑅‘𝑥)))
81	80	oveqd 7434	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥)) = (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))
82	32, 81	mpteq12dv 5196	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))
83	82	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥))))
84	79, 39, 83	mpoeq123dv 7492	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))
85	84	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))
86		prdsval.m	. . . . . . . . . . . 12 ⊢ (𝜑 → · = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))
87	86	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → · = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))
88	85, 87	eqtr4d 2800	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥)))) = · )
89	88	opeq2d 4843	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩ = ⟨( ·𝑠 ‘ndx), · ⟩)
90	26	fveq2d 6886	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (·𝑖‘(𝑟‘𝑥)) = (·𝑖‘(𝑅‘𝑥)))
91	90	oveqd 7434	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))
92	32, 91	mpteq12dv 5196	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))
93	92	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))
94	76, 93	oveq12d 7435	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))) = (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))
95	39, 39, 94	mpoeq123dv 7492	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))
96	95	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))
97		prdsval.j	. . . . . . . . . . . 12 ⊢ (𝜑 → , = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))
98	97	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → , = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))
99	96, 98	eqtr4d 2800	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥))))) = , )
100	99	opeq2d 4843	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩ = ⟨(·𝑖‘ndx), , ⟩)
101	75, 89, 100	tpeq123d 4712	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩} = {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩})
102	73, 101	uneq12d 4119	. . . . . . 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 788	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → 𝑟 = 𝑅)
104	103	coeq2d 5846	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (TopOpen ∘ 𝑟) = (TopOpen ∘ 𝑅))
105	104	fveq2d 6886	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (∏t‘(TopOpen ∘ 𝑟)) = (∏t‘(TopOpen ∘ 𝑅)))
106		prdsval.o	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑂 = (∏t‘(TopOpen ∘ 𝑅)))
107	106	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → 𝑂 = (∏t‘(TopOpen ∘ 𝑅)))
108	105, 107	eqtr4d 2800	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (∏t‘(TopOpen ∘ 𝑟)) = 𝑂)
109	108	opeq2d 4843	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩ = ⟨(TopSet‘ndx), 𝑂⟩)
110	39	sseq2d 3966	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → ({𝑓, 𝑔} ⊆ 𝑣 ↔ {𝑓, 𝑔} ⊆ 𝐵))
111	26	fveq2d 6886	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (le‘(𝑟‘𝑥)) = (le‘(𝑅‘𝑥)))
112	111	breqd 5118	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥) ↔ (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥)))
113	32, 112	raleqbidv 3336	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥) ↔ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥)))
114	113	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥) ↔ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥)))
115	110, 114	anbi12d 644	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥)) ↔ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))))
116	115	opabbidv 5175	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))} = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})
117	116	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))} = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})
118		prdsval.l	. . . . . . . . . . . 12 ⊢ (𝜑 → ≤ = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})
119	118	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ≤ = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})
120	117, 119	eqtr4d 2800	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))} = ≤ )
121	120	opeq2d 4843	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩ = ⟨(le‘ndx), ≤ ⟩)
122	26	fveq2d 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (dist‘(𝑟‘𝑥)) = (dist‘(𝑅‘𝑥)))
123	122	oveqd 7434	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥)))
124	32, 123	mpteq12dv 5196	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))))
125	124	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))))
126	125	rneqd 5926	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) = ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))))
127	126	uneq1d 4117	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}) = (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}))
128	127	supeq1d 9420	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ) = sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))
129	39, 39, 128	mpoeq123dv 7492	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )))
130	129	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )))
131		prdsval.d	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )))
132	131	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )))
133	130, 132	eqtr4d 2800	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )) = 𝐷)
134	133	opeq2d 4843	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩ = ⟨(dist‘ndx), 𝐷⟩)
135	109, 121, 134	tpeq123d 4712	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} = {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩})
136		simpr 490	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ℎ = 𝐻)
137	136	opeq2d 4843	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(Hom ‘ndx), ℎ⟩ = ⟨(Hom ‘ndx), 𝐻⟩)
138	51	sqxpeqd 5691	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑣 × 𝑣) = (𝐵 × 𝐵))
139	136	oveqd 7434	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ((2nd ‘𝑎)ℎ𝑐) = ((2nd ‘𝑎)𝐻𝑐))
140	136	fveq1d 6884	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (ℎ‘𝑎) = (𝐻‘𝑎))
141	26	fveq2d 6886	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (comp‘(𝑟‘𝑥)) = (comp‘(𝑅‘𝑥)))
142	141	oveqd 7434	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥)) = (⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥)))
143	142	oveqd 7434	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)) = ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))
144	32, 143	mpteq12dv 5196	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))
145	144	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))
146	139, 140, 145	mpoeq123dv 7492	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))) = (𝑑 ∈ ((2nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))
147	138, 51, 146	mpoeq123dv 7492	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))) = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))))
148		prdsval.x	. . . . . . . . . . . 12 ⊢ (𝜑 → ∙ = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))))
149	148	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ∙ = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))))
150	147, 149	eqtr4d 2800	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))) = ∙ )
151	150	opeq2d 4843	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩ = ⟨(comp‘ndx), ∙ ⟩)
152	137, 151	preq12d 4705	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ ℎ = 𝐻) → {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩} = {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})
153	135, 152	uneq12d 4119	. . . . . . 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 4119	. . . . . 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 3887	. . . . 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 3887	. . . 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 472	. . 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 3476	. . 3 ⊢ (𝜑 → 𝑆 ∈ V)
160		prdsval.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑍)
161	160	elexd 3476	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
162		tpex 7751	. . . . . 6 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∈ V
163		tpex 7751	. . . . . 6 ⊢ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩} ∈ V
164	162, 163	unex 7750	. . . . 5 ⊢ ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∈ V
165		tpex 7751	. . . . . 6 ⊢ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∈ V
166		prex 5407	. . . . . 6 ⊢ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩} ∈ V
167	165, 166	unex 7750	. . . . 5 ⊢ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩}) ∈ V
168	164, 167	unex 7750	. . . 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 7569	. 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 2809	1 ⊢ (𝜑 → 𝑃 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3078  Vcvv 3453  ⦋csb 3850   ∪ cun 3900   ⊆ wss 3902  {csn 4587  {cpr 4589  {ctp 4591  ⟨cop 4593  ∪ cuni 4870  ∪ ciun 4954   class class class wbr 5107  {copab 5171   ↦ cmpt 5190   × cxp 5657  dom cdm 5659  ran crn 5660   ∘ ccom 5663  ‘cfv 6537  (class class class)co 7417   ∈ cmpo 7419  1^st c1st 7988  2^nd c2nd 7989   ↑_m cmap 8830  Xcixp 8908  supcsup 9414  0cc0 11128  ℝ^*cxr 11270   < clt 11271  ndxcnx 17291  Basecbs 17307  +_gcplusg 17348  ._rcmulr 17349  Scalarcsca 17351   ·_𝑠 cvsca 17352  ·_𝑖cip 17353  TopSetcts 17354  lecple 17355  distcds 17357  Hom chom 17359  compcco 17360  TopOpenctopn 17512  ∏_tcpt 17529   Σ_g cgsu 17531  X_scprds 17536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-cnex 11184  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7867  df-1st 7990  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-map 8832  df-ixp 8909  df-en 8957  df-dom 8958  df-sdom 8959  df-sup 9416  df-pnf 11273  df-mnf 11274  df-ltxr 11276  df-nn 12262  df-2 12331  df-3 12332  df-4 12333  df-5 12334  df-6 12335  df-7 12336  df-8 12337  df-9 12338  df-n0 12533  df-dec 12741  df-slot 17280  df-ndx 17292  df-base 17308  df-hom 17372  df-prds 17538

This theorem is used by:  prdssca  17547  prdsbas  17548  prdsplusg  17549  prdsmulr  17550  prdsvsca  17551  prdsip  17552  prdsle  17553  prdsds  17555  prdstset  17557  prdshom  17558  prdsco  17559