Definition df-extv

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cextv	⊢ extendVars
1		vi	⊢ 𝑖
2		cvv	⊢ V
3		vr	⊢ 𝑟
4		va	⊢ 𝑎
5	1	cv	⊢ 𝑖
6		vf	⊢ 𝑓
7		cbs	⊢ Base
8	4	cv	⊢ 𝑎
9	8	csn	⊢ { 𝑎 }
10	5 9	cdif	⊢ ( 𝑖 ∖ { 𝑎 } )
11		cmpl	⊢ mPoly
12	3	cv	⊢ 𝑟
13	10 12 11	co	⊢ ( ( 𝑖 ∖ { 𝑎 } ) mPoly 𝑟 )
14	13 7	cfv	⊢ ( Base ‘ ( ( 𝑖 ∖ { 𝑎 } ) mPoly 𝑟 ) )
15		vx	⊢ 𝑥
16		vh	⊢ ℎ
17		cn0	⊢ ℕ0
18		cmap	⊢ ↑m
19	17 5 18	co	⊢ ( ℕ0 ↑m 𝑖 )
20	16	cv	⊢ ℎ
21		cfsupp	⊢ finSupp
22		cc0	⊢ 0
23	20 22 21	wbr	⊢ ℎ finSupp 0
24	23 16 19	crab	⊢ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 }
25	15	cv	⊢ 𝑥
26	8 25	cfv	⊢ ( 𝑥 ‘ 𝑎 )
27	26 22	wceq	⊢ ( 𝑥 ‘ 𝑎 ) = 0
28	6	cv	⊢ 𝑓
29	25 10	cres	⊢ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) )
30	29 28	cfv	⊢ ( 𝑓 ‘ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) )
31		c0g	⊢ 0g
32	12 31	cfv	⊢ ( 0g ‘ 𝑟 )
33	27 30 32	cif	⊢ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) ) , ( 0g ‘ 𝑟 ) )
34	15 24 33	cmpt	⊢ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) ) , ( 0g ‘ 𝑟 ) ) )
35	6 14 34	cmpt	⊢ ( 𝑓 ∈ ( Base ‘ ( ( 𝑖 ∖ { 𝑎 } ) mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) ) , ( 0g ‘ 𝑟 ) ) ) )
36	4 5 35	cmpt	⊢ ( 𝑎 ∈ 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( ( 𝑖 ∖ { 𝑎 } ) mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) ) , ( 0g ‘ 𝑟 ) ) ) ) )
37	1 3 2 2 36	cmpo	⊢ ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑎 ∈ 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( ( 𝑖 ∖ { 𝑎 } ) mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) ) , ( 0g ‘ 𝑟 ) ) ) ) ) )
38	0 37	wceq	⊢ extendVars = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑎 ∈ 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( ( 𝑖 ∖ { 𝑎 } ) mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) ) , ( 0g ‘ 𝑟 ) ) ) ) ) )