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 f must either be injective or satisfy the well-definedness condition f ( a ) = f ( c ) /\ f ( b ) = f ( d ) -> f ( a + b ) = f ( c + d ) for each relevant operation.
Note that although we call this an "image" by association to df-ima , in order to keep the definition simple we consider only the case when the domain of F is equal to the base set of R . Other cases can be achieved by restricting F (with df-res ) and/or R ( with df-ress ) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015) (Revised by AV, 6-Oct-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 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 ‘ 𝑟 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) ⟩ } ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cimas | ⊢ “s | |
| 1 | vf | ⊢ 𝑓 | |
| 2 | cvv | ⊢ V | |
| 3 | vr | ⊢ 𝑟 | |
| 4 | cbs | ⊢ Base | |
| 5 | 3 | cv | ⊢ 𝑟 |
| 6 | 5 4 | cfv | ⊢ ( Base ‘ 𝑟 ) |
| 7 | vv | ⊢ 𝑣 | |
| 8 | cnx | ⊢ ndx | |
| 9 | 8 4 | cfv | ⊢ ( Base ‘ ndx ) |
| 10 | 1 | cv | ⊢ 𝑓 |
| 11 | 10 | crn | ⊢ ran 𝑓 |
| 12 | 9 11 | cop | ⊢ ⟨ ( Base ‘ ndx ) , ran 𝑓 ⟩ |
| 13 | cplusg | ⊢ +g | |
| 14 | 8 13 | cfv | ⊢ ( +g ‘ ndx ) |
| 15 | vp | ⊢ 𝑝 | |
| 16 | 7 | cv | ⊢ 𝑣 |
| 17 | vq | ⊢ 𝑞 | |
| 18 | 15 | cv | ⊢ 𝑝 |
| 19 | 18 10 | cfv | ⊢ ( 𝑓 ‘ 𝑝 ) |
| 20 | 17 | cv | ⊢ 𝑞 |
| 21 | 20 10 | cfv | ⊢ ( 𝑓 ‘ 𝑞 ) |
| 22 | 19 21 | cop | ⊢ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ |
| 23 | 5 13 | cfv | ⊢ ( +g ‘ 𝑟 ) |
| 24 | 18 20 23 | co | ⊢ ( 𝑝 ( +g ‘ 𝑟 ) 𝑞 ) |
| 25 | 24 10 | cfv | ⊢ ( 𝑓 ‘ ( 𝑝 ( +g ‘ 𝑟 ) 𝑞 ) ) |
| 26 | 22 25 | cop | ⊢ ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑓 ‘ ( 𝑝 ( +g ‘ 𝑟 ) 𝑞 ) ) ⟩ |
| 27 | 26 | csn | ⊢ { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑓 ‘ ( 𝑝 ( +g ‘ 𝑟 ) 𝑞 ) ) ⟩ } |
| 28 | 17 16 27 | ciun | ⊢ ∪ 𝑞 ∈ 𝑣 { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑓 ‘ ( 𝑝 ( +g ‘ 𝑟 ) 𝑞 ) ) ⟩ } |
| 29 | 15 16 28 | ciun | ⊢ ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑓 ‘ ( 𝑝 ( +g ‘ 𝑟 ) 𝑞 ) ) ⟩ } |
| 30 | 14 29 | cop | ⊢ ⟨ ( +g ‘ ndx ) , ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑓 ‘ ( 𝑝 ( +g ‘ 𝑟 ) 𝑞 ) ) ⟩ } ⟩ |
| 31 | cmulr | ⊢ .r | |
| 32 | 8 31 | cfv | ⊢ ( .r ‘ ndx ) |
| 33 | 5 31 | cfv | ⊢ ( .r ‘ 𝑟 ) |
| 34 | 18 20 33 | co | ⊢ ( 𝑝 ( .r ‘ 𝑟 ) 𝑞 ) |
| 35 | 34 10 | cfv | ⊢ ( 𝑓 ‘ ( 𝑝 ( .r ‘ 𝑟 ) 𝑞 ) ) |
| 36 | 22 35 | cop | ⊢ ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑓 ‘ ( 𝑝 ( .r ‘ 𝑟 ) 𝑞 ) ) ⟩ |
| 37 | 36 | csn | ⊢ { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑓 ‘ ( 𝑝 ( .r ‘ 𝑟 ) 𝑞 ) ) ⟩ } |
| 38 | 17 16 37 | ciun | ⊢ ∪ 𝑞 ∈ 𝑣 { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑓 ‘ ( 𝑝 ( .r ‘ 𝑟 ) 𝑞 ) ) ⟩ } |
| 39 | 15 16 38 | ciun | ⊢ ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑓 ‘ ( 𝑝 ( .r ‘ 𝑟 ) 𝑞 ) ) ⟩ } |
| 40 | 32 39 | cop | ⊢ ⟨ ( .r ‘ ndx ) , ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑓 ‘ ( 𝑝 ( .r ‘ 𝑟 ) 𝑞 ) ) ⟩ } ⟩ |
| 41 | 12 30 40 | ctp | ⊢ { ⟨ ( Base ‘ ndx ) , ran 𝑓 ⟩ , ⟨ ( +g ‘ ndx ) , ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑓 ‘ ( 𝑝 ( +g ‘ 𝑟 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑓 ‘ ( 𝑝 ( .r ‘ 𝑟 ) 𝑞 ) ) ⟩ } ⟩ } |
| 42 | csca | ⊢ Scalar | |
| 43 | 8 42 | cfv | ⊢ ( Scalar ‘ ndx ) |
| 44 | 5 42 | cfv | ⊢ ( Scalar ‘ 𝑟 ) |
| 45 | 43 44 | cop | ⊢ ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ |
| 46 | cvsca | ⊢ ·𝑠 | |
| 47 | 8 46 | cfv | ⊢ ( ·𝑠 ‘ ndx ) |
| 48 | 44 4 | cfv | ⊢ ( Base ‘ ( Scalar ‘ 𝑟 ) ) |
| 49 | vx | ⊢ 𝑥 | |
| 50 | 21 | csn | ⊢ { ( 𝑓 ‘ 𝑞 ) } |
| 51 | 5 46 | cfv | ⊢ ( ·𝑠 ‘ 𝑟 ) |
| 52 | 18 20 51 | co | ⊢ ( 𝑝 ( ·𝑠 ‘ 𝑟 ) 𝑞 ) |
| 53 | 52 10 | cfv | ⊢ ( 𝑓 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑟 ) 𝑞 ) ) |
| 54 | 15 49 48 50 53 | cmpo | ⊢ ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑥 ∈ { ( 𝑓 ‘ 𝑞 ) } ↦ ( 𝑓 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑟 ) 𝑞 ) ) ) |
| 55 | 17 16 54 | ciun | ⊢ ∪ 𝑞 ∈ 𝑣 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑥 ∈ { ( 𝑓 ‘ 𝑞 ) } ↦ ( 𝑓 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑟 ) 𝑞 ) ) ) |
| 56 | 47 55 | cop | ⊢ ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑣 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑥 ∈ { ( 𝑓 ‘ 𝑞 ) } ↦ ( 𝑓 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑟 ) 𝑞 ) ) ) ⟩ |
| 57 | cip | ⊢ ·𝑖 | |
| 58 | 8 57 | cfv | ⊢ ( ·𝑖 ‘ ndx ) |
| 59 | 5 57 | cfv | ⊢ ( ·𝑖 ‘ 𝑟 ) |
| 60 | 18 20 59 | co | ⊢ ( 𝑝 ( ·𝑖 ‘ 𝑟 ) 𝑞 ) |
| 61 | 22 60 | cop | ⊢ ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑟 ) 𝑞 ) ⟩ |
| 62 | 61 | csn | ⊢ { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑟 ) 𝑞 ) ⟩ } |
| 63 | 17 16 62 | ciun | ⊢ ∪ 𝑞 ∈ 𝑣 { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑟 ) 𝑞 ) ⟩ } |
| 64 | 15 16 63 | ciun | ⊢ ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑟 ) 𝑞 ) ⟩ } |
| 65 | 58 64 | cop | ⊢ ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑟 ) 𝑞 ) ⟩ } ⟩ |
| 66 | 45 56 65 | ctp | ⊢ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑣 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑥 ∈ { ( 𝑓 ‘ 𝑞 ) } ↦ ( 𝑓 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑟 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑟 ) 𝑞 ) ⟩ } ⟩ } |
| 67 | 41 66 | cun | ⊢ ( { ⟨ ( Base ‘ ndx ) , ran 𝑓 ⟩ , ⟨ ( +g ‘ ndx ) , ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑓 ‘ ( 𝑝 ( +g ‘ 𝑟 ) 𝑞 ) ) ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑓 ‘ ( 𝑝 ( .r ‘ 𝑟 ) 𝑞 ) ) ⟩ } ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑣 ( 𝑝 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑥 ∈ { ( 𝑓 ‘ 𝑞 ) } ↦ ( 𝑓 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑟 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 { ⟨ ⟨ ( 𝑓 ‘ 𝑝 ) , ( 𝑓 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑟 ) 𝑞 ) ⟩ } ⟩ } ) |
| 68 | cts | ⊢ TopSet | |
| 69 | 8 68 | cfv | ⊢ ( TopSet ‘ ndx ) |
| 70 | ctopn | ⊢ TopOpen | |
| 71 | 5 70 | cfv | ⊢ ( TopOpen ‘ 𝑟 ) |
| 72 | cqtop | ⊢ qTop | |
| 73 | 71 10 72 | co | ⊢ ( ( TopOpen ‘ 𝑟 ) qTop 𝑓 ) |
| 74 | 69 73 | cop | ⊢ ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑟 ) qTop 𝑓 ) ⟩ |
| 75 | cple | ⊢ le | |
| 76 | 8 75 | cfv | ⊢ ( le ‘ ndx ) |
| 77 | 5 75 | cfv | ⊢ ( le ‘ 𝑟 ) |
| 78 | 10 77 | ccom | ⊢ ( 𝑓 ∘ ( le ‘ 𝑟 ) ) |
| 79 | 10 | ccnv | ⊢ ◡ 𝑓 |
| 80 | 78 79 | ccom | ⊢ ( ( 𝑓 ∘ ( le ‘ 𝑟 ) ) ∘ ◡ 𝑓 ) |
| 81 | 76 80 | cop | ⊢ ⟨ ( le ‘ ndx ) , ( ( 𝑓 ∘ ( le ‘ 𝑟 ) ) ∘ ◡ 𝑓 ) ⟩ |
| 82 | cds | ⊢ dist | |
| 83 | 8 82 | cfv | ⊢ ( dist ‘ ndx ) |
| 84 | vy | ⊢ 𝑦 | |
| 85 | vn | ⊢ 𝑛 | |
| 86 | cn | ⊢ ℕ | |
| 87 | vg | ⊢ 𝑔 | |
| 88 | vh | ⊢ ℎ | |
| 89 | 16 16 | cxp | ⊢ ( 𝑣 × 𝑣 ) |
| 90 | cmap | ⊢ ↑m | |
| 91 | c1 | ⊢ 1 | |
| 92 | cfz | ⊢ ... | |
| 93 | 85 | cv | ⊢ 𝑛 |
| 94 | 91 93 92 | co | ⊢ ( 1 ... 𝑛 ) |
| 95 | 89 94 90 | co | ⊢ ( ( 𝑣 × 𝑣 ) ↑m ( 1 ... 𝑛 ) ) |
| 96 | c1st | ⊢ 1st | |
| 97 | 88 | cv | ⊢ ℎ |
| 98 | 91 97 | cfv | ⊢ ( ℎ ‘ 1 ) |
| 99 | 98 96 | cfv | ⊢ ( 1st ‘ ( ℎ ‘ 1 ) ) |
| 100 | 99 10 | cfv | ⊢ ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) |
| 101 | 49 | cv | ⊢ 𝑥 |
| 102 | 100 101 | wceq | ⊢ ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 |
| 103 | c2nd | ⊢ 2nd | |
| 104 | 93 97 | cfv | ⊢ ( ℎ ‘ 𝑛 ) |
| 105 | 104 103 | cfv | ⊢ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) |
| 106 | 105 10 | cfv | ⊢ ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) |
| 107 | 84 | cv | ⊢ 𝑦 |
| 108 | 106 107 | wceq | ⊢ ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 |
| 109 | vi | ⊢ 𝑖 | |
| 110 | cmin | ⊢ − | |
| 111 | 93 91 110 | co | ⊢ ( 𝑛 − 1 ) |
| 112 | 91 111 92 | co | ⊢ ( 1 ... ( 𝑛 − 1 ) ) |
| 113 | 109 | cv | ⊢ 𝑖 |
| 114 | 113 97 | cfv | ⊢ ( ℎ ‘ 𝑖 ) |
| 115 | 114 103 | cfv | ⊢ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) |
| 116 | 115 10 | cfv | ⊢ ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) |
| 117 | caddc | ⊢ + | |
| 118 | 113 91 117 | co | ⊢ ( 𝑖 + 1 ) |
| 119 | 118 97 | cfv | ⊢ ( ℎ ‘ ( 𝑖 + 1 ) ) |
| 120 | 119 96 | cfv | ⊢ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) |
| 121 | 120 10 | cfv | ⊢ ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) |
| 122 | 116 121 | wceq | ⊢ ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) |
| 123 | 122 109 112 | wral | ⊢ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) |
| 124 | 102 108 123 | w3a | ⊢ ( ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) |
| 125 | 124 88 95 | crab | ⊢ { ℎ ∈ ( ( 𝑣 × 𝑣 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } |
| 126 | cxrs | ⊢ ℝ*𝑠 | |
| 127 | cgsu | ⊢ Σg | |
| 128 | 5 82 | cfv | ⊢ ( dist ‘ 𝑟 ) |
| 129 | 87 | cv | ⊢ 𝑔 |
| 130 | 128 129 | ccom | ⊢ ( ( dist ‘ 𝑟 ) ∘ 𝑔 ) |
| 131 | 126 130 127 | co | ⊢ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑟 ) ∘ 𝑔 ) ) |
| 132 | 87 125 131 | cmpt | ⊢ ( 𝑔 ∈ { ℎ ∈ ( ( 𝑣 × 𝑣 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑟 ) ∘ 𝑔 ) ) ) |
| 133 | 132 | crn | ⊢ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑣 × 𝑣 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑟 ) ∘ 𝑔 ) ) ) |
| 134 | 85 86 133 | ciun | ⊢ ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑣 × 𝑣 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑟 ) ∘ 𝑔 ) ) ) |
| 135 | cxr | ⊢ ℝ* | |
| 136 | clt | ⊢ < | |
| 137 | 134 135 136 | cinf | ⊢ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑣 × 𝑣 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑟 ) ∘ 𝑔 ) ) ) , ℝ* , < ) |
| 138 | 49 84 11 11 137 | cmpo | ⊢ ( 𝑥 ∈ ran 𝑓 , 𝑦 ∈ ran 𝑓 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑣 × 𝑣 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑟 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) |
| 139 | 83 138 | cop | ⊢ ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ran 𝑓 , 𝑦 ∈ ran 𝑓 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑣 × 𝑣 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝑓 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝑓 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑟 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) ⟩ |
| 140 | 74 81 139 | ctp | ⊢ { ⟨ ( 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 ‘ 𝑟 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) ⟩ } |
| 141 | 67 140 | cun | ⊢ ( ( { ⟨ ( 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 ‘ 𝑟 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) ⟩ } ) |
| 142 | 7 6 141 | csb | ⊢ ⦋ ( 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 ‘ 𝑟 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) ⟩ } ) |
| 143 | 1 3 2 2 142 | cmpo | ⊢ ( 𝑓 ∈ 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 ‘ 𝑟 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) ⟩ } ) ) |
| 144 | 0 143 | wceq | ⊢ “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 ‘ 𝑟 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) ⟩ } ) ) |