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	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
	extvfvvcl.3	$⊢ \underset{˙}{0} = 0_{R}$
	extvfvvcl.i	$⊢ φ \to I \in V$
	extvfvvcl.r	$⊢ φ \to R \in Ring$
	extvfvvcl.b	$⊢ B = {Base}_{R}$
	extvfvvcl.j	$⊢ J = I ∖ \{A\}$
	extvfvvcl.m	$⊢ M = {Base}_{(J mPoly R)}$
	extvfvvcl.1	$⊢ φ \to A \in I$
	extvfvalf.n	$⊢ N = {Base}_{(I mPoly R)}$
Assertion	extvfvalf	Could not format assertion : No typesetting found for \|- ( ph -> ( ( I extendVars R ) ` A ) : M --> N ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		extvfvvcl.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
2		extvfvvcl.3	$⊢ \underset{˙}{0} = 0_{R}$
3		extvfvvcl.i	$⊢ φ \to I \in V$
4		extvfvvcl.r	$⊢ φ \to R \in Ring$
5		extvfvvcl.b	$⊢ B = {Base}_{R}$
6		extvfvvcl.j	$⊢ J = I ∖ \{A\}$
7		extvfvvcl.m	$⊢ M = {Base}_{(J mPoly R)}$
8		extvfvvcl.1	$⊢ φ \to A \in I$
9		extvfvalf.n	$⊢ N = {Base}_{(I mPoly R)}$
10		ovex	$⊢ {ℕ_{0}}^{I} \in V$
11	1 10	rabex2	$⊢ D \in V$
12	11	a1i	$⊢ (φ \land f \in M) \to D \in V$
13	12	mptexd	$⊢ (φ \land f \in M) \to (x \in D ⟼ if (x (A) = 0, f ({x ↾}_{J}), \underset{˙}{0})) \in V$
14	1 2 3 4 8 6 7	extvfval	Could not format ( ph -> ( ( I extendVars R ) ` A ) = ( f e. M \|-> ( x e. D \|-> if ( ( x ` A ) = 0 , ( f ` ( x \|` J ) ) , .0. ) ) ) ) : No typesetting found for \|- ( ph -> ( ( I extendVars R ) ` A ) = ( f e. M \|-> ( x e. D \|-> if ( ( x ` A ) = 0 , ( f ` ( x \|` J ) ) , .0. ) ) ) ) with typecode \|-
15	3	adantr	$⊢ (φ \land f \in M) \to I \in V$
16	4	adantr	$⊢ (φ \land f \in M) \to R \in Ring$
17	8	adantr	$⊢ (φ \land f \in M) \to A \in I$
18		simpr	$⊢ (φ \land f \in M) \to f \in M$
19	1 2 15 16 5 6 7 17 18 9	extvfvcl	Could not format ( ( ph /\ f e. M ) -> ( ( ( I extendVars R ) ` A ) ` f ) e. N ) : No typesetting found for \|- ( ( ph /\ f e. M ) -> ( ( ( I extendVars R ) ` A ) ` f ) e. N ) with typecode \|-
20	13 14 19	fmpt2d	Could not format ( ph -> ( ( I extendVars R ) ` A ) : M --> N ) : No typesetting found for \|- ( ph -> ( ( I extendVars R ) ` A ) : M --> N ) with typecode \|-

Metamath Proof Explorer

Theorem extvfvalf

Proof