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	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
	extvval.1	$$⊢\underset{\dot{}}{0}=0_R$$
	extvval.i	$$⊢\phi \to I\in V$$
	extvval.r	$$⊢\phi \to R\in W$$
	extvfval.a	$$⊢\phi \to A\in I$$
	extvfval.j	$$⊢J=I\setminus \left\{A\right\}$$
	extvfval.m	$$⊢M={\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}$$
	extvfv.1	$$⊢\phi \to F\in M$$
	extvfvv.1	$$⊢\phi \to X\in D$$
Assertion	extvfvv	Could not format assertion : No typesetting found for |- ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) = if ( ( X ` A ) = 0 , ( F ` ( X |` J ) ) , .0. ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		extvval.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
2		extvval.1	$$⊢\underset{\dot{}}{0}=0_R$$
3		extvval.i	$$⊢\phi \to I\in V$$
4		extvval.r	$$⊢\phi \to R\in W$$
5		extvfval.a	$$⊢\phi \to A\in I$$
6		extvfval.j	$$⊢J=I\setminus \left\{A\right\}$$
7		extvfval.m	$$⊢M={\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}$$
8		extvfv.1	$$⊢\phi \to F\in M$$
9		extvfvv.1	$$⊢\phi \to X\in D$$
10		fveq1	$$⊢x=X\to x\left(A\right)=X\left(A\right)$$
11	10	eqeq1d	$$⊢x=X\to \left(x\left(A\right)=0\leftrightarrow X\left(A\right)=0\right)$$
12		reseq1	$$⊢x=X\to {x\upharpoonright }_J={X\upharpoonright }_J$$
13	12	fveq2d	$$⊢x=X\to F\left({x\upharpoonright }_J\right)=F\left({X\upharpoonright }_J\right)$$
14	11 13	ifbieq1d	$$⊢x=X\to if\left(x\left(A\right)=0,F\left({x\upharpoonright }_J\right),\underset{\dot{}}{0}\right)=if\left(X\left(A\right)=0,F\left({X\upharpoonright }_J\right),\underset{\dot{}}{0}\right)$$
15	1 2 3 4 5 6 7 8	extvfv	Could not format ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) ) : No typesetting found for |- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) ) with typecode |-
16		fvexd	$$⊢\phi \to F\left({X\upharpoonright }_J\right)\in \mathrm{V}$$
17	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
18	17	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
19	16 18	ifcld	$$⊢\phi \to if\left(X\left(A\right)=0,F\left({X\upharpoonright }_J\right),\underset{\dot{}}{0}\right)\in \mathrm{V}$$
20	14 15 9 19	fvmptd4	Could not format ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) = if ( ( X ` A ) = 0 , ( F ` ( X |` J ) ) , .0. ) ) : No typesetting found for |- ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) = if ( ( X ` A ) = 0 , ( F ` ( X |` J ) ) , .0. ) ) with typecode |-