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

Theorem imasval 16379
Description: Value of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 6-Oct-2020.)
Hypotheses
Ref Expression
imasval.u (𝜑𝑈 = (𝐹s 𝑅))
imasval.v (𝜑𝑉 = (Base‘𝑅))
imasval.p + = (+g𝑅)
imasval.m × = (.r𝑅)
imasval.g 𝐺 = (Scalar‘𝑅)
imasval.k 𝐾 = (Base‘𝐺)
imasval.q · = ( ·𝑠𝑅)
imasval.i , = (·𝑖𝑅)
imasval.j 𝐽 = (TopOpen‘𝑅)
imasval.e 𝐸 = (dist‘𝑅)
imasval.n 𝑁 = (le‘𝑅)
imasval.a (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
imasval.t (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
imasval.s (𝜑 = 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
imasval.w (𝜑𝐼 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
imasval.o (𝜑𝑂 = (𝐽 qTop 𝐹))
imasval.d (𝜑𝐷 = (𝑥𝐵, 𝑦𝐵 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < )))
imasval.l (𝜑 = ((𝐹𝑁) ∘ 𝐹))
imasval.f (𝜑𝐹:𝑉onto𝐵)
imasval.r (𝜑𝑅𝑍)
Assertion
Ref Expression
imasval (𝜑𝑈 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩}))
Distinct variable groups:   𝑔,,𝑖,𝑛,𝑝,𝑞,𝑥,𝑦,𝐹   𝑅,𝑔,,𝑖,𝑛,𝑝,𝑞,𝑥,𝑦   ,𝑉,𝑝,𝑞   𝜑,𝑔,,𝑖,𝑛,𝑝,𝑞,𝑥,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   𝐷(𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   + (𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   (𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   (𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   · (𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   × (𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   (𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   𝑈(𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   𝐸(𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   𝐺(𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   , (𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   𝐼(𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   𝐽(𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   𝐾(𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   (𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   𝑁(𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   𝑂(𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)   𝑉(𝑥,𝑦,𝑔,𝑖,𝑛)   𝑍(𝑥,𝑦,𝑔,,𝑖,𝑛,𝑞,𝑝)

Proof of Theorem imasval
Dummy variables 𝑓 𝑟 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imasval.u . 2 (𝜑𝑈 = (𝐹s 𝑅))
2 df-imas 16376 . . . 4 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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}))
32a1i 11 . . 3 (𝜑 → “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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩})))
4 fvexd 6344 . . . 4 ((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) → (Base‘𝑟) ∈ V)
5 simplrl 762 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑓 = 𝐹)
65rneqd 5491 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = ran 𝐹)
7 imasval.f . . . . . . . . . . 11 (𝜑𝐹:𝑉onto𝐵)
8 forn 6259 . . . . . . . . . . 11 (𝐹:𝑉onto𝐵 → ran 𝐹 = 𝐵)
97, 8syl 17 . . . . . . . . . 10 (𝜑 → ran 𝐹 = 𝐵)
109ad2antrr 705 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝐹 = 𝐵)
116, 10eqtrd 2805 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = 𝐵)
1211opeq2d 4546 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Base‘ndx), ran 𝑓⟩ = ⟨(Base‘ndx), 𝐵⟩)
13 simplrr 763 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑟 = 𝑅)
1413fveq2d 6336 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘𝑟) = (Base‘𝑅))
15 simpr 471 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = (Base‘𝑟))
16 imasval.v . . . . . . . . . . . 12 (𝜑𝑉 = (Base‘𝑅))
1716ad2antrr 705 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑉 = (Base‘𝑅))
1814, 15, 173eqtr4d 2815 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = 𝑉)
195fveq1d 6334 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓𝑝) = (𝐹𝑝))
205fveq1d 6334 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓𝑞) = (𝐹𝑞))
2119, 20opeq12d 4547 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(𝑓𝑝), (𝑓𝑞)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩)
2213fveq2d 6336 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g𝑟) = (+g𝑅))
23 imasval.p . . . . . . . . . . . . . . . 16 + = (+g𝑅)
2422, 23syl6eqr 2823 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g𝑟) = + )
2524oveqd 6810 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(+g𝑟)𝑞) = (𝑝 + 𝑞))
265, 25fveq12d 6338 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(+g𝑟)𝑞)) = (𝐹‘(𝑝 + 𝑞)))
2721, 26opeq12d 4547 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩)
2827sneqd 4328 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
2918, 28iuneq12d 4680 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3018, 29iuneq12d 4680 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
31 imasval.a . . . . . . . . . 10 (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3231ad2antrr 705 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3330, 32eqtr4d 2808 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = )
3433opeq2d 4546 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩ = ⟨(+g‘ndx), ⟩)
3513fveq2d 6336 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r𝑟) = (.r𝑅))
36 imasval.m . . . . . . . . . . . . . . . 16 × = (.r𝑅)
3735, 36syl6eqr 2823 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r𝑟) = × )
3837oveqd 6810 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(.r𝑟)𝑞) = (𝑝 × 𝑞))
395, 38fveq12d 6338 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(.r𝑟)𝑞)) = (𝐹‘(𝑝 × 𝑞)))
4021, 39opeq12d 4547 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩)
4140sneqd 4328 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4218, 41iuneq12d 4680 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4318, 42iuneq12d 4680 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
44 imasval.t . . . . . . . . . 10 (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4544ad2antrr 705 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4643, 45eqtr4d 2808 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = )
4746opeq2d 4546 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩ = ⟨(.r‘ndx), ⟩)
4812, 34, 47tpeq123d 4419 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩})
4913fveq2d 6336 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Scalar‘𝑟) = (Scalar‘𝑅))
50 imasval.g . . . . . . . . 9 𝐺 = (Scalar‘𝑅)
5149, 50syl6eqr 2823 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Scalar‘𝑟) = 𝐺)
5251opeq2d 4546 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Scalar‘ndx), (Scalar‘𝑟)⟩ = ⟨(Scalar‘ndx), 𝐺⟩)
5351fveq2d 6336 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘(Scalar‘𝑟)) = (Base‘𝐺))
54 imasval.k . . . . . . . . . . . 12 𝐾 = (Base‘𝐺)
5553, 54syl6eqr 2823 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘(Scalar‘𝑟)) = 𝐾)
5620sneqd 4328 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {(𝑓𝑞)} = {(𝐹𝑞)})
5713fveq2d 6336 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ( ·𝑠𝑟) = ( ·𝑠𝑅))
58 imasval.q . . . . . . . . . . . . . 14 · = ( ·𝑠𝑅)
5957, 58syl6eqr 2823 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ( ·𝑠𝑟) = · )
6059oveqd 6810 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝( ·𝑠𝑟)𝑞) = (𝑝 · 𝑞))
615, 60fveq12d 6338 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝( ·𝑠𝑟)𝑞)) = (𝐹‘(𝑝 · 𝑞)))
6255, 56, 61mpt2eq123dv 6864 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))) = (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
6362iuneq2d 4681 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))) = 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
6418iuneq1d 4679 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))) = 𝑞𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))))
65 imasval.s . . . . . . . . . 10 (𝜑 = 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
6665ad2antrr 705 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
6763, 64, 663eqtr4d 2815 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))) = )
6867opeq2d 4546 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩ = ⟨( ·𝑠 ‘ndx), ⟩)
6913fveq2d 6336 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (·𝑖𝑟) = (·𝑖𝑅))
70 imasval.i . . . . . . . . . . . . . . 15 , = (·𝑖𝑅)
7169, 70syl6eqr 2823 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (·𝑖𝑟) = , )
7271oveqd 6810 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(·𝑖𝑟)𝑞) = (𝑝 , 𝑞))
7321, 72opeq12d 4547 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩)
7473sneqd 4328 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩} = {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
7518, 74iuneq12d 4680 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩} = 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
7618, 75iuneq12d 4680 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩} = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
77 imasval.w . . . . . . . . . 10 (𝜑𝐼 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
7877ad2antrr 705 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝐼 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
7976, 78eqtr4d 2808 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩} = 𝐼)
8079opeq2d 4546 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩ = ⟨(·𝑖‘ndx), 𝐼⟩)
8152, 68, 80tpeq123d 4419 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩} = {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})
8248, 81uneq12d 3919 . . . . 5 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ({⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩}) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}))
8313fveq2d 6336 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (TopOpen‘𝑟) = (TopOpen‘𝑅))
84 imasval.j . . . . . . . . . 10 𝐽 = (TopOpen‘𝑅)
8583, 84syl6eqr 2823 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (TopOpen‘𝑟) = 𝐽)
8685, 5oveq12d 6811 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((TopOpen‘𝑟) qTop 𝑓) = (𝐽 qTop 𝐹))
87 imasval.o . . . . . . . . 9 (𝜑𝑂 = (𝐽 qTop 𝐹))
8887ad2antrr 705 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑂 = (𝐽 qTop 𝐹))
8986, 88eqtr4d 2808 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((TopOpen‘𝑟) qTop 𝑓) = 𝑂)
9089opeq2d 4546 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩ = ⟨(TopSet‘ndx), 𝑂⟩)
9113fveq2d 6336 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (le‘𝑟) = (le‘𝑅))
92 imasval.n . . . . . . . . . . 11 𝑁 = (le‘𝑅)
9391, 92syl6eqr 2823 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (le‘𝑟) = 𝑁)
945, 93coeq12d 5425 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓 ∘ (le‘𝑟)) = (𝐹𝑁))
955cnveqd 5436 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑓 = 𝐹)
9694, 95coeq12d 5425 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓) = ((𝐹𝑁) ∘ 𝐹))
97 imasval.l . . . . . . . . 9 (𝜑 = ((𝐹𝑁) ∘ 𝐹))
9897ad2antrr 705 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = ((𝐹𝑁) ∘ 𝐹))
9996, 98eqtr4d 2808 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓) = )
10099opeq2d 4546 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)⟩ = ⟨(le‘ndx), ⟩)
10118sqxpeqd 5281 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑣 × 𝑣) = (𝑉 × 𝑉))
102101oveq1d 6808 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) = ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)))
1035fveq1d 6334 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(1st ‘(‘1))) = (𝐹‘(1st ‘(‘1))))
104103eqeq1d 2773 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(1st ‘(‘1))) = 𝑥 ↔ (𝐹‘(1st ‘(‘1))) = 𝑥))
1055fveq1d 6334 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(2nd ‘(𝑛))) = (𝐹‘(2nd ‘(𝑛))))
106105eqeq1d 2773 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(2nd ‘(𝑛))) = 𝑦 ↔ (𝐹‘(2nd ‘(𝑛))) = 𝑦))
1075fveq1d 6334 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(2nd ‘(𝑖))) = (𝐹‘(2nd ‘(𝑖))))
1085fveq1d 6334 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(1st ‘(‘(𝑖 + 1)))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))
109107, 108eqeq12d 2786 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1))))))
110109ralbidv 3135 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1))))))
111104, 106, 1103anbi123d 1547 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))))
112102, 111rabeqbidv 3345 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} = { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))})
11313fveq2d 6336 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (dist‘𝑟) = (dist‘𝑅))
114 imasval.e . . . . . . . . . . . . . . . 16 𝐸 = (dist‘𝑅)
115113, 114syl6eqr 2823 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (dist‘𝑟) = 𝐸)
116115coeq1d 5422 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((dist‘𝑟) ∘ 𝑔) = (𝐸𝑔))
117116oveq2d 6809 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)) = (ℝ*𝑠 Σg (𝐸𝑔)))
118112, 117mpteq12dv 4867 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))) = (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
119118rneqd 5491 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))) = ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
120119iuneq2d 4681 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))) = 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
121120infeq1d 8539 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ) = inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < ))
12211, 11, 121mpt2eq123dv 6864 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < )) = (𝑥𝐵, 𝑦𝐵 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < )))
123 imasval.d . . . . . . . . 9 (𝜑𝐷 = (𝑥𝐵, 𝑦𝐵 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < )))
124123ad2antrr 705 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝐷 = (𝑥𝐵, 𝑦𝐵 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < )))
125122, 124eqtr4d 2808 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < )) = 𝐷)
126125opeq2d 4546 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩ = ⟨(dist‘ndx), 𝐷⟩)
12790, 100, 126tpeq123d 4419 . . . . 5 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩, ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)⟩, ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩} = {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩})
12882, 127uneq12d 3919 . . . 4 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩}))
1294, 128csbied 3709 . . 3 ((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) → (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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩}))
130 fof 6256 . . . . 5 (𝐹:𝑉onto𝐵𝐹:𝑉𝐵)
1317, 130syl 17 . . . 4 (𝜑𝐹:𝑉𝐵)
132 fvex 6342 . . . . 5 (Base‘𝑅) ∈ V
13316, 132syl6eqel 2858 . . . 4 (𝜑𝑉 ∈ V)
134 fex 6633 . . . 4 ((𝐹:𝑉𝐵𝑉 ∈ V) → 𝐹 ∈ V)
135131, 133, 134syl2anc 573 . . 3 (𝜑𝐹 ∈ V)
136 imasval.r . . . 4 (𝜑𝑅𝑍)
137 elex 3364 . . . 4 (𝑅𝑍𝑅 ∈ V)
138136, 137syl 17 . . 3 (𝜑𝑅 ∈ V)
139 tpex 7104 . . . . . 6 {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∈ V
140 tpex 7104 . . . . . 6 {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩} ∈ V
141139, 140unex 7103 . . . . 5 ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∈ V
142 tpex 7104 . . . . 5 {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∈ V
143141, 142unex 7103 . . . 4 (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩}) ∈ V
144143a1i 11 . . 3 (𝜑 → (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩}) ∈ V)
1453, 129, 135, 138, 144ovmpt2d 6935 . 2 (𝜑 → (𝐹s 𝑅) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩}))
1461, 145eqtrd 2805 1 (𝜑𝑈 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071   = wceq 1631  wcel 2145  wral 3061  {crab 3065  Vcvv 3351  csb 3682  cun 3721  {csn 4316  {ctp 4320  cop 4322   ciun 4654  cmpt 4863   × cxp 5247  ccnv 5248  ran crn 5250  ccom 5253  wf 6027  ontowfo 6029  cfv 6031  (class class class)co 6793  cmpt2 6795  1st c1st 7313  2nd c2nd 7314  𝑚 cmap 8009  infcinf 8503  1c1 10139   + caddc 10141  *cxr 10275   < clt 10276  cmin 10468  cn 11222  ...cfz 12533  ndxcnx 16061  Basecbs 16064  +gcplusg 16149  .rcmulr 16150  Scalarcsca 16152   ·𝑠 cvsca 16153  ·𝑖cip 16154  TopSetcts 16155  lecple 16156  distcds 16158  TopOpenctopn 16290   Σg cgsu 16309  *𝑠cxrs 16368   qTop cqtop 16371  s cimas 16372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-sup 8504  df-inf 8505  df-imas 16376
This theorem is referenced by:  imasbas  16380  imasds  16381  imasplusg  16385  imasmulr  16386  imassca  16387  imasvsca  16388  imasip  16389  imastset  16390  imasle  16391
  Copyright terms: Public domain W3C validator