Theorem extvfvalf

Description: The "variable extension" function maps polynomials with variables indexed in J to polynomials with variables indexed in I . (Contributed by Thierry Arnoux, 25-Jan-2026)

	Ref	Expression
Hypotheses	extvfvvcl.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
	extvfvvcl.3	⊢ 0 = ( 0g ‘ 𝑅 )
	extvfvvcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	extvfvvcl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	extvfvvcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	extvfvvcl.j	⊢ 𝐽 = ( 𝐼 ∖ { 𝐴 } )
	extvfvvcl.m	⊢ 𝑀 = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
	extvfvvcl.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
	extvfvalf.n	⊢ 𝑁 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
Assertion	extvfvalf	⊢ ( 𝜑 → ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) : 𝑀 ⟶ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		extvfvvcl.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2		extvfvvcl.3	⊢ 0 = ( 0g ‘ 𝑅 )
3		extvfvvcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4		extvfvvcl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		extvfvvcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
6		extvfvvcl.j	⊢ 𝐽 = ( 𝐼 ∖ { 𝐴 } )
7		extvfvvcl.m	⊢ 𝑀 = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
8		extvfvvcl.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
9		extvfvalf.n	⊢ 𝑁 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
10		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
11	1 10	rabex2	⊢ 𝐷 ∈ V
12	11	a1i	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑀 ) → 𝐷 ∈ V )
13	12	mptexd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑀 ) → ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) ∈ V )
14	1 2 3 4 8 6 7	extvfval	⊢ ( 𝜑 → ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) = ( 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝐴 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ 𝐽 ) ) , 0 ) ) ) )
15	3	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑀 ) → 𝐼 ∈ 𝑉 )
16	4	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑀 ) → 𝑅 ∈ Ring )
17	8	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑀 ) → 𝐴 ∈ 𝐼 )
18		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑀 ) → 𝑓 ∈ 𝑀 )
19	1 2 15 16 5 6 7 17 18 9	extvfvcl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑀 ) → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝑓 ) ∈ 𝑁 )
20	13 14 19	fmpt2d	⊢ ( 𝜑 → ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) : 𝑀 ⟶ 𝑁 )