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

Definition df-prds 17167
Description: Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this is usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
Assertion
Ref Expression
df-prds 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‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩})))
Distinct variable group:   𝑎,𝑐,𝑑,𝑒,𝑓,𝑔,,𝑠,𝑟,𝑥,𝑣

Detailed syntax breakdown of Definition df-prds
StepHypRef Expression
1 cprds 17165 . 2 class Xs
2 vs . . 3 setvar 𝑠
3 vr . . 3 setvar 𝑟
4 cvv 3433 . . 3 class V
5 vv . . . 4 setvar 𝑣
6 vx . . . . 5 setvar 𝑥
73cv 1538 . . . . . 6 class 𝑟
87cdm 5590 . . . . 5 class dom 𝑟
96cv 1538 . . . . . . 7 class 𝑥
109, 7cfv 6437 . . . . . 6 class (𝑟𝑥)
11 cbs 16921 . . . . . 6 class Base
1210, 11cfv 6437 . . . . 5 class (Base‘(𝑟𝑥))
136, 8, 12cixp 8694 . . . 4 class X𝑥 ∈ dom 𝑟(Base‘(𝑟𝑥))
14 vh . . . . 5 setvar
15 vf . . . . . 6 setvar 𝑓
16 vg . . . . . 6 setvar 𝑔
175cv 1538 . . . . . 6 class 𝑣
1815cv 1538 . . . . . . . . 9 class 𝑓
199, 18cfv 6437 . . . . . . . 8 class (𝑓𝑥)
2016cv 1538 . . . . . . . . 9 class 𝑔
219, 20cfv 6437 . . . . . . . 8 class (𝑔𝑥)
22 chom 16982 . . . . . . . . 9 class Hom
2310, 22cfv 6437 . . . . . . . 8 class (Hom ‘(𝑟𝑥))
2419, 21, 23co 7284 . . . . . . 7 class ((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))
256, 8, 24cixp 8694 . . . . . 6 class X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥))
2615, 16, 17, 17, 25cmpo 7286 . . . . 5 class (𝑓𝑣, 𝑔𝑣X𝑥 ∈ dom 𝑟((𝑓𝑥)(Hom ‘(𝑟𝑥))(𝑔𝑥)))
27 cnx 16903 . . . . . . . . . 10 class ndx
2827, 11cfv 6437 . . . . . . . . 9 class (Base‘ndx)
2928, 17cop 4568 . . . . . . . 8 class ⟨(Base‘ndx), 𝑣
30 cplusg 16971 . . . . . . . . . 10 class +g
3127, 30cfv 6437 . . . . . . . . 9 class (+g‘ndx)
3210, 30cfv 6437 . . . . . . . . . . . 12 class (+g‘(𝑟𝑥))
3319, 21, 32co 7284 . . . . . . . . . . 11 class ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))
346, 8, 33cmpt 5158 . . . . . . . . . 10 class (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥)))
3515, 16, 17, 17, 34cmpo 7286 . . . . . . . . 9 class (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))))
3631, 35cop 4568 . . . . . . . 8 class ⟨(+g‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))))⟩
37 cmulr 16972 . . . . . . . . . 10 class .r
3827, 37cfv 6437 . . . . . . . . 9 class (.r‘ndx)
3910, 37cfv 6437 . . . . . . . . . . . 12 class (.r‘(𝑟𝑥))
4019, 21, 39co 7284 . . . . . . . . . . 11 class ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))
416, 8, 40cmpt 5158 . . . . . . . . . 10 class (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥)))
4215, 16, 17, 17, 41cmpo 7286 . . . . . . . . 9 class (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))))
4338, 42cop 4568 . . . . . . . 8 class ⟨(.r‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))))⟩
4429, 36, 43ctp 4566 . . . . . . 7 class {⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))))⟩, ⟨(.r‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))))⟩}
45 csca 16974 . . . . . . . . . 10 class Scalar
4627, 45cfv 6437 . . . . . . . . 9 class (Scalar‘ndx)
472cv 1538 . . . . . . . . 9 class 𝑠
4846, 47cop 4568 . . . . . . . 8 class ⟨(Scalar‘ndx), 𝑠
49 cvsca 16975 . . . . . . . . . 10 class ·𝑠
5027, 49cfv 6437 . . . . . . . . 9 class ( ·𝑠 ‘ndx)
5147, 11cfv 6437 . . . . . . . . . 10 class (Base‘𝑠)
5210, 49cfv 6437 . . . . . . . . . . . 12 class ( ·𝑠 ‘(𝑟𝑥))
5318, 21, 52co 7284 . . . . . . . . . . 11 class (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))
546, 8, 53cmpt 5158 . . . . . . . . . 10 class (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥)))
5515, 16, 51, 17, 54cmpo 7286 . . . . . . . . 9 class (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))))
5650, 55cop 4568 . . . . . . . 8 class ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))))⟩
57 cip 16976 . . . . . . . . . 10 class ·𝑖
5827, 57cfv 6437 . . . . . . . . 9 class (·𝑖‘ndx)
5910, 57cfv 6437 . . . . . . . . . . . . 13 class (·𝑖‘(𝑟𝑥))
6019, 21, 59co 7284 . . . . . . . . . . . 12 class ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))
616, 8, 60cmpt 5158 . . . . . . . . . . 11 class (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)))
62 cgsu 17160 . . . . . . . . . . 11 class Σg
6347, 61, 62co 7284 . . . . . . . . . 10 class (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥))))
6415, 16, 17, 17, 63cmpo 7286 . . . . . . . . 9 class (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)))))
6558, 64cop 4568 . . . . . . . 8 class ⟨(·𝑖‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)))))⟩
6648, 56, 65ctp 4566 . . . . . . 7 class {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)))))⟩}
6744, 66cun 3886 . . . . . 6 class ({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(+g‘(𝑟𝑥))(𝑔𝑥))))⟩, ⟨(.r‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(.r‘(𝑟𝑥))(𝑔𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟𝑥))(𝑔𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(·𝑖‘(𝑟𝑥))(𝑔𝑥)))))⟩})
68 cts 16977 . . . . . . . . . 10 class TopSet
6927, 68cfv 6437 . . . . . . . . 9 class (TopSet‘ndx)
70 ctopn 17141 . . . . . . . . . . 11 class TopOpen
7170, 7ccom 5594 . . . . . . . . . 10 class (TopOpen ∘ 𝑟)
72 cpt 17158 . . . . . . . . . 10 class t
7371, 72cfv 6437 . . . . . . . . 9 class (∏t‘(TopOpen ∘ 𝑟))
7469, 73cop 4568 . . . . . . . 8 class ⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩
75 cple 16978 . . . . . . . . . 10 class le
7627, 75cfv 6437 . . . . . . . . 9 class (le‘ndx)
7718, 20cpr 4564 . . . . . . . . . . . 12 class {𝑓, 𝑔}
7877, 17wss 3888 . . . . . . . . . . 11 wff {𝑓, 𝑔} ⊆ 𝑣
7910, 75cfv 6437 . . . . . . . . . . . . 13 class (le‘(𝑟𝑥))
8019, 21, 79wbr 5075 . . . . . . . . . . . 12 wff (𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥)
8180, 6, 8wral 3065 . . . . . . . . . . 11 wff 𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥)
8278, 81wa 396 . . . . . . . . . 10 wff ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))
8382, 15, 16copab 5137 . . . . . . . . 9 class {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))}
8476, 83cop 4568 . . . . . . . 8 class ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))}⟩
85 cds 16980 . . . . . . . . . 10 class dist
8627, 85cfv 6437 . . . . . . . . 9 class (dist‘ndx)
8710, 85cfv 6437 . . . . . . . . . . . . . . 15 class (dist‘(𝑟𝑥))
8819, 21, 87co 7284 . . . . . . . . . . . . . 14 class ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))
896, 8, 88cmpt 5158 . . . . . . . . . . . . 13 class (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥)))
9089crn 5591 . . . . . . . . . . . 12 class ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥)))
91 cc0 10880 . . . . . . . . . . . . 13 class 0
9291csn 4562 . . . . . . . . . . . 12 class {0}
9390, 92cun 3886 . . . . . . . . . . 11 class (ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0})
94 cxr 11017 . . . . . . . . . . 11 class *
95 clt 11018 . . . . . . . . . . 11 class <
9693, 94, 95csup 9208 . . . . . . . . . 10 class sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )
9715, 16, 17, 17, 96cmpo 7286 . . . . . . . . 9 class (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < ))
9886, 97cop 4568 . . . . . . . 8 class ⟨(dist‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < ))⟩
9974, 84, 98ctp 4566 . . . . . . 7 class {⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))}⟩, ⟨(dist‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < ))⟩}
10027, 22cfv 6437 . . . . . . . . 9 class (Hom ‘ndx)
10114cv 1538 . . . . . . . . 9 class
102100, 101cop 4568 . . . . . . . 8 class ⟨(Hom ‘ndx),
103 cco 16983 . . . . . . . . . 10 class comp
10427, 103cfv 6437 . . . . . . . . 9 class (comp‘ndx)
105 va . . . . . . . . . 10 setvar 𝑎
106 vc . . . . . . . . . 10 setvar 𝑐
10717, 17cxp 5588 . . . . . . . . . 10 class (𝑣 × 𝑣)
108 vd . . . . . . . . . . 11 setvar 𝑑
109 ve . . . . . . . . . . 11 setvar 𝑒
110105cv 1538 . . . . . . . . . . . . 13 class 𝑎
111 c2nd 7839 . . . . . . . . . . . . 13 class 2nd
112110, 111cfv 6437 . . . . . . . . . . . 12 class (2nd𝑎)
113106cv 1538 . . . . . . . . . . . 12 class 𝑐
114112, 113, 101co 7284 . . . . . . . . . . 11 class ((2nd𝑎)𝑐)
115110, 101cfv 6437 . . . . . . . . . . 11 class (𝑎)
116108cv 1538 . . . . . . . . . . . . . 14 class 𝑑
1179, 116cfv 6437 . . . . . . . . . . . . 13 class (𝑑𝑥)
118109cv 1538 . . . . . . . . . . . . . 14 class 𝑒
1199, 118cfv 6437 . . . . . . . . . . . . 13 class (𝑒𝑥)
120 c1st 7838 . . . . . . . . . . . . . . . . 17 class 1st
121110, 120cfv 6437 . . . . . . . . . . . . . . . 16 class (1st𝑎)
1229, 121cfv 6437 . . . . . . . . . . . . . . 15 class ((1st𝑎)‘𝑥)
1239, 112cfv 6437 . . . . . . . . . . . . . . 15 class ((2nd𝑎)‘𝑥)
124122, 123cop 4568 . . . . . . . . . . . . . 14 class ⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩
1259, 113cfv 6437 . . . . . . . . . . . . . 14 class (𝑐𝑥)
12610, 103cfv 6437 . . . . . . . . . . . . . 14 class (comp‘(𝑟𝑥))
127124, 125, 126co 7284 . . . . . . . . . . . . 13 class (⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))
128117, 119, 127co 7284 . . . . . . . . . . . 12 class ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥))
1296, 8, 128cmpt 5158 . . . . . . . . . . 11 class (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))
130108, 109, 114, 115, 129cmpo 7286 . . . . . . . . . 10 class (𝑑 ∈ ((2nd𝑎)𝑐), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥))))
131105, 106, 107, 17, 130cmpo 7286 . . . . . . . . 9 class (𝑎 ∈ (𝑣 × 𝑣), 𝑐𝑣 ↦ (𝑑 ∈ ((2nd𝑎)𝑐), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))
132104, 131cop 4568 . . . . . . . 8 class ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐𝑣 ↦ (𝑑 ∈ ((2nd𝑎)𝑐), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩
133102, 132cpr 4564 . . . . . . 7 class {⟨(Hom ‘ndx), ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐𝑣 ↦ (𝑑 ∈ ((2nd𝑎)𝑐), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩}
13499, 133cun 3886 . . . . . 6 class ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓𝑥)(le‘(𝑟𝑥))(𝑔𝑥))}⟩, ⟨(dist‘ndx), (𝑓𝑣, 𝑔𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓𝑥)(dist‘(𝑟𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐𝑣 ↦ (𝑑 ∈ ((2nd𝑎)𝑐), 𝑒 ∈ (𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩})
13567, 134cun 3886 . . . . 5 class (({⟨(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‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩}))
13614, 26, 135csb 3833 . . . 4 class (𝑓𝑣, 𝑔𝑣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‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩}))
1375, 13, 136csb 3833 . . 3 class 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‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩}))
1382, 3, 4, 4, 137cmpo 7286 . 2 class (𝑠 ∈ 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‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩})))
1391, 138wceq 1539 1 wff 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‘(𝑟𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩})))
Colors of variables: wff setvar class
This definition is referenced by:  reldmprds  17168  prdsval  17175
  Copyright terms: Public domain W3C validator