Theorem extvfvv

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	⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
	extvfvv.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
Assertion	extvfvv	⊢ ( 𝜑 → ( ( ( ( 𝐼 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		extvfvv.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
10		fveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ‘ 𝐴 ) = ( 𝑋 ‘ 𝐴 ) )
11	10	eqeq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ‘ 𝐴 ) = 0 ↔ ( 𝑋 ‘ 𝐴 ) = 0 ) )
12		reseq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ↾ 𝐽 ) = ( 𝑋 ↾ 𝐽 ) )
13	12	fveq2d	⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) = ( 𝐹 ‘ ( 𝑋 ↾ 𝐽 ) ) )
14	11 13	ifbieq1d	⊢ ( 𝑥 = 𝑋 → if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) = if ( ( 𝑋 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑋 ↾ 𝐽 ) ) , 0 ) )
15	1 2 3 4 5 6 7 8	extvfv	⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) = ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) )
16		fvexd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 ↾ 𝐽 ) ) ∈ V )
17	2	fvexi	⊢ 0 ∈ V
18	17	a1i	⊢ ( 𝜑 → 0 ∈ V )
19	16 18	ifcld	⊢ ( 𝜑 → if ( ( 𝑋 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑋 ↾ 𝐽 ) ) , 0 ) ∈ V )
20	14 15 9 19	fvmptd4	⊢ ( 𝜑 → ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ‘ 𝑋 ) = if ( ( 𝑋 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑋 ↾ 𝐽 ) ) , 0 ) )