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