Theorem extvfvvcl

Description: Closure for 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	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	⊢ ( 𝜑 → 𝐴 ∈ 𝐼 )
	extvfvvcl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
	extvfvvcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
Assertion	extvfvvcl	⊢ ( 𝜑 → ( ( ( ( 𝐼 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		extvfvvcl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑀 )
10		extvfvvcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
11	1 2 3 4 8 6 7 9 10	extvfvv	⊢ ( 𝜑 → ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ‘ 𝑋 ) = if ( ( 𝑋 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑋 ↾ 𝐽 ) ) , 0 ) )
12		eqid	⊢ ( 𝐽 mPoly 𝑅 ) = ( 𝐽 mPoly 𝑅 )
13		eqid	⊢ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 }
14	13	psrbasfsupp	⊢ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
15	12 5 7 14 9	mplelf	⊢ ( 𝜑 → 𝐹 : { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } ⟶ 𝐵 )
16		breq1	⊢ ( ℎ = ( 𝑋 ↾ 𝐽 ) → ( ℎ finSupp 0 ↔ ( 𝑋 ↾ 𝐽 ) finSupp 0 ) )
17	1	ssrab3	⊢ 𝐷 ⊆ ( ℕ0 ↑m 𝐼 )
18	17 10	sselid	⊢ ( 𝜑 → 𝑋 ∈ ( ℕ0 ↑m 𝐼 ) )
19		difssd	⊢ ( 𝜑 → ( 𝐼 ∖ { 𝐴 } ) ⊆ 𝐼 )
20	6 19	eqsstrid	⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
21	18 20	elmapssresd	⊢ ( 𝜑 → ( 𝑋 ↾ 𝐽 ) ∈ ( ℕ0 ↑m 𝐽 ) )
22		breq1	⊢ ( ℎ = 𝑋 → ( ℎ finSupp 0 ↔ 𝑋 finSupp 0 ) )
23	10 1	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
24	22 23	elrabrd	⊢ ( 𝜑 → 𝑋 finSupp 0 )
25		c0ex	⊢ 0 ∈ V
26	25	a1i	⊢ ( 𝜑 → 0 ∈ V )
27	24 26	fsuppres	⊢ ( 𝜑 → ( 𝑋 ↾ 𝐽 ) finSupp 0 )
28	16 21 27	elrabd	⊢ ( 𝜑 → ( 𝑋 ↾ 𝐽 ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 } )
29	15 28	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 ↾ 𝐽 ) ) ∈ 𝐵 )
30	5 2	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 )
31	4 30	syl	⊢ ( 𝜑 → 0 ∈ 𝐵 )
32	29 31	ifcld	⊢ ( 𝜑 → if ( ( 𝑋 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑋 ↾ 𝐽 ) ) , 0 ) ∈ 𝐵 )
33	11 32	eqeltrd	⊢ ( 𝜑 → ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ‘ 𝑋 ) ∈ 𝐵 )