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