Theorem imasval

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)

	Ref	Expression
Hypotheses	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	imasval	⊢ ( 𝜑 → 𝑈 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , ∙ ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ⊗ ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , 𝐼 ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ) )

Proof

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