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

Metamath Proof Explorer

Theorem extvfv

Description: The "variable extension" function evaluated for converting a given polynomial F by adding a variable with index A . (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Hypotheses extvval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
extvval.1 ⊢ 0 = ( 0g ‘ 𝑅 )
extvval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
extvval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
extvfval.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
extvfval.j ⊢ 𝐽 = ( 𝐼 ∖ { 𝐴 } )
extvfval.m ⊢ 𝑀 = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
extvfv.1 ⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
Assertion extvfv ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) = ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) )

Proof

Step Hyp Ref Expression
1 extvval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 extvval.1 ⊢ 0 = ( 0g ‘ 𝑅 )
3 extvval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 extvval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
5 extvfval.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
6 extvfval.j ⊢ 𝐽 = ( 𝐼 ∖ { 𝐴 } )
7 extvfval.m ⊢ 𝑀 = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
8 extvfv.1 ⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
9 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑥 ↾ 𝐽 ) ) = ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) )
10 9 ifeq1d ⊢ ( 𝑓 = 𝐹 → if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) = if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) )
11 10 mpteq2dv ⊢ ( 𝑓 = 𝐹 → ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) = ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) )
12 1 2 3 4 5 6 7 extvfval ⊢ ( 𝜑 → ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) = ( 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) ) )
13 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
14 1 13 rabex2 ⊢ 𝐷 ∈ V
15 14 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
16 15 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) ∈ V )
17 11 12 8 16 fvmptd4 ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) = ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) )