Metamath Proof Explorer

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 ) , 𝐷 ⟩ } ) )