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

Theorem imasval 16775
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 (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑m (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 16772 . . . 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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩})))
4 fvexd 6667 . . . 4 ((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) → (Base‘𝑟) ∈ V)
5 simplrl 776 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑓 = 𝐹)
65rneqd 5785 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = ran 𝐹)
7 imasval.f . . . . . . . . . . 11 (𝜑𝐹:𝑉onto𝐵)
8 forn 6575 . . . . . . . . . . 11 (𝐹:𝑉onto𝐵 → ran 𝐹 = 𝐵)
97, 8syl 17 . . . . . . . . . 10 (𝜑 → ran 𝐹 = 𝐵)
109ad2antrr 725 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝐹 = 𝐵)
116, 10eqtrd 2857 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = 𝐵)
1211opeq2d 4785 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Base‘ndx), ran 𝑓⟩ = ⟨(Base‘ndx), 𝐵⟩)
13 simplrr 777 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑟 = 𝑅)
1413fveq2d 6656 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘𝑟) = (Base‘𝑅))
15 simpr 488 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = (Base‘𝑟))
16 imasval.v . . . . . . . . . . . 12 (𝜑𝑉 = (Base‘𝑅))
1716ad2antrr 725 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑉 = (Base‘𝑅))
1814, 15, 173eqtr4d 2867 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = 𝑉)
195fveq1d 6654 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓𝑝) = (𝐹𝑝))
205fveq1d 6654 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓𝑞) = (𝐹𝑞))
2119, 20opeq12d 4786 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(𝑓𝑝), (𝑓𝑞)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩)
2213fveq2d 6656 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g𝑟) = (+g𝑅))
23 imasval.p . . . . . . . . . . . . . . . 16 + = (+g𝑅)
2422, 23eqtr4di 2875 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g𝑟) = + )
2524oveqd 7157 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(+g𝑟)𝑞) = (𝑝 + 𝑞))
265, 25fveq12d 6659 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(+g𝑟)𝑞)) = (𝐹‘(𝑝 + 𝑞)))
2721, 26opeq12d 4786 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩)
2827sneqd 4551 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
2918, 28iuneq12d 4922 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3018, 29iuneq12d 4922 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
31 imasval.a . . . . . . . . . 10 (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3231ad2antrr 725 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3330, 32eqtr4d 2860 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = )
3433opeq2d 4785 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩ = ⟨(+g‘ndx), ⟩)
3513fveq2d 6656 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r𝑟) = (.r𝑅))
36 imasval.m . . . . . . . . . . . . . . . 16 × = (.r𝑅)
3735, 36eqtr4di 2875 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r𝑟) = × )
3837oveqd 7157 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(.r𝑟)𝑞) = (𝑝 × 𝑞))
395, 38fveq12d 6659 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(.r𝑟)𝑞)) = (𝐹‘(𝑝 × 𝑞)))
4021, 39opeq12d 4786 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩)
4140sneqd 4551 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4218, 41iuneq12d 4922 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4318, 42iuneq12d 4922 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
44 imasval.t . . . . . . . . . 10 (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4544ad2antrr 725 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4643, 45eqtr4d 2860 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = )
4746opeq2d 4785 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩ = ⟨(.r‘ndx), ⟩)
4812, 34, 47tpeq123d 4658 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩})
4913fveq2d 6656 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Scalar‘𝑟) = (Scalar‘𝑅))
50 imasval.g . . . . . . . . 9 𝐺 = (Scalar‘𝑅)
5149, 50eqtr4di 2875 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Scalar‘𝑟) = 𝐺)
5251opeq2d 4785 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Scalar‘ndx), (Scalar‘𝑟)⟩ = ⟨(Scalar‘ndx), 𝐺⟩)
5351fveq2d 6656 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘(Scalar‘𝑟)) = (Base‘𝐺))
54 imasval.k . . . . . . . . . . . 12 𝐾 = (Base‘𝐺)
5553, 54eqtr4di 2875 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘(Scalar‘𝑟)) = 𝐾)
5620sneqd 4551 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {(𝑓𝑞)} = {(𝐹𝑞)})
5713fveq2d 6656 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ( ·𝑠𝑟) = ( ·𝑠𝑅))
58 imasval.q . . . . . . . . . . . . . 14 · = ( ·𝑠𝑅)
5957, 58eqtr4di 2875 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ( ·𝑠𝑟) = · )
6059oveqd 7157 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝( ·𝑠𝑟)𝑞) = (𝑝 · 𝑞))
615, 60fveq12d 6659 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝( ·𝑠𝑟)𝑞)) = (𝐹‘(𝑝 · 𝑞)))
6255, 56, 61mpoeq123dv 7213 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))) = (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
6362iuneq2d 4923 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))) = 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
6418iuneq1d 4921 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))) = 𝑞𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))))
65 imasval.s . . . . . . . . . 10 (𝜑 = 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
6665ad2antrr 725 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
6763, 64, 663eqtr4d 2867 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))) = )
6867opeq2d 4785 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩ = ⟨( ·𝑠 ‘ndx), ⟩)
6913fveq2d 6656 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (·𝑖𝑟) = (·𝑖𝑅))
70 imasval.i . . . . . . . . . . . . . . 15 , = (·𝑖𝑅)
7169, 70eqtr4di 2875 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (·𝑖𝑟) = , )
7271oveqd 7157 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(·𝑖𝑟)𝑞) = (𝑝 , 𝑞))
7321, 72opeq12d 4786 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩)
7473sneqd 4551 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩} = {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
7518, 74iuneq12d 4922 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩} = 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
7618, 75iuneq12d 4922 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩} = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
77 imasval.w . . . . . . . . . 10 (𝜑𝐼 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
7877ad2antrr 725 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝐼 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
7976, 78eqtr4d 2860 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩} = 𝐼)
8079opeq2d 4785 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩ = ⟨(·𝑖‘ndx), 𝐼⟩)
8152, 68, 80tpeq123d 4658 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩} = {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})
8248, 81uneq12d 4115 . . . . 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 6656 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (TopOpen‘𝑟) = (TopOpen‘𝑅))
84 imasval.j . . . . . . . . . 10 𝐽 = (TopOpen‘𝑅)
8583, 84eqtr4di 2875 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (TopOpen‘𝑟) = 𝐽)
8685, 5oveq12d 7158 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((TopOpen‘𝑟) qTop 𝑓) = (𝐽 qTop 𝐹))
87 imasval.o . . . . . . . . 9 (𝜑𝑂 = (𝐽 qTop 𝐹))
8887ad2antrr 725 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑂 = (𝐽 qTop 𝐹))
8986, 88eqtr4d 2860 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((TopOpen‘𝑟) qTop 𝑓) = 𝑂)
9089opeq2d 4785 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩ = ⟨(TopSet‘ndx), 𝑂⟩)
9113fveq2d 6656 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (le‘𝑟) = (le‘𝑅))
92 imasval.n . . . . . . . . . . 11 𝑁 = (le‘𝑅)
9391, 92eqtr4di 2875 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (le‘𝑟) = 𝑁)
945, 93coeq12d 5712 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓 ∘ (le‘𝑟)) = (𝐹𝑁))
955cnveqd 5723 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑓 = 𝐹)
9694, 95coeq12d 5712 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓) = ((𝐹𝑁) ∘ 𝐹))
97 imasval.l . . . . . . . . 9 (𝜑 = ((𝐹𝑁) ∘ 𝐹))
9897ad2antrr 725 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = ((𝐹𝑁) ∘ 𝐹))
9996, 98eqtr4d 2860 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓) = )
10099opeq2d 4785 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)⟩ = ⟨(le‘ndx), ⟩)
10118sqxpeqd 5564 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑣 × 𝑣) = (𝑉 × 𝑉))
102101oveq1d 7155 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑣 × 𝑣) ↑m (1...𝑛)) = ((𝑉 × 𝑉) ↑m (1...𝑛)))
1035fveq1d 6654 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(1st ‘(‘1))) = (𝐹‘(1st ‘(‘1))))
104103eqeq1d 2824 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(1st ‘(‘1))) = 𝑥 ↔ (𝐹‘(1st ‘(‘1))) = 𝑥))
1055fveq1d 6654 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(2nd ‘(𝑛))) = (𝐹‘(2nd ‘(𝑛))))
106105eqeq1d 2824 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(2nd ‘(𝑛))) = 𝑦 ↔ (𝐹‘(2nd ‘(𝑛))) = 𝑦))
1075fveq1d 6654 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(2nd ‘(𝑖))) = (𝐹‘(2nd ‘(𝑖))))
1085fveq1d 6654 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(1st ‘(‘(𝑖 + 1)))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))
109107, 108eqeq12d 2838 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1))))))
110109ralbidv 3187 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1))))))
111104, 106, 1103anbi123d 1433 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))))
112102, 111rabeqbidv 3461 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} = { ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))})
11313fveq2d 6656 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (dist‘𝑟) = (dist‘𝑅))
114 imasval.e . . . . . . . . . . . . . . . 16 𝐸 = (dist‘𝑅)
115113, 114eqtr4di 2875 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (dist‘𝑟) = 𝐸)
116115coeq1d 5709 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((dist‘𝑟) ∘ 𝑔) = (𝐸𝑔))
117116oveq2d 7156 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)) = (ℝ*𝑠 Σg (𝐸𝑔)))
118112, 117mpteq12dv 5127 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))) = (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
119118rneqd 5785 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))) = ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
120119iuneq2d 4923 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))) = 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
121120infeq1d 8929 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ) = inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < ))
12211, 11, 121mpoeq123dv 7213 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < )) = (𝑥𝐵, 𝑦𝐵 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < )))
123 imasval.d . . . . . . . . 9 (𝜑𝐷 = (𝑥𝐵, 𝑦𝐵 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < )))
124123ad2antrr 725 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝐷 = (𝑥𝐵, 𝑦𝐵 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < )))
125122, 124eqtr4d 2860 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < )) = 𝐷)
126125opeq2d 4785 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩ = ⟨(dist‘ndx), 𝐷⟩)
12790, 100, 126tpeq123d 4658 . . . . 5 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(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‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩} = {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩})
12882, 127uneq12d 4115 . . . 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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (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 3891 . . 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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑m (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 6572 . . . . 5 (𝐹:𝑉onto𝐵𝐹:𝑉𝐵)
1317, 130syl 17 . . . 4 (𝜑𝐹:𝑉𝐵)
132 fvex 6665 . . . . 5 (Base‘𝑅) ∈ V
13316, 132eqeltrdi 2922 . . . 4 (𝜑𝑉 ∈ V)
134 fex 6971 . . . 4 ((𝐹:𝑉𝐵𝑉 ∈ V) → 𝐹 ∈ V)
135131, 133, 134syl2anc 587 . . 3 (𝜑𝐹 ∈ V)
136 imasval.r . . . 4 (𝜑𝑅𝑍)
137136elexd 3489 . . 3 (𝜑𝑅 ∈ V)
138 tpex 7455 . . . . . 6 {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∈ V
139 tpex 7455 . . . . . 6 {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩} ∈ V
140138, 139unex 7454 . . . . 5 ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∈ V
141 tpex 7455 . . . . 5 {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∈ V
142140, 141unex 7454 . . . 4 (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩}) ∈ V
143142a1i 11 . . 3 (𝜑 → (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩}) ∈ V)
1443, 129, 135, 137, 143ovmpod 7286 . 2 (𝜑 → (𝐹s 𝑅) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩}))
1451, 144eqtrd 2857 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 399  w3a 1084   = wceq 1538  wcel 2114  wral 3130  {crab 3134  Vcvv 3469  csb 3855  cun 3906  {csn 4539  {ctp 4543  cop 4545   ciun 4894  cmpt 5122   × cxp 5530  ccnv 5531  ran crn 5533  ccom 5536  wf 6330  ontowfo 6332  cfv 6334  (class class class)co 7140  cmpo 7142  1st c1st 7673  2nd c2nd 7674  m cmap 8393  infcinf 8893  1c1 10527   + caddc 10529  *cxr 10663   < clt 10664  cmin 10859  cn 11625  ...cfz 12885  ndxcnx 16471  Basecbs 16474  +gcplusg 16556  .rcmulr 16557  Scalarcsca 16559   ·𝑠 cvsca 16560  ·𝑖cip 16561  TopSetcts 16562  lecple 16563  distcds 16565  TopOpenctopn 16686   Σg cgsu 16705  *𝑠cxrs 16764   qTop cqtop 16767  s cimas 16768
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pr 5307  ax-un 7446
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-reu 3137  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-ov 7143  df-oprab 7144  df-mpo 7145  df-sup 8894  df-inf 8895  df-imas 16772
This theorem is referenced by:  imasbas  16776  imasds  16777  imasplusg  16781  imasmulr  16782  imassca  16783  imasvsca  16784  imasip  16785  imastset  16786  imasle  16787
  Copyright terms: Public domain W3C validator