imasval - Metamath Proof Explorer

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

Theorem imasval 17500

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...𝑛)) ∣ ((𝐹‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 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 17497	. . . 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...𝑛)) ∣ ((𝑓‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝑓‘(1^st ‘(ℎ‘(𝑖 + 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...𝑛)) ∣ ((𝑓‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝑓‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g ((dist‘𝑟) ∘ 𝑔))), ℝ^, < ))⟩})))
4		fvexd 6917	. . . 4 ⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) → (Base‘𝑟) ∈ V)
5		simplrl 775	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑓 = 𝐹)
6	5	rneqd 5944	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = ran 𝐹)
7		imasval.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
8		forn 6819	. . . . . . . . . . 11 ⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵)
9	7, 8	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝐹 = 𝐵)
10	9	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝐹 = 𝐵)
11	6, 10	eqtrd 2768	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = 𝐵)
12	11	opeq2d 4885	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Base‘ndx), ran 𝑓⟩ = ⟨(Base‘ndx), 𝐵⟩)
13		simplrr 776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑟 = 𝑅)
14	13	fveq2d 6906	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘𝑟) = (Base‘𝑅))
15		simpr 483	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = (Base‘𝑟))
16		imasval.v	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 = (Base‘𝑅))
17	16	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑉 = (Base‘𝑅))
18	14, 15, 17	3eqtr4d 2778	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = 𝑉)
19	5	fveq1d 6904	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘𝑝) = (𝐹‘𝑝))
20	5	fveq1d 6904	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘𝑞) = (𝐹‘𝑞))
21	19, 20	opeq12d 4886	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩)
22	13	fveq2d 6906	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+_g‘𝑟) = (+_g‘𝑅))
23		imasval.p	. . . . . . . . . . . . . . . 16 ⊢ + = (+_g‘𝑅)
24	22, 23	eqtr4di 2786	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+_g‘𝑟) = + )
25	24	oveqd 7443	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(+_g‘𝑟)𝑞) = (𝑝 + 𝑞))
26	5, 25	fveq12d 6909	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(+_g‘𝑟)𝑞)) = (𝐹‘(𝑝 + 𝑞)))
27	21, 26	opeq12d 4886	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+_g‘𝑟)𝑞))⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩)
28	27	sneqd 4644	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+_g‘𝑟)𝑞))⟩} = {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
29	18, 28	iuneq12d 5028	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+_g‘𝑟)𝑞))⟩} = ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
30	18, 29	iuneq12d 5028	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+_g‘𝑟)𝑞))⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
31		imasval.a	. . . . . . . . . 10 ⊢ (𝜑 → ✚ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
32	31	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ✚ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
33	30, 32	eqtr4d 2771	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+_g‘𝑟)𝑞))⟩} = ✚ )
34	33	opeq2d 4885	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(+_g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+_g‘𝑟)𝑞))⟩}⟩ = ⟨(+_g‘ndx), ✚ ⟩)
35	13	fveq2d 6906	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (._r‘𝑟) = (._r‘𝑅))
36		imasval.m	. . . . . . . . . . . . . . . 16 ⊢ × = (._r‘𝑅)
37	35, 36	eqtr4di 2786	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (._r‘𝑟) = × )
38	37	oveqd 7443	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(._r‘𝑟)𝑞) = (𝑝 × 𝑞))
39	5, 38	fveq12d 6909	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(._r‘𝑟)𝑞)) = (𝐹‘(𝑝 × 𝑞)))
40	21, 39	opeq12d 4886	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(._r‘𝑟)𝑞))⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩)
41	40	sneqd 4644	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(._r‘𝑟)𝑞))⟩} = {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
42	18, 41	iuneq12d 5028	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(._r‘𝑟)𝑞))⟩} = ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
43	18, 42	iuneq12d 5028	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(._r‘𝑟)𝑞))⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
44		imasval.t	. . . . . . . . . 10 ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
45	44	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
46	43, 45	eqtr4d 2771	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(._r‘𝑟)𝑞))⟩} = ∙ )
47	46	opeq2d 4885	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(._r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(._r‘𝑟)𝑞))⟩}⟩ = ⟨(._r‘ndx), ∙ ⟩)
48	12, 34, 47	tpeq123d 4757	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Base‘ndx), ran 𝑓⟩, ⟨(+_g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+_g‘𝑟)𝑞))⟩}⟩, ⟨(._r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(._r‘𝑟)𝑞))⟩}⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), ✚ ⟩, ⟨(._r‘ndx), ∙ ⟩})
49	13	fveq2d 6906	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Scalar‘𝑟) = (Scalar‘𝑅))
50		imasval.g	. . . . . . . . 9 ⊢ 𝐺 = (Scalar‘𝑅)
51	49, 50	eqtr4di 2786	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Scalar‘𝑟) = 𝐺)
52	51	opeq2d 4885	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Scalar‘ndx), (Scalar‘𝑟)⟩ = ⟨(Scalar‘ndx), 𝐺⟩)
53	51	fveq2d 6906	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘(Scalar‘𝑟)) = (Base‘𝐺))
54		imasval.k	. . . . . . . . . . . 12 ⊢ 𝐾 = (Base‘𝐺)
55	53, 54	eqtr4di 2786	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘(Scalar‘𝑟)) = 𝐾)
56	20	sneqd 4644	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {(𝑓‘𝑞)} = {(𝐹‘𝑞)})
57	13	fveq2d 6906	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ( ·_𝑠 ‘𝑟) = ( ·_𝑠 ‘𝑅))
58		imasval.q	. . . . . . . . . . . . . 14 ⊢ · = ( ·_𝑠 ‘𝑅)
59	57, 58	eqtr4di 2786	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ( ·_𝑠 ‘𝑟) = · )
60	59	oveqd 7443	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝( ·_𝑠 ‘𝑟)𝑞) = (𝑝 · 𝑞))
61	5, 60	fveq12d 6909	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝( ·_𝑠 ‘𝑟)𝑞)) = (𝐹‘(𝑝 · 𝑞)))
62	55, 56, 61	mpoeq123dv 7501	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·_𝑠 ‘𝑟)𝑞))) = (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
63	62	iuneq2d 5029	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·_𝑠 ‘𝑟)𝑞))) = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
64	18	iuneq1d 5027	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·_𝑠 ‘𝑟)𝑞))) = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·_𝑠 ‘𝑟)𝑞))))
65		imasval.s	. . . . . . . . . 10 ⊢ (𝜑 → ⊗ = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
66	65	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⊗ = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
67	63, 64, 66	3eqtr4d 2778	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·_𝑠 ‘𝑟)𝑞))) = ⊗ )
68	67	opeq2d 4885	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨( ·_𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·_𝑠 ‘𝑟)𝑞)))⟩ = ⟨( ·_𝑠 ‘ndx), ⊗ ⟩)
69	13	fveq2d 6906	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (·_𝑖‘𝑟) = (·_𝑖‘𝑅))
70		imasval.i	. . . . . . . . . . . . . . 15 ⊢ , = (·_𝑖‘𝑅)
71	69, 70	eqtr4di 2786	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (·_𝑖‘𝑟) = , )
72	71	oveqd 7443	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(·_𝑖‘𝑟)𝑞) = (𝑝 , 𝑞))
73	21, 72	opeq12d 4886	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·_𝑖‘𝑟)𝑞)⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩)
74	73	sneqd 4644	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·_𝑖‘𝑟)𝑞)⟩} = {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
75	18, 74	iuneq12d 5028	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·_𝑖‘𝑟)𝑞)⟩} = ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
76	18, 75	iuneq12d 5028	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·_𝑖‘𝑟)𝑞)⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
77		imasval.w	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
78	77	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝐼 = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
79	76, 78	eqtr4d 2771	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·_𝑖‘𝑟)𝑞)⟩} = 𝐼)
80	79	opeq2d 4885	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(·_𝑖‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·_𝑖‘𝑟)𝑞)⟩}⟩ = ⟨(·_𝑖‘ndx), 𝐼⟩)
81	52, 68, 80	tpeq123d 4757	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·_𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓‘𝑞)} ↦ (𝑓‘(𝑝( ·_𝑠 ‘𝑟)𝑞)))⟩, ⟨(·_𝑖‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑝(·_𝑖‘𝑟)𝑞)⟩}⟩} = {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·_𝑠 ‘ndx), ⊗ ⟩, ⟨(·_𝑖‘ndx), 𝐼⟩})
82	48, 81	uneq12d 4165	. . . . 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 6906	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (TopOpen‘𝑟) = (TopOpen‘𝑅))
84		imasval.j	. . . . . . . . . 10 ⊢ 𝐽 = (TopOpen‘𝑅)
85	83, 84	eqtr4di 2786	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (TopOpen‘𝑟) = 𝐽)
86	85, 5	oveq12d 7444	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((TopOpen‘𝑟) qTop 𝑓) = (𝐽 qTop 𝐹))
87		imasval.o	. . . . . . . . 9 ⊢ (𝜑 → 𝑂 = (𝐽 qTop 𝐹))
88	87	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑂 = (𝐽 qTop 𝐹))
89	86, 88	eqtr4d 2771	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((TopOpen‘𝑟) qTop 𝑓) = 𝑂)
90	89	opeq2d 4885	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩ = ⟨(TopSet‘ndx), 𝑂⟩)
91	13	fveq2d 6906	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (le‘𝑟) = (le‘𝑅))
92		imasval.n	. . . . . . . . . . 11 ⊢ 𝑁 = (le‘𝑅)
93	91, 92	eqtr4di 2786	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (le‘𝑟) = 𝑁)
94	5, 93	coeq12d 5871	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓 ∘ (le‘𝑟)) = (𝐹 ∘ 𝑁))
95	5	cnveqd 5882	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ^◡𝑓 = ^◡𝐹)
96	94, 95	coeq12d 5871	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓 ∘ (le‘𝑟)) ∘ ^◡𝑓) = ((𝐹 ∘ 𝑁) ∘ ^◡𝐹))
97		imasval.l	. . . . . . . . 9 ⊢ (𝜑 → ≤ = ((𝐹 ∘ 𝑁) ∘ ^◡𝐹))
98	97	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ≤ = ((𝐹 ∘ 𝑁) ∘ ^◡𝐹))
99	96, 98	eqtr4d 2771	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓 ∘ (le‘𝑟)) ∘ ^◡𝑓) = ≤ )
100	99	opeq2d 4885	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ ^◡𝑓)⟩ = ⟨(le‘ndx), ≤ ⟩)
101	18	sqxpeqd 5714	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑣 × 𝑣) = (𝑉 × 𝑉))
102	101	oveq1d 7441	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑣 × 𝑣) ↑_m (1...𝑛)) = ((𝑉 × 𝑉) ↑_m (1...𝑛)))
103	5	fveq1d 6904	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(1^st ‘(ℎ‘1))) = (𝐹‘(1^st ‘(ℎ‘1))))
104	103	eqeq1d 2730	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(1^st ‘(ℎ‘1))) = 𝑥 ↔ (𝐹‘(1^st ‘(ℎ‘1))) = 𝑥))
105	5	fveq1d 6904	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(2^nd ‘(ℎ‘𝑛))) = (𝐹‘(2^nd ‘(ℎ‘𝑛))))
106	105	eqeq1d 2730	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ↔ (𝐹‘(2^nd ‘(ℎ‘𝑛))) = 𝑦))
107	5	fveq1d 6904	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(2^nd ‘(ℎ‘𝑖))))
108	5	fveq1d 6904	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(1^st ‘(ℎ‘(𝑖 + 1)))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1)))))
109	107, 108	eqeq12d 2744	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝑓‘(1^st ‘(ℎ‘(𝑖 + 1)))) ↔ (𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1))))))
110	109	ralbidv 3175	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝑓‘(1^st ‘(ℎ‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1))))))
111	104, 106, 110	3anbi123d 1432	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (((𝑓‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝑓‘(1^st ‘(ℎ‘(𝑖 + 1))))) ↔ ((𝐹‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1)))))))
112	102, 111	rabeqbidv 3448	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {ℎ ∈ ((𝑣 × 𝑣) ↑_m (1...𝑛)) ∣ ((𝑓‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝑓‘(1^st ‘(ℎ‘(𝑖 + 1)))))} = {ℎ ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛)) ∣ ((𝐹‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1)))))})
113	13	fveq2d 6906	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (dist‘𝑟) = (dist‘𝑅))
114		imasval.e	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 = (dist‘𝑅)
115	113, 114	eqtr4di 2786	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (dist‘𝑟) = 𝐸)
116	115	coeq1d 5868	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((dist‘𝑟) ∘ 𝑔) = (𝐸 ∘ 𝑔))
117	116	oveq2d 7442	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (ℝ^_𝑠 Σ_g ((dist‘𝑟) ∘ 𝑔)) = (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔)))
118	112, 117	mpteq12dv 5243	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑_m (1...𝑛)) ∣ ((𝑓‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝑓‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g ((dist‘𝑟) ∘ 𝑔))) = (𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛)) ∣ ((𝐹‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))))
119	118	rneqd 5944	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑_m (1...𝑛)) ∣ ((𝑓‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝑓‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g ((dist‘𝑟) ∘ 𝑔))) = ran (𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛)) ∣ ((𝐹‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))))
120	119	iuneq2d 5029	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑_m (1...𝑛)) ∣ ((𝑓‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝑓‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g ((dist‘𝑟) ∘ 𝑔))) = ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛)) ∣ ((𝐹‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))))
121	120	infeq1d 9508	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑_m (1...𝑛)) ∣ ((𝑓‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝑓‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g ((dist‘𝑟) ∘ 𝑔))), ℝ^, < ) = inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛)) ∣ ((𝐹‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))), ℝ^, < ))
122	11, 11, 121	mpoeq123dv 7501	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑_m (1...𝑛)) ∣ ((𝑓‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝑓‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g ((dist‘𝑟) ∘ 𝑔))), ℝ^, < )) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛)) ∣ ((𝐹‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))), ℝ^, < )))
123		imasval.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛)) ∣ ((𝐹‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))), ℝ^, < )))
124	123	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝐷 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑_m (1...𝑛)) ∣ ((𝐹‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2^nd ‘(ℎ‘𝑖))) = (𝐹‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g (𝐸 ∘ 𝑔))), ℝ^, < )))
125	122, 124	eqtr4d 2771	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑_m (1...𝑛)) ∣ ((𝑓‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝑓‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g ((dist‘𝑟) ∘ 𝑔))), ℝ^, < )) = 𝐷)
126	125	opeq2d 4885	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑_m (1...𝑛)) ∣ ((𝑓‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝑓‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g ((dist‘𝑟) ∘ 𝑔))), ℝ^, < ))⟩ = ⟨(dist‘ndx), 𝐷⟩)
127	90, 100, 126	tpeq123d 4757	. . . . 5 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩, ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ ^◡𝑓)⟩, ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑣 × 𝑣) ↑_m (1...𝑛)) ∣ ((𝑓‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝑓‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g ((dist‘𝑟) ∘ 𝑔))), ℝ^, < ))⟩} = {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩})
128	82, 127	uneq12d 4165	. . . 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...𝑛)) ∣ ((𝑓‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝑓‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g ((dist‘𝑟) ∘ 𝑔))), ℝ^, < ))⟩}) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), ✚ ⟩, ⟨(._r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·_𝑠 ‘ndx), ⊗ ⟩, ⟨(·_𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}))
129	4, 128	csbied 3932	. . 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...𝑛)) ∣ ((𝑓‘(1^st ‘(ℎ‘1))) = 𝑥 ∧ (𝑓‘(2^nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2^nd ‘(ℎ‘𝑖))) = (𝑓‘(1^st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ^_𝑠 Σ_g ((dist‘𝑟) ∘ 𝑔))), ℝ^, < ))⟩}) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), ✚ ⟩, ⟨(._r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·_𝑠 ‘ndx), ⊗ ⟩, ⟨(·_𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}))
130		fof 6816	. . . . 5 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
131	7, 130	syl 17	. . . 4 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
132		fvex 6915	. . . . 5 ⊢ (Base‘𝑅) ∈ V
133	16, 132	eqeltrdi 2837	. . . 4 ⊢ (𝜑 → 𝑉 ∈ V)
134	131, 133	fexd 7245	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
135		imasval.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑍)
136	135	elexd 3494	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
137		tpex 7755	. . . . . 6 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), ✚ ⟩, ⟨(._r‘ndx), ∙ ⟩} ∈ V
138		tpex 7755	. . . . . 6 ⊢ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·_𝑠 ‘ndx), ⊗ ⟩, ⟨(·_𝑖‘ndx), 𝐼⟩} ∈ V
139	137, 138	unex 7754	. . . . 5 ⊢ ({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), ✚ ⟩, ⟨(._r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·_𝑠 ‘ndx), ⊗ ⟩, ⟨(·_𝑖‘ndx), 𝐼⟩}) ∈ V
140		tpex 7755	. . . . 5 ⊢ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∈ V
141	139, 140	unex 7754	. . . 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 7579	. 2 ⊢ (𝜑 → (𝐹 “_s 𝑅) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), ✚ ⟩, ⟨(._r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·_𝑠 ‘ndx), ⊗ ⟩, ⟨(·_𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}))
144	1, 143	eqtrd 2768	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 394 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ∀wral 3058 {crab 3430 Vcvv 3473 ⦋csb 3894 ∪ cun 3947 {csn 4632 {ctp 4636 ⟨cop 4638 ∪ ciun 5000 ↦ cmpt 5235 × cxp 5680 ^◡ccnv 5681 ran crn 5683 ∘ ccom 5686 ⟶wf 6549 –onto→wfo 6551 ‘cfv 6553 (class class class)co 7426 ∈ cmpo 7428 1^st c1st 7997 2^nd c2nd 7998 ↑_m cmap 8851 infcinf 9472 1c1 11147 + caddc 11149 ℝ^*cxr 11285 < clt 11286 − cmin 11482 ℕcn 12250 ...cfz 13524 ndxcnx 17169 Basecbs 17187 +_gcplusg 17240 ._rcmulr 17241 Scalarcsca 17243 ·_𝑠 cvsca 17244 ·_𝑖cip 17245 TopSetcts 17246 lecple 17247 distcds 17249 TopOpenctopn 17410 Σ_g cgsu 17429 ℝ^*_𝑠cxrs 17489 qTop cqtop 17492 “_s cimas 17493

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2699 ax-rep 5289 ax-sep 5303 ax-nul 5310 ax-pr 5433 ax-un 7746

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2529 df-eu 2558 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2938 df-ral 3059 df-rex 3068 df-reu 3375 df-rab 3431 df-v 3475 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4327 df-if 4533 df-sn 4633 df-pr 4635 df-tp 4637 df-op 4639 df-uni 4913 df-iun 5002 df-br 5153 df-opab 5215 df-mpt 5236 df-id 5580 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-iota 6505 df-fun 6555 df-fn 6556 df-f 6557 df-f1 6558 df-fo 6559 df-f1o 6560 df-fv 6561 df-ov 7429 df-oprab 7430 df-mpo 7431 df-sup 9473 df-inf 9474 df-imas 17497

This theorem is referenced by: imasbas 17501 imasds 17502 imasplusg 17506 imasmulr 17507 imassca 17508 imasvsca 17509 imasip 17510 imastset 17511 imasle 17512

W3C validator