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

Theorem prdsval 16313
 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 16306 . . . 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 3339 . . . . . . . . . . . 12 𝑟 ∈ V
54rnex 7261 . . . . . . . . . . 11 ran 𝑟 ∈ V
65uniex 7114 . . . . . . . . . 10 ran 𝑟 ∈ V
76rnex 7261 . . . . . . . . 9 ran ran 𝑟 ∈ V
87uniex 7114 . . . . . . . 8 ran ran 𝑟 ∈ V
9 baseid 16117 . . . . . . . . . . . 12 Base = Slot (Base‘ndx)
109strfvss 16078 . . . . . . . . . . 11 (Base‘(𝑟𝑥)) ⊆ ran (𝑟𝑥)
11 fvssunirn 6374 . . . . . . . . . . . 12 (𝑟𝑥) ⊆ ran 𝑟
12 rnss 5505 . . . . . . . . . . . 12 ((𝑟𝑥) ⊆ ran 𝑟 → ran (𝑟𝑥) ⊆ ran ran 𝑟)
13 uniss 4606 . . . . . . . . . . . 12 (ran (𝑟𝑥) ⊆ ran ran 𝑟 ran (𝑟𝑥) ⊆ ran ran 𝑟)
1411, 12, 13mp2b 10 . . . . . . . . . . 11 ran (𝑟𝑥) ⊆ ran ran 𝑟
1510, 14sstri 3749 . . . . . . . . . 10 (Base‘(𝑟𝑥)) ⊆ ran ran 𝑟
1615rgenw 3058 . . . . . . . . 9 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ran ran 𝑟
17 iunss 4709 . . . . . . . . 9 ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ran ran 𝑟 ↔ ∀𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ran ran 𝑟)
1816, 17mpbir 221 . . . . . . . 8 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ran ran 𝑟
198, 18ssexi 4951 . . . . . . 7 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∈ V
20 ixpssmap2g 8099 . . . . . . 7 ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∈ V → X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ↑𝑚 dom 𝑟))
2119, 20ax-mp 5 . . . . . 6 X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ↑𝑚 dom 𝑟)
22 ovex 6837 . . . . . . 7 ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ↑𝑚 dom 𝑟) ∈ V
2322ssex 4950 . . . . . 6 (X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ↑𝑚 dom 𝑟) → X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∈ V)
2421, 23mp1i 13 . . . . 5 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∈ V)
25 simpr 479 . . . . . . . . 9 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → 𝑟 = 𝑅)
2625fveq1d 6350 . . . . . . . 8 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑟𝑥) = (𝑅𝑥))
2726fveq2d 6352 . . . . . . 7 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (Base‘(𝑟𝑥)) = (Base‘(𝑅𝑥)))
2827ixpeq2dv 8086 . . . . . 6 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥𝐼 (Base‘(𝑟𝑥)) = X𝑥𝐼 (Base‘(𝑅𝑥)))
2925dmeqd 5477 . . . . . . . 8 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑟 = dom 𝑅)
30 prdsval.i . . . . . . . . 9 (𝜑 → dom 𝑅 = 𝐼)
3130ad2antrr 764 . . . . . . . 8 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑅 = 𝐼)
3229, 31eqtrd 2790 . . . . . . 7 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑟 = 𝐼)
3332ixpeq1d 8082 . . . . . 6 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) = X𝑥𝐼 (Base‘(𝑟𝑥)))
34 prdsval.b . . . . . . 7 (𝜑𝐵 = X𝑥𝐼 (Base‘(𝑅𝑥)))
3534ad2antrr 764 . . . . . 6 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → 𝐵 = X𝑥𝐼 (Base‘(𝑅𝑥)))
3628, 33, 353eqtr4d 2800 . . . . 5 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) = 𝐵)
37 ovssunirn 6840 . . . . . . . . . . . . . . 15 ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ ran (Hom ‘(𝑟𝑥))
38 df-hom 16164 . . . . . . . . . . . . . . . . . 18 Hom = Slot 14
3938strfvss 16078 . . . . . . . . . . . . . . . . 17 (Hom ‘(𝑟𝑥)) ⊆ ran (𝑟𝑥)
4039, 14sstri 3749 . . . . . . . . . . . . . . . 16 (Hom ‘(𝑟𝑥)) ⊆ ran ran 𝑟
41 rnss 5505 . . . . . . . . . . . . . . . 16 ((Hom ‘(𝑟𝑥)) ⊆ ran ran 𝑟 → ran (Hom ‘(𝑟𝑥)) ⊆ ran ran ran 𝑟)
42 uniss 4606 . . . . . . . . . . . . . . . 16 (ran (Hom ‘(𝑟𝑥)) ⊆ ran ran ran 𝑟 ran (Hom ‘(𝑟𝑥)) ⊆ ran ran ran 𝑟)
4340, 41, 42mp2b 10 . . . . . . . . . . . . . . 15 ran (Hom ‘(𝑟𝑥)) ⊆ ran ran ran 𝑟
4437, 43sstri 3749 . . . . . . . . . . . . . 14 ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ ran ran ran 𝑟
4544rgenw 3058 . . . . . . . . . . . . 13 𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ ran ran ran 𝑟
46 ss2ixp 8083 . . . . . . . . . . . . 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 7260 . . . . . . . . . . . . 13 dom 𝑟 ∈ V
498rnex 7261 . . . . . . . . . . . . . 14 ran ran ran 𝑟 ∈ V
5049uniex 7114 . . . . . . . . . . . . 13 ran ran ran 𝑟 ∈ V
5148, 50ixpconst 8080 . . . . . . . . . . . 12 X𝑥 ∈ dom 𝑟 ran ran ran 𝑟 = ( ran ran ran 𝑟𝑚 dom 𝑟)
5247, 51sseqtri 3774 . . . . . . . . . . 11 X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ ( ran ran ran 𝑟𝑚 dom 𝑟)
53 ovex 6837 . . . . . . . . . . . 12 ( ran ran ran 𝑟𝑚 dom 𝑟) ∈ V
5453elpw2 4973 . . . . . . . . . . 11 (X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ∈ 𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟) ↔ X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ ( ran ran ran 𝑟𝑚 dom 𝑟))
5552, 54mpbir 221 . . . . . . . . . 10 X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ∈ 𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟)
5655rgen2w 3059 . . . . . . . . 9 𝑓𝑣𝑔𝑣 X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ∈ 𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟)
57 eqid 2756 . . . . . . . . . 10 (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) = (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)))
5857fmpt2 7401 . . . . . . . . 9 (∀𝑓𝑣𝑔𝑣 X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ∈ 𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟) ↔ (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))):(𝑣 × 𝑣)⟶𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟))
5956, 58mpbi 220 . . . . . . . 8 (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))):(𝑣 × 𝑣)⟶𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟)
60 vex 3339 . . . . . . . . 9 𝑣 ∈ V
6160, 60xpex 7123 . . . . . . . 8 (𝑣 × 𝑣) ∈ V
6253pwex 4993 . . . . . . . 8 𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟) ∈ V
63 fex2 7282 . . . . . . . 8 (((𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))):(𝑣 × 𝑣)⟶𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟) ∧ (𝑣 × 𝑣) ∈ V ∧ 𝒫 ( ran ran ran 𝑟𝑚 dom 𝑟) ∈ V) → (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) ∈ V)
6459, 61, 62, 63mp3an 1569 . . . . . . 7 (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) ∈ V
6564a1i 11 . . . . . 6 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) ∈ V)
66 simpr 479 . . . . . . . 8 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝑣 = 𝐵)
6732adantr 472 . . . . . . . . . 10 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → dom 𝑟 = 𝐼)
6867ixpeq1d 8082 . . . . . . . . 9 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) = X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)))
6926fveq2d 6352 . . . . . . . . . . . 12 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (Hom ‘(𝑟𝑥)) = (Hom ‘(𝑅𝑥)))
7069oveqd 6826 . . . . . . . . . . 11 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) = ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))
7170ixpeq2dv 8086 . . . . . . . . . 10 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) = X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))
7271adantr 472 . . . . . . . . 9 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) = X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))
7368, 72eqtrd 2790 . . . . . . . 8 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) = X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))
7466, 66, 73mpt2eq123dv 6878 . . . . . . 7 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) = (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))))
75 prdsval.h . . . . . . . 8 (𝜑𝐻 = (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))))
7675ad3antrrr 768 . . . . . . 7 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝐻 = (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))))
7774, 76eqtr4d 2793 . . . . . 6 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) = 𝐻)
78 simplr 809 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → 𝑣 = 𝐵)
7978opeq2d 4556 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(Base‘ndx), 𝑣⟩ = ⟨(Base‘ndx), 𝐵⟩)
8026fveq2d 6352 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (+g‘(𝑟𝑥)) = (+g‘(𝑅𝑥)))
8180oveqd 6826 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥)) = ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥)))
8232, 81mpteq12dv 4881 . . . . . . . . . . . . . 14 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥))))
8382adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥))))
8466, 66, 83mpt2eq123dv 6878 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥)))))
8584adantr 472 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥)))))
86 prdsval.a . . . . . . . . . . . 12 (𝜑+ = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥)))))
8786ad4antr 771 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → + = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥)))))
8885, 87eqtr4d 2793 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥)))) = + )
8988opeq2d 4556 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(+g‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))))⟩ = ⟨(+g‘ndx), + ⟩)
9026fveq2d 6352 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (.r‘(𝑟𝑥)) = (.r‘(𝑅𝑥)))
9190oveqd 6826 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥)) = ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥)))
9232, 91mpteq12dv 4881 . . . . . . . . . . . . . 14 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥))))
9392adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥))))
9466, 66, 93mpt2eq123dv 6878 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥)))))
9594adantr 472 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥)))))
96 prdsval.t . . . . . . . . . . . 12 (𝜑× = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥)))))
9796ad4antr 771 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → × = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥)))))
9895, 97eqtr4d 2793 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥)))) = × )
9998opeq2d 4556 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(.r‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))))⟩ = ⟨(.r‘ndx), × ⟩)
10079, 89, 99tpeq123d 4423 . . . . . . . 8 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))))⟩, ⟨(.r‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩})
101 simp-4r 827 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → 𝑠 = 𝑆)
102101opeq2d 4556 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(Scalar‘ndx), 𝑠⟩ = ⟨(Scalar‘ndx), 𝑆⟩)
103 simpllr 817 . . . . . . . . . . . . . . 15 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝑠 = 𝑆)
104103fveq2d 6352 . . . . . . . . . . . . . 14 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (Base‘𝑠) = (Base‘𝑆))
105 prdsval.k . . . . . . . . . . . . . 14 𝐾 = (Base‘𝑆)
106104, 105syl6eqr 2808 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (Base‘𝑠) = 𝐾)
10726fveq2d 6352 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ( ·𝑠 ‘(𝑟𝑥)) = ( ·𝑠 ‘(𝑅𝑥)))
108107oveqd 6826 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥)) = (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥)))
10932, 108mpteq12dv 4881 . . . . . . . . . . . . . 14 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥))))
110109adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥))))
111106, 66, 110mpt2eq123dv 6878 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐾, 𝑔𝐵 ↦ (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥)))))
112111adantr 472 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐾, 𝑔𝐵 ↦ (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥)))))
113 prdsval.m . . . . . . . . . . . 12 (𝜑· = (𝑓𝐾, 𝑔𝐵 ↦ (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥)))))
114113ad4antr 771 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → · = (𝑓𝐾, 𝑔𝐵 ↦ (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥)))))
115112, 114eqtr4d 2793 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥)))) = · )
116115opeq2d 4556 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))))⟩ = ⟨( ·𝑠 ‘ndx), · ⟩)
11726fveq2d 6352 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (·𝑖‘(𝑟𝑥)) = (·𝑖‘(𝑅𝑥)))
118117oveqd 6826 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)) = ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥)))
11932, 118mpteq12dv 4881 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))
120119adantr 472 . . . . . . . . . . . . . 14 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))
121103, 120oveq12d 6827 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)))) = (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥)))))
12266, 66, 121mpt2eq123dv 6878 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))))
123122adantr 472 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))))
124 prdsval.j . . . . . . . . . . . 12 (𝜑, = (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))))
125124ad4antr 771 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → , = (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))))
126123, 125eqtr4d 2793 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))))) = , )
127126opeq2d 4556 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(·𝑖‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)))))⟩ = ⟨(·𝑖‘ndx), , ⟩)
128102, 116, 127tpeq123d 4423 . . . . . . . 8 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)))))⟩} = {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩})
129100, 128uneq12d 3907 . . . . . . 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 817 . . . . . . . . . . . . 13 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → 𝑟 = 𝑅)
131130coeq2d 5436 . . . . . . . . . . . 12 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (TopOpen ∘ 𝑟) = (TopOpen ∘ 𝑅))
132131fveq2d 6352 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (∏t‘(TopOpen ∘ 𝑟)) = (∏t‘(TopOpen ∘ 𝑅)))
133 prdsval.o . . . . . . . . . . . 12 (𝜑𝑂 = (∏t‘(TopOpen ∘ 𝑅)))
134133ad4antr 771 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → 𝑂 = (∏t‘(TopOpen ∘ 𝑅)))
135132, 134eqtr4d 2793 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (∏t‘(TopOpen ∘ 𝑟)) = 𝑂)
136135opeq2d 4556 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩ = ⟨(TopSet‘ndx), 𝑂⟩)
13766sseq2d 3770 . . . . . . . . . . . . . 14 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → ({𝑓, 𝑔} ⊆ 𝑣 ↔ {𝑓, 𝑔} ⊆ 𝐵))
13826fveq2d 6352 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (le‘(𝑟𝑥)) = (le‘(𝑅𝑥)))
139138breqd 4811 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥) ↔ (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥)))
14032, 139raleqbidv 3287 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥) ↔ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥)))
141140adantr 472 . . . . . . . . . . . . . 14 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥) ↔ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥)))
142137, 141anbi12d 749 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥)) ↔ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥))))
143142opabbidv 4864 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))} = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥))})
144143adantr 472 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))} = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥))})
145 prdsval.l . . . . . . . . . . . 12 (𝜑 = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥))})
146145ad4antr 771 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥))})
147144, 146eqtr4d 2793 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))} = )
148147opeq2d 4556 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))}⟩ = ⟨(le‘ndx), ⟩)
14926fveq2d 6352 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (dist‘(𝑟𝑥)) = (dist‘(𝑅𝑥)))
150149oveqd 6826 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥)) = ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥)))
15132, 150mpteq12dv 4881 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))))
152151adantr 472 . . . . . . . . . . . . . . . 16 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))))
153152rneqd 5504 . . . . . . . . . . . . . . 15 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) = ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))))
154153uneq1d 3905 . . . . . . . . . . . . . 14 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}) = (ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}))
155154supeq1d 8513 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < ) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < ))
15666, 66, 155mpt2eq123dv 6878 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )) = (𝑓𝐵, 𝑔𝐵 ↦ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )))
157156adantr 472 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )) = (𝑓𝐵, 𝑔𝐵 ↦ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )))
158 prdsval.d . . . . . . . . . . . 12 (𝜑𝐷 = (𝑓𝐵, 𝑔𝐵 ↦ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )))
159158ad4antr 771 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → 𝐷 = (𝑓𝐵, 𝑔𝐵 ↦ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )))
160157, 159eqtr4d 2793 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )) = 𝐷)
161160opeq2d 4556 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(dist‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < ))⟩ = ⟨(dist‘ndx), 𝐷⟩)
162136, 148, 161tpeq123d 4423 . . . . . . . 8 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))}⟩, ⟨(dist‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < ))⟩} = {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩})
163 simpr 479 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → = 𝐻)
164163opeq2d 4556 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(Hom ‘ndx), ⟩ = ⟨(Hom ‘ndx), 𝐻⟩)
16578sqxpeqd 5294 . . . . . . . . . . . 12 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑣 × 𝑣) = (𝐵 × 𝐵))
166163oveqd 6826 . . . . . . . . . . . . 13 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑐(2nd𝑎)) = (𝑐𝐻(2nd𝑎)))
167163fveq1d 6350 . . . . . . . . . . . . 13 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑎) = (𝐻𝑎))
16826fveq2d 6352 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (comp‘(𝑟𝑥)) = (comp‘(𝑅𝑥)))
169168oveqd 6826 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥)) = (⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥)))
170169oveqd 6826 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)) = ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥)))
17132, 170mpteq12dv 4881 . . . . . . . . . . . . . 14 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥))) = (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))
172171ad2antrr 764 . . . . . . . . . . . . 13 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥))) = (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))
173166, 167, 172mpt2eq123dv 6878 . . . . . . . . . . . 12 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑑 ∈ (𝑐(2nd𝑎)), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))) = (𝑑 ∈ (𝑐𝐻(2nd𝑎)), 𝑒 ∈ (𝐻𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥)))))
174165, 78, 173mpt2eq123dv 6878 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑎 ∈ (𝑣 × 𝑣), 𝑐𝑣 ↦ (𝑑 ∈ (𝑐(2nd𝑎)), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥))))) = (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐𝐻(2nd𝑎)), 𝑒 ∈ (𝐻𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))))
175 prdsval.x . . . . . . . . . . . 12 (𝜑 = (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐𝐻(2nd𝑎)), 𝑒 ∈ (𝐻𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))))
176175ad4antr 771 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → = (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐𝐻(2nd𝑎)), 𝑒 ∈ (𝐻𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))))
177174, 176eqtr4d 2793 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑎 ∈ (𝑣 × 𝑣), 𝑐𝑣 ↦ (𝑑 ∈ (𝑐(2nd𝑎)), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥))))) = )
178177opeq2d 4556 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐𝑣 ↦ (𝑑 ∈ (𝑐(2nd𝑎)), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩ = ⟨(comp‘ndx), ⟩)
179164, 178preq12d 4416 . . . . . . . 8 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨(Hom ‘ndx), ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐𝑣 ↦ (𝑑 ∈ (𝑐(2nd𝑎)), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩} = {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩})
180162, 179uneq12d 3907 . . . . . . 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 3907 . . . . . 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 3698 . . . . 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 3698 . . . 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 682 . . 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 3348 . . . 4 (𝑆𝑊𝑆 ∈ V)
187185, 186syl 17 . . 3 (𝜑𝑆 ∈ V)
188 prdsval.r . . . 4 (𝜑𝑅𝑍)
189 elex 3348 . . . 4 (𝑅𝑍𝑅 ∈ V)
190188, 189syl 17 . . 3 (𝜑𝑅 ∈ V)
191 tpex 7118 . . . . . 6 {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∈ V
192 tpex 7118 . . . . . 6 {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩} ∈ V
193191, 192unex 7117 . . . . 5 ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∈ V
194 tpex 7118 . . . . . 6 {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∈ V
195 prex 5054 . . . . . 6 {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩} ∈ V
196194, 195unex 7117 . . . . 5 ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩}) ∈ V
197193, 196unex 7117 . . . 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 6949 . 2 (𝜑 → (𝑆Xs𝑅) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩})))
2001, 199syl5eq 2802 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 196   ∧ wa 383   = wceq 1628   ∈ wcel 2135  ∀wral 3046  Vcvv 3336  ⦋csb 3670   ∪ cun 3709   ⊆ wss 3711  𝒫 cpw 4298  {csn 4317  {cpr 4319  {ctp 4321  ⟨cop 4323  ∪ cuni 4584  ∪ ciun 4668   class class class wbr 4800  {copab 4860   ↦ cmpt 4877   × cxp 5260  dom cdm 5262  ran crn 5263   ∘ ccom 5266  ⟶wf 6041  ‘cfv 6045  (class class class)co 6809   ↦ cmpt2 6811  1st c1st 7327  2nd c2nd 7328   ↑𝑚 cmap 8019  Xcixp 8070  supcsup 8507  0cc0 10124  1c1 10125  ℝ*cxr 10261   < clt 10262  4c4 11260  ;cdc 11681  ndxcnx 16052  Basecbs 16055  +gcplusg 16139  .rcmulr 16140  Scalarcsca 16142   ·𝑠 cvsca 16143  ·𝑖cip 16144  TopSetcts 16145  lecple 16146  distcds 16148  Hom chom 16150  compcco 16151  TopOpenctopn 16280  ∏tcpt 16297   Σg cgsu 16299  Xscprds 16304 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-cnex 10180  ax-resscn 10181  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-addrcl 10185  ax-mulcl 10186  ax-mulrcl 10187  ax-i2m1 10192  ax-1ne0 10193  ax-rrecex 10196  ax-cnre 10197 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-reu 3053  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-1st 7329  df-2nd 7330  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-map 8021  df-ixp 8071  df-sup 8509  df-nn 11209  df-ndx 16058  df-slot 16059  df-base 16061  df-hom 16164  df-prds 16306 This theorem is referenced by:  prdssca  16314  prdsbas  16315  prdsplusg  16316  prdsmulr  16317  prdsvsca  16318  prdsip  16319  prdsle  16320  prdsds  16322  prdstset  16324  prdshom  16325  prdsco  16326
 Copyright terms: Public domain W3C validator