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

Theorem imasval 16393
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 16390 . . . 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 6365 . . . 4 ((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) → (Base‘𝑟) ∈ V)
5 simplrl 819 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑓 = 𝐹)
65rneqd 5508 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = ran 𝐹)
7 imasval.f . . . . . . . . . . 11 (𝜑𝐹:𝑉onto𝐵)
8 forn 6280 . . . . . . . . . . 11 (𝐹:𝑉onto𝐵 → ran 𝐹 = 𝐵)
97, 8syl 17 . . . . . . . . . 10 (𝜑 → ran 𝐹 = 𝐵)
109ad2antrr 764 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝐹 = 𝐵)
116, 10eqtrd 2794 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = 𝐵)
1211opeq2d 4560 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Base‘ndx), ran 𝑓⟩ = ⟨(Base‘ndx), 𝐵⟩)
13 simplrr 820 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑟 = 𝑅)
1413fveq2d 6357 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘𝑟) = (Base‘𝑅))
15 simpr 479 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = (Base‘𝑟))
16 imasval.v . . . . . . . . . . . 12 (𝜑𝑉 = (Base‘𝑅))
1716ad2antrr 764 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑉 = (Base‘𝑅))
1814, 15, 173eqtr4d 2804 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = 𝑉)
195fveq1d 6355 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓𝑝) = (𝐹𝑝))
205fveq1d 6355 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓𝑞) = (𝐹𝑞))
2119, 20opeq12d 4561 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(𝑓𝑝), (𝑓𝑞)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩)
2213fveq2d 6357 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g𝑟) = (+g𝑅))
23 imasval.p . . . . . . . . . . . . . . . 16 + = (+g𝑅)
2422, 23syl6eqr 2812 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g𝑟) = + )
2524oveqd 6831 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(+g𝑟)𝑞) = (𝑝 + 𝑞))
265, 25fveq12d 6359 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(+g𝑟)𝑞)) = (𝐹‘(𝑝 + 𝑞)))
2721, 26opeq12d 4561 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩)
2827sneqd 4333 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
2918, 28iuneq12d 4698 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3018, 29iuneq12d 4698 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
31 imasval.a . . . . . . . . . 10 (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3231ad2antrr 764 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3330, 32eqtr4d 2797 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = )
3433opeq2d 4560 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩ = ⟨(+g‘ndx), ⟩)
3513fveq2d 6357 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r𝑟) = (.r𝑅))
36 imasval.m . . . . . . . . . . . . . . . 16 × = (.r𝑅)
3735, 36syl6eqr 2812 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r𝑟) = × )
3837oveqd 6831 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(.r𝑟)𝑞) = (𝑝 × 𝑞))
395, 38fveq12d 6359 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(.r𝑟)𝑞)) = (𝐹‘(𝑝 × 𝑞)))
4021, 39opeq12d 4561 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩)
4140sneqd 4333 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4218, 41iuneq12d 4698 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4318, 42iuneq12d 4698 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
44 imasval.t . . . . . . . . . 10 (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4544ad2antrr 764 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4643, 45eqtr4d 2797 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = )
4746opeq2d 4560 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩ = ⟨(.r‘ndx), ⟩)
4812, 34, 47tpeq123d 4427 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩})
4913fveq2d 6357 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Scalar‘𝑟) = (Scalar‘𝑅))
50 imasval.g . . . . . . . . 9 𝐺 = (Scalar‘𝑅)
5149, 50syl6eqr 2812 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Scalar‘𝑟) = 𝐺)
5251opeq2d 4560 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Scalar‘ndx), (Scalar‘𝑟)⟩ = ⟨(Scalar‘ndx), 𝐺⟩)
5351fveq2d 6357 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘(Scalar‘𝑟)) = (Base‘𝐺))
54 imasval.k . . . . . . . . . . . 12 𝐾 = (Base‘𝐺)
5553, 54syl6eqr 2812 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘(Scalar‘𝑟)) = 𝐾)
5620sneqd 4333 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {(𝑓𝑞)} = {(𝐹𝑞)})
5713fveq2d 6357 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ( ·𝑠𝑟) = ( ·𝑠𝑅))
58 imasval.q . . . . . . . . . . . . . 14 · = ( ·𝑠𝑅)
5957, 58syl6eqr 2812 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ( ·𝑠𝑟) = · )
6059oveqd 6831 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝( ·𝑠𝑟)𝑞) = (𝑝 · 𝑞))
615, 60fveq12d 6359 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝( ·𝑠𝑟)𝑞)) = (𝐹‘(𝑝 · 𝑞)))
6255, 56, 61mpt2eq123dv 6883 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))) = (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
6362iuneq2d 4699 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))) = 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
6418iuneq1d 4697 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))) = 𝑞𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))))
65 imasval.s . . . . . . . . . 10 (𝜑 = 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
6665ad2antrr 764 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
6763, 64, 663eqtr4d 2804 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))) = )
6867opeq2d 4560 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩ = ⟨( ·𝑠 ‘ndx), ⟩)
6913fveq2d 6357 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (·𝑖𝑟) = (·𝑖𝑅))
70 imasval.i . . . . . . . . . . . . . . 15 , = (·𝑖𝑅)
7169, 70syl6eqr 2812 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (·𝑖𝑟) = , )
7271oveqd 6831 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(·𝑖𝑟)𝑞) = (𝑝 , 𝑞))
7321, 72opeq12d 4561 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩)
7473sneqd 4333 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩} = {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
7518, 74iuneq12d 4698 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩} = 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
7618, 75iuneq12d 4698 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩} = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
77 imasval.w . . . . . . . . . 10 (𝜑𝐼 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
7877ad2antrr 764 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝐼 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
7976, 78eqtr4d 2797 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩} = 𝐼)
8079opeq2d 4560 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩ = ⟨(·𝑖‘ndx), 𝐼⟩)
8152, 68, 80tpeq123d 4427 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩} = {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})
8248, 81uneq12d 3911 . . . . 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 6357 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (TopOpen‘𝑟) = (TopOpen‘𝑅))
84 imasval.j . . . . . . . . . 10 𝐽 = (TopOpen‘𝑅)
8583, 84syl6eqr 2812 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (TopOpen‘𝑟) = 𝐽)
8685, 5oveq12d 6832 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((TopOpen‘𝑟) qTop 𝑓) = (𝐽 qTop 𝐹))
87 imasval.o . . . . . . . . 9 (𝜑𝑂 = (𝐽 qTop 𝐹))
8887ad2antrr 764 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑂 = (𝐽 qTop 𝐹))
8986, 88eqtr4d 2797 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((TopOpen‘𝑟) qTop 𝑓) = 𝑂)
9089opeq2d 4560 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩ = ⟨(TopSet‘ndx), 𝑂⟩)
9113fveq2d 6357 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (le‘𝑟) = (le‘𝑅))
92 imasval.n . . . . . . . . . . 11 𝑁 = (le‘𝑅)
9391, 92syl6eqr 2812 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (le‘𝑟) = 𝑁)
945, 93coeq12d 5442 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓 ∘ (le‘𝑟)) = (𝐹𝑁))
955cnveqd 5453 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑓 = 𝐹)
9694, 95coeq12d 5442 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓) = ((𝐹𝑁) ∘ 𝐹))
97 imasval.l . . . . . . . . 9 (𝜑 = ((𝐹𝑁) ∘ 𝐹))
9897ad2antrr 764 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = ((𝐹𝑁) ∘ 𝐹))
9996, 98eqtr4d 2797 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓) = )
10099opeq2d 4560 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)⟩ = ⟨(le‘ndx), ⟩)
10118sqxpeqd 5298 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑣 × 𝑣) = (𝑉 × 𝑉))
102101oveq1d 6829 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) = ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)))
1035fveq1d 6355 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(1st ‘(‘1))) = (𝐹‘(1st ‘(‘1))))
104103eqeq1d 2762 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(1st ‘(‘1))) = 𝑥 ↔ (𝐹‘(1st ‘(‘1))) = 𝑥))
1055fveq1d 6355 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(2nd ‘(𝑛))) = (𝐹‘(2nd ‘(𝑛))))
106105eqeq1d 2762 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(2nd ‘(𝑛))) = 𝑦 ↔ (𝐹‘(2nd ‘(𝑛))) = 𝑦))
1075fveq1d 6355 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(2nd ‘(𝑖))) = (𝐹‘(2nd ‘(𝑖))))
1085fveq1d 6355 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(1st ‘(‘(𝑖 + 1)))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))
109107, 108eqeq12d 2775 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1))))))
110109ralbidv 3124 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1))))))
111104, 106, 1103anbi123d 1548 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))))
112102, 111rabeqbidv 3335 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} = { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))})
11313fveq2d 6357 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (dist‘𝑟) = (dist‘𝑅))
114 imasval.e . . . . . . . . . . . . . . . 16 𝐸 = (dist‘𝑅)
115113, 114syl6eqr 2812 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (dist‘𝑟) = 𝐸)
116115coeq1d 5439 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((dist‘𝑟) ∘ 𝑔) = (𝐸𝑔))
117116oveq2d 6830 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)) = (ℝ*𝑠 Σg (𝐸𝑔)))
118112, 117mpteq12dv 4885 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))) = (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
119118rneqd 5508 . . . . . . . . . . 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 4699 . . . . . . . . . 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 8550 . . . . . . . . 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 6883 . . . . . . . 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 764 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝐷 = (𝑥𝐵, 𝑦𝐵 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < )))
125122, 124eqtr4d 2797 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < )) = 𝐷)
126125opeq2d 4560 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩ = ⟨(dist‘ndx), 𝐷⟩)
12790, 100, 126tpeq123d 4427 . . . . 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 3911 . . . 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 3701 . . 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 6277 . . . . 5 (𝐹:𝑉onto𝐵𝐹:𝑉𝐵)
1317, 130syl 17 . . . 4 (𝜑𝐹:𝑉𝐵)
132 fvex 6363 . . . . 5 (Base‘𝑅) ∈ V
13316, 132syl6eqel 2847 . . . 4 (𝜑𝑉 ∈ V)
134 fex 6654 . . . 4 ((𝐹:𝑉𝐵𝑉 ∈ V) → 𝐹 ∈ V)
135131, 133, 134syl2anc 696 . . 3 (𝜑𝐹 ∈ V)
136 imasval.r . . . 4 (𝜑𝑅𝑍)
137 elex 3352 . . . 4 (𝑅𝑍𝑅 ∈ V)
138136, 137syl 17 . . 3 (𝜑𝑅 ∈ V)
139 tpex 7123 . . . . . 6 {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∈ V
140 tpex 7123 . . . . . 6 {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩} ∈ V
141139, 140unex 7122 . . . . 5 ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∈ V
142 tpex 7123 . . . . 5 {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∈ V
143141, 142unex 7122 . . . 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 6954 . 2 (𝜑 → (𝐹s 𝑅) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩}))
1461, 145eqtrd 2794 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 383  w3a 1072   = wceq 1632  wcel 2139  wral 3050  {crab 3054  Vcvv 3340  csb 3674  cun 3713  {csn 4321  {ctp 4325  cop 4327   ciun 4672  cmpt 4881   × cxp 5264  ccnv 5265  ran crn 5267  ccom 5270  wf 6045  ontowfo 6047  cfv 6049  (class class class)co 6814  cmpt2 6816  1st c1st 7332  2nd c2nd 7333  𝑚 cmap 8025  infcinf 8514  1c1 10149   + caddc 10151  *cxr 10285   < clt 10286  cmin 10478  cn 11232  ...cfz 12539  ndxcnx 16076  Basecbs 16079  +gcplusg 16163  .rcmulr 16164  Scalarcsca 16166   ·𝑠 cvsca 16167  ·𝑖cip 16168  TopSetcts 16169  lecple 16170  distcds 16172  TopOpenctopn 16304   Σg cgsu 16323  *𝑠cxrs 16382   qTop cqtop 16385  s cimas 16386
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pr 5055  ax-un 7115
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-sup 8515  df-inf 8516  df-imas 16390
This theorem is referenced by:  imasbas  16394  imasds  16395  imasplusg  16399  imasmulr  16400  imassca  16401  imasvsca  16402  imasip  16403  imastset  16404  imasle  16405
  Copyright terms: Public domain W3C validator