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

Definition df-imas 17013
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 5564, 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 5563) and/or 𝑅 ( with df-ress 16785) 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 17009 . 2 class s
2 vf . . 3 setvar 𝑓
3 vr . . 3 setvar 𝑟
4 cvv 3408 . . 3 class V
5 vv . . . 4 setvar 𝑣
63cv 1542 . . . . 5 class 𝑟
7 cbs 16760 . . . . 5 class Base
86, 7cfv 6380 . . . 4 class (Base‘𝑟)
9 cnx 16744 . . . . . . . . 9 class ndx
109, 7cfv 6380 . . . . . . . 8 class (Base‘ndx)
112cv 1542 . . . . . . . . 9 class 𝑓
1211crn 5552 . . . . . . . 8 class ran 𝑓
1310, 12cop 4547 . . . . . . 7 class ⟨(Base‘ndx), ran 𝑓
14 cplusg 16802 . . . . . . . . 9 class +g
159, 14cfv 6380 . . . . . . . 8 class (+g‘ndx)
16 vp . . . . . . . . 9 setvar 𝑝
175cv 1542 . . . . . . . . 9 class 𝑣
18 vq . . . . . . . . . 10 setvar 𝑞
1916cv 1542 . . . . . . . . . . . . . 14 class 𝑝
2019, 11cfv 6380 . . . . . . . . . . . . 13 class (𝑓𝑝)
2118cv 1542 . . . . . . . . . . . . . 14 class 𝑞
2221, 11cfv 6380 . . . . . . . . . . . . 13 class (𝑓𝑞)
2320, 22cop 4547 . . . . . . . . . . . 12 class ⟨(𝑓𝑝), (𝑓𝑞)⟩
246, 14cfv 6380 . . . . . . . . . . . . . 14 class (+g𝑟)
2519, 21, 24co 7213 . . . . . . . . . . . . 13 class (𝑝(+g𝑟)𝑞)
2625, 11cfv 6380 . . . . . . . . . . . 12 class (𝑓‘(𝑝(+g𝑟)𝑞))
2723, 26cop 4547 . . . . . . . . . . 11 class ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩
2827csn 4541 . . . . . . . . . 10 class {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}
2918, 17, 28ciun 4904 . . . . . . . . 9 class 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}
3016, 17, 29ciun 4904 . . . . . . . 8 class 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}
3115, 30cop 4547 . . . . . . 7 class ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩
32 cmulr 16803 . . . . . . . . 9 class .r
339, 32cfv 6380 . . . . . . . 8 class (.r‘ndx)
346, 32cfv 6380 . . . . . . . . . . . . . 14 class (.r𝑟)
3519, 21, 34co 7213 . . . . . . . . . . . . 13 class (𝑝(.r𝑟)𝑞)
3635, 11cfv 6380 . . . . . . . . . . . 12 class (𝑓‘(𝑝(.r𝑟)𝑞))
3723, 36cop 4547 . . . . . . . . . . 11 class ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩
3837csn 4541 . . . . . . . . . 10 class {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}
3918, 17, 38ciun 4904 . . . . . . . . 9 class 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}
4016, 17, 39ciun 4904 . . . . . . . 8 class 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}
4133, 40cop 4547 . . . . . . 7 class ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩
4213, 31, 41ctp 4545 . . . . . 6 class {⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩}
43 csca 16805 . . . . . . . . 9 class Scalar
449, 43cfv 6380 . . . . . . . 8 class (Scalar‘ndx)
456, 43cfv 6380 . . . . . . . 8 class (Scalar‘𝑟)
4644, 45cop 4547 . . . . . . 7 class ⟨(Scalar‘ndx), (Scalar‘𝑟)⟩
47 cvsca 16806 . . . . . . . . 9 class ·𝑠
489, 47cfv 6380 . . . . . . . 8 class ( ·𝑠 ‘ndx)
49 vx . . . . . . . . . 10 setvar 𝑥
5045, 7cfv 6380 . . . . . . . . . 10 class (Base‘(Scalar‘𝑟))
5122csn 4541 . . . . . . . . . 10 class {(𝑓𝑞)}
526, 47cfv 6380 . . . . . . . . . . . 12 class ( ·𝑠𝑟)
5319, 21, 52co 7213 . . . . . . . . . . 11 class (𝑝( ·𝑠𝑟)𝑞)
5453, 11cfv 6380 . . . . . . . . . 10 class (𝑓‘(𝑝( ·𝑠𝑟)𝑞))
5516, 49, 50, 51, 54cmpo 7215 . . . . . . . . 9 class (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))
5618, 17, 55ciun 4904 . . . . . . . 8 class 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))
5748, 56cop 4547 . . . . . . 7 class ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩
58 cip 16807 . . . . . . . . 9 class ·𝑖
599, 58cfv 6380 . . . . . . . 8 class (·𝑖‘ndx)
606, 58cfv 6380 . . . . . . . . . . . . 13 class (·𝑖𝑟)
6119, 21, 60co 7213 . . . . . . . . . . . 12 class (𝑝(·𝑖𝑟)𝑞)
6223, 61cop 4547 . . . . . . . . . . 11 class ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩
6362csn 4541 . . . . . . . . . 10 class {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}
6418, 17, 63ciun 4904 . . . . . . . . 9 class 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}
6516, 17, 64ciun 4904 . . . . . . . 8 class 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}
6659, 65cop 4547 . . . . . . 7 class ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩
6746, 57, 66ctp 4545 . . . . . 6 class {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩}
6842, 67cun 3864 . . . . 5 class ({⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩})
69 cts 16808 . . . . . . . 8 class TopSet
709, 69cfv 6380 . . . . . . 7 class (TopSet‘ndx)
71 ctopn 16926 . . . . . . . . 9 class TopOpen
726, 71cfv 6380 . . . . . . . 8 class (TopOpen‘𝑟)
73 cqtop 17008 . . . . . . . 8 class qTop
7472, 11, 73co 7213 . . . . . . 7 class ((TopOpen‘𝑟) qTop 𝑓)
7570, 74cop 4547 . . . . . 6 class ⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩
76 cple 16809 . . . . . . . 8 class le
779, 76cfv 6380 . . . . . . 7 class (le‘ndx)
786, 76cfv 6380 . . . . . . . . 9 class (le‘𝑟)
7911, 78ccom 5555 . . . . . . . 8 class (𝑓 ∘ (le‘𝑟))
8011ccnv 5550 . . . . . . . 8 class 𝑓
8179, 80ccom 5555 . . . . . . 7 class ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)
8277, 81cop 4547 . . . . . 6 class ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)⟩
83 cds 16811 . . . . . . . 8 class dist
849, 83cfv 6380 . . . . . . 7 class (dist‘ndx)
85 vy . . . . . . . 8 setvar 𝑦
86 vn . . . . . . . . . 10 setvar 𝑛
87 cn 11830 . . . . . . . . . 10 class
88 vg . . . . . . . . . . . 12 setvar 𝑔
89 c1 10730 . . . . . . . . . . . . . . . . . 18 class 1
90 vh . . . . . . . . . . . . . . . . . . 19 setvar
9190cv 1542 . . . . . . . . . . . . . . . . . 18 class
9289, 91cfv 6380 . . . . . . . . . . . . . . . . 17 class (‘1)
93 c1st 7759 . . . . . . . . . . . . . . . . 17 class 1st
9492, 93cfv 6380 . . . . . . . . . . . . . . . 16 class (1st ‘(‘1))
9594, 11cfv 6380 . . . . . . . . . . . . . . 15 class (𝑓‘(1st ‘(‘1)))
9649cv 1542 . . . . . . . . . . . . . . 15 class 𝑥
9795, 96wceq 1543 . . . . . . . . . . . . . 14 wff (𝑓‘(1st ‘(‘1))) = 𝑥
9886cv 1542 . . . . . . . . . . . . . . . . . 18 class 𝑛
9998, 91cfv 6380 . . . . . . . . . . . . . . . . 17 class (𝑛)
100 c2nd 7760 . . . . . . . . . . . . . . . . 17 class 2nd
10199, 100cfv 6380 . . . . . . . . . . . . . . . 16 class (2nd ‘(𝑛))
102101, 11cfv 6380 . . . . . . . . . . . . . . 15 class (𝑓‘(2nd ‘(𝑛)))
10385cv 1542 . . . . . . . . . . . . . . 15 class 𝑦
104102, 103wceq 1543 . . . . . . . . . . . . . 14 wff (𝑓‘(2nd ‘(𝑛))) = 𝑦
105 vi . . . . . . . . . . . . . . . . . . . 20 setvar 𝑖
106105cv 1542 . . . . . . . . . . . . . . . . . . 19 class 𝑖
107106, 91cfv 6380 . . . . . . . . . . . . . . . . . 18 class (𝑖)
108107, 100cfv 6380 . . . . . . . . . . . . . . . . 17 class (2nd ‘(𝑖))
109108, 11cfv 6380 . . . . . . . . . . . . . . . 16 class (𝑓‘(2nd ‘(𝑖)))
110 caddc 10732 . . . . . . . . . . . . . . . . . . . 20 class +
111106, 89, 110co 7213 . . . . . . . . . . . . . . . . . . 19 class (𝑖 + 1)
112111, 91cfv 6380 . . . . . . . . . . . . . . . . . 18 class (‘(𝑖 + 1))
113112, 93cfv 6380 . . . . . . . . . . . . . . . . 17 class (1st ‘(‘(𝑖 + 1)))
114113, 11cfv 6380 . . . . . . . . . . . . . . . 16 class (𝑓‘(1st ‘(‘(𝑖 + 1))))
115109, 114wceq 1543 . . . . . . . . . . . . . . 15 wff (𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1))))
116 cmin 11062 . . . . . . . . . . . . . . . . 17 class
11798, 89, 116co 7213 . . . . . . . . . . . . . . . 16 class (𝑛 − 1)
118 cfz 13095 . . . . . . . . . . . . . . . 16 class ...
11989, 117, 118co 7213 . . . . . . . . . . . . . . 15 class (1...(𝑛 − 1))
120115, 105, 119wral 3061 . . . . . . . . . . . . . 14 wff 𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1))))
12197, 104, 120w3a 1089 . . . . . . . . . . . . 13 wff ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))
12217, 17cxp 5549 . . . . . . . . . . . . . 14 class (𝑣 × 𝑣)
12389, 98, 118co 7213 . . . . . . . . . . . . . 14 class (1...𝑛)
124 cmap 8508 . . . . . . . . . . . . . 14 class m
125122, 123, 124co 7213 . . . . . . . . . . . . 13 class ((𝑣 × 𝑣) ↑m (1...𝑛))
126121, 90, 125crab 3065 . . . . . . . . . . . 12 class { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))}
127 cxrs 17005 . . . . . . . . . . . . 13 class *𝑠
1286, 83cfv 6380 . . . . . . . . . . . . . 14 class (dist‘𝑟)
12988cv 1542 . . . . . . . . . . . . . 14 class 𝑔
130128, 129ccom 5555 . . . . . . . . . . . . 13 class ((dist‘𝑟) ∘ 𝑔)
131 cgsu 16945 . . . . . . . . . . . . 13 class Σg
132127, 130, 131co 7213 . . . . . . . . . . . 12 class (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))
13388, 126, 132cmpt 5135 . . . . . . . . . . 11 class (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)))
134133crn 5552 . . . . . . . . . 10 class ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)))
13586, 87, 134ciun 4904 . . . . . . . . 9 class 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)))
136 cxr 10866 . . . . . . . . 9 class *
137 clt 10867 . . . . . . . . 9 class <
138135, 136, 137cinf 9057 . . . . . . . 8 class inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < )
13949, 85, 12, 12, 138cmpo 7215 . . . . . . 7 class (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))
14084, 139cop 4547 . . . . . 6 class ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩
14175, 82, 140ctp 4545 . . . . 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 3864 . . . 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 3811 . . 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 7215 . 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 1543 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  17016
  Copyright terms: Public domain W3C validator