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 Could not format assertion : No typesetting found for |- extendVars = ( i e. _V , r e. _V |-> ( a e. i |-> ( f e. ( Base ` ( ( i \ { a } ) mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) ) ) ) with typecode |-

Detailed syntax breakdown

Step Hyp Ref Expression
0 cextv Could not format extendVars : No typesetting found for class extendVars with typecode class
1 vi setvar i
2 cvv class V
3 vr setvar r
4 va setvar a
5 1 cv setvar i
6 vf setvar f
7 cbs class Base
8 4 cv setvar a
9 8 csn class a
10 5 9 cdif class i ∖ a
11 cmpl class mPoly
12 3 cv setvar r
13 10 12 11 co class i ∖ a mPoly r
14 13 7 cfv class Base i ∖ a mPoly r
15 vx setvar x
16 vh setvar h
17 cn0 class ℕ 0
18 cmap class ↑ 𝑚
19 17 5 18 co class ℕ 0 i
20 16 cv setvar h
21 cfsupp class finSupp
22 cc0 class 0
23 20 22 21 wbr wff finSupp 0 ⁡ h
24 23 16 19 crab class h ∈ ℕ 0 i | finSupp 0 ⁡ h
25 15 cv setvar x
26 8 25 cfv class x ⁡ a
27 26 22 wceq wff x ⁡ a = 0
28 6 cv setvar f
29 25 10 cres class x ↾ i ∖ a
30 29 28 cfv class f ⁡ x ↾ i ∖ a
31 c0g class 0 𝑔
32 12 31 cfv class 0 r
33 27 30 32 cif class if x ⁡ a = 0 f ⁡ x ↾ i ∖ a 0 r
34 15 24 33 cmpt class x ∈ h ∈ ℕ 0 i | finSupp 0 ⁡ h ⟼ if x ⁡ a = 0 f ⁡ x ↾ i ∖ a 0 r
35 6 14 34 cmpt class f ∈ Base i ∖ a mPoly r ⟼ x ∈ h ∈ ℕ 0 i | finSupp 0 ⁡ h ⟼ if x ⁡ a = 0 f ⁡ x ↾ i ∖ a 0 r
36 4 5 35 cmpt class a ∈ i ⟼ f ∈ Base i ∖ a mPoly r ⟼ x ∈ h ∈ ℕ 0 i | finSupp 0 ⁡ h ⟼ if x ⁡ a = 0 f ⁡ x ↾ i ∖ a 0 r
37 1 3 2 2 36 cmpo class i ∈ V , r ∈ V ⟼ a ∈ i ⟼ f ∈ Base i ∖ a mPoly r ⟼ x ∈ h ∈ ℕ 0 i | finSupp 0 ⁡ h ⟼ if x ⁡ a = 0 f ⁡ x ↾ i ∖ a 0 r
38 0 37 wceq Could not format extendVars = ( i e. _V , r e. _V |-> ( a e. i |-> ( f e. ( Base ` ( ( i \ { a } ) mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) ) ) ) : No typesetting found for wff extendVars = ( i e. _V , r e. _V |-> ( a e. i |-> ( f e. ( Base ` ( ( i \ { a } ) mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) ) ) ) with typecode wff