Theorem psrval 21189

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 21183	. . . 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 768	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → 𝑖 = 𝐼)
5	4	oveq2d 7329	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → (ℕ0 ↑m 𝑖) = (ℕ0 ↑m 𝐼))
6		rabeq 3417	. . . . . . 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 3845	. . . 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 7346	. . . . . . 7 ⊢ (ℕ0 ↑m 𝑖) ∈ V
12	11	rabex 5269	. . . . . 6 ⊢ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈ V
13	9, 12	eqeltrrdi 2847	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → 𝐷 ∈ V)
14		simplrr 775	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝑟 = 𝑅)
15	14	fveq2d 6813	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → (Base‘𝑟) = (Base‘𝑅))
16		psrval.k	. . . . . . . . . 10 ⊢ 𝐾 = (Base‘𝑅)
17	15, 16	eqtr4di 2795	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → (Base‘𝑟) = 𝐾)
18		simpr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷)
19	17, 18	oveq12d 7331	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → ((Base‘𝑟) ↑m 𝑑) = (𝐾 ↑m 𝐷))
20		psrval.b	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 = (𝐾 ↑m 𝐷))
21	20	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝐵 = (𝐾 ↑m 𝐷))
22	19, 21	eqtr4d 2780	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → ((Base‘𝑟) ↑m 𝑑) = 𝐵)
23	22	csbeq1d 3845	. . . . . 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 7346	. . . . . . . 8 ⊢ ((Base‘𝑟) ↑m 𝑑) ∈ V
25	22, 24	eqeltrrdi 2847	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝐵 ∈ V)
26		simpr 485	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
27	26	opeq2d 4820	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(Base‘ndx), 𝑏⟩ = ⟨(Base‘ndx), 𝐵⟩)
28	14	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑟 = 𝑅)
29	28	fveq2d 6813	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (+g‘𝑟) = (+g‘𝑅))
30		psrval.a	. . . . . . . . . . . . . 14 ⊢ + = (+g‘𝑅)
31	29, 30	eqtr4di 2795	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (+g‘𝑟) = + )
32	31	ofeqd 7573	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ∘f (+g‘𝑟) = ∘f + )
33	26, 26	xpeq12d 5636	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵))
34	32, 33	reseq12d 5909	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏)) = ( ∘f + ↾ (𝐵 × 𝐵)))
35		psrval.p	. . . . . . . . . . 11 ⊢ ✚ = ( ∘f + ↾ (𝐵 × 𝐵))
36	34, 35	eqtr4di 2795	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏)) = ✚ )
37	36	opeq2d 4820	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(+g‘ndx), ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩ = ⟨(+g‘ndx), ✚ ⟩)
38	18	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑑 = 𝐷)
39		rabeq 3417	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝐷 → {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘})
40	38, 39	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘})
41	28	fveq2d 6813	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (.r‘𝑟) = (.r‘𝑅))
42		psrval.m	. . . . . . . . . . . . . . . . 17 ⊢ · = (.r‘𝑅)
43	41, 42	eqtr4di 2795	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (.r‘𝑟) = · )
44	43	oveqd 7330	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥))) = ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥))))
45	40, 44	mpteq12dv 5176	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥)))))
46	28, 45	oveq12d 7331	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥))))) = (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥))))))
47	38, 46	mpteq12dv 5176	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥)))))))
48	26, 26, 47	mpoeq123dv 7388	. . . . . . . . . . 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 4820	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))⟩ = ⟨(.r‘ndx), × ⟩)
52	27, 37, 51	tpeq123d 4692	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩})
53	28	opeq2d 4820	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(Scalar‘ndx), 𝑟⟩ = ⟨(Scalar‘ndx), 𝑅⟩)
54	17	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (Base‘𝑟) = 𝐾)
55	43	ofeqd 7573	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ∘f (.r‘𝑟) = ∘f · )
56	38	xpeq1d 5634	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑑 × {𝑥}) = (𝐷 × {𝑥}))
57		eqidd 2738	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑓 = 𝑓)
58	55, 56, 57	oveq123d 7334	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓) = ((𝐷 × {𝑥}) ∘f · 𝑓))
59	54, 26, 58	mpoeq123dv 7388	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓)) = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓)))
60		psrval.v	. . . . . . . . . . 11 ⊢ ∙ = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))
61	59, 60	eqtr4di 2795	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓)) = ∙ )
62	61	opeq2d 4820	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))⟩ = ⟨( ·𝑠 ‘ndx), ∙ ⟩)
63	28	fveq2d 6813	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (TopOpen‘𝑟) = (TopOpen‘𝑅))
64		psrval.o	. . . . . . . . . . . . . . 15 ⊢ 𝑂 = (TopOpen‘𝑅)
65	63, 64	eqtr4di 2795	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (TopOpen‘𝑟) = 𝑂)
66	65	sneqd 4581	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {(TopOpen‘𝑟)} = {𝑂})
67	38, 66	xpeq12d 5636	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑑 × {(TopOpen‘𝑟)}) = (𝐷 × {𝑂}))
68	67	fveq2d 6813	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (∏t‘(𝑑 × {(TopOpen‘𝑟)})) = (∏t‘(𝐷 × {𝑂})))
69		psrval.j	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 = (∏t‘(𝐷 × {𝑂})))
70	69	ad3antrrr 727	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝐽 = (∏t‘(𝐷 × {𝑂})))
71	68, 70	eqtr4d 2780	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (∏t‘(𝑑 × {(TopOpen‘𝑟)})) = 𝐽)
72	71	opeq2d 4820	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩ = ⟨(TopSet‘ndx), 𝐽⟩)
73	53, 62, 72	tpeq123d 4692	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩} = {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩})
74	52, 73	uneq12d 4108	. . . . . . 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 3879	. . . . . 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 3879	. . . 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 3461	. . 3 ⊢ (𝜑 → 𝐼 ∈ V)
81		psrval.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑋)
82	81	elexd 3461	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
83		tpex 7635	. . . . 5 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∈ V
84		tpex 7635	. . . . 5 ⊢ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩} ∈ V
85	83, 84	unex 7634	. . . 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 7463	. 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 396   = wceq 1540   ∈ wcel 2105  {crab 3404  Vcvv 3441  ⦋csb 3841   ∪ cun 3894  {csn 4569  {ctp 4573  ⟨cop 4575   class class class wbr 5085   ↦ cmpt 5168   × cxp 5603  ^◡ccnv 5604   ↾ cres 5607   “ cima 5608  ‘cfv 6463  (class class class)co 7313   ∈ cmpo 7315   ∘_f cof 7569   ∘_r cofr 7570   ↑_m cmap 8661  Fincfn 8779   ≤ cle 11080   − cmin 11275  ℕcn 12043  ℕ₀cn0 12303  ndxcnx 16961  Basecbs 16979  +_gcplusg 17029  ._rcmulr 17030  Scalarcsca 17032   ·_𝑠 cvsca 17033  TopSetcts 17035  TopOpenctopn 17199  ∏_tcpt 17216   Σ_g cgsu 17218   mPwSer cmps 21178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5236  ax-nul 5243  ax-pr 5365  ax-un 7626

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4470  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4849  df-br 5086  df-opab 5148  df-mpt 5169  df-id 5505  df-xp 5611  df-rel 5612  df-cnv 5613  df-co 5614  df-dm 5615  df-res 5617  df-iota 6415  df-fun 6465  df-fv 6471  df-ov 7316  df-oprab 7317  df-mpo 7318  df-of 7571  df-psr 21183

This theorem is referenced by:  psrbas  21218  psrplusg  21221  psrmulr  21224  psrsca  21229  psrvscafval  21230