Theorem imasval 17139

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 17136	. . . 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 6771	. . . 4 ⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) → (Base‘𝑟) ∈ V)
5		simplrl 773	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑓 = 𝐹)
6	5	rneqd 5836	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = ran 𝐹)
7		imasval.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
8		forn 6675	. . . . . . . . . . 11 ⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵)
9	7, 8	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝐹 = 𝐵)
10	9	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝐹 = 𝐵)
11	6, 10	eqtrd 2778	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = 𝐵)
12	11	opeq2d 4808	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Base‘ndx), ran 𝑓⟩ = ⟨(Base‘ndx), 𝐵⟩)
13		simplrr 774	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑟 = 𝑅)
14	13	fveq2d 6760	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘𝑟) = (Base‘𝑅))
15		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = (Base‘𝑟))
16		imasval.v	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 = (Base‘𝑅))
17	16	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑉 = (Base‘𝑅))
18	14, 15, 17	3eqtr4d 2788	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = 𝑉)
19	5	fveq1d 6758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘𝑝) = (𝐹‘𝑝))
20	5	fveq1d 6758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘𝑞) = (𝐹‘𝑞))
21	19, 20	opeq12d 4809	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩)
22	13	fveq2d 6760	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g‘𝑟) = (+g‘𝑅))
23		imasval.p	. . . . . . . . . . . . . . . 16 ⊢ + = (+g‘𝑅)
24	22, 23	eqtr4di 2797	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g‘𝑟) = + )
25	24	oveqd 7272	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(+g‘𝑟)𝑞) = (𝑝 + 𝑞))
26	5, 25	fveq12d 6763	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(+g‘𝑟)𝑞)) = (𝐹‘(𝑝 + 𝑞)))
27	21, 26	opeq12d 4809	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩)
28	27	sneqd 4570	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩} = {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
29	18, 28	iuneq12d 4949	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩} = ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
30	18, 29	iuneq12d 4949	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
31		imasval.a	. . . . . . . . . 10 ⊢ (𝜑 → ✚ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
32	31	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ✚ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
33	30, 32	eqtr4d 2781	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩} = ✚ )
34	33	opeq2d 4808	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩ = ⟨(+g‘ndx), ✚ ⟩)
35	13	fveq2d 6760	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r‘𝑟) = (.r‘𝑅))
36		imasval.m	. . . . . . . . . . . . . . . 16 ⊢ × = (.r‘𝑅)
37	35, 36	eqtr4di 2797	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r‘𝑟) = × )
38	37	oveqd 7272	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(.r‘𝑟)𝑞) = (𝑝 × 𝑞))
39	5, 38	fveq12d 6763	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(.r‘𝑟)𝑞)) = (𝐹‘(𝑝 × 𝑞)))
40	21, 39	opeq12d 4809	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩)
41	40	sneqd 4570	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩} = {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
42	18, 41	iuneq12d 4949	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩} = ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
43	18, 42	iuneq12d 4949	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
44		imasval.t	. . . . . . . . . 10 ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
45	44	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
46	43, 45	eqtr4d 2781	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩} = ∙ )
47	46	opeq2d 4808	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩ = ⟨(.r‘ndx), ∙ ⟩)
48	12, 34, 47	tpeq123d 4681	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩})
49	13	fveq2d 6760	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Scalar‘𝑟) = (Scalar‘𝑅))
50		imasval.g	. . . . . . . . 9 ⊢ 𝐺 = (Scalar‘𝑅)
51	49, 50	eqtr4di 2797	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Scalar‘𝑟) = 𝐺)
52	51	opeq2d 4808	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Scalar‘ndx), (Scalar‘𝑟)⟩ = ⟨(Scalar‘ndx), 𝐺⟩)
53	51	fveq2d 6760	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘(Scalar‘𝑟)) = (Base‘𝐺))
54		imasval.k	. . . . . . . . . . . 12 ⊢ 𝐾 = (Base‘𝐺)
55	53, 54	eqtr4di 2797	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘(Scalar‘𝑟)) = 𝐾)
56	20	sneqd 4570	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {(𝑓‘𝑞)} = {(𝐹‘𝑞)})
57	13	fveq2d 6760	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ( ·𝑠 ‘𝑟) = ( ·𝑠 ‘𝑅))
58		imasval.q	. . . . . . . . . . . . . 14 ⊢ · = ( ·𝑠 ‘𝑅)
59	57, 58	eqtr4di 2797	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ( ·𝑠 ‘𝑟) = · )
60	59	oveqd 7272	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝( ·𝑠 ‘𝑟)𝑞) = (𝑝 · 𝑞))
61	5, 60	fveq12d 6763	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)) = (𝐹‘(𝑝 · 𝑞)))
62	55, 56, 61	mpoeq123dv 7328	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞))) = (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
63	62	iuneq2d 4950	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞))) = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
64	18	iuneq1d 4948	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞))) = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞))))
65		imasval.s	. . . . . . . . . 10 ⊢ (𝜑 → ⊗ = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
66	65	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⊗ = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
67	63, 64, 66	3eqtr4d 2788	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞))) = ⊗ )
68	67	opeq2d 4808	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨( ·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)))⟩ = ⟨( ·𝑠 ‘ndx), ⊗ ⟩)
69	13	fveq2d 6760	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (·𝑖‘𝑟) = (·𝑖‘𝑅))
70		imasval.i	. . . . . . . . . . . . . . 15 ⊢ , = (·𝑖‘𝑅)
71	69, 70	eqtr4di 2797	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (·𝑖‘𝑟) = , )
72	71	oveqd 7272	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(·𝑖‘𝑟)𝑞) = (𝑝 , 𝑞))
73	21, 72	opeq12d 4809	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩)
74	73	sneqd 4570	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩} = {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
75	18, 74	iuneq12d 4949	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩} = ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
76	18, 75	iuneq12d 4949	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
77		imasval.w	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
78	77	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝐼 = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
79	76, 78	eqtr4d 2781	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩} = 𝐼)
80	79	opeq2d 4808	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}⟩ = ⟨(·𝑖‘ndx), 𝐼⟩)
81	52, 68, 80	tpeq123d 4681	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}⟩} = {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})
82	48, 81	uneq12d 4094	. . . . 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 6760	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (TopOpen‘𝑟) = (TopOpen‘𝑅))
84		imasval.j	. . . . . . . . . 10 ⊢ 𝐽 = (TopOpen‘𝑅)
85	83, 84	eqtr4di 2797	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (TopOpen‘𝑟) = 𝐽)
86	85, 5	oveq12d 7273	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((TopOpen‘𝑟) qTop 𝑓) = (𝐽 qTop 𝐹))
87		imasval.o	. . . . . . . . 9 ⊢ (𝜑 → 𝑂 = (𝐽 qTop 𝐹))
88	87	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑂 = (𝐽 qTop 𝐹))
89	86, 88	eqtr4d 2781	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((TopOpen‘𝑟) qTop 𝑓) = 𝑂)
90	89	opeq2d 4808	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩ = ⟨(TopSet‘ndx), 𝑂⟩)
91	13	fveq2d 6760	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (le‘𝑟) = (le‘𝑅))
92		imasval.n	. . . . . . . . . . 11 ⊢ 𝑁 = (le‘𝑅)
93	91, 92	eqtr4di 2797	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (le‘𝑟) = 𝑁)
94	5, 93	coeq12d 5762	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓 ∘ (le‘𝑟)) = (𝐹 ∘ 𝑁))
95	5	cnveqd 5773	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ◡𝑓 = ◡𝐹)
96	94, 95	coeq12d 5762	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓) = ((𝐹 ∘ 𝑁) ∘ ◡𝐹))
97		imasval.l	. . . . . . . . 9 ⊢ (𝜑 → ≤ = ((𝐹 ∘ 𝑁) ∘ ◡𝐹))
98	97	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ≤ = ((𝐹 ∘ 𝑁) ∘ ◡𝐹))
99	96, 98	eqtr4d 2781	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓) = ≤ )
100	99	opeq2d 4808	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓)⟩ = ⟨(le‘ndx), ≤ ⟩)
101	18	sqxpeqd 5612	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑣 × 𝑣) = (𝑉 × 𝑉))
102	101	oveq1d 7270	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑣 × 𝑣) ↑m (1...𝑛)) = ((𝑉 × 𝑉) ↑m (1...𝑛)))
103	5	fveq1d 6758	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(1st ‘(ℎ‘1))) = (𝐹‘(1st ‘(ℎ‘1))))
104	103	eqeq1d 2740	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ↔ (𝐹‘(1st ‘(ℎ‘1))) = 𝑥))
105	5	fveq1d 6758	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘(2nd ‘(ℎ‘𝑛))))
106	105	eqeq1d 2740	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ↔ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦))
107	5	fveq1d 6758	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(2nd ‘(ℎ‘𝑖))))
108	5	fveq1d 6758	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))
109	107, 108	eqeq12d 2754	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1))))))
110	109	ralbidv 3120	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1))))))
111	104, 106, 110	3anbi123d 1434	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))))
112	102, 111	rabeqbidv 3410	. . . . . . . . . . . . 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 6760	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (dist‘𝑟) = (dist‘𝑅))
114		imasval.e	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 = (dist‘𝑅)
115	113, 114	eqtr4di 2797	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (dist‘𝑟) = 𝐸)
116	115	coeq1d 5759	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((dist‘𝑟) ∘ 𝑔) = (𝐸 ∘ 𝑔))
117	116	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
118	112, 117	mpteq12dv 5161	. . . . . . . . . . . 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 5836	. . . . . . . . . . 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 4950	. . . . . . . . . 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 9166	. . . . . . . . 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 7328	. . . . . . . 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 722	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝐷 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))), ℝ*, < )))
125	122, 124	eqtr4d 2781	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑m (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < )) = 𝐷)
126	125	opeq2d 4808	. . . . . 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 4681	. . . . 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 4094	. . . 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 3866	. . 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 6672	. . . . 5 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
131	7, 130	syl 17	. . . 4 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
132		fvex 6769	. . . . 5 ⊢ (Base‘𝑅) ∈ V
133	16, 132	eqeltrdi 2847	. . . 4 ⊢ (𝜑 → 𝑉 ∈ V)
134	131, 133	fexd 7085	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
135		imasval.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑍)
136	135	elexd 3442	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
137		tpex 7575	. . . . . 6 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∈ V
138		tpex 7575	. . . . . 6 ⊢ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩} ∈ V
139	137, 138	unex 7574	. . . . 5 ⊢ ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∈ V
140		tpex 7575	. . . . 5 ⊢ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∈ V
141	139, 140	unex 7574	. . . 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 7403	. 2 ⊢ (𝜑 → (𝐹 “s 𝑅) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}))
144	1, 143	eqtrd 2778	1 ⊢ (𝜑 → 𝑈 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  ∀wral 3063  {crab 3067  Vcvv 3422  ⦋csb 3828   ∪ cun 3881  {csn 4558  {ctp 4562  ⟨cop 4564  ∪ ciun 4921   ↦ cmpt 5153   × cxp 5578  ^◡ccnv 5579  ran crn 5581   ∘ ccom 5584  ⟶wf 6414  –onto→wfo 6416  ‘cfv 6418  (class class class)co 7255   ∈ cmpo 7257  1^st c1st 7802  2^nd c2nd 7803   ↑_m cmap 8573  infcinf 9130  1c1 10803   + caddc 10805  ℝ^*cxr 10939   < clt 10940   − cmin 11135  ℕcn 11903  ...cfz 13168  ndxcnx 16822  Basecbs 16840  +_gcplusg 16888  ._rcmulr 16889  Scalarcsca 16891   ·_𝑠 cvsca 16892  ·_𝑖cip 16893  TopSetcts 16894  lecple 16895  distcds 16897  TopOpenctopn 17049   Σ_g cgsu 17068  ℝ^*_𝑠cxrs 17128   qTop cqtop 17131   “_s cimas 17132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-sup 9131  df-inf 9132  df-imas 17136

This theorem is referenced by:  imasbas  17140  imasds  17141  imasplusg  17145  imasmulr  17146  imassca  17147  imasvsca  17148  imasip  17149  imastset  17150  imasle  17151