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

Definition df-imas 16776
 Description: Define an image structure, which takes a structure and a function on the base set, and maps all the operations via the function. For this to work properly 𝑓 must either be injective or satisfy the well-definedness condition 𝑓(𝑎) = 𝑓(𝑐) ∧ 𝑓(𝑏) = 𝑓(𝑑) → 𝑓(𝑎 + 𝑏) = 𝑓(𝑐 + 𝑑) for each relevant operation. Note that although we call this an "image" by association to df-ima 5533, in order to keep the definition simple we consider only the case when the domain of 𝐹 is equal to the base set of 𝑅. Other cases can be achieved by restricting 𝐹 (with df-res 5532) and/or 𝑅 ( with df-ress 16486) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by AV, 6-Oct-2020.)
Assertion
Ref Expression
df-imas s = (𝑓 ∈ V, 𝑟 ∈ V ↦ (Base‘𝑟) / 𝑣(({⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩}) ∪ {⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩, ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)⟩, ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}))
Distinct variable group:   𝑓,𝑔,,𝑖,𝑛,𝑝,𝑞,𝑟,𝑣,𝑥,𝑦

Detailed syntax breakdown of Definition df-imas
StepHypRef Expression
1 cimas 16772 . 2 class s
2 vf . . 3 setvar 𝑓
3 vr . . 3 setvar 𝑟
4 cvv 3441 . . 3 class V
5 vv . . . 4 setvar 𝑣
63cv 1537 . . . . 5 class 𝑟
7 cbs 16478 . . . . 5 class Base
86, 7cfv 6325 . . . 4 class (Base‘𝑟)
9 cnx 16475 . . . . . . . . 9 class ndx
109, 7cfv 6325 . . . . . . . 8 class (Base‘ndx)
112cv 1537 . . . . . . . . 9 class 𝑓
1211crn 5521 . . . . . . . 8 class ran 𝑓
1310, 12cop 4531 . . . . . . 7 class ⟨(Base‘ndx), ran 𝑓
14 cplusg 16560 . . . . . . . . 9 class +g
159, 14cfv 6325 . . . . . . . 8 class (+g‘ndx)
16 vp . . . . . . . . 9 setvar 𝑝
175cv 1537 . . . . . . . . 9 class 𝑣
18 vq . . . . . . . . . 10 setvar 𝑞
1916cv 1537 . . . . . . . . . . . . . 14 class 𝑝
2019, 11cfv 6325 . . . . . . . . . . . . 13 class (𝑓𝑝)
2118cv 1537 . . . . . . . . . . . . . 14 class 𝑞
2221, 11cfv 6325 . . . . . . . . . . . . 13 class (𝑓𝑞)
2320, 22cop 4531 . . . . . . . . . . . 12 class ⟨(𝑓𝑝), (𝑓𝑞)⟩
246, 14cfv 6325 . . . . . . . . . . . . . 14 class (+g𝑟)
2519, 21, 24co 7136 . . . . . . . . . . . . 13 class (𝑝(+g𝑟)𝑞)
2625, 11cfv 6325 . . . . . . . . . . . 12 class (𝑓‘(𝑝(+g𝑟)𝑞))
2723, 26cop 4531 . . . . . . . . . . 11 class ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩
2827csn 4525 . . . . . . . . . 10 class {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}
2918, 17, 28ciun 4882 . . . . . . . . 9 class 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}
3016, 17, 29ciun 4882 . . . . . . . 8 class 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}
3115, 30cop 4531 . . . . . . 7 class ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩
32 cmulr 16561 . . . . . . . . 9 class .r
339, 32cfv 6325 . . . . . . . 8 class (.r‘ndx)
346, 32cfv 6325 . . . . . . . . . . . . . 14 class (.r𝑟)
3519, 21, 34co 7136 . . . . . . . . . . . . 13 class (𝑝(.r𝑟)𝑞)
3635, 11cfv 6325 . . . . . . . . . . . 12 class (𝑓‘(𝑝(.r𝑟)𝑞))
3723, 36cop 4531 . . . . . . . . . . 11 class ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩
3837csn 4525 . . . . . . . . . 10 class {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}
3918, 17, 38ciun 4882 . . . . . . . . 9 class 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}
4016, 17, 39ciun 4882 . . . . . . . 8 class 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}
4133, 40cop 4531 . . . . . . 7 class ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩
4213, 31, 41ctp 4529 . . . . . 6 class {⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩}
43 csca 16563 . . . . . . . . 9 class Scalar
449, 43cfv 6325 . . . . . . . 8 class (Scalar‘ndx)
456, 43cfv 6325 . . . . . . . 8 class (Scalar‘𝑟)
4644, 45cop 4531 . . . . . . 7 class ⟨(Scalar‘ndx), (Scalar‘𝑟)⟩
47 cvsca 16564 . . . . . . . . 9 class ·𝑠
489, 47cfv 6325 . . . . . . . 8 class ( ·𝑠 ‘ndx)
49 vx . . . . . . . . . 10 setvar 𝑥
5045, 7cfv 6325 . . . . . . . . . 10 class (Base‘(Scalar‘𝑟))
5122csn 4525 . . . . . . . . . 10 class {(𝑓𝑞)}
526, 47cfv 6325 . . . . . . . . . . . 12 class ( ·𝑠𝑟)
5319, 21, 52co 7136 . . . . . . . . . . 11 class (𝑝( ·𝑠𝑟)𝑞)
5453, 11cfv 6325 . . . . . . . . . 10 class (𝑓‘(𝑝( ·𝑠𝑟)𝑞))
5516, 49, 50, 51, 54cmpo 7138 . . . . . . . . 9 class (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))
5618, 17, 55ciun 4882 . . . . . . . 8 class 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))
5748, 56cop 4531 . . . . . . 7 class ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩
58 cip 16565 . . . . . . . . 9 class ·𝑖
599, 58cfv 6325 . . . . . . . 8 class (·𝑖‘ndx)
606, 58cfv 6325 . . . . . . . . . . . . 13 class (·𝑖𝑟)
6119, 21, 60co 7136 . . . . . . . . . . . 12 class (𝑝(·𝑖𝑟)𝑞)
6223, 61cop 4531 . . . . . . . . . . 11 class ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩
6362csn 4525 . . . . . . . . . 10 class {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}
6418, 17, 63ciun 4882 . . . . . . . . 9 class 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}
6516, 17, 64ciun 4882 . . . . . . . 8 class 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}
6659, 65cop 4531 . . . . . . 7 class ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩
6746, 57, 66ctp 4529 . . . . . 6 class {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩}
6842, 67cun 3879 . . . . 5 class ({⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩})
69 cts 16566 . . . . . . . 8 class TopSet
709, 69cfv 6325 . . . . . . 7 class (TopSet‘ndx)
71 ctopn 16690 . . . . . . . . 9 class TopOpen
726, 71cfv 6325 . . . . . . . 8 class (TopOpen‘𝑟)
73 cqtop 16771 . . . . . . . 8 class qTop
7472, 11, 73co 7136 . . . . . . 7 class ((TopOpen‘𝑟) qTop 𝑓)
7570, 74cop 4531 . . . . . 6 class ⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩
76 cple 16567 . . . . . . . 8 class le
779, 76cfv 6325 . . . . . . 7 class (le‘ndx)
786, 76cfv 6325 . . . . . . . . 9 class (le‘𝑟)
7911, 78ccom 5524 . . . . . . . 8 class (𝑓 ∘ (le‘𝑟))
8011ccnv 5519 . . . . . . . 8 class 𝑓
8179, 80ccom 5524 . . . . . . 7 class ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)
8277, 81cop 4531 . . . . . 6 class ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)⟩
83 cds 16569 . . . . . . . 8 class dist
849, 83cfv 6325 . . . . . . 7 class (dist‘ndx)
85 vy . . . . . . . 8 setvar 𝑦
86 vn . . . . . . . . . 10 setvar 𝑛
87 cn 11628 . . . . . . . . . 10 class
88 vg . . . . . . . . . . . 12 setvar 𝑔
89 c1 10530 . . . . . . . . . . . . . . . . . 18 class 1
90 vh . . . . . . . . . . . . . . . . . . 19 setvar
9190cv 1537 . . . . . . . . . . . . . . . . . 18 class
9289, 91cfv 6325 . . . . . . . . . . . . . . . . 17 class (‘1)
93 c1st 7672 . . . . . . . . . . . . . . . . 17 class 1st
9492, 93cfv 6325 . . . . . . . . . . . . . . . 16 class (1st ‘(‘1))
9594, 11cfv 6325 . . . . . . . . . . . . . . 15 class (𝑓‘(1st ‘(‘1)))
9649cv 1537 . . . . . . . . . . . . . . 15 class 𝑥
9795, 96wceq 1538 . . . . . . . . . . . . . 14 wff (𝑓‘(1st ‘(‘1))) = 𝑥
9886cv 1537 . . . . . . . . . . . . . . . . . 18 class 𝑛
9998, 91cfv 6325 . . . . . . . . . . . . . . . . 17 class (𝑛)
100 c2nd 7673 . . . . . . . . . . . . . . . . 17 class 2nd
10199, 100cfv 6325 . . . . . . . . . . . . . . . 16 class (2nd ‘(𝑛))
102101, 11cfv 6325 . . . . . . . . . . . . . . 15 class (𝑓‘(2nd ‘(𝑛)))
10385cv 1537 . . . . . . . . . . . . . . 15 class 𝑦
104102, 103wceq 1538 . . . . . . . . . . . . . 14 wff (𝑓‘(2nd ‘(𝑛))) = 𝑦
105 vi . . . . . . . . . . . . . . . . . . . 20 setvar 𝑖
106105cv 1537 . . . . . . . . . . . . . . . . . . 19 class 𝑖
107106, 91cfv 6325 . . . . . . . . . . . . . . . . . 18 class (𝑖)
108107, 100cfv 6325 . . . . . . . . . . . . . . . . 17 class (2nd ‘(𝑖))
109108, 11cfv 6325 . . . . . . . . . . . . . . . 16 class (𝑓‘(2nd ‘(𝑖)))
110 caddc 10532 . . . . . . . . . . . . . . . . . . . 20 class +
111106, 89, 110co 7136 . . . . . . . . . . . . . . . . . . 19 class (𝑖 + 1)
112111, 91cfv 6325 . . . . . . . . . . . . . . . . . 18 class (‘(𝑖 + 1))
113112, 93cfv 6325 . . . . . . . . . . . . . . . . 17 class (1st ‘(‘(𝑖 + 1)))
114113, 11cfv 6325 . . . . . . . . . . . . . . . 16 class (𝑓‘(1st ‘(‘(𝑖 + 1))))
115109, 114wceq 1538 . . . . . . . . . . . . . . 15 wff (𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1))))
116 cmin 10862 . . . . . . . . . . . . . . . . 17 class
11798, 89, 116co 7136 . . . . . . . . . . . . . . . 16 class (𝑛 − 1)
118 cfz 12888 . . . . . . . . . . . . . . . 16 class ...
11989, 117, 118co 7136 . . . . . . . . . . . . . . 15 class (1...(𝑛 − 1))
120115, 105, 119wral 3106 . . . . . . . . . . . . . 14 wff 𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1))))
12197, 104, 120w3a 1084 . . . . . . . . . . . . 13 wff ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))
12217, 17cxp 5518 . . . . . . . . . . . . . 14 class (𝑣 × 𝑣)
12389, 98, 118co 7136 . . . . . . . . . . . . . 14 class (1...𝑛)
124 cmap 8392 . . . . . . . . . . . . . 14 class m
125122, 123, 124co 7136 . . . . . . . . . . . . 13 class ((𝑣 × 𝑣) ↑m (1...𝑛))
126121, 90, 125crab 3110 . . . . . . . . . . . 12 class { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))}
127 cxrs 16768 . . . . . . . . . . . . 13 class *𝑠
1286, 83cfv 6325 . . . . . . . . . . . . . 14 class (dist‘𝑟)
12988cv 1537 . . . . . . . . . . . . . 14 class 𝑔
130128, 129ccom 5524 . . . . . . . . . . . . 13 class ((dist‘𝑟) ∘ 𝑔)
131 cgsu 16709 . . . . . . . . . . . . 13 class Σg
132127, 130, 131co 7136 . . . . . . . . . . . 12 class (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))
13388, 126, 132cmpt 5111 . . . . . . . . . . 11 class (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)))
134133crn 5521 . . . . . . . . . 10 class ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)))
13586, 87, 134ciun 4882 . . . . . . . . 9 class 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)))
136 cxr 10666 . . . . . . . . 9 class *
137 clt 10667 . . . . . . . . 9 class <
138135, 136, 137cinf 8892 . . . . . . . 8 class inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < )
13949, 85, 12, 12, 138cmpo 7138 . . . . . . 7 class (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))
14084, 139cop 4531 . . . . . 6 class ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩
14175, 82, 140ctp 4529 . . . . 5 class {⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩, ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)⟩, ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}
14268, 141cun 3879 . . . 4 class (({⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩}) ∪ {⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩, ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)⟩, ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩})
1435, 8, 142csb 3828 . . 3 class (Base‘𝑟) / 𝑣(({⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩}) ∪ {⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩, ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)⟩, ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩})
1442, 3, 4, 4, 143cmpo 7138 . 2 class (𝑓 ∈ V, 𝑟 ∈ V ↦ (Base‘𝑟) / 𝑣(({⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩}) ∪ {⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩, ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)⟩, ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}))
1451, 144wceq 1538 1 wff s = (𝑓 ∈ V, 𝑟 ∈ V ↦ (Base‘𝑟) / 𝑣(({⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩}) ∪ {⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩, ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)⟩, ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}))
 Colors of variables: wff setvar class This definition is referenced by:  imasval  16779
 Copyright terms: Public domain W3C validator