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	⊢ 𝐷 = { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 }
	extvfvvcl.3	⊢ 0 = ( 0_g ‘ 𝑅 )
	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	⊢ 𝐷 = { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 }
2		extvfvvcl.3	⊢ 0 = ( 0_g ‘ 𝑅 )
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	⊢ { ℎ ∈ ( ℕ₀ ↑_m 𝐽 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ₀ ↑_m 𝐽 ) ∣ ℎ finSupp 0 }
14	13	psrbasfsupp	⊢ { ℎ ∈ ( ℕ₀ ↑_m 𝐽 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ₀ ↑_m 𝐽 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin }
15	12 5 7 14 9	mplelf	⊢ ( 𝜑 → 𝐹 : { ℎ ∈ ( ℕ₀ ↑_m 𝐽 ) ∣ ℎ finSupp 0 } ⟶ 𝐵 )
16		breq1	⊢ ( ℎ = ( 𝑋 ↾ 𝐽 ) → ( ℎ finSupp 0 ↔ ( 𝑋 ↾ 𝐽 ) finSupp 0 ) )
17		nn0ex	⊢ ℕ₀ ∈ V
18	17	a1i	⊢ ( 𝜑 → ℕ₀ ∈ V )
19	3	difexd	⊢ ( 𝜑 → ( 𝐼 ∖ { 𝐴 } ) ∈ V )
20	6 19	eqeltrid	⊢ ( 𝜑 → 𝐽 ∈ V )
21	1	ssrab3	⊢ 𝐷 ⊆ ( ℕ₀ ↑_m 𝐼 )
22	21 10	sselid	⊢ ( 𝜑 → 𝑋 ∈ ( ℕ₀ ↑_m 𝐼 ) )
23	3 18 22	elmaprd	⊢ ( 𝜑 → 𝑋 : 𝐼 ⟶ ℕ₀ )
24		difssd	⊢ ( 𝜑 → ( 𝐼 ∖ { 𝐴 } ) ⊆ 𝐼 )
25	6 24	eqsstrid	⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
26	23 25	fssresd	⊢ ( 𝜑 → ( 𝑋 ↾ 𝐽 ) : 𝐽 ⟶ ℕ₀ )
27	18 20 26	elmapdd	⊢ ( 𝜑 → ( 𝑋 ↾ 𝐽 ) ∈ ( ℕ₀ ↑_m 𝐽 ) )
28		breq1	⊢ ( ℎ = 𝑋 → ( ℎ finSupp 0 ↔ 𝑋 finSupp 0 ) )
29	10 1	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } )
30	28 29	elrabrd	⊢ ( 𝜑 → 𝑋 finSupp 0 )
31		c0ex	⊢ 0 ∈ V
32	31	a1i	⊢ ( 𝜑 → 0 ∈ V )
33	30 32	fsuppres	⊢ ( 𝜑 → ( 𝑋 ↾ 𝐽 ) finSupp 0 )
34	16 27 33	elrabd	⊢ ( 𝜑 → ( 𝑋 ↾ 𝐽 ) ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐽 ) ∣ ℎ finSupp 0 } )
35	15 34	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 ↾ 𝐽 ) ) ∈ 𝐵 )
36	5 2	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 )
37	4 36	syl	⊢ ( 𝜑 → 0 ∈ 𝐵 )
38	35 37	ifcld	⊢ ( 𝜑 → if ( ( 𝑋 ‘ 𝐴 ) = 0 , ( 𝐹 ‘ ( 𝑋 ↾ 𝐽 ) ) , 0 ) ∈ 𝐵 )
39	11 38	eqeltrd	⊢ ( 𝜑 → ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝐴 ) ‘ 𝐹 ) ‘ 𝑋 ) ∈ 𝐵 )

Metamath Proof Explorer

Theorem extvfvvcl

Proof