This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑟 ) ) ) ) ) )