Theorem imasval 15994

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.

Step	Hyp	Ref	Expression
1		imasval.u	. 2 ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))
2		df-imas 15991	. . . 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‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}))
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 (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩})))
4		fvex 6113	. . . . 5 ⊢ (Base‘𝑟) ∈ V
5	4	a1i 11	. . . 4 ⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) → (Base‘𝑟) ∈ V)
6		simplrl 796	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑓 = 𝐹)
7	6	rneqd 5274	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = ran 𝐹)
8		imasval.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
9		forn 6031	. . . . . . . . . . 11 ⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵)
10	8, 9	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝐹 = 𝐵)
11	10	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝐹 = 𝐵)
12	7, 11	eqtrd 2644	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = 𝐵)
13	12	opeq2d 4347	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Base‘ndx), ran 𝑓⟩ = ⟨(Base‘ndx), 𝐵⟩)
14		simplrr 797	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑟 = 𝑅)
15	14	fveq2d 6107	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘𝑟) = (Base‘𝑅))
16		simpr 476	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = (Base‘𝑟))
17		imasval.v	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 = (Base‘𝑅))
18	17	ad2antrr 758	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑉 = (Base‘𝑅))
19	15, 16, 18	3eqtr4d 2654	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = 𝑉)
20	6	fveq1d 6105	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘𝑝) = (𝐹‘𝑝))
21	6	fveq1d 6105	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘𝑞) = (𝐹‘𝑞))
22	20, 21	opeq12d 4348	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩)
23	14	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g‘𝑟) = (+g‘𝑅))
24		imasval.p	. . . . . . . . . . . . . . . 16 ⊢ + = (+g‘𝑅)
25	23, 24	syl6eqr 2662	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g‘𝑟) = + )
26	25	oveqd 6566	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(+g‘𝑟)𝑞) = (𝑝 + 𝑞))
27	6, 26	fveq12d 6109	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(+g‘𝑟)𝑞)) = (𝐹‘(𝑝 + 𝑞)))
28	22, 27	opeq12d 4348	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩)
29	28	sneqd 4137	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩} = {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
30	19, 29	iuneq12d 4482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩} = ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
31	19, 30	iuneq12d 4482	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
32		imasval.a	. . . . . . . . . 10 ⊢ (𝜑 → ✚ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
33	32	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ✚ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
34	31, 33	eqtr4d 2647	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩} = ✚ )
35	34	opeq2d 4347	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩ = ⟨(+g‘ndx), ✚ ⟩)
36	14	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r‘𝑟) = (.r‘𝑅))
37		imasval.m	. . . . . . . . . . . . . . . 16 ⊢ × = (.r‘𝑅)
38	36, 37	syl6eqr 2662	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r‘𝑟) = × )
39	38	oveqd 6566	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(.r‘𝑟)𝑞) = (𝑝 × 𝑞))
40	6, 39	fveq12d 6109	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(.r‘𝑟)𝑞)) = (𝐹‘(𝑝 × 𝑞)))
41	22, 40	opeq12d 4348	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩)
42	41	sneqd 4137	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩} = {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
43	19, 42	iuneq12d 4482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩} = ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
44	19, 43	iuneq12d 4482	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
45		imasval.t	. . . . . . . . . 10 ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
46	45	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
47	44, 46	eqtr4d 2647	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩} = ∙ )
48	47	opeq2d 4347	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩ = ⟨(.r‘ndx), ∙ ⟩)
49	13, 35, 48	tpeq123d 4227	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩})
50	14	fveq2d 6107	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Scalar‘𝑟) = (Scalar‘𝑅))
51		imasval.g	. . . . . . . . 9 ⊢ 𝐺 = (Scalar‘𝑅)
52	50, 51	syl6eqr 2662	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Scalar‘𝑟) = 𝐺)
53	52	opeq2d 4347	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Scalar‘ndx), (Scalar‘𝑟)⟩ = ⟨(Scalar‘ndx), 𝐺⟩)
54	52	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘(Scalar‘𝑟)) = (Base‘𝐺))
55		imasval.k	. . . . . . . . . . . 12 ⊢ 𝐾 = (Base‘𝐺)
56	54, 55	syl6eqr 2662	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘(Scalar‘𝑟)) = 𝐾)
57	21	sneqd 4137	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {(𝑓‘𝑞)} = {(𝐹‘𝑞)})
58	14	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ( ·𝑠 ‘𝑟) = ( ·𝑠 ‘𝑅))
59		imasval.q	. . . . . . . . . . . . . 14 ⊢ · = ( ·𝑠 ‘𝑅)
60	58, 59	syl6eqr 2662	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ( ·𝑠 ‘𝑟) = · )
61	60	oveqd 6566	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝( ·𝑠 ‘𝑟)𝑞) = (𝑝 · 𝑞))
62	6, 61	fveq12d 6109	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)) = (𝐹‘(𝑝 · 𝑞)))
63	56, 57, 62	mpt2eq123dv 6615	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞))) = (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
64	63	iuneq2d 4483	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞))) = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
65	19	iuneq1d 4481	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞))) = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞))))
66		imasval.s	. . . . . . . . . 10 ⊢ (𝜑 → ⊗ = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
67	66	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⊗ = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
68	64, 65, 67	3eqtr4d 2654	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞))) = ⊗ )
69	68	opeq2d 4347	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨( ·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)))⟩ = ⟨( ·𝑠 ‘ndx), ⊗ ⟩)
70	14	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (·𝑖‘𝑟) = (·𝑖‘𝑅))
71		imasval.i	. . . . . . . . . . . . . . 15 ⊢ , = (·𝑖‘𝑅)
72	70, 71	syl6eqr 2662	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (·𝑖‘𝑟) = , )
73	72	oveqd 6566	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(·𝑖‘𝑟)𝑞) = (𝑝 , 𝑞))
74	22, 73	opeq12d 4348	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩)
75	74	sneqd 4137	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩} = {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
76	19, 75	iuneq12d 4482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩} = ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
77	19, 76	iuneq12d 4482	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
78		imasval.w	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
79	78	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝐼 = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
80	77, 79	eqtr4d 2647	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩} = 𝐼)
81	80	opeq2d 4347	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}⟩ = ⟨(·𝑖‘ndx), 𝐼⟩)
82	53, 69, 81	tpeq123d 4227	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·𝑠 ‘𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·𝑖‘𝑟)𝑞)⟩}⟩} = {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})
83	49, 82	uneq12d 3730	. . . . 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), 𝐼⟩}))
84	14	fveq2d 6107	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (TopOpen‘𝑟) = (TopOpen‘𝑅))
85		imasval.j	. . . . . . . . . 10 ⊢ 𝐽 = (TopOpen‘𝑅)
86	84, 85	syl6eqr 2662	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (TopOpen‘𝑟) = 𝐽)
87	86, 6	oveq12d 6567	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((TopOpen‘𝑟) qTop 𝑓) = (𝐽 qTop 𝐹))
88		imasval.o	. . . . . . . . 9 ⊢ (𝜑 → 𝑂 = (𝐽 qTop 𝐹))
89	88	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑂 = (𝐽 qTop 𝐹))
90	87, 89	eqtr4d 2647	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((TopOpen‘𝑟) qTop 𝑓) = 𝑂)
91	90	opeq2d 4347	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩ = ⟨(TopSet‘ndx), 𝑂⟩)
92	14	fveq2d 6107	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (le‘𝑟) = (le‘𝑅))
93		imasval.n	. . . . . . . . . . 11 ⊢ 𝑁 = (le‘𝑅)
94	92, 93	syl6eqr 2662	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (le‘𝑟) = 𝑁)
95	6, 94	coeq12d 5208	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓 ∘ (le‘𝑟)) = (𝐹 ∘ 𝑁))
96	6	cnveqd 5220	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ◡𝑓 = ◡𝐹)
97	95, 96	coeq12d 5208	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓) = ((𝐹 ∘ 𝑁) ∘ ◡𝐹))
98		imasval.l	. . . . . . . . 9 ⊢ (𝜑 → ≤ = ((𝐹 ∘ 𝑁) ∘ ◡𝐹))
99	98	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ≤ = ((𝐹 ∘ 𝑁) ∘ ◡𝐹))
100	97, 99	eqtr4d 2647	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓) = ≤ )
101	100	opeq2d 4347	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ ◡𝑓)⟩ = ⟨(le‘ndx), ≤ ⟩)
102	19	sqxpeqd 5065	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑣 × 𝑣) = (𝑉 × 𝑉))
103	102	oveq1d 6564	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) = ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)))
104	6	fveq1d 6105	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(1st ‘(ℎ‘1))) = (𝐹‘(1st ‘(ℎ‘1))))
105	104	eqeq1d 2612	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ↔ (𝐹‘(1st ‘(ℎ‘1))) = 𝑥))
106	6	fveq1d 6105	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘(2nd ‘(ℎ‘𝑛))))
107	106	eqeq1d 2612	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ↔ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦))
108	6	fveq1d 6105	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(2nd ‘(ℎ‘𝑖))))
109	6	fveq1d 6105	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))
110	108, 109	eqeq12d 2625	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1))))))
111	110	ralbidv 2969	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1))))))
112	105, 107, 111	3anbi123d 1391	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))))
113	103, 112	rabeqbidv 3168	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {ℎ ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} = {ℎ ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))})
114	14	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (dist‘𝑟) = (dist‘𝑅))
115		imasval.e	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 = (dist‘𝑅)
116	114, 115	syl6eqr 2662	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (dist‘𝑟) = 𝐸)
117	116	coeq1d 5205	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((dist‘𝑟) ∘ 𝑔) = (𝐸 ∘ 𝑔))
118	117	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)) = (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))
119	113, 118	mpteq12dv 4663	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))) = (𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))))
120	119	rneqd 5274	. . . . . . . . . . 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 (𝐸 ∘ 𝑔))))
121	120	iuneq2d 4483	. . . . . . . . . 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 (𝐸 ∘ 𝑔))))
122	121	infeq1d 8266	. . . . . . . . 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 (𝐸 ∘ 𝑔))), ℝ*, < ))
123	12, 12, 122	mpt2eq123dv 6615	. . . . . . . 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 (𝐸 ∘ 𝑔))), ℝ*, < )))
124		imasval.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))), ℝ*, < )))
125	124	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝐷 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))), ℝ*, < )))
126	123, 125	eqtr4d 2647	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < )) = 𝐷)
127	126	opeq2d 4347	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(ℎ‘𝑖))) = (𝑓‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩ = ⟨(dist‘ndx), 𝐷⟩)
128	91, 101, 127	tpeq123d 4227	. . . . 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), 𝐷⟩})
129	83, 128	uneq12d 3730	. . . 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), 𝐷⟩}))
130	5, 129	csbied 3526	. . 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), 𝐷⟩}))
131		fof 6028	. . . . 5 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
132	8, 131	syl 17	. . . 4 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
133		fvex 6113	. . . . 5 ⊢ (Base‘𝑅) ∈ V
134	17, 133	syl6eqel 2696	. . . 4 ⊢ (𝜑 → 𝑉 ∈ V)
135		fex 6394	. . . 4 ⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑉 ∈ V) → 𝐹 ∈ V)
136	132, 134, 135	syl2anc 691	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
137		imasval.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑍)
138		elex 3185	. . . 4 ⊢ (𝑅 ∈ 𝑍 → 𝑅 ∈ V)
139	137, 138	syl 17	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
140		tpex 6855	. . . . . 6 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∈ V
141		tpex 6855	. . . . . 6 ⊢ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩} ∈ V
142	140, 141	unex 6854	. . . . 5 ⊢ ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∈ V
143		tpex 6855	. . . . 5 ⊢ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∈ V
144	142, 143	unex 6854	. . . 4 ⊢ (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}) ∈ V
145	144	a1i 11	. . 3 ⊢ (𝜑 → (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}) ∈ V)
146	3, 130, 136, 139, 145	ovmpt2d 6686	. 2 ⊢ (𝜑 → (𝐹 “s 𝑅) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}))
147	1, 146	eqtrd 2644	1 ⊢ (𝜑 → 𝑈 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}))

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  {crab 2900  Vcvv 3173  ⦋csb 3499   ∪ cun 3538  {csn 4125  {ctp 4129  ⟨cop 4131  ∪ ciun 4455   ↦ cmpt 4643   × cxp 5036  ^◡ccnv 5037  ran crn 5039   ∘ ccom 5042  ⟶wf 5800  –onto→wfo 5802  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  1^st c1st 7057  2^nd c2nd 7058   ↑_𝑚 cmap 7744  infcinf 8230  1c1 9816   + caddc 9818  ℝ^*cxr 9952   < clt 9953   − cmin 10145  ℕcn 10897  ...cfz 12197  ndxcnx 15692  Basecbs 15695  +_gcplusg 15768  ._rcmulr 15769  Scalarcsca 15771   ·_𝑠 cvsca 15772  ·_𝑖cip 15773  TopSetcts 15774  lecple 15775  distcds 15777  TopOpenctopn 15905   Σ_g cgsu 15924  ℝ^*_𝑠cxrs 15983   qTop cqtop 15986   “_s cimas 15987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-sup 8231  df-inf 8232  df-imas 15991

This theorem is referenced by:  imasbas  15995  imasds  15996  imasplusg  16000  imasmulr  16001  imassca  16002  imasvsca  16003  imasip  16004  imastset  16005  imasle  16006