Theorem psrval 21028

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 21022	. . . 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 767	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → 𝑖 = 𝐼)
5	4	oveq2d 7271	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → (ℕ0 ↑m 𝑖) = (ℕ0 ↑m 𝐼))
6		rabeq 3408	. . . . . . 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 2797	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} = 𝐷)
10	9	csbeq1d 3832	. . . 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 7288	. . . . . . 7 ⊢ (ℕ0 ↑m 𝑖) ∈ V
12	11	rabex 5251	. . . . . 6 ⊢ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ∈ V
13	9, 12	eqeltrrdi 2848	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) → 𝐷 ∈ V)
14		simplrr 774	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝑟 = 𝑅)
15	14	fveq2d 6760	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → (Base‘𝑟) = (Base‘𝑅))
16		psrval.k	. . . . . . . . . 10 ⊢ 𝐾 = (Base‘𝑅)
17	15, 16	eqtr4di 2797	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → (Base‘𝑟) = 𝐾)
18		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷)
19	17, 18	oveq12d 7273	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → ((Base‘𝑟) ↑m 𝑑) = (𝐾 ↑m 𝐷))
20		psrval.b	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 = (𝐾 ↑m 𝐷))
21	20	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝐵 = (𝐾 ↑m 𝐷))
22	19, 21	eqtr4d 2781	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → ((Base‘𝑟) ↑m 𝑑) = 𝐵)
23	22	csbeq1d 3832	. . . . . 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 7288	. . . . . . . 8 ⊢ ((Base‘𝑟) ↑m 𝑑) ∈ V
25	22, 24	eqeltrrdi 2848	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) → 𝐵 ∈ V)
26		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
27	26	opeq2d 4808	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(Base‘ndx), 𝑏⟩ = ⟨(Base‘ndx), 𝐵⟩)
28	14	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑟 = 𝑅)
29	28	fveq2d 6760	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (+g‘𝑟) = (+g‘𝑅))
30		psrval.a	. . . . . . . . . . . . . 14 ⊢ + = (+g‘𝑅)
31	29, 30	eqtr4di 2797	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (+g‘𝑟) = + )
32	31	ofeqd 7513	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ∘f (+g‘𝑟) = ∘f + )
33	26, 26	xpeq12d 5611	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵))
34	32, 33	reseq12d 5881	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏)) = ( ∘f + ↾ (𝐵 × 𝐵)))
35		psrval.p	. . . . . . . . . . 11 ⊢ ✚ = ( ∘f + ↾ (𝐵 × 𝐵))
36	34, 35	eqtr4di 2797	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏)) = ✚ )
37	36	opeq2d 4808	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(+g‘ndx), ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩ = ⟨(+g‘ndx), ✚ ⟩)
38	18	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑑 = 𝐷)
39		rabeq 3408	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝐷 → {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘})
40	38, 39	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘})
41	28	fveq2d 6760	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (.r‘𝑟) = (.r‘𝑅))
42		psrval.m	. . . . . . . . . . . . . . . . 17 ⊢ · = (.r‘𝑅)
43	41, 42	eqtr4di 2797	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (.r‘𝑟) = · )
44	43	oveqd 7272	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥))) = ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥))))
45	40, 44	mpteq12dv 5161	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))) = (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥)))))
46	28, 45	oveq12d 7273	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥))))) = (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥))))))
47	38, 46	mpteq12dv 5161	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥)))))))
48	26, 26, 47	mpoeq123dv 7328	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥))))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥))))))))
49		psrval.t	. . . . . . . . . . 11 ⊢ × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑥 ∈ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥) · (𝑔‘(𝑘 ∘f − 𝑥)))))))
50	48, 49	eqtr4di 2797	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥))))))) = × )
51	50	opeq2d 4808	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))⟩ = ⟨(.r‘ndx), × ⟩)
52	27, 37, 51	tpeq123d 4681	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩})
53	28	opeq2d 4808	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(Scalar‘ndx), 𝑟⟩ = ⟨(Scalar‘ndx), 𝑅⟩)
54	17	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (Base‘𝑟) = 𝐾)
55	43	ofeqd 7513	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ∘f (.r‘𝑟) = ∘f · )
56	38	xpeq1d 5609	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑑 × {𝑥}) = (𝐷 × {𝑥}))
57		eqidd 2739	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝑓 = 𝑓)
58	55, 56, 57	oveq123d 7276	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓) = ((𝐷 × {𝑥}) ∘f · 𝑓))
59	54, 26, 58	mpoeq123dv 7328	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓)) = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓)))
60		psrval.v	. . . . . . . . . . 11 ⊢ ∙ = (𝑥 ∈ 𝐾, 𝑓 ∈ 𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))
61	59, 60	eqtr4di 2797	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓)) = ∙ )
62	61	opeq2d 4808	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))⟩ = ⟨( ·𝑠 ‘ndx), ∙ ⟩)
63	28	fveq2d 6760	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (TopOpen‘𝑟) = (TopOpen‘𝑅))
64		psrval.o	. . . . . . . . . . . . . . 15 ⊢ 𝑂 = (TopOpen‘𝑅)
65	63, 64	eqtr4di 2797	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (TopOpen‘𝑟) = 𝑂)
66	65	sneqd 4570	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {(TopOpen‘𝑟)} = {𝑂})
67	38, 66	xpeq12d 5611	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (𝑑 × {(TopOpen‘𝑟)}) = (𝐷 × {𝑂}))
68	67	fveq2d 6760	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (∏t‘(𝑑 × {(TopOpen‘𝑟)})) = (∏t‘(𝐷 × {𝑂})))
69		psrval.j	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 = (∏t‘(𝐷 × {𝑂})))
70	69	ad3antrrr 726	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → 𝐽 = (∏t‘(𝐷 × {𝑂})))
71	68, 70	eqtr4d 2781	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → (∏t‘(𝑑 × {(TopOpen‘𝑟)})) = 𝐽)
72	71	opeq2d 4808	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩ = ⟨(TopSet‘ndx), 𝐽⟩)
73	53, 62, 72	tpeq123d 4681	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑟 = 𝑅)) ∧ 𝑑 = 𝐷) ∧ 𝑏 = 𝐵) → {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩} = {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩})
74	52, 73	uneq12d 4094	. . . . . . 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 3866	. . . . . 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 2778	. . . . 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 3866	. . . 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 2778	. . 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 3442	. . 3 ⊢ (𝜑 → 𝐼 ∈ V)
81		psrval.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑋)
82	81	elexd 3442	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
83		tpex 7575	. . . . 5 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∈ V
84		tpex 7575	. . . . 5 ⊢ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩} ∈ V
85	83, 84	unex 7574	. . . 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 7403	. 2 ⊢ (𝜑 → (𝐼 mPwSer 𝑅) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩}))
88	1, 87	eqtrid 2790	1 ⊢ (𝜑 → 𝑆 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑅⟩, ⟨( ·𝑠 ‘ndx), ∙ ⟩, ⟨(TopSet‘ndx), 𝐽⟩}))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {crab 3067  Vcvv 3422  ⦋csb 3828   ∪ cun 3881  {csn 4558  {ctp 4562  ⟨cop 4564   class class class wbr 5070   ↦ cmpt 5153   × cxp 5578  ^◡ccnv 5579   ↾ cres 5582   “ cima 5583  ‘cfv 6418  (class class class)co 7255   ∈ cmpo 7257   ∘_f cof 7509   ∘_r cofr 7510   ↑_m cmap 8573  Fincfn 8691   ≤ cle 10941   − cmin 11135  ℕcn 11903  ℕ₀cn0 12163  ndxcnx 16822  Basecbs 16840  +_gcplusg 16888  ._rcmulr 16889  Scalarcsca 16891   ·_𝑠 cvsca 16892  TopSetcts 16894  TopOpenctopn 17049  ∏_tcpt 17066   Σ_g cgsu 17068   mPwSer cmps 21017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-res 5592  df-iota 6376  df-fun 6420  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-of 7511  df-psr 21022

This theorem is referenced by:  psrbas  21057  psrplusg  21060  psrmulr  21063  psrsca  21068  psrvscafval  21069