Theorem psrval 21935

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {crab 3436  Vcvv 3480  ⦋csb 3899   ∪ cun 3949  {csn 4626  {ctp 4630  ⟨cop 4632   class class class wbr 5143   ↦ cmpt 5225   × cxp 5683  ^◡ccnv 5684   ↾ cres 5687   “ cima 5688  ‘cfv 6561  (class class class)co 7431   ∈ cmpo 7433   ∘_f cof 7695   ∘_r cofr 7696   ↑_m cmap 8866  Fincfn 8985   ≤ cle 11296   − cmin 11492  ℕcn 12266  ℕ₀cn0 12526  ndxcnx 17230  Basecbs 17247  +_gcplusg 17297  ._rcmulr 17298  Scalarcsca 17300   ·_𝑠 cvsca 17301  TopSetcts 17303  TopOpenctopn 17466  ∏_tcpt 17483   Σ_g cgsu 17485   mPwSer cmps 21924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-res 5697  df-iota 6514  df-fun 6563  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-psr 21929

This theorem is referenced by:  psrbas  21953  psrplusg  21956  psrmulr  21962  psrsca  21967  psrvscafval  21968