MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prdsval Structured version   Visualization version   GIF version

Theorem prdsval 16316
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.)
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.
StepHypRef Expression
1 prdsval.p . 2 𝑃 = (𝑆Xs𝑅)
2 df-prds 16309 . . . 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‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩})))
32a1i 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 3394 . . . . . . . . . . . 12 𝑟 ∈ V
54rnex 7326 . . . . . . . . . . 11 ran 𝑟 ∈ V
65uniex 7179 . . . . . . . . . 10 ran 𝑟 ∈ V
76rnex 7326 . . . . . . . . 9 ran ran 𝑟 ∈ V
87uniex 7179 . . . . . . . 8 ran ran 𝑟 ∈ V
9 baseid 16126 . . . . . . . . . . . 12 Base = Slot (Base‘ndx)
109strfvss 16087 . . . . . . . . . . 11 (Base‘(𝑟𝑥)) ⊆ ran (𝑟𝑥)
11 fvssunirn 6433 . . . . . . . . . . . 12 (𝑟𝑥) ⊆ ran 𝑟
12 rnss 5555 . . . . . . . . . . . 12 ((𝑟𝑥) ⊆ ran 𝑟 → ran (𝑟𝑥) ⊆ ran ran 𝑟)
13 uniss 4653 . . . . . . . . . . . 12 (ran (𝑟𝑥) ⊆ ran ran 𝑟 ran (𝑟𝑥) ⊆ ran ran 𝑟)
1411, 12, 13mp2b 10 . . . . . . . . . . 11 ran (𝑟𝑥) ⊆ ran ran 𝑟
1510, 14sstri 3807 . . . . . . . . . 10 (Base‘(𝑟𝑥)) ⊆ ran ran 𝑟
1615rgenw 3112 . . . . . . . . 9 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ran ran 𝑟
17 iunss 4753 . . . . . . . . 9 ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ran ran 𝑟 ↔ ∀𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ran ran 𝑟)
1816, 17mpbir 222 . . . . . . . 8 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ran ran 𝑟
198, 18ssexi 4998 . . . . . . 7 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∈ V
20 ixpssmap2g 8170 . . . . . . 7 ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∈ V → X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ↑𝑚 dom 𝑟))
2119, 20ax-mp 5 . . . . . 6 X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ↑𝑚 dom 𝑟)
22 ovex 6902 . . . . . . 7 ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ↑𝑚 dom 𝑟) ∈ V
2322ssex 4997 . . . . . 6 (X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ↑𝑚 dom 𝑟) → X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∈ V)
2421, 23mp1i 13 . . . . 5 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∈ V)
25 simpr 473 . . . . . . . . 9 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → 𝑟 = 𝑅)
2625fveq1d 6406 . . . . . . . 8 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑟𝑥) = (𝑅𝑥))
2726fveq2d 6408 . . . . . . 7 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (Base‘(𝑟𝑥)) = (Base‘(𝑅𝑥)))
2827ixpeq2dv 8157 . . . . . 6 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥𝐼 (Base‘(𝑟𝑥)) = X𝑥𝐼 (Base‘(𝑅𝑥)))
2925dmeqd 5527 . . . . . . . 8 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑟 = dom 𝑅)
30 prdsval.i . . . . . . . . 9 (𝜑 → dom 𝑅 = 𝐼)
3130ad2antrr 708 . . . . . . . 8 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑅 = 𝐼)
3229, 31eqtrd 2840 . . . . . . 7 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑟 = 𝐼)
3332ixpeq1d 8153 . . . . . 6 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) = X𝑥𝐼 (Base‘(𝑟𝑥)))
34 prdsval.b . . . . . . 7 (𝜑𝐵 = X𝑥𝐼 (Base‘(𝑅𝑥)))
3534ad2antrr 708 . . . . . 6 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → 𝐵 = X𝑥𝐼 (Base‘(𝑅𝑥)))
3628, 33, 353eqtr4d 2850 . . . . 5 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) = 𝐵)
37 ovssunirn 6905 . . . . . . . . . . . . . . 15 ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ ran (Hom ‘(𝑟𝑥))
38 df-hom 16173 . . . . . . . . . . . . . . . . . 18 Hom = Slot 14
3938strfvss 16087 . . . . . . . . . . . . . . . . 17 (Hom ‘(𝑟𝑥)) ⊆ ran (𝑟𝑥)
4039, 14sstri 3807 . . . . . . . . . . . . . . . 16 (Hom ‘(𝑟𝑥)) ⊆ ran ran 𝑟
41 rnss 5555 . . . . . . . . . . . . . . . 16 ((Hom ‘(𝑟𝑥)) ⊆ ran ran 𝑟 → ran (Hom ‘(𝑟𝑥)) ⊆ ran ran ran 𝑟)
42 uniss 4653 . . . . . . . . . . . . . . . 16 (ran (Hom ‘(𝑟𝑥)) ⊆ ran ran ran 𝑟 ran (Hom ‘(𝑟𝑥)) ⊆ ran ran ran 𝑟)
4340, 41, 42mp2b 10 . . . . . . . . . . . . . . 15 ran (Hom ‘(𝑟𝑥)) ⊆ ran ran ran 𝑟
4437, 43sstri 3807 . . . . . . . . . . . . . 14 ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ ran ran ran 𝑟
4544rgenw 3112 . . . . . . . . . . . . 13 𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ ran ran ran 𝑟
46 ss2ixp 8154 . . . . . . . . . . . . 13 (∀𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ ran ran ran 𝑟X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ X𝑥 ∈ dom 𝑟 ran ran ran 𝑟)
4745, 46ax-mp 5 . . . . . . . . . . . 12 X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ X𝑥 ∈ dom 𝑟 ran ran ran 𝑟
484dmex 7325 . . . . . . . . . . . . 13 dom 𝑟 ∈ V
498rnex 7326 . . . . . . . . . . . . . 14 ran ran ran 𝑟 ∈ V
5049uniex 7179 . . . . . . . . . . . . 13 ran ran ran 𝑟 ∈ V
5148, 50ixpconst 8151 . . . . . . . . . . . 12 X𝑥 ∈ dom 𝑟 ran ran ran 𝑟 = ( ran ran ran 𝑟𝑚 dom 𝑟)
5247, 51sseqtri 3834 . . . . . . . . . . 11 X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ ( ran ran ran 𝑟𝑚 dom 𝑟)
53 ovex 6902 . . . . . . . . . . . 12 ( ran ran ran 𝑟𝑚 dom 𝑟) ∈ V
5453elpw2 5020 . . . . . . . . . . 11 (X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ∈ 𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟) ↔ X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ ( ran ran ran 𝑟𝑚 dom 𝑟))
5552, 54mpbir 222 . . . . . . . . . 10 X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ∈ 𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟)
5655rgen2w 3113 . . . . . . . . 9 𝑓𝑣𝑔𝑣 X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ∈ 𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟)
57 eqid 2806 . . . . . . . . . 10 (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) = (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)))
5857fmpt2 7466 . . . . . . . . 9 (∀𝑓𝑣𝑔𝑣 X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ∈ 𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟) ↔ (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))):(𝑣 × 𝑣)⟶𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟))
5956, 58mpbi 221 . . . . . . . 8 (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))):(𝑣 × 𝑣)⟶𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟)
60 vex 3394 . . . . . . . . 9 𝑣 ∈ V
6160, 60xpex 7188 . . . . . . . 8 (𝑣 × 𝑣) ∈ V
6253pwex 5050 . . . . . . . 8 𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟) ∈ V
63 fex2 7347 . . . . . . . 8 (((𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))):(𝑣 × 𝑣)⟶𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟) ∧ (𝑣 × 𝑣) ∈ V ∧ 𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟) ∈ V) → (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) ∈ V)
6459, 61, 62, 63mp3an 1578 . . . . . . 7 (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) ∈ V
6564a1i 11 . . . . . 6 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) ∈ V)
66 simpr 473 . . . . . . . 8 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝑣 = 𝐵)
6732adantr 468 . . . . . . . . . 10 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → dom 𝑟 = 𝐼)
6867ixpeq1d 8153 . . . . . . . . 9 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) = X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)))
6926fveq2d 6408 . . . . . . . . . . . 12 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (Hom ‘(𝑟𝑥)) = (Hom ‘(𝑅𝑥)))
7069oveqd 6887 . . . . . . . . . . 11 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) = ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))
7170ixpeq2dv 8157 . . . . . . . . . 10 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) = X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))
7271adantr 468 . . . . . . . . 9 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) = X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))
7368, 72eqtrd 2840 . . . . . . . 8 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) = X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))
7466, 66, 73mpt2eq123dv 6943 . . . . . . 7 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) = (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))))
75 prdsval.h . . . . . . . 8 (𝜑𝐻 = (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))))
7675ad3antrrr 712 . . . . . . 7 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝐻 = (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))))
7774, 76eqtr4d 2843 . . . . . 6 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) = 𝐻)
78 simplr 776 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → 𝑣 = 𝐵)
7978opeq2d 4602 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(Base‘ndx), 𝑣⟩ = ⟨(Base‘ndx), 𝐵⟩)
8026fveq2d 6408 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (+g‘(𝑟𝑥)) = (+g‘(𝑅𝑥)))
8180oveqd 6887 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥)) = ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥)))
8232, 81mpteq12dv 4927 . . . . . . . . . . . . . 14 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥))))
8382adantr 468 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥))))
8466, 66, 83mpt2eq123dv 6943 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥)))))
8584adantr 468 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥)))))
86 prdsval.a . . . . . . . . . . . 12 (𝜑+ = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥)))))
8786ad4antr 715 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → + = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥)))))
8885, 87eqtr4d 2843 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥)))) = + )
8988opeq2d 4602 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(+g‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))))⟩ = ⟨(+g‘ndx), + ⟩)
9026fveq2d 6408 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (.r‘(𝑟𝑥)) = (.r‘(𝑅𝑥)))
9190oveqd 6887 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥)) = ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥)))
9232, 91mpteq12dv 4927 . . . . . . . . . . . . . 14 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥))))
9392adantr 468 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥))))
9466, 66, 93mpt2eq123dv 6943 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥)))))
9594adantr 468 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥)))))
96 prdsval.t . . . . . . . . . . . 12 (𝜑× = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥)))))
9796ad4antr 715 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → × = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥)))))
9895, 97eqtr4d 2843 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥)))) = × )
9998opeq2d 4602 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(.r‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))))⟩ = ⟨(.r‘ndx), × ⟩)
10079, 89, 99tpeq123d 4474 . . . . . . . 8 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))))⟩, ⟨(.r‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩})
101 simp-4r 794 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → 𝑠 = 𝑆)
102101opeq2d 4602 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(Scalar‘ndx), 𝑠⟩ = ⟨(Scalar‘ndx), 𝑆⟩)
103 simpllr 784 . . . . . . . . . . . . . . 15 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝑠 = 𝑆)
104103fveq2d 6408 . . . . . . . . . . . . . 14 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (Base‘𝑠) = (Base‘𝑆))
105 prdsval.k . . . . . . . . . . . . . 14 𝐾 = (Base‘𝑆)
106104, 105syl6eqr 2858 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (Base‘𝑠) = 𝐾)
10726fveq2d 6408 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ( ·𝑠 ‘(𝑟𝑥)) = ( ·𝑠 ‘(𝑅𝑥)))
108107oveqd 6887 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥)) = (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥)))
10932, 108mpteq12dv 4927 . . . . . . . . . . . . . 14 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥))))
110109adantr 468 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥))))
111106, 66, 110mpt2eq123dv 6943 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐾, 𝑔𝐵 ↦ (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥)))))
112111adantr 468 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐾, 𝑔𝐵 ↦ (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥)))))
113 prdsval.m . . . . . . . . . . . 12 (𝜑· = (𝑓𝐾, 𝑔𝐵 ↦ (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥)))))
114113ad4antr 715 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → · = (𝑓𝐾, 𝑔𝐵 ↦ (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥)))))
115112, 114eqtr4d 2843 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥)))) = · )
116115opeq2d 4602 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))))⟩ = ⟨( ·𝑠 ‘ndx), · ⟩)
11726fveq2d 6408 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (·𝑖‘(𝑟𝑥)) = (·𝑖‘(𝑅𝑥)))
118117oveqd 6887 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)) = ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥)))
11932, 118mpteq12dv 4927 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))
120119adantr 468 . . . . . . . . . . . . . 14 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))
121103, 120oveq12d 6888 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)))) = (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥)))))
12266, 66, 121mpt2eq123dv 6943 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))))
123122adantr 468 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))))
124 prdsval.j . . . . . . . . . . . 12 (𝜑, = (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))))
125124ad4antr 715 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → , = (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))))
126123, 125eqtr4d 2843 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))))) = , )
127126opeq2d 4602 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(·𝑖‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)))))⟩ = ⟨(·𝑖‘ndx), , ⟩)
128102, 116, 127tpeq123d 4474 . . . . . . . 8 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)))))⟩} = {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩})
129100, 128uneq12d 3967 . . . . . . 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), , ⟩}))
130 simpllr 784 . . . . . . . . . . . . 13 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → 𝑟 = 𝑅)
131130coeq2d 5486 . . . . . . . . . . . 12 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (TopOpen ∘ 𝑟) = (TopOpen ∘ 𝑅))
132131fveq2d 6408 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (∏t‘(TopOpen ∘ 𝑟)) = (∏t‘(TopOpen ∘ 𝑅)))
133 prdsval.o . . . . . . . . . . . 12 (𝜑𝑂 = (∏t‘(TopOpen ∘ 𝑅)))
134133ad4antr 715 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → 𝑂 = (∏t‘(TopOpen ∘ 𝑅)))
135132, 134eqtr4d 2843 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (∏t‘(TopOpen ∘ 𝑟)) = 𝑂)
136135opeq2d 4602 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩ = ⟨(TopSet‘ndx), 𝑂⟩)
13766sseq2d 3830 . . . . . . . . . . . . . 14 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → ({𝑓, 𝑔} ⊆ 𝑣 ↔ {𝑓, 𝑔} ⊆ 𝐵))
13826fveq2d 6408 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (le‘(𝑟𝑥)) = (le‘(𝑅𝑥)))
139138breqd 4855 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥) ↔ (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥)))
14032, 139raleqbidv 3341 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥) ↔ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥)))
141140adantr 468 . . . . . . . . . . . . . 14 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥) ↔ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥)))
142137, 141anbi12d 618 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥)) ↔ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥))))
143142opabbidv 4910 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))} = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥))})
144143adantr 468 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))} = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥))})
145 prdsval.l . . . . . . . . . . . 12 (𝜑 = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥))})
146145ad4antr 715 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥))})
147144, 146eqtr4d 2843 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))} = )
148147opeq2d 4602 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))}⟩ = ⟨(le‘ndx), ⟩)
14926fveq2d 6408 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (dist‘(𝑟𝑥)) = (dist‘(𝑅𝑥)))
150149oveqd 6887 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥)) = ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥)))
15132, 150mpteq12dv 4927 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))))
152151adantr 468 . . . . . . . . . . . . . . . 16 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))))
153152rneqd 5554 . . . . . . . . . . . . . . 15 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) = ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))))
154153uneq1d 3965 . . . . . . . . . . . . . 14 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}) = (ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}))
155154supeq1d 8587 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < ) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < ))
15666, 66, 155mpt2eq123dv 6943 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )) = (𝑓𝐵, 𝑔𝐵 ↦ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )))
157156adantr 468 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )) = (𝑓𝐵, 𝑔𝐵 ↦ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )))
158 prdsval.d . . . . . . . . . . . 12 (𝜑𝐷 = (𝑓𝐵, 𝑔𝐵 ↦ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )))
159158ad4antr 715 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → 𝐷 = (𝑓𝐵, 𝑔𝐵 ↦ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )))
160157, 159eqtr4d 2843 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )) = 𝐷)
161160opeq2d 4602 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(dist‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < ))⟩ = ⟨(dist‘ndx), 𝐷⟩)
162136, 148, 161tpeq123d 4474 . . . . . . . 8 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))}⟩, ⟨(dist‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < ))⟩} = {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩})
163 simpr 473 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → = 𝐻)
164163opeq2d 4602 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(Hom ‘ndx), ⟩ = ⟨(Hom ‘ndx), 𝐻⟩)
16578sqxpeqd 5342 . . . . . . . . . . . 12 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑣 × 𝑣) = (𝐵 × 𝐵))
166163oveqd 6887 . . . . . . . . . . . . 13 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑐(2nd𝑎)) = (𝑐𝐻(2nd𝑎)))
167163fveq1d 6406 . . . . . . . . . . . . 13 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑎) = (𝐻𝑎))
16826fveq2d 6408 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (comp‘(𝑟𝑥)) = (comp‘(𝑅𝑥)))
169168oveqd 6887 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥)) = (⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥)))
170169oveqd 6887 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)) = ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥)))
17132, 170mpteq12dv 4927 . . . . . . . . . . . . . 14 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥))) = (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))
172171ad2antrr 708 . . . . . . . . . . . . 13 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥))) = (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))
173166, 167, 172mpt2eq123dv 6943 . . . . . . . . . . . 12 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑑 ∈ (𝑐(2nd𝑎)), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))) = (𝑑 ∈ (𝑐𝐻(2nd𝑎)), 𝑒 ∈ (𝐻𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥)))))
174165, 78, 173mpt2eq123dv 6943 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑎 ∈ (𝑣 × 𝑣), 𝑐𝑣 ↦ (𝑑 ∈ (𝑐(2nd𝑎)), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥))))) = (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐𝐻(2nd𝑎)), 𝑒 ∈ (𝐻𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))))
175 prdsval.x . . . . . . . . . . . 12 (𝜑 = (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐𝐻(2nd𝑎)), 𝑒 ∈ (𝐻𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))))
176175ad4antr 715 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → = (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐𝐻(2nd𝑎)), 𝑒 ∈ (𝐻𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))))
177174, 176eqtr4d 2843 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑎 ∈ (𝑣 × 𝑣), 𝑐𝑣 ↦ (𝑑 ∈ (𝑐(2nd𝑎)), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥))))) = )
178177opeq2d 4602 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐𝑣 ↦ (𝑑 ∈ (𝑐(2nd𝑎)), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩ = ⟨(comp‘ndx), ⟩)
179164, 178preq12d 4467 . . . . . . . 8 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨(Hom ‘ndx), ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐𝑣 ↦ (𝑑 ∈ (𝑐(2nd𝑎)), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩} = {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩})
180162, 179uneq12d 3967 . . . . . . 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), ⟩}))
181129, 180uneq12d 3967 . . . . . 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), ⟩})))
18265, 77, 181csbied2 3756 . . . . 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), ⟩})))
18324, 36, 182csbied2 3756 . . . 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), ⟩})))
184183anasss 454 . . 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), ⟩})))
185 prdsval.s . . . 4 (𝜑𝑆𝑊)
186 elex 3406 . . . 4 (𝑆𝑊𝑆 ∈ V)
187185, 186syl 17 . . 3 (𝜑𝑆 ∈ V)
188 prdsval.r . . . 4 (𝜑𝑅𝑍)
189 elex 3406 . . . 4 (𝑅𝑍𝑅 ∈ V)
190188, 189syl 17 . . 3 (𝜑𝑅 ∈ V)
191 tpex 7183 . . . . . 6 {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∈ V
192 tpex 7183 . . . . . 6 {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩} ∈ V
193191, 192unex 7182 . . . . 5 ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∈ V
194 tpex 7183 . . . . . 6 {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∈ V
195 prex 5099 . . . . . 6 {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩} ∈ V
196194, 195unex 7182 . . . . 5 ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩}) ∈ V
197193, 196unex 7182 . . . 4 (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩})) ∈ V
198197a1i 11 . . 3 (𝜑 → (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩})) ∈ V)
1993, 184, 187, 190, 198ovmpt2d 7014 . 2 (𝜑 → (𝑆Xs𝑅) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩})))
2001, 199syl5eq 2852 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 setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2156  wral 3096  Vcvv 3391  csb 3728  cun 3767  wss 3769  𝒫 cpw 4351  {csn 4370  {cpr 4372  {ctp 4374  cop 4376   cuni 4630   ciun 4712   class class class wbr 4844  {copab 4906  cmpt 4923   × cxp 5309  dom cdm 5311  ran crn 5312  ccom 5315  wf 6093  cfv 6097  (class class class)co 6870  cmpt2 6872  1st c1st 7392  2nd c2nd 7393  𝑚 cmap 8088  Xcixp 8141  supcsup 8581  0cc0 10217  1c1 10218  *cxr 10354   < clt 10355  4c4 11354  cdc 11755  ndxcnx 16061  Basecbs 16064  +gcplusg 16149  .rcmulr 16150  Scalarcsca 16152   ·𝑠 cvsca 16153  ·𝑖cip 16154  TopSetcts 16155  lecple 16156  distcds 16158  Hom chom 16160  compcco 16161  TopOpenctopn 16283  tcpt 16300   Σg cgsu 16302  Xscprds 16307
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-i2m1 10285  ax-1ne0 10286  ax-rrecex 10289  ax-cnre 10290
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-om 7292  df-1st 7394  df-2nd 7395  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-map 8090  df-ixp 8142  df-sup 8583  df-nn 11302  df-ndx 16067  df-slot 16068  df-base 16070  df-hom 16173  df-prds 16309
This theorem is referenced by:  prdssca  16317  prdsbas  16318  prdsplusg  16319  prdsmulr  16320  prdsvsca  16321  prdsip  16322  prdsle  16323  prdsds  16325  prdstset  16327  prdshom  16328  prdsco  16329
  Copyright terms: Public domain W3C validator