Theorem psrval 21947

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 21941	. . . 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 780	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → 𝑖 = 𝐼)
5	4	oveq2d 7408	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → (ℕ0 ↑m 𝑖) = (ℕ0 ↑m 𝐼))
6		rabeq 3427	. . . . . . 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 2814	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} = 𝐷)
10	9	csbeq1d 3856	. . . 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 7425	. . . . . . 7 ⊢ (ℕ0 ↑m 𝑖) ∈ V
12	11	rabex 5294	. . . . . 6 ⊢ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈ V
13	9, 12	eqeltrrdi 2870	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → 𝐷 ∈ V)
14		simplrr 787	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝑟 = 𝑅)
15	14	fveq2d 6867	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → (Base‘𝑟) = (Base‘𝑅))
16		psrval.k	. . . . . . . . . 10 ⊢ 𝐾 = (Base‘𝑅)
17	15, 16	eqtr4di 2814	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → (Base‘𝑟) = 𝐾)
18		simpr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷)
19	17, 18	oveq12d 7410	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → ((Base‘𝑟) ↑m 𝑑) = (𝐾 ↑m 𝐷))
20		psrval.b	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 = (𝐾 ↑m 𝐷))
21	20	ad2antrr 736	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝐵 = (𝐾 ↑m 𝐷))
22	19, 21	eqtr4d 2799	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → ((Base‘𝑟) ↑m 𝑑) = 𝐵)
23	22	csbeq1d 3856	. . . . . 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 7425	. . . . . . . 8 ⊢ ((Base‘𝑟) ↑m 𝑑) ∈ V
25	22, 24	eqeltrrdi 2870	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝐵 ∈ V)
26		simpr 488	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
27	26	opeq2d 4837	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(Base‘ndx), 𝑏⟩ = ⟨(Base‘ndx), 𝐵⟩)
28	14	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑟 = 𝑅)
29	28	fveq2d 6867	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (+g‘𝑟) = (+g‘𝑅))
30		psrval.a	. . . . . . . . . . . . . 14 ⊢ + = (+g‘𝑅)
31	29, 30	eqtr4di 2814	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (+g‘𝑟) = + )
32	31	ofeqd 7658	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ∘f (+g‘𝑟) = ∘f + )
33	26, 26	xpeq12d 5676	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵))
34	32, 33	reseq12d 5964	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏)) = ( ∘f + ↾ (𝐵 × 𝐵)))
35		psrval.p	. . . . . . . . . . 11 ⊢ ✚ = ( ∘f + ↾ (𝐵 × 𝐵))
36	34, 35	eqtr4di 2814	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏)) = ✚ )
37	36	opeq2d 4837	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(+g‘ndx), ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩ = ⟨(+g‘ndx), ✚ ⟩)
38	18	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑑 = 𝐷)
39		rabeq 3427	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝐷 → {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘})
40	38, 39	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘})
41	28	fveq2d 6867	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (.r‘𝑟) = (.r‘𝑅))
42		psrval.m	. . . . . . . . . . . . . . . . 17 ⊢ · = (.r‘𝑅)
43	41, 42	eqtr4di 2814	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (.r‘𝑟) = · )
44	43	oveqd 7409	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥))) = ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥))))
45	40, 44	mpteq12dv 5186	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥)))))
46	28, 45	oveq12d 7410	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥))))) = (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥))))))
47	38, 46	mpteq12dv 5186	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥)))))))
48	26, 26, 47	mpoeq123dv 7467	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥))))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥))))))))
49		psrval.t	. . . . . . . . . . 11 ⊢ × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥)))))))
50	48, 49	eqtr4di 2814	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥))))))) = × )
51	50	opeq2d 4837	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))⟩ = ⟨(.r‘ndx), × ⟩)
52	27, 37, 51	tpeq123d 4706	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩})
53	28	opeq2d 4837	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(Scalar‘ndx), 𝑟⟩ = ⟨(Scalar‘ndx), 𝑅⟩)
54	17	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (Base‘𝑟) = 𝐾)
55	43	ofeqd 7658	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ∘f (.r‘𝑟) = ∘f · )
56	38	xpeq1d 5674	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑑 × {𝑥}) = (𝐷 × {𝑥}))
57		eqidd 2762	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑓 = 𝑓)
58	55, 56, 57	oveq123d 7413	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓) = ((𝐷 × {𝑥}) ∘f · 𝑓))
59	54, 26, 58	mpoeq123dv 7467	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓)) = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓)))
60		psrval.v	. . . . . . . . . . 11 ⊢ ∙ = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))
61	59, 60	eqtr4di 2814	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓)) = ∙ )
62	61	opeq2d 4837	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))⟩ = ⟨( ·𝑠 ‘ndx), ∙ ⟩)
63	28	fveq2d 6867	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (TopOpen‘𝑟) = (TopOpen‘𝑅))
64		psrval.o	. . . . . . . . . . . . . . 15 ⊢ 𝑂 = (TopOpen‘𝑅)
65	63, 64	eqtr4di 2814	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (TopOpen‘𝑟) = 𝑂)
66	65	sneqd 4593	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {(TopOpen‘𝑟)} = {𝑂})
67	38, 66	xpeq12d 5676	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑑 × {(TopOpen‘𝑟)}) = (𝐷 × {𝑂}))
68	67	fveq2d 6867	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (∏t‘(𝑑 × {(TopOpen‘𝑟)})) = (∏t‘(𝐷 × {𝑂})))
69		psrval.j	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 = (∏t‘(𝐷 × {𝑂})))
70	69	ad3antrrr 740	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝐽 = (∏t‘(𝐷 × {𝑂})))
71	68, 70	eqtr4d 2799	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (∏t‘(𝑑 × {(TopOpen‘𝑟)})) = 𝐽)
72	71	opeq2d 4837	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩ = ⟨(TopSet‘ndx), 𝐽⟩)
73	53, 62, 72	tpeq123d 4706	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩} = {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩})
74	52, 73	uneq12d 4122	. . . . . . 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 3888	. . . . . 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 2796	. . . . 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 3888	. . . 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 2796	. . 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 3476	. . 3 ⊢ (𝜑 → 𝐼 ∈ V)
81		psrval.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑋)
82	81	elexd 3476	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
83		tpex 7725	. . . . 5 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∈ V
84		tpex 7725	. . . . 5 ⊢ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩} ∈ V
85	83, 84	unex 7723	. . . 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 7544	. 2 ⊢ (𝜑 → (𝐼 mPwSer 𝑅) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩}))
88	1, 87	eqtrid 2808	1 ⊢ (𝜑 → 𝑆 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩}))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  {crab 3413  Vcvv 3453  ⦋csb 3852   ∪ cun 3902  {csn 4581  {ctp 4585  ⟨cop 4587   class class class wbr 5099   ↦ cmpt 5180   × cxp 5643  ^◡ccnv 5644   ↾ cres 5647   “ cima 5648  ‘cfv 6517  (class class class)co 7392   ∈ cmpo 7394   ∘_f cof 7654   ∘_r cofr 7655   ↑_m cmap 8803  Fincfn 8923   ≤ cle 11214   − cmin 11411  ℕcn 12207  ℕ₀cn0 12478  ndxcnx 17212  Basecbs 17228  +_gcplusg 17269  ._rcmulr 17270  Scalarcsca 17272   ·_𝑠 cvsca 17273  TopSetcts 17275  TopOpenctopn 17433  ∏_tcpt 17450   Σ_g cgsu 17452   mPwSer cmps 21936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-tp 4586  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-res 5657  df-iota 6473  df-fun 6519  df-fv 6525  df-ov 7395  df-oprab 7396  df-mpo 7397  df-of 7656  df-psr 21941

This theorem is referenced by:  psrbas  21966  psrplusg  21969  psrmulr  21974  psrsca  21979  psrvscafval  21980