This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psrval

Description: Value of the multivariate power series structure. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses psrval.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrval.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
psrval.a ⊢ + = ( +g ‘ 𝑅 )
psrval.m ⊢ · = ( .r ‘ 𝑅 )
psrval.o ⊢ 𝑂 = ( TopOpen ‘ 𝑅 )
psrval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
psrval.b ⊢ ( 𝜑 → 𝐵 = ( 𝐾 ↑m 𝐷 ) )
psrval.p ⊢ ✚ = ( ∘f + ↾ ( 𝐵 × 𝐵 ) )
psrval.t ⊢ × = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
psrval.v ⊢ ∙ = ( 𝑥 ∈ 𝐾 , 𝑓 ∈ 𝐵 ↦ ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) )
psrval.j ⊢ ( 𝜑 → 𝐽 = ( ∏t ‘ ( 𝐷 × { 𝑂 } ) ) )
psrval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
psrval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
Assertion psrval ( 𝜑 → 𝑆 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )

Proof

Step Hyp Ref Expression
1 psrval.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrval.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
3 psrval.a ⊢ + = ( +g ‘ 𝑅 )
4 psrval.m ⊢ · = ( .r ‘ 𝑅 )
5 psrval.o ⊢ 𝑂 = ( TopOpen ‘ 𝑅 )
6 psrval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
7 psrval.b ⊢ ( 𝜑 → 𝐵 = ( 𝐾 ↑m 𝐷 ) )
8 psrval.p ⊢ ✚ = ( ∘f + ↾ ( 𝐵 × 𝐵 ) )
9 psrval.t ⊢ × = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
10 psrval.v ⊢ ∙ = ( 𝑥 ∈ 𝐾 , 𝑓 ∈ 𝐵 ↦ ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) )
11 psrval.j ⊢ ( 𝜑 → 𝐽 = ( ∏t ‘ ( 𝐷 × { 𝑂 } ) ) )
12 psrval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
13 psrval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
14 df-psr ⊢ mPwSer = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ⦋ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ⦌ ⦋ ( ( Base ‘ 𝑟 ) ↑m 𝑑 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } ) )
15 14 a1i ⊢ ( 𝜑 → mPwSer = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ⦋ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ⦌ ⦋ ( ( Base ‘ 𝑟 ) ↑m 𝑑 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } ) ) )
16 simprl ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) → 𝑖 = 𝐼 )
17 16 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) → ( ℕ0 ↑m 𝑖 ) = ( ℕ0 ↑m 𝐼 ) )
18 rabeq ⊢ ( ( ℕ0 ↑m 𝑖 ) = ( ℕ0 ↑m 𝐼 ) → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
19 17 18 syl ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
20 19 6 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = 𝐷 )
21 20 csbeq1d ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) → ⦋ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ⦌ ⦋ ( ( Base ‘ 𝑟 ) ↑m 𝑑 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } ) = ⦋ 𝐷 / 𝑑 ⦌ ⦋ ( ( Base ‘ 𝑟 ) ↑m 𝑑 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } ) )
22 ovex ⊢ ( ℕ0 ↑m 𝑖 ) ∈ V
23 22 rabex ⊢ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V
24 20 23 eqeltrrdi ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) → 𝐷 ∈ V )
25 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) → 𝑟 = 𝑅 )
26 25 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
27 26 2 eqtr4di ⊢ ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑟 ) = 𝐾 )
28 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
29 27 28 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) → ( ( Base ‘ 𝑟 ) ↑m 𝑑 ) = ( 𝐾 ↑m 𝐷 ) )
30 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) → 𝐵 = ( 𝐾 ↑m 𝐷 ) )
31 29 30 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) → ( ( Base ‘ 𝑟 ) ↑m 𝑑 ) = 𝐵 )
32 31 csbeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) → ⦋ ( ( Base ‘ 𝑟 ) ↑m 𝑑 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } ) = ⦋ 𝐵 / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } ) )
33 ovex ⊢ ( ( Base ‘ 𝑟 ) ↑m 𝑑 ) ∈ V
34 31 33 eqeltrrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) → 𝐵 ∈ V )
35 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
36 35 opeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ )
37 25 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → 𝑟 = 𝑅 )
38 37 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑟 ) = ( +g ‘ 𝑅 ) )
39 38 3 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑟 ) = + )
40 39 ofeqd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ∘f ( +g ‘ 𝑟 ) = ∘f + )
41 35 35 xpeq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑏 × 𝑏 ) = ( 𝐵 × 𝐵 ) )
42 40 41 reseq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) = ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) )
43 42 8 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) = ✚ )
44 43 opeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ = ⟨ ( +g ‘ ndx ) , ✚ ⟩ )
45 28 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → 𝑑 = 𝐷 )
46 rabeq ⊢ ( 𝑑 = 𝐷 → { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
47 45 46 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
48 37 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) )
49 48 4 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( .r ‘ 𝑟 ) = · )
50 49 oveqd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
51 47 50 mpteq12dv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
52 37 51 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) )
53 45 52 mpteq12dv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
54 35 35 53 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) )
55 54 9 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) = × )
56 55 opeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ = ⟨ ( .r ‘ ndx ) , × ⟩ )
57 36 44 56 tpeq123d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } )
58 37 opeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ = ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ )
59 27 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( Base ‘ 𝑟 ) = 𝐾 )
60 49 ofeqd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ∘f ( .r ‘ 𝑟 ) = ∘f · )
61 45 xpeq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑑 × { 𝑥 } ) = ( 𝐷 × { 𝑥 } ) )
62 eqidd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → 𝑓 = 𝑓 )
63 60 61 62 oveq123d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) = ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) )
64 59 35 63 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) = ( 𝑥 ∈ 𝐾 , 𝑓 ∈ 𝐵 ↦ ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) ) )
65 64 10 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) = ∙ )
66 65 opeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ = ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ )
67 37 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( TopOpen ‘ 𝑟 ) = ( TopOpen ‘ 𝑅 ) )
68 67 5 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( TopOpen ‘ 𝑟 ) = 𝑂 )
69 68 sneqd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → { ( TopOpen ‘ 𝑟 ) } = { 𝑂 } )
70 45 69 xpeq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) = ( 𝐷 × { 𝑂 } ) )
71 70 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) = ( ∏t ‘ ( 𝐷 × { 𝑂 } ) ) )
72 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → 𝐽 = ( ∏t ‘ ( 𝐷 × { 𝑂 } ) ) )
73 71 72 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) = 𝐽 )
74 73 opeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ = ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ )
75 58 66 74 tpeq123d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } = { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
76 57 75 uneq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )
77 34 76 csbied ⊢ ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) → ⦋ 𝐵 / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )
78 32 77 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) → ⦋ ( ( Base ‘ 𝑟 ) ↑m 𝑑 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )
79 24 78 csbied ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) → ⦋ 𝐷 / 𝑑 ⦌ ⦋ ( ( Base ‘ 𝑟 ) ↑m 𝑑 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )
80 21 79 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) → ⦋ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ⦌ ⦋ ( ( Base ‘ 𝑟 ) ↑m 𝑑 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )
81 12 elexd ⊢ ( 𝜑 → 𝐼 ∈ V )
82 13 elexd ⊢ ( 𝜑 → 𝑅 ∈ V )
83 tpex ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∈ V
84 tpex ⊢ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ∈ V
85 83 84 unex ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) ∈ V
86 85 a1i ⊢ ( 𝜑 → ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) ∈ V )
87 15 80 81 82 86 ovmpod ⊢ ( 𝜑 → ( 𝐼 mPwSer 𝑅 ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )
88 1 87 eqtrid ⊢ ( 𝜑 → 𝑆 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )