Theorem psrval 14638

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

Hypotheses

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

Assertion

Ref	Expression
psrval	⊢ (𝜑 → 𝑆 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩}))

Distinct variable groups:   𝑦,ℎ   𝑓,𝑔,𝑘,𝑥,𝜑   𝐵,𝑓,𝑔,𝑘,𝑥   𝑓,ℎ,𝐼,𝑔,𝑘,𝑥   𝑅,𝑓,𝑔,𝑘,𝑥   𝑦,𝑓,𝐷,𝑔,𝑘,𝑥   𝑓,𝐾,𝑥

Allowed substitution hints:   𝜑(𝑦,ℎ)   𝐵(𝑦,ℎ)   𝐷(ℎ)   + (𝑥,𝑦,𝑓,𝑔,ℎ,𝑘)   ✚ (𝑥,𝑦,𝑓,𝑔,ℎ,𝑘)   𝑅(𝑦,ℎ)   𝑆(𝑥,𝑦,𝑓,𝑔,ℎ,𝑘)   ∙ (𝑥,𝑦,𝑓,𝑔,ℎ,𝑘)   · (𝑥,𝑦,𝑓,𝑔,ℎ,𝑘)   × (𝑥,𝑦,𝑓,𝑔,ℎ,𝑘)   𝐼(𝑦)   𝐽(𝑥,𝑦,𝑓,𝑔,ℎ,𝑘)   𝐾(𝑦,𝑔,ℎ,𝑘)   𝑂(𝑥,𝑦,𝑓,𝑔,ℎ,𝑘)   𝑊(𝑥,𝑦,𝑓,𝑔,ℎ,𝑘)   𝑋(𝑥,𝑦,𝑓,𝑔,ℎ,𝑘)

Proof of Theorem psrval

Dummy variables 𝑖 𝑟 𝑏 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		psrval.s	. 2 ⊢ 𝑆 = (𝐼 mPwSer 𝑅)
2		df-psr 14635	. . . 4 ⊢ mPwSer = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋{ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}))
3	2	a1i 9	. . 3 ⊢ (𝜑 → mPwSer = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋{ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩})))
4		simprl 529	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → 𝑖 = 𝐼)
5	4	oveq2d 6023	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → (ℕ0 ↑𝑚 𝑖) = (ℕ0 ↑𝑚 𝐼))
6	5	rabeqdv 2793	. . . . . 6 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin})
7		psrval.d	. . . . . 6 ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
8	6, 7	eqtr4di 2280	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} = 𝐷)
9	8	csbeq1d 3131	. . . 4 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → ⦋{ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}) = ⦋𝐷 / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}))
10		nn0ex 9383	. . . . . . . . 9 ⊢ ℕ0 ∈ V
11		vex 2802	. . . . . . . . 9 ⊢ 𝑖 ∈ V
12	10, 11	mapval 6815	. . . . . . . 8 ⊢ (ℕ0 ↑𝑚 𝑖) = {𝑓 ∣ 𝑓:𝑖⟶ℕ0}
13		mapex 6809	. . . . . . . . 9 ⊢ ((𝑖 ∈ V ∧ ℕ0 ∈ V) → {𝑓 ∣ 𝑓:𝑖⟶ℕ0} ∈ V)
14	11, 10, 13	mp2an 426	. . . . . . . 8 ⊢ {𝑓 ∣ 𝑓:𝑖⟶ℕ0} ∈ V
15	12, 14	eqeltri 2302	. . . . . . 7 ⊢ (ℕ0 ↑𝑚 𝑖) ∈ V
16	15	rabex 4228	. . . . . 6 ⊢ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈ V
17	8, 16	eqeltrrdi 2321	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → 𝐷 ∈ V)
18		simplrr 536	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝑟 = 𝑅)
19	18	fveq2d 5633	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → (Base‘𝑟) = (Base‘𝑅))
20		psrval.k	. . . . . . . . . 10 ⊢ 𝐾 = (Base‘𝑅)
21	19, 20	eqtr4di 2280	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → (Base‘𝑟) = 𝐾)
22		simpr 110	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷)
23	21, 22	oveq12d 6025	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → ((Base‘𝑟) ↑𝑚 𝑑) = (𝐾 ↑𝑚 𝐷))
24		psrval.b	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 = (𝐾 ↑𝑚 𝐷))
25	24	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝐵 = (𝐾 ↑𝑚 𝐷))
26	23, 25	eqtr4d 2265	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → ((Base‘𝑟) ↑𝑚 𝑑) = 𝐵)
27	26	csbeq1d 3131	. . . . . 6 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → ⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}) = ⦋𝐵 / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}))
28		basfn 13099	. . . . . . . . . . 11 ⊢ Base Fn V
29		vex 2802	. . . . . . . . . . 11 ⊢ 𝑟 ∈ V
30		funfvex 5646	. . . . . . . . . . . 12 ⊢ ((Fun Base ∧ 𝑟 ∈ dom Base) → (Base‘𝑟) ∈ V)
31	30	funfni 5423	. . . . . . . . . . 11 ⊢ ((Base Fn V ∧ 𝑟 ∈ V) → (Base‘𝑟) ∈ V)
32	28, 29, 31	mp2an 426	. . . . . . . . . 10 ⊢ (Base‘𝑟) ∈ V
33		vex 2802	. . . . . . . . . 10 ⊢ 𝑑 ∈ V
34	32, 33	mapval 6815	. . . . . . . . 9 ⊢ ((Base‘𝑟) ↑𝑚 𝑑) = {𝑓 ∣ 𝑓:𝑑⟶(Base‘𝑟)}
35		mapex 6809	. . . . . . . . . 10 ⊢ ((𝑑 ∈ V ∧ (Base‘𝑟) ∈ V) → {𝑓 ∣ 𝑓:𝑑⟶(Base‘𝑟)} ∈ V)
36	33, 32, 35	mp2an 426	. . . . . . . . 9 ⊢ {𝑓 ∣ 𝑓:𝑑⟶(Base‘𝑟)} ∈ V
37	34, 36	eqeltri 2302	. . . . . . . 8 ⊢ ((Base‘𝑟) ↑𝑚 𝑑) ∈ V
38	26, 37	eqeltrrdi 2321	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝐵 ∈ V)
39		simpr 110	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
40	39	opeq2d 3864	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(Base‘ndx), 𝑏⟩ = ⟨(Base‘ndx), 𝐵⟩)
41	18	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑟 = 𝑅)
42	41	fveq2d 5633	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (+g‘𝑟) = (+g‘𝑅))
43		psrval.a	. . . . . . . . . . . . . 14 ⊢ + = (+g‘𝑅)
44	42, 43	eqtr4di 2280	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (+g‘𝑟) = + )
45	44	ofeqd 6226	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ∘𝑓 (+g‘𝑟) = ∘𝑓 + )
46	39, 39	xpeq12d 4744	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵))
47	45, 46	reseq12d 5006	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏)) = ( ∘𝑓 + ↾ (𝐵 × 𝐵)))
48		psrval.p	. . . . . . . . . . 11 ⊢ ✚ = ( ∘𝑓 + ↾ (𝐵 × 𝐵))
49	47, 48	eqtr4di 2280	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏)) = ✚ )
50	49	opeq2d 3864	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩ = ⟨(+g‘ndx), ✚ ⟩)
51	22	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑑 = 𝐷)
52	51	rabeqdv 2793	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘})
53	41	fveq2d 5633	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (.r‘𝑟) = (.r‘𝑅))
54		psrval.m	. . . . . . . . . . . . . . . . 17 ⊢ · = (.r‘𝑅)
55	53, 54	eqtr4di 2280	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (.r‘𝑟) = · )
56	55	oveqd 6024	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥))) = ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))
57	52, 56	mpteq12dv 4166	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))
58	41, 57	oveq12d 6025	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥))))) = (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))
59	51, 58	mpteq12dv 4166	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))
60	39, 39, 59	mpoeq123dv 6072	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥))))))))
61		psrval.t	. . . . . . . . . . 11 ⊢ × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))
62	60, 61	eqtr4di 2280	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥))))))) = × )
63	62	opeq2d 3864	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩ = ⟨(.r‘ndx), × ⟩)
64	40, 50, 63	tpeq123d 3758	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩})
65	41	opeq2d 3864	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(Scalar‘ndx), 𝑟⟩ = ⟨(Scalar‘ndx), 𝑅⟩)
66	21	adantr 276	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (Base‘𝑟) = 𝐾)
67	55	ofeqd 6226	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ∘𝑓 (.r‘𝑟) = ∘𝑓 · )
68	51	xpeq1d 4742	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑑 × {𝑥}) = (𝐷 × {𝑥}))
69		eqidd 2230	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑓 = 𝑓)
70	67, 68, 69	oveq123d 6028	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓) = ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))
71	66, 39, 70	mpoeq123dv 6072	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓)) = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓)))
72		psrval.v	. . . . . . . . . . 11 ⊢ ∙ = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘𝑓 · 𝑓))
73	71, 72	eqtr4di 2280	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓)) = ∙ )
74	73	opeq2d 3864	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩ = ⟨( ·𝑠 ‘ndx), ∙ ⟩)
75	41	fveq2d 5633	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (TopOpen‘𝑟) = (TopOpen‘𝑅))
76		psrval.o	. . . . . . . . . . . . . . 15 ⊢ 𝑂 = (TopOpen‘𝑅)
77	75, 76	eqtr4di 2280	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (TopOpen‘𝑟) = 𝑂)
78	77	sneqd 3679	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {(TopOpen‘𝑟)} = {𝑂})
79	51, 78	xpeq12d 4744	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑑 × {(TopOpen‘𝑟)}) = (𝐷 × {𝑂}))
80	79	fveq2d 5633	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (∏t‘(𝑑 × {(TopOpen‘𝑟)})) = (∏t‘(𝐷 × {𝑂})))
81		psrval.j	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 = (∏t‘(𝐷 × {𝑂})))
82	81	ad3antrrr 492	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝐽 = (∏t‘(𝐷 × {𝑂})))
83	80, 82	eqtr4d 2265	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (∏t‘(𝑑 × {(TopOpen‘𝑟)})) = 𝐽)
84	83	opeq2d 3864	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩ = ⟨(TopSet‘ndx), 𝐽⟩)
85	65, 74, 84	tpeq123d 3758	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩} = {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩})
86	64, 85	uneq12d 3359	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩}))
87	38, 86	csbied 3171	. . . . . 6 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → ⦋𝐵 / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩}))
88	27, 87	eqtrd 2262	. . . . 5 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → ⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩}))
89	17, 88	csbied 3171	. . . 4 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → ⦋𝐷 / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩}))
90	9, 89	eqtrd 2262	. . 3 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → ⦋{ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑𝑚 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘𝑟 ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘𝑓 − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘𝑓 (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩}))
91		psrval.i	. . . 4 ⊢ (𝜑 → 𝐼 ∈ 𝑊)
92	91	elexd 2813	. . 3 ⊢ (𝜑 → 𝐼 ∈ V)
93		psrval.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑋)
94	93	elexd 2813	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
95		basendxnn 13096	. . . . . 6 ⊢ (Base‘ndx) ∈ ℕ
96		funfvex 5646	. . . . . . . . . . . 12 ⊢ ((Fun Base ∧ 𝑅 ∈ dom Base) → (Base‘𝑅) ∈ V)
97	96	funfni 5423	. . . . . . . . . . 11 ⊢ ((Base Fn V ∧ 𝑅 ∈ V) → (Base‘𝑅) ∈ V)
98	28, 94, 97	sylancr 414	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝑅) ∈ V)
99	20, 98	eqeltrid 2316	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ V)
100		mapvalg 6813	. . . . . . . . . . . . 13 ⊢ ((ℕ0 ∈ V ∧ 𝐼 ∈ 𝑊) → (ℕ0 ↑𝑚 𝐼) = {𝑓 ∣ 𝑓:𝐼⟶ℕ0})
101	10, 91, 100	sylancr 414	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℕ0 ↑𝑚 𝐼) = {𝑓 ∣ 𝑓:𝐼⟶ℕ0})
102		mapex 6809	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑊 ∧ ℕ0 ∈ V) → {𝑓 ∣ 𝑓:𝐼⟶ℕ0} ∈ V)
103	91, 10, 102	sylancl 413	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑓 ∣ 𝑓:𝐼⟶ℕ0} ∈ V)
104	101, 103	eqeltrd 2306	. . . . . . . . . . 11 ⊢ (𝜑 → (ℕ0 ↑𝑚 𝐼) ∈ V)
105		rabexg 4227	. . . . . . . . . . 11 ⊢ ((ℕ0 ↑𝑚 𝐼) ∈ V → {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈ V)
106	104, 105	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → {ℎ ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈ V)
107	7, 106	eqeltrid 2316	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ V)
108		mapvalg 6813	. . . . . . . . 9 ⊢ ((𝐾 ∈ V ∧ 𝐷 ∈ V) → (𝐾 ↑𝑚 𝐷) = {𝑓 ∣ 𝑓:𝐷⟶𝐾})
109	99, 107, 108	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → (𝐾 ↑𝑚 𝐷) = {𝑓 ∣ 𝑓:𝐷⟶𝐾})
110		mapex 6809	. . . . . . . . 9 ⊢ ((𝐷 ∈ V ∧ 𝐾 ∈ V) → {𝑓 ∣ 𝑓:𝐷⟶𝐾} ∈ V)
111	107, 99, 110	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → {𝑓 ∣ 𝑓:𝐷⟶𝐾} ∈ V)
112	109, 111	eqeltrd 2306	. . . . . . 7 ⊢ (𝜑 → (𝐾 ↑𝑚 𝐷) ∈ V)
113	24, 112	eqeltrd 2306	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ V)
114		opexg 4314	. . . . . 6 ⊢ (((Base‘ndx) ∈ ℕ ∧ 𝐵 ∈ V) → ⟨(Base‘ndx), 𝐵⟩ ∈ V)
115	95, 113, 114	sylancr 414	. . . . 5 ⊢ (𝜑 → ⟨(Base‘ndx), 𝐵⟩ ∈ V)
116		plusgndxnn 13152	. . . . . 6 ⊢ (+g‘ndx) ∈ ℕ
117	113, 113	ofmresex 6288	. . . . . . 7 ⊢ (𝜑 → ( ∘𝑓 + ↾ (𝐵 × 𝐵)) ∈ V)
118	48, 117	eqeltrid 2316	. . . . . 6 ⊢ (𝜑 → ✚ ∈ V)
119		opexg 4314	. . . . . 6 ⊢ (((+g‘ndx) ∈ ℕ ∧ ✚ ∈ V) → ⟨(+g‘ndx), ✚ ⟩ ∈ V)
120	116, 118, 119	sylancr 414	. . . . 5 ⊢ (𝜑 → ⟨(+g‘ndx), ✚ ⟩ ∈ V)
121		mulrslid 13173	. . . . . . 7 ⊢ (.r = Slot (.r‘ndx) ∧ (.r‘ndx) ∈ ℕ)
122	121	simpri 113	. . . . . 6 ⊢ (.r‘ndx) ∈ ℕ
123	61	mpoexg 6363	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝐵 ∈ V) → × ∈ V)
124	113, 113, 123	syl2anc 411	. . . . . 6 ⊢ (𝜑 → × ∈ V)
125		opexg 4314	. . . . . 6 ⊢ (((.r‘ndx) ∈ ℕ ∧ × ∈ V) → ⟨(.r‘ndx), × ⟩ ∈ V)
126	122, 124, 125	sylancr 414	. . . . 5 ⊢ (𝜑 → ⟨(.r‘ndx), × ⟩ ∈ V)
127		tpexg 4535	. . . . 5 ⊢ ((⟨(Base‘ndx), 𝐵⟩ ∈ V ∧ ⟨(+g‘ndx), ✚ ⟩ ∈ V ∧ ⟨(.r‘ndx), × ⟩ ∈ V) → {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∈ V)
128	115, 120, 126, 127	syl3anc 1271	. . . 4 ⊢ (𝜑 → {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∈ V)
129		scaslid 13194	. . . . . . 7 ⊢ (Scalar = Slot (Scalar‘ndx) ∧ (Scalar‘ndx) ∈ ℕ)
130	129	simpri 113	. . . . . 6 ⊢ (Scalar‘ndx) ∈ ℕ
131		opexg 4314	. . . . . 6 ⊢ (((Scalar‘ndx) ∈ ℕ ∧ 𝑅 ∈ 𝑋) → ⟨(Scalar‘ndx), 𝑅⟩ ∈ V)
132	130, 93, 131	sylancr 414	. . . . 5 ⊢ (𝜑 → ⟨(Scalar‘ndx), 𝑅⟩ ∈ V)
133		vscaslid 13204	. . . . . . 7 ⊢ ( ·𝑠 = Slot ( ·𝑠 ‘ndx) ∧ ( ·𝑠 ‘ndx) ∈ ℕ)
134	133	simpri 113	. . . . . 6 ⊢ ( ·𝑠 ‘ndx) ∈ ℕ
135	72	mpoexg 6363	. . . . . . 7 ⊢ ((𝐾 ∈ V ∧ 𝐵 ∈ V) → ∙ ∈ V)
136	99, 113, 135	syl2anc 411	. . . . . 6 ⊢ (𝜑 → ∙ ∈ V)
137		opexg 4314	. . . . . 6 ⊢ ((( ·𝑠 ‘ndx) ∈ ℕ ∧ ∙ ∈ V) → ⟨( ·𝑠 ‘ndx), ∙ ⟩ ∈ V)
138	134, 136, 137	sylancr 414	. . . . 5 ⊢ (𝜑 → ⟨( ·𝑠 ‘ndx), ∙ ⟩ ∈ V)
139		tsetndxnn 13230	. . . . . 6 ⊢ (TopSet‘ndx) ∈ ℕ
140		topnfn 13285	. . . . . . . . . . . 12 ⊢ TopOpen Fn V
141		funfvex 5646	. . . . . . . . . . . . 13 ⊢ ((Fun TopOpen ∧ 𝑅 ∈ dom TopOpen) → (TopOpen‘𝑅) ∈ V)
142	141	funfni 5423	. . . . . . . . . . . 12 ⊢ ((TopOpen Fn V ∧ 𝑅 ∈ V) → (TopOpen‘𝑅) ∈ V)
143	140, 94, 142	sylancr 414	. . . . . . . . . . 11 ⊢ (𝜑 → (TopOpen‘𝑅) ∈ V)
144	76, 143	eqeltrid 2316	. . . . . . . . . 10 ⊢ (𝜑 → 𝑂 ∈ V)
145		snexg 4268	. . . . . . . . . 10 ⊢ (𝑂 ∈ V → {𝑂} ∈ V)
146	144, 145	syl 14	. . . . . . . . 9 ⊢ (𝜑 → {𝑂} ∈ V)
147		xpexg 4833	. . . . . . . . 9 ⊢ ((𝐷 ∈ V ∧ {𝑂} ∈ V) → (𝐷 × {𝑂}) ∈ V)
148	107, 146, 147	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → (𝐷 × {𝑂}) ∈ V)
149		ptex 13305	. . . . . . . 8 ⊢ ((𝐷 × {𝑂}) ∈ V → (∏t‘(𝐷 × {𝑂})) ∈ V)
150	148, 149	syl 14	. . . . . . 7 ⊢ (𝜑 → (∏t‘(𝐷 × {𝑂})) ∈ V)
151	81, 150	eqeltrd 2306	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ V)
152		opexg 4314	. . . . . 6 ⊢ (((TopSet‘ndx) ∈ ℕ ∧ 𝐽 ∈ V) → ⟨(TopSet‘ndx), 𝐽⟩ ∈ V)
153	139, 151, 152	sylancr 414	. . . . 5 ⊢ (𝜑 → ⟨(TopSet‘ndx), 𝐽⟩ ∈ V)
154		tpexg 4535	. . . . 5 ⊢ ((⟨(Scalar‘ndx), 𝑅⟩ ∈ V ∧ ⟨( ·𝑠 ‘ndx), ∙ ⟩ ∈ V ∧ ⟨(TopSet‘ndx), 𝐽⟩ ∈ V) → {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩} ∈ V)
155	132, 138, 153, 154	syl3anc 1271	. . . 4 ⊢ (𝜑 → {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩} ∈ V)
156		unexg 4534	. . . 4 ⊢ (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∈ V ∧ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩} ∈ V) → ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩}) ∈ V)
157	128, 155, 156	syl2anc 411	. . 3 ⊢ (𝜑 → ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩}) ∈ V)
158	3, 90, 92, 94, 157	ovmpod 6138	. 2 ⊢ (𝜑 → (𝐼 mPwSer 𝑅) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩}))
159	1, 158	eqtrid 2274	1 ⊢ (𝜑 → 𝑆 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩}))

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395   ∈ wcel 2200  {cab 2215  {crab 2512  Vcvv 2799  ⦋csb 3124   ∪ cun 3195  {csn 3666  {ctp 3668  ⟨cop 3669   class class class wbr 4083   ↦ cmpt 4145   × cxp 4717  ^◡ccnv 4718   ↾ cres 4721   “ cima 4722   Fn wfn 5313  ⟶wf 5314  ‘cfv 5318  (class class class)co 6007   ∈ cmpo 6009   ∘_𝑓 cof 6222   ∘_𝑟 cofr 6223   ↑_𝑚 cmap 6803  Fincfn 6895   ≤ cle 8190   − cmin 8325  ℕcn 9118  ℕ₀cn0 9377  ndxcnx 13037  Slot cslot 13039  Basecbs 13040  +_gcplusg 13118  ._rcmulr 13119  Scalarcsca 13121   ·_𝑠 cvsca 13122  TopSetcts 13124  TopOpenctopn 13281  ∏_tcpt 13296   Σ_g cgsu 13298   mPwSer cmps 14633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4199  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-cnex 8098  ax-resscn 8099  ax-1cn 8100  ax-1re 8101  ax-icn 8102  ax-addcl 8103  ax-addrcl 8104  ax-mulcl 8105  ax-i2m1 8112

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-tp 3674  df-op 3675  df-uni 3889  df-int 3924  df-iun 3967  df-br 4084  df-opab 4146  df-mpt 4147  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-rn 4730  df-res 4731  df-ima 4732  df-iota 5278  df-fun 5320  df-fn 5321  df-f 5322  df-f1 5323  df-fo 5324  df-f1o 5325  df-fv 5326  df-ov 6010  df-oprab 6011  df-mpo 6012  df-of 6224  df-1st 6292  df-2nd 6293  df-map 6805  df-ixp 6854  df-inn 9119  df-2 9177  df-3 9178  df-4 9179  df-5 9180  df-6 9181  df-7 9182  df-8 9183  df-9 9184  df-n0 9378  df-ndx 13043  df-slot 13044  df-base 13046  df-plusg 13131  df-mulr 13132  df-sca 13134  df-vsca 13135  df-tset 13137  df-rest 13282  df-topn 13283  df-topgen 13301  df-pt 13302  df-psr 14635

This theorem is referenced by:  psrbasg  14646  psrplusgg  14650