Definition df-extv 33581

Description: Define the "variable extension" function. The function ((𝐼extendVars𝑅)‘𝐴) converts polynomials with variables indexed by (𝐼 ∖ {𝐴}) into polynomials indexed by 𝐼, and therefore maps elements of ((𝐼 ∖ {𝐴}) mPoly 𝑅) onto (𝐼 mPoly 𝑅). (Contributed by Thierry Arnoux, 20-Jan-2026.)

Assertion

Ref	Expression
df-extv	⊢ extendVars = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑎 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘((𝑖 ∖ {𝑎}) mPoly 𝑟)) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ if((𝑥‘𝑎) = 0, (𝑓‘(𝑥 ↾ (𝑖 ∖ {𝑎}))), (0g‘𝑟))))))

Distinct variable group:   𝑖,𝑟,𝑎,ℎ,𝑓,𝑥

Detailed syntax breakdown of Definition df-extv

Step	Hyp	Ref	Expression
1		cextv 33580	. 2 class extendVars
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 3437	. . 3 class V
5		va	. . . 4 setvar 𝑎
6	2	cv 1540	. . . 4 class 𝑖
7		vf	. . . . 5 setvar 𝑓
8	5	cv 1540	. . . . . . . . 9 class 𝑎
9	8	csn 4575	. . . . . . . 8 class {𝑎}
10	6, 9	cdif 3895	. . . . . . 7 class (𝑖 ∖ {𝑎})
11	3	cv 1540	. . . . . . 7 class 𝑟
12		cmpl 21845	. . . . . . 7 class mPoly
13	10, 11, 12	co 7352	. . . . . 6 class ((𝑖 ∖ {𝑎}) mPoly 𝑟)
14		cbs 17122	. . . . . 6 class Base
15	13, 14	cfv 6486	. . . . 5 class (Base‘((𝑖 ∖ {𝑎}) mPoly 𝑟))
16		vx	. . . . . 6 setvar 𝑥
17		vh	. . . . . . . . 9 setvar ℎ
18	17	cv 1540	. . . . . . . 8 class ℎ
19		cc0 11013	. . . . . . . 8 class 0
20		cfsupp 9252	. . . . . . . 8 class finSupp
21	18, 19, 20	wbr 5093	. . . . . . 7 wff ℎ finSupp 0
22		cn0 12388	. . . . . . . 8 class ℕ0
23		cmap 8756	. . . . . . . 8 class ↑m
24	22, 6, 23	co 7352	. . . . . . 7 class (ℕ0 ↑m 𝑖)
25	21, 17, 24	crab 3396	. . . . . 6 class {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0}
26	16	cv 1540	. . . . . . . . 9 class 𝑥
27	8, 26	cfv 6486	. . . . . . . 8 class (𝑥‘𝑎)
28	27, 19	wceq 1541	. . . . . . 7 wff (𝑥‘𝑎) = 0
29	26, 10	cres 5621	. . . . . . . 8 class (𝑥 ↾ (𝑖 ∖ {𝑎}))
30	7	cv 1540	. . . . . . . 8 class 𝑓
31	29, 30	cfv 6486	. . . . . . 7 class (𝑓‘(𝑥 ↾ (𝑖 ∖ {𝑎})))
32		c0g 17345	. . . . . . . 8 class 0g
33	11, 32	cfv 6486	. . . . . . 7 class (0g‘𝑟)
34	28, 31, 33	cif 4474	. . . . . 6 class if((𝑥‘𝑎) = 0, (𝑓‘(𝑥 ↾ (𝑖 ∖ {𝑎}))), (0g‘𝑟))
35	16, 25, 34	cmpt 5174	. . . . 5 class (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ if((𝑥‘𝑎) = 0, (𝑓‘(𝑥 ↾ (𝑖 ∖ {𝑎}))), (0g‘𝑟)))
36	7, 15, 35	cmpt 5174	. . . 4 class (𝑓 ∈ (Base‘((𝑖 ∖ {𝑎}) mPoly 𝑟)) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ if((𝑥‘𝑎) = 0, (𝑓‘(𝑥 ↾ (𝑖 ∖ {𝑎}))), (0g‘𝑟))))
37	5, 6, 36	cmpt 5174	. . 3 class (𝑎 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘((𝑖 ∖ {𝑎}) mPoly 𝑟)) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ if((𝑥‘𝑎) = 0, (𝑓‘(𝑥 ↾ (𝑖 ∖ {𝑎}))), (0g‘𝑟)))))
38	2, 3, 4, 4, 37	cmpo 7354	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑎 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘((𝑖 ∖ {𝑎}) mPoly 𝑟)) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ if((𝑥‘𝑎) = 0, (𝑓‘(𝑥 ↾ (𝑖 ∖ {𝑎}))), (0g‘𝑟))))))
39	1, 38	wceq 1541	1 wff extendVars = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑎 ∈ 𝑖 ↦ (𝑓 ∈ (Base‘((𝑖 ∖ {𝑎}) mPoly 𝑟)) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝑖) ∣ ℎ finSupp 0} ↦ if((𝑥‘𝑎) = 0, (𝑓‘(𝑥 ↾ (𝑖 ∖ {𝑎}))), (0g‘𝑟))))))

This definition is referenced by:  extvval  33582