Theorem extvfval

Description: The "variable extension" function evaluated for 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 𝑅 ) )
Assertion	extvfval	⊢ ( 𝜑 → ( ( 𝐼 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		sneq	⊢ ( 𝑎 = 𝐴 → { 𝑎 } = { 𝐴 } )
9	8	difeq2d	⊢ ( 𝑎 = 𝐴 → ( 𝐼 ∖ { 𝑎 } ) = ( 𝐼 ∖ { 𝐴 } ) )
10	9 6	eqtr4di	⊢ ( 𝑎 = 𝐴 → ( 𝐼 ∖ { 𝑎 } ) = 𝐽 )
11	10	fvoveq1d	⊢ ( 𝑎 = 𝐴 → ( Base ‘ ( ( 𝐼 ∖ { 𝑎 } ) mPoly 𝑅 ) ) = ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
12	11 7	eqtr4di	⊢ ( 𝑎 = 𝐴 → ( Base ‘ ( ( 𝐼 ∖ { 𝑎 } ) mPoly 𝑅 ) ) = 𝑀 )
13		fveqeq2	⊢ ( 𝑎 = 𝐴 → ( ( 𝑥 ‘ 𝑎 ) = 0 ↔ ( 𝑥 ‘ 𝐴 ) = 0 ) )
14	10	reseq2d	⊢ ( 𝑎 = 𝐴 → ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) = ( 𝑥 ↾ 𝐽 ) )
15	14	fveq2d	⊢ ( 𝑎 = 𝐴 → ( 𝑓 ‘ ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) ) = ( 𝑓 ‘ ( 𝑥 ↾ 𝐽 ) ) )
16	13 15	ifbieq1d	⊢ ( 𝑎 = 𝐴 → if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) ) , 0 ) = if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) )
17	16	mpteq2dv	⊢ ( 𝑎 = 𝐴 → ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) ) , 0 ) ) = ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) )
18	12 17	mpteq12dv	⊢ ( 𝑎 = 𝐴 → ( 𝑓 ∈ ( Base ‘ ( ( 𝐼 ∖ { 𝑎 } ) mPoly 𝑅 ) ) ↦ ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) ) , 0 ) ) ) = ( 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) ) )
19		eqid	⊢ ( 𝐼 ∖ { 𝑎 } ) = ( 𝐼 ∖ { 𝑎 } )
20		eqid	⊢ ( Base ‘ ( ( 𝐼 ∖ { 𝑎 } ) mPoly 𝑅 ) ) = ( Base ‘ ( ( 𝐼 ∖ { 𝑎 } ) mPoly 𝑅 ) )
21	1 2 3 4 19 20	extvval	⊢ ( 𝜑 → ( 𝐼 extendVars 𝑅 ) = ( 𝑎 ∈ 𝐼 ↦ ( 𝑓 ∈ ( Base ‘ ( ( 𝐼 ∖ { 𝑎 } ) mPoly 𝑅 ) ) ↦ ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) ) , 0 ) ) ) ) )
22	7	fvexi	⊢ 𝑀 ∈ V
23	22	mptex	⊢ ( 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) ) ∈ V
24	23	a1i	⊢ ( 𝜑 → ( 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) ) ∈ V )
25	18 21 5 24	fvmptd4	⊢ ( 𝜑 → ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) = ( 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) ) )