Theorem imasval 17590

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.

Step	Hyp	Ref	Expression
1		imasval.u	. 2 ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))
2		df-imas 17587	. . . 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‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}))
3	2	a1i 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 6903	. . . 4 ⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) → (Base‘𝑟) ∈ V)
5		simplrl 789	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑓 = 𝐹)
6	5	rneqd 5933	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = ran 𝐹)
7		imasval.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
8		forn 6802	. . . . . . . . . . 11 ⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵)
9	7, 8	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝐹 = 𝐵)
10	9	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝐹 = 𝐵)
11	6, 10	eqtrd 2801	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = 𝐵)
12	11	opeq2d 4850	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Base‘ndx), ran 𝑓⟩ = ⟨(Base‘ndx), 𝐵⟩)
13		simplrr 790	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑟 = 𝑅)
14	13	fveq2d 6892	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘𝑟) = (Base‘𝑅))
15		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = (Base‘𝑟))
16		imasval.v	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 = (Base‘𝑅))
17	16	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑉 = (Base‘𝑅))
18	14, 15, 17	3eqtr4d 2811	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = 𝑉)
19	5	fveq1d 6890	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘𝑝) = (𝐹‘𝑝))
20	5	fveq1d 6890	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘𝑞) = (𝐹‘𝑞))
21	19, 20	opeq12d 4851	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩)
22	13	fveq2d 6892	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g‘𝑟) = (+g‘𝑅))
23		imasval.p	. . . . . . . . . . . . . . . 16 ⊢ + = (+g‘𝑅)
24	22, 23	eqtr4di 2819	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g‘𝑟) = + )
25	24	oveqd 7440	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(+g‘𝑟)𝑞) = (𝑝 + 𝑞))
26	5, 25	fveq12d 6895	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(+g‘𝑟)𝑞)) = (𝐹‘(𝑝 + 𝑞)))
27	21, 26	opeq12d 4851	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩)
28	27	sneqd 4606	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩} = {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
29	18, 28	iuneq12d 4991	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩} = ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
30	18, 29	iuneq12d 4991	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
31		imasval.a	. . . . . . . . . 10 ⊢ (𝜑 → ✚ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
32	31	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ✚ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
33	30, 32	eqtr4d 2804	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩} = ✚ )
34	33	opeq2d 4850	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩ = ⟨(+g‘ndx), ✚ ⟩)
35	13	fveq2d 6892	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r‘𝑟) = (.r‘𝑅))
36		imasval.m	. . . . . . . . . . . . . . . 16 ⊢ × = (.r‘𝑅)
37	35, 36	eqtr4di 2819	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r‘𝑟) = × )
38	37	oveqd 7440	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(.r‘𝑟)𝑞) = (𝑝 × 𝑞))
39	5, 38	fveq12d 6895	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(.r‘𝑟)𝑞)) = (𝐹‘(𝑝 × 𝑞)))
40	21, 39	opeq12d 4851	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩)
41	40	sneqd 4606	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩} = {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
42	18, 41	iuneq12d 4991	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩} = ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
43	18, 42	iuneq12d 4991	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
44		imasval.t	. . . . . . . . . 10 ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
45	44	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
46	43, 45	eqtr4d 2804	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩} = ∙ )
47	46	opeq2d 4850	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩ = ⟨(.r‘ndx), ∙ ⟩)
48	12, 34, 47	tpeq123d 4719	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩})
49	13	fveq2d 6892	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Scalar‘𝑟) = (Scalar‘𝑅))
50		imasval.g	. . . . . . . . 9 ⊢ 𝐺 = (Scalar‘𝑅)
51	49, 50	eqtr4di 2819	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Scalar‘𝑟) = 𝐺)
52	51	opeq2d 4850	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Scalar‘ndx), (Scalar‘𝑟)⟩ = ⟨(Scalar‘ndx), 𝐺⟩)
53	51	fveq2d 6892	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘(Scalar‘𝑟)) = (Base‘𝐺))
54		imasval.k	. . . . . . . . . . . 12 ⊢ 𝐾 = (Base‘𝐺)
55	53, 54	eqtr4di 2819	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘(Scalar‘𝑟)) = 𝐾)
56	20	sneqd 4606	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {(𝑓‘𝑞)} = {(𝐹‘𝑞)})
57	13	fveq2d 6892	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ( ·𝑠 ‘𝑟) = ( ·𝑠 ‘𝑅))
58		imasval.q	. . . . . . . . . . . . . 14 ⊢ · = ( ·𝑠 ‘𝑅)
59	57, 58	eqtr4di 2819	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ( ·𝑠 ‘𝑟) = · )
60	59	oveqd 7440	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝( ·𝑠 ‘𝑟)𝑞) = (𝑝 · 𝑞))
61	5, 60	fveq12d 6895	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)) = (𝐹‘(𝑝 · 𝑞)))
62	55, 56, 61	mpoeq123dv 7498	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞))) = (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
63	62	iuneq2d 4992	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞))) = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
64	18	iuneq1d 4989	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞))) = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞))))
65		imasval.s	. . . . . . . . . 10 ⊢ (𝜑 → ⊗ = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
66	65	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⊗ = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
67	63, 64, 66	3eqtr4d 2811	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞))) = ⊗ )
68	67	opeq2d 4850	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨( ·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)))⟩ = ⟨( ·𝑠 ‘ndx), ⊗ ⟩)
69	13	fveq2d 6892	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (·𝑖‘𝑟) = (·𝑖‘𝑅))
70		imasval.i	. . . . . . . . . . . . . . 15 ⊢ , = (·𝑖‘𝑅)
71	69, 70	eqtr4di 2819	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (·𝑖‘𝑟) = , )
72	71	oveqd 7440	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(·𝑖‘𝑟)𝑞) = (𝑝 , 𝑞))
73	21, 72	opeq12d 4851	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩)
74	73	sneqd 4606	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩} = {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
75	18, 74	iuneq12d 4991	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩} = ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
76	18, 75	iuneq12d 4991	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
77		imasval.w	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
78	77	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝐼 = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
79	76, 78	eqtr4d 2804	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩} = 𝐼)
80	79	opeq2d 4850	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}⟩ = ⟨(·𝑖‘ndx), 𝐼⟩)
81	52, 68, 80	tpeq123d 4719	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}⟩} = {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})
82	48, 81	uneq12d 4126	. . . . 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), 𝐼⟩}))
83	13	fveq2d 6892	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (TopOpen‘𝑟) = (TopOpen‘𝑅))
84		imasval.j	. . . . . . . . . 10 ⊢ 𝐽 = (TopOpen‘𝑅)
85	83, 84	eqtr4di 2819	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (TopOpen‘𝑟) = 𝐽)
86	85, 5	oveq12d 7441	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((TopOpen‘𝑟) qTop 𝑓) = (𝐽 qTop 𝐹))
87		imasval.o	. . . . . . . . 9 ⊢ (𝜑 → 𝑂 = (𝐽 qTop 𝐹))
88	87	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑂 = (𝐽 qTop 𝐹))
89	86, 88	eqtr4d 2804	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((TopOpen‘𝑟) qTop 𝑓) = 𝑂)
90	89	opeq2d 4850	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩ = ⟨(TopSet‘ndx), 𝑂⟩)
91	13	fveq2d 6892	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (le‘𝑟) = (le‘𝑅))
92		imasval.n	. . . . . . . . . . 11 ⊢ 𝑁 = (le‘𝑅)
93	91, 92	eqtr4di 2819	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (le‘𝑟) = 𝑁)
94	5, 93	coeq12d 5855	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓 ∘ (le‘𝑟)) = (𝐹 ∘ 𝑁))
95	5	cnveqd 5866	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ◡𝑓 = ◡𝐹)
96	94, 95	coeq12d 5855	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓) = ((𝐹 ∘ 𝑁) ∘ ◡𝐹))
97		imasval.l	. . . . . . . . 9 ⊢ (𝜑 → ≤ = ((𝐹 ∘ 𝑁) ∘ ◡𝐹))
98	97	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ≤ = ((𝐹 ∘ 𝑁) ∘ ◡𝐹))
99	96, 98	eqtr4d 2804	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓) = ≤ )
100	99	opeq2d 4850	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓)⟩ = ⟨(le‘ndx), ≤ ⟩)
101	18	sqxpeqd 5698	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑣 × 𝑣) = (𝑉 × 𝑉))
102	101	oveq1d 7438	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑣 × 𝑣) ↑m (1...𝑛)) = ((𝑉 × 𝑉) ↑m (1...𝑛)))
103	5	fveq1d 6890	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(1st ‘(ℎ‘1))) = (𝐹‘(1st ‘(ℎ‘1))))
104	103	eqeq1d 2768	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ↔ (𝐹‘(1st ‘(ℎ‘1))) = 𝑥))
105	5	fveq1d 6890	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘(2nd ‘(ℎ‘𝑛))))
106	105	eqeq1d 2768	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ↔ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦))
107	5	fveq1d 6890	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(2nd ‘(ℎ‘𝑖))))
108	5	fveq1d 6890	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))
109	107, 108	eqeq12d 2782	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1))))))
110	109	ralbidv 3191	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1))))))
111	104, 106, 110	3anbi123d 1464	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))))
112	102, 111	rabeqbidv 3437	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} = {ℎ ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))})
113	13	fveq2d 6892	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (dist‘𝑟) = (dist‘𝑅))
114		imasval.e	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 = (dist‘𝑅)
115	113, 114	eqtr4di 2819	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (dist‘𝑟) = 𝐸)
116	115	coeq1d 5852	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((dist‘𝑟) ∘ 𝑔) = (𝐸 ∘ 𝑔))
117	116	oveq2d 7439	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
118	112, 117	mpteq12dv 5203	. . . . . . . . . . . 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 (𝐸 ∘ 𝑔))))
119	118	rneqd 5933	. . . . . . . . . . 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 (𝐸 ∘ 𝑔))))
120	119	iuneq2d 4992	. . . . . . . . . 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 (𝐸 ∘ 𝑔))))
121	120	infeq1d 9448	. . . . . . . . 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 (𝐸 ∘ 𝑔))), ℝ*, < ))
122	11, 11, 121	mpoeq123dv 7498	. . . . . . . 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 (𝐸 ∘ 𝑔))), ℝ*, < )))
124	123	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝐷 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))), ℝ*, < )))
125	122, 124	eqtr4d 2804	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < )) = 𝐷)
126	125	opeq2d 4850	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩ = ⟨(dist‘ndx), 𝐷⟩)
127	90, 100, 126	tpeq123d 4719	. . . . 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), 𝐷⟩})
128	82, 127	uneq12d 4126	. . . 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), 𝐷⟩}))
129	4, 128	csbied 3892	. . 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 6799	. . . . 5 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
131	7, 130	syl 18	. . . 4 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
132		fvex 6901	. . . . 5 ⊢ (Base‘𝑅) ∈ V
133	16, 132	eqeltrdi 2874	. . . 4 ⊢ (𝜑 → 𝑉 ∈ V)
134	131, 133	fexd 7232	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
135		imasval.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑍)
136	135	elexd 3481	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
137		tpex 7756	. . . . . 6 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∈ V
138		tpex 7756	. . . . . 6 ⊢ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩} ∈ V
139	137, 138	unex 7755	. . . . 5 ⊢ ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∈ V
140		tpex 7756	. . . . 5 ⊢ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∈ V
141	139, 140	unex 7755	. . . 4 ⊢ (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}) ∈ V
142	141	a1i 11	. . 3 ⊢ (𝜑 → (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}) ∈ V)
143	3, 129, 134, 136, 142	ovmpod 7575	. 2 ⊢ (𝜑 → (𝐹 “s 𝑅) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}))
144	1, 143	eqtrd 2801	1 ⊢ (𝜑 → 𝑈 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ∀wral 3082  {crab 3419  Vcvv 3458  ⦋csb 3856   ∪ cun 3906  {csn 4594  {ctp 4598  ⟨cop 4600  ∪ ciun 4961   ↦ cmpt 5197   × cxp 5664  ^◡ccnv 5665  ran crn 5667   ∘ ccom 5670  ⟶wf 6539  –onto→wfo 6541  ‘cfv 6543  (class class class)co 7423   ∈ cmpo 7425  1^st c1st 7993  2^nd c2nd 7994   ↑_m cmap 8833  infcinf 9411  1c1 11119   + caddc 11121  ℝ^*cxr 11260   < clt 11261   − cmin 11459  ℕcn 12251  ...cfz 13553  ndxcnx 17278  Basecbs 17294  +_gcplusg 17335  ._rcmulr 17336  Scalarcsca 17338   ·_𝑠 cvsca 17339  ·_𝑖cip 17340  TopSetcts 17341  lecple 17342  distcds 17344  TopOpenctopn 17499   Σ_g cgsu 17518  ℝ^*_𝑠cxrs 17579   qTop cqtop 17582   “_s cimas 17583

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-tp 4599  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-sup 9412  df-inf 9413  df-imas 17587

This theorem is used by:  imasbas  17591  imasds  17592  imasplusg  17596  imasmulr  17597  imassca  17598  imasvsca  17599  imasip  17600  imastset  17601  imasle  17602