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 ofeq ⊢ ( ( +g ‘ 𝑟 ) = + → ∘f ( +g ‘ 𝑟 ) = ∘f + )
41 39 40 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ∘f ( +g ‘ 𝑟 ) = ∘f + )
42 35 35 xpeq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑏 × 𝑏 ) = ( 𝐵 × 𝐵 ) )
43 41 42 reseq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) = ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) )
44 43 8 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) = ✚ )
45 44 opeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ = ⟨ ( +g ‘ ndx ) , ✚ ⟩ )
46 28 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → 𝑑 = 𝐷 )
47 rabeq ⊢ ( 𝑑 = 𝐷 → { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
48 46 47 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
49 37 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) )
50 49 4 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( .r ‘ 𝑟 ) = · )
51 50 oveqd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
52 48 51 mpteq12dv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) )
53 37 52 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) )
54 46 53 mpteq12dv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
55 35 35 54 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) )
56 55 9 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) = × )
57 56 opeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ = ⟨ ( .r ‘ ndx ) , × ⟩ )
58 36 45 57 tpeq123d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f ( +g ‘ 𝑟 ) ↾ ( 𝑏 × 𝑏 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝑏 , 𝑔 ∈ 𝑏 ↦ ( 𝑘 ∈ 𝑑 ↦ ( 𝑟 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑟 ) ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } )
59 37 opeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ = ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ )
60 27 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( Base ‘ 𝑟 ) = 𝐾 )
61 ofeq ⊢ ( ( .r ‘ 𝑟 ) = · → ∘f ( .r ‘ 𝑟 ) = ∘f · )
62 50 61 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ∘f ( .r ‘ 𝑟 ) = ∘f · )
63 46 xpeq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑑 × { 𝑥 } ) = ( 𝐷 × { 𝑥 } ) )
64 eqidd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → 𝑓 = 𝑓 )
65 62 63 64 oveq123d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) = ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) )
66 60 35 65 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) = ( 𝑥 ∈ 𝐾 , 𝑓 ∈ 𝐵 ↦ ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) ) )
67 66 10 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) = ∙ )
68 67 opeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ = ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ )
69 37 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( TopOpen ‘ 𝑟 ) = ( TopOpen ‘ 𝑅 ) )
70 69 5 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( TopOpen ‘ 𝑟 ) = 𝑂 )
71 70 sneqd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → { ( TopOpen ‘ 𝑟 ) } = { 𝑂 } )
72 46 71 xpeq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) = ( 𝐷 × { 𝑂 } ) )
73 72 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) = ( ∏t ‘ ( 𝐷 × { 𝑂 } ) ) )
74 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → 𝐽 = ( ∏t ‘ ( 𝐷 × { 𝑂 } ) ) )
75 73 74 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) = 𝐽 )
76 75 opeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ = ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ )
77 59 68 76 tpeq123d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → { ⟨ ( Scalar ‘ ndx ) , 𝑟 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑓 ∈ 𝑏 ↦ ( ( 𝑑 × { 𝑥 } ) ∘f ( .r ‘ 𝑟 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝑑 × { ( TopOpen ‘ 𝑟 ) } ) ) ⟩ } = { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } )
78 58 77 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 ) , 𝐽 ⟩ } ) )
79 34 78 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 ) , 𝐽 ⟩ } ) )
80 32 79 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 ) , 𝐽 ⟩ } ) )
81 24 80 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 ) , 𝐽 ⟩ } ) )
82 21 81 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 ) , 𝐽 ⟩ } ) )
83 12 elexd ⊢ ( 𝜑 → 𝐼 ∈ V )
84 13 elexd ⊢ ( 𝜑 → 𝑅 ∈ V )
85 tpex ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∈ V
86 tpex ⊢ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ∈ V
87 85 86 unex ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) ∈ V
88 87 a1i ⊢ ( 𝜑 → ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) ∈ V )
89 15 82 83 84 88 ovmpod ⊢ ( 𝜑 → ( 𝐼 mPwSer 𝑅 ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )
90 1 89 syl5eq ⊢ ( 𝜑 → 𝑆 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ✚ ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∙ ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ) )