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

Theorem prdsval 16723
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 16716 . . . 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 3447 . . . . . . . . . . . 12 𝑟 ∈ V
54rnex 7603 . . . . . . . . . . 11 ran 𝑟 ∈ V
65uniex 7451 . . . . . . . . . 10 ran 𝑟 ∈ V
76rnex 7603 . . . . . . . . 9 ran ran 𝑟 ∈ V
87uniex 7451 . . . . . . . 8 ran ran 𝑟 ∈ V
9 baseid 16538 . . . . . . . . . . . 12 Base = Slot (Base‘ndx)
109strfvss 16501 . . . . . . . . . . 11 (Base‘(𝑟𝑥)) ⊆ ran (𝑟𝑥)
11 fvssunirn 6678 . . . . . . . . . . . 12 (𝑟𝑥) ⊆ ran 𝑟
12 rnss 5777 . . . . . . . . . . . 12 ((𝑟𝑥) ⊆ ran 𝑟 → ran (𝑟𝑥) ⊆ ran ran 𝑟)
13 uniss 4811 . . . . . . . . . . . 12 (ran (𝑟𝑥) ⊆ ran ran 𝑟 ran (𝑟𝑥) ⊆ ran ran 𝑟)
1411, 12, 13mp2b 10 . . . . . . . . . . 11 ran (𝑟𝑥) ⊆ ran ran 𝑟
1510, 14sstri 3927 . . . . . . . . . 10 (Base‘(𝑟𝑥)) ⊆ ran ran 𝑟
1615rgenw 3121 . . . . . . . . 9 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ran ran 𝑟
17 iunss 4935 . . . . . . . . 9 ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ran ran 𝑟 ↔ ∀𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ran ran 𝑟)
1816, 17mpbir 234 . . . . . . . 8 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ran ran 𝑟
198, 18ssexi 5193 . . . . . . 7 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∈ V
20 ixpssmap2g 8478 . . . . . . 7 ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∈ V → X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ↑m dom 𝑟))
2119, 20ax-mp 5 . . . . . 6 X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ↑m dom 𝑟)
22 ovex 7172 . . . . . . 7 ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ↑m dom 𝑟) ∈ V
2322ssex 5192 . . . . . 6 (X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ⊆ ( 𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ↑m dom 𝑟) → X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∈ V)
2421, 23mp1i 13 . . . . 5 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) ∈ V)
25 simpr 488 . . . . . . . . 9 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → 𝑟 = 𝑅)
2625fveq1d 6651 . . . . . . . 8 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑟𝑥) = (𝑅𝑥))
2726fveq2d 6653 . . . . . . 7 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (Base‘(𝑟𝑥)) = (Base‘(𝑅𝑥)))
2827ixpeq2dv 8464 . . . . . 6 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥𝐼 (Base‘(𝑟𝑥)) = X𝑥𝐼 (Base‘(𝑅𝑥)))
2925dmeqd 5742 . . . . . . . 8 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑟 = dom 𝑅)
30 prdsval.i . . . . . . . . 9 (𝜑 → dom 𝑅 = 𝐼)
3130ad2antrr 725 . . . . . . . 8 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑅 = 𝐼)
3229, 31eqtrd 2836 . . . . . . 7 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → dom 𝑟 = 𝐼)
3332ixpeq1d 8460 . . . . . 6 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) = X𝑥𝐼 (Base‘(𝑟𝑥)))
34 prdsval.b . . . . . . 7 (𝜑𝐵 = X𝑥𝐼 (Base‘(𝑅𝑥)))
3534ad2antrr 725 . . . . . 6 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → 𝐵 = X𝑥𝐼 (Base‘(𝑅𝑥)))
3628, 33, 353eqtr4d 2846 . . . . 5 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥)) = 𝐵)
37 ovex 7172 . . . . . . . . . . 11 ( ran ran ran 𝑟m dom 𝑟) ∈ V
38 ovssunirn 7175 . . . . . . . . . . . . . . 15 ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ ran (Hom ‘(𝑟𝑥))
39 df-hom 16584 . . . . . . . . . . . . . . . . . 18 Hom = Slot 14
4039strfvss 16501 . . . . . . . . . . . . . . . . 17 (Hom ‘(𝑟𝑥)) ⊆ ran (𝑟𝑥)
4140, 14sstri 3927 . . . . . . . . . . . . . . . 16 (Hom ‘(𝑟𝑥)) ⊆ ran ran 𝑟
42 rnss 5777 . . . . . . . . . . . . . . . 16 ((Hom ‘(𝑟𝑥)) ⊆ ran ran 𝑟 → ran (Hom ‘(𝑟𝑥)) ⊆ ran ran ran 𝑟)
43 uniss 4811 . . . . . . . . . . . . . . . 16 (ran (Hom ‘(𝑟𝑥)) ⊆ ran ran ran 𝑟 ran (Hom ‘(𝑟𝑥)) ⊆ ran ran ran 𝑟)
4441, 42, 43mp2b 10 . . . . . . . . . . . . . . 15 ran (Hom ‘(𝑟𝑥)) ⊆ ran ran ran 𝑟
4538, 44sstri 3927 . . . . . . . . . . . . . 14 ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ ran ran ran 𝑟
4645rgenw 3121 . . . . . . . . . . . . 13 𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ ran ran ran 𝑟
47 ss2ixp 8461 . . . . . . . . . . . . 13 (∀𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ ran ran ran 𝑟X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ X𝑥 ∈ dom 𝑟 ran ran ran 𝑟)
4846, 47ax-mp 5 . . . . . . . . . . . 12 X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ X𝑥 ∈ dom 𝑟 ran ran ran 𝑟
494dmex 7602 . . . . . . . . . . . . 13 dom 𝑟 ∈ V
508rnex 7603 . . . . . . . . . . . . . 14 ran ran ran 𝑟 ∈ V
5150uniex 7451 . . . . . . . . . . . . 13 ran ran ran 𝑟 ∈ V
5249, 51ixpconst 8458 . . . . . . . . . . . 12 X𝑥 ∈ dom 𝑟 ran ran ran 𝑟 = ( ran ran ran 𝑟m dom 𝑟)
5348, 52sseqtri 3954 . . . . . . . . . . 11 X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ⊆ ( ran ran ran 𝑟m dom 𝑟)
5437, 53elpwi2 5216 . . . . . . . . . 10 X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ∈ 𝒫 ( ran ran ran 𝑟m dom 𝑟)
5554rgen2w 3122 . . . . . . . . 9 𝑓𝑣𝑔𝑣 X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ∈ 𝒫 ( ran ran ran 𝑟m dom 𝑟)
56 eqid 2801 . . . . . . . . . 10 (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) = (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)))
5756fmpo 7752 . . . . . . . . 9 (∀𝑓𝑣𝑔𝑣 X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) ∈ 𝒫 ( ran ran ran 𝑟m dom 𝑟) ↔ (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))):(𝑣 × 𝑣)⟶𝒫 ( ran ran ran 𝑟m dom 𝑟))
5855, 57mpbi 233 . . . . . . . 8 (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))):(𝑣 × 𝑣)⟶𝒫 ( ran ran ran 𝑟m dom 𝑟)
59 vex 3447 . . . . . . . . 9 𝑣 ∈ V
6059, 59xpex 7460 . . . . . . . 8 (𝑣 × 𝑣) ∈ V
6137pwex 5249 . . . . . . . 8 𝒫 ( ran ran ran 𝑟m dom 𝑟) ∈ V
62 fex2 7624 . . . . . . . 8 (((𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))):(𝑣 × 𝑣)⟶𝒫 ( ran ran ran 𝑟m dom 𝑟) ∧ (𝑣 × 𝑣) ∈ V ∧ 𝒫 ( ran ran ran 𝑟m dom 𝑟) ∈ V) → (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) ∈ V)
6358, 60, 61, 62mp3an 1458 . . . . . . 7 (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) ∈ V
6463a1i 11 . . . . . 6 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) ∈ V)
65 simpr 488 . . . . . . . 8 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝑣 = 𝐵)
6632adantr 484 . . . . . . . . . 10 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → dom 𝑟 = 𝐼)
6766ixpeq1d 8460 . . . . . . . . 9 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) = X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)))
6826fveq2d 6653 . . . . . . . . . . . 12 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (Hom ‘(𝑟𝑥)) = (Hom ‘(𝑅𝑥)))
6968oveqd 7156 . . . . . . . . . . 11 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) = ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))
7069ixpeq2dv 8464 . . . . . . . . . 10 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) = X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))
7170adantr 484 . . . . . . . . 9 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) = X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))
7267, 71eqtrd 2836 . . . . . . . 8 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)) = X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))
7365, 65, 72mpoeq123dv 7212 . . . . . . 7 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) = (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))))
74 prdsval.h . . . . . . . 8 (𝜑𝐻 = (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))))
7574ad3antrrr 729 . . . . . . 7 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝐻 = (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))))
7673, 75eqtr4d 2839 . . . . . 6 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))) = 𝐻)
77 simplr 768 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → 𝑣 = 𝐵)
7877opeq2d 4775 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(Base‘ndx), 𝑣⟩ = ⟨(Base‘ndx), 𝐵⟩)
7926fveq2d 6653 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (+g‘(𝑟𝑥)) = (+g‘(𝑅𝑥)))
8079oveqd 7156 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥)) = ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥)))
8132, 80mpteq12dv 5118 . . . . . . . . . . . . . 14 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥))))
8281adantr 484 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥))))
8365, 65, 82mpoeq123dv 7212 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥)))))
8483adantr 484 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥)))))
85 prdsval.a . . . . . . . . . . . 12 (𝜑+ = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥)))))
8685ad4antr 731 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → + = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥)))))
8784, 86eqtr4d 2839 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥)))) = + )
8887opeq2d 4775 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(+g‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))))⟩ = ⟨(+g‘ndx), + ⟩)
8926fveq2d 6653 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (.r‘(𝑟𝑥)) = (.r‘(𝑅𝑥)))
9089oveqd 7156 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥)) = ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥)))
9132, 90mpteq12dv 5118 . . . . . . . . . . . . . 14 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥))))
9291adantr 484 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥))))
9365, 65, 92mpoeq123dv 7212 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥)))))
9493adantr 484 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥)))))
95 prdsval.t . . . . . . . . . . . 12 (𝜑× = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥)))))
9695ad4antr 731 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → × = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥)))))
9794, 96eqtr4d 2839 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥)))) = × )
9897opeq2d 4775 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(.r‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))))⟩ = ⟨(.r‘ndx), × ⟩)
9978, 88, 98tpeq123d 4647 . . . . . . . 8 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))))⟩, ⟨(.r‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩})
100 simp-4r 783 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → 𝑠 = 𝑆)
101100opeq2d 4775 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(Scalar‘ndx), 𝑠⟩ = ⟨(Scalar‘ndx), 𝑆⟩)
102 simpllr 775 . . . . . . . . . . . . . . 15 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → 𝑠 = 𝑆)
103102fveq2d 6653 . . . . . . . . . . . . . 14 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (Base‘𝑠) = (Base‘𝑆))
104 prdsval.k . . . . . . . . . . . . . 14 𝐾 = (Base‘𝑆)
105103, 104eqtr4di 2854 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (Base‘𝑠) = 𝐾)
10626fveq2d 6653 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ( ·𝑠 ‘(𝑟𝑥)) = ( ·𝑠 ‘(𝑅𝑥)))
107106oveqd 7156 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥)) = (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥)))
10832, 107mpteq12dv 5118 . . . . . . . . . . . . . 14 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥))))
109108adantr 484 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥))))
110105, 65, 109mpoeq123dv 7212 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐾, 𝑔𝐵 ↦ (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥)))))
111110adantr 484 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥)))) = (𝑓𝐾, 𝑔𝐵 ↦ (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥)))))
112 prdsval.m . . . . . . . . . . . 12 (𝜑· = (𝑓𝐾, 𝑔𝐵 ↦ (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥)))))
113112ad4antr 731 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → · = (𝑓𝐾, 𝑔𝐵 ↦ (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥)))))
114111, 113eqtr4d 2839 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥)))) = · )
115114opeq2d 4775 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))))⟩ = ⟨( ·𝑠 ‘ndx), · ⟩)
11626fveq2d 6653 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (·𝑖‘(𝑟𝑥)) = (·𝑖‘(𝑅𝑥)))
117116oveqd 7156 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)) = ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥)))
11832, 117mpteq12dv 5118 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))
119118adantr 484 . . . . . . . . . . . . . 14 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))
120102, 119oveq12d 7157 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)))) = (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥)))))
12165, 65, 120mpoeq123dv 7212 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))))
122121adantr 484 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))))
123 prdsval.j . . . . . . . . . . . 12 (𝜑, = (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))))
124123ad4antr 731 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → , = (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))))
125122, 124eqtr4d 2839 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))))) = , )
126125opeq2d 4775 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(·𝑖‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)))))⟩ = ⟨(·𝑖‘ndx), , ⟩)
127101, 115, 126tpeq123d 4647 . . . . . . . 8 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)))))⟩} = {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩})
12899, 127uneq12d 4094 . . . . . . 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), , ⟩}))
129 simpllr 775 . . . . . . . . . . . . 13 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → 𝑟 = 𝑅)
130129coeq2d 5701 . . . . . . . . . . . 12 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (TopOpen ∘ 𝑟) = (TopOpen ∘ 𝑅))
131130fveq2d 6653 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (∏t‘(TopOpen ∘ 𝑟)) = (∏t‘(TopOpen ∘ 𝑅)))
132 prdsval.o . . . . . . . . . . . 12 (𝜑𝑂 = (∏t‘(TopOpen ∘ 𝑅)))
133132ad4antr 731 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → 𝑂 = (∏t‘(TopOpen ∘ 𝑅)))
134131, 133eqtr4d 2839 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (∏t‘(TopOpen ∘ 𝑟)) = 𝑂)
135134opeq2d 4775 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩ = ⟨(TopSet‘ndx), 𝑂⟩)
13665sseq2d 3950 . . . . . . . . . . . . . 14 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → ({𝑓, 𝑔} ⊆ 𝑣 ↔ {𝑓, 𝑔} ⊆ 𝐵))
13726fveq2d 6653 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (le‘(𝑟𝑥)) = (le‘(𝑅𝑥)))
138137breqd 5044 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥) ↔ (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥)))
13932, 138raleqbidv 3357 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥) ↔ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥)))
140139adantr 484 . . . . . . . . . . . . . 14 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥) ↔ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥)))
141136, 140anbi12d 633 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥)) ↔ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥))))
142141opabbidv 5099 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))} = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥))})
143142adantr 484 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))} = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥))})
144 prdsval.l . . . . . . . . . . . 12 (𝜑 = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥))})
145144ad4antr 731 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥))})
146143, 145eqtr4d 2839 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))} = )
147146opeq2d 4775 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))}⟩ = ⟨(le‘ndx), ⟩)
14826fveq2d 6653 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (dist‘(𝑟𝑥)) = (dist‘(𝑅𝑥)))
149148oveqd 7156 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥)) = ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥)))
15032, 149mpteq12dv 5118 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))))
151150adantr 484 . . . . . . . . . . . . . . . 16 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))))
152151rneqd 5776 . . . . . . . . . . . . . . 15 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) = ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))))
153152uneq1d 4092 . . . . . . . . . . . . . 14 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}) = (ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}))
154153supeq1d 8898 . . . . . . . . . . . . 13 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < ) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < ))
15565, 65, 154mpoeq123dv 7212 . . . . . . . . . . . 12 ((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) → (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )) = (𝑓𝐵, 𝑔𝐵 ↦ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )))
156155adantr 484 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )) = (𝑓𝐵, 𝑔𝐵 ↦ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )))
157 prdsval.d . . . . . . . . . . . 12 (𝜑𝐷 = (𝑓𝐵, 𝑔𝐵 ↦ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )))
158157ad4antr 731 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → 𝐷 = (𝑓𝐵, 𝑔𝐵 ↦ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )))
159156, 158eqtr4d 2839 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )) = 𝐷)
160159opeq2d 4775 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(dist‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < ))⟩ = ⟨(dist‘ndx), 𝐷⟩)
161135, 147, 160tpeq123d 4647 . . . . . . . 8 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))}⟩, ⟨(dist‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < ))⟩} = {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩})
162 simpr 488 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → = 𝐻)
163162opeq2d 4775 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(Hom ‘ndx), ⟩ = ⟨(Hom ‘ndx), 𝐻⟩)
16477sqxpeqd 5555 . . . . . . . . . . . 12 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑣 × 𝑣) = (𝐵 × 𝐵))
165162oveqd 7156 . . . . . . . . . . . . 13 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑐(2nd𝑎)) = (𝑐𝐻(2nd𝑎)))
166162fveq1d 6651 . . . . . . . . . . . . 13 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑎) = (𝐻𝑎))
16726fveq2d 6653 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (comp‘(𝑟𝑥)) = (comp‘(𝑅𝑥)))
168167oveqd 7156 . . . . . . . . . . . . . . . 16 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥)) = (⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥)))
169168oveqd 7156 . . . . . . . . . . . . . . 15 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)) = ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥)))
17032, 169mpteq12dv 5118 . . . . . . . . . . . . . 14 (((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) → (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥))) = (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))
171170ad2antrr 725 . . . . . . . . . . . . 13 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥))) = (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))
172165, 166, 171mpoeq123dv 7212 . . . . . . . . . . . 12 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑑 ∈ (𝑐(2nd𝑎)), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))) = (𝑑 ∈ (𝑐𝐻(2nd𝑎)), 𝑒 ∈ (𝐻𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥)))))
173164, 77, 172mpoeq123dv 7212 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑎 ∈ (𝑣 × 𝑣), 𝑐𝑣 ↦ (𝑑 ∈ (𝑐(2nd𝑎)), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥))))) = (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐𝐻(2nd𝑎)), 𝑒 ∈ (𝐻𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))))
174 prdsval.x . . . . . . . . . . . 12 (𝜑 = (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐𝐻(2nd𝑎)), 𝑒 ∈ (𝐻𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))))
175174ad4antr 731 . . . . . . . . . . 11 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → = (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐𝐻(2nd𝑎)), 𝑒 ∈ (𝐻𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))))
176173, 175eqtr4d 2839 . . . . . . . . . 10 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → (𝑎 ∈ (𝑣 × 𝑣), 𝑐𝑣 ↦ (𝑑 ∈ (𝑐(2nd𝑎)), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥))))) = )
177176opeq2d 4775 . . . . . . . . 9 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐𝑣 ↦ (𝑑 ∈ (𝑐(2nd𝑎)), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩ = ⟨(comp‘ndx), ⟩)
178163, 177preq12d 4640 . . . . . . . 8 (((((𝜑𝑠 = 𝑆) ∧ 𝑟 = 𝑅) ∧ 𝑣 = 𝐵) ∧ = 𝐻) → {⟨(Hom ‘ndx), ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐𝑣 ↦ (𝑑 ∈ (𝑐(2nd𝑎)), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩} = {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩})
179161, 178uneq12d 4094 . . . . . . 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), ⟩}))
180128, 179uneq12d 4094 . . . . . 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), ⟩})))
18164, 76, 180csbied2 3868 . . . . 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), ⟩})))
18224, 36, 181csbied2 3868 . . . 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), ⟩})))
183182anasss 470 . . 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), ⟩})))
184 prdsval.s . . . 4 (𝜑𝑆𝑊)
185184elexd 3464 . . 3 (𝜑𝑆 ∈ V)
186 prdsval.r . . . 4 (𝜑𝑅𝑍)
187186elexd 3464 . . 3 (𝜑𝑅 ∈ V)
188 tpex 7454 . . . . . 6 {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∈ V
189 tpex 7454 . . . . . 6 {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩} ∈ V
190188, 189unex 7453 . . . . 5 ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∈ V
191 tpex 7454 . . . . . 6 {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∈ V
192 prex 5301 . . . . . 6 {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩} ∈ V
193191, 192unex 7453 . . . . 5 ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩}) ∈ V
194190, 193unex 7453 . . . 4 (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩})) ∈ V
195194a1i 11 . . 3 (𝜑 → (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩})) ∈ V)
1963, 183, 185, 187, 195ovmpod 7285 . 2 (𝜑 → (𝑆Xs𝑅) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩})))
1971, 196syl5eq 2848 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 209  wa 399   = wceq 1538  wcel 2112  wral 3109  Vcvv 3444  csb 3831  cun 3882  wss 3884  𝒫 cpw 4500  {csn 4528  {cpr 4530  {ctp 4532  cop 4534   cuni 4803   ciun 4884   class class class wbr 5033  {copab 5095  cmpt 5113   × cxp 5521  dom cdm 5523  ran crn 5524  ccom 5527  wf 6324  cfv 6328  (class class class)co 7139  cmpo 7141  1st c1st 7673  2nd c2nd 7674  m cmap 8393  Xcixp 8448  supcsup 8892  0cc0 10530  1c1 10531  *cxr 10667   < clt 10668  4c4 11686  cdc 12090  ndxcnx 16475  Basecbs 16478  +gcplusg 16560  .rcmulr 16561  Scalarcsca 16563   ·𝑠 cvsca 16564  ·𝑖cip 16565  TopSetcts 16566  lecple 16567  distcds 16569  Hom chom 16571  compcco 16572  TopOpenctopn 16690  tcpt 16707   Σg cgsu 16709  Xscprds 16714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-1cn 10588  ax-addcl 10590
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-map 8395  df-ixp 8449  df-sup 8894  df-nn 11630  df-ndx 16481  df-slot 16482  df-base 16484  df-hom 16584  df-prds 16716
This theorem is referenced by:  prdssca  16724  prdsbas  16725  prdsplusg  16726  prdsmulr  16727  prdsvsca  16728  prdsip  16729  prdsle  16730  prdsds  16732  prdstset  16734  prdshom  16735  prdsco  16736
  Copyright terms: Public domain W3C validator