Theorem extvval

Description: Value of the "variable extension" function. (Contributed by Thierry Arnoux, 25-Jan-2026)

	Ref	Expression
Hypotheses	extvval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
	extvval.1	⊢ 0 = ( 0g ‘ 𝑅 )
	extvval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	extvval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
	extvval.j	⊢ 𝐽 = ( 𝐼 ∖ { 𝑎 } )
	extvval.m	⊢ 𝑀 = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
Assertion	extvval	⊢ ( 𝜑 → ( 𝐼 extendVars 𝑅 ) = ( 𝑎 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) ) , 0 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		extvval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2		extvval.1	⊢ 0 = ( 0g ‘ 𝑅 )
3		extvval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4		extvval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
5		extvval.j	⊢ 𝐽 = ( 𝐼 ∖ { 𝑎 } )
6		extvval.m	⊢ 𝑀 = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
7		df-extv	⊢ extendVars = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑎 ∈ 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( ( 𝑖 ∖ { 𝑎 } ) mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) ) , ( 0g ‘ 𝑟 ) ) ) ) ) )
8	7	a1i	⊢ ( 𝜑 → extendVars = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑎 ∈ 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( ( 𝑖 ∖ { 𝑎 } ) mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) ) , ( 0g ‘ 𝑟 ) ) ) ) ) ) )
9		simpl	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → 𝑖 = 𝐼 )
10		difeq1	⊢ ( 𝑖 = 𝐼 → ( 𝑖 ∖ { 𝑎 } ) = ( 𝐼 ∖ { 𝑎 } ) )
11	10 5	eqtr4di	⊢ ( 𝑖 = 𝐼 → ( 𝑖 ∖ { 𝑎 } ) = 𝐽 )
12	11	adantr	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑖 ∖ { 𝑎 } ) = 𝐽 )
13		simpr	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
14	12 13	oveq12d	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ( 𝑖 ∖ { 𝑎 } ) mPoly 𝑟 ) = ( 𝐽 mPoly 𝑅 ) )
15	14	fveq2d	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( ( 𝑖 ∖ { 𝑎 } ) mPoly 𝑟 ) ) = ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
16	15 6	eqtr4di	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( ( 𝑖 ∖ { 𝑎 } ) mPoly 𝑟 ) ) = 𝑀 )
17		oveq2	⊢ ( 𝑖 = 𝐼 → ( ℕ0 ↑m 𝑖 ) = ( ℕ0 ↑m 𝐼 ) )
18	17	rabeqdv	⊢ ( 𝑖 = 𝐼 → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
19	18 1	eqtr4di	⊢ ( 𝑖 = 𝐼 → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } = 𝐷 )
20	19	adantr	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } = 𝐷 )
21	10	reseq2d	⊢ ( 𝑖 = 𝐼 → ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) = ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) )
22	21	fveq2d	⊢ ( 𝑖 = 𝐼 → ( 𝑓 ‘ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) ) = ( 𝑓 ‘ ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) ) )
23	22	adantr	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑓 ‘ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) ) = ( 𝑓 ‘ ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) ) )
24		fveq2	⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
25	24	adantl	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
26	25 2	eqtr4di	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 0g ‘ 𝑟 ) = 0 )
27	23 26	ifeq12d	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) ) , ( 0g ‘ 𝑟 ) ) = if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) ) , 0 ) )
28	20 27	mpteq12dv	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) ) , ( 0g ‘ 𝑟 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) ) , 0 ) ) )
29	16 28	mpteq12dv	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑓 ∈ ( Base ‘ ( ( 𝑖 ∖ { 𝑎 } ) mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) ) , ( 0g ‘ 𝑟 ) ) ) ) = ( 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) ) , 0 ) ) ) )
30	9 29	mpteq12dv	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑎 ∈ 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( ( 𝑖 ∖ { 𝑎 } ) mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) ) , ( 0g ‘ 𝑟 ) ) ) ) ) = ( 𝑎 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) ) , 0 ) ) ) ) )
31	30	adantl	⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) → ( 𝑎 ∈ 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( ( 𝑖 ∖ { 𝑎 } ) mPoly 𝑟 ) ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ℎ finSupp 0 } ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝑖 ∖ { 𝑎 } ) ) ) , ( 0g ‘ 𝑟 ) ) ) ) ) = ( 𝑎 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) ) , 0 ) ) ) ) )
32	3	elexd	⊢ ( 𝜑 → 𝐼 ∈ V )
33	4	elexd	⊢ ( 𝜑 → 𝑅 ∈ V )
34	3	mptexd	⊢ ( 𝜑 → ( 𝑎 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) ) , 0 ) ) ) ) ∈ V )
35	8 31 32 33 34	ovmpod	⊢ ( 𝜑 → ( 𝐼 extendVars 𝑅 ) = ( 𝑎 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ 𝐷 ↦ if ( ( 𝑥 ‘ 𝑎 ) = 0 , ( 𝑓 ‘ ( 𝑥 ↾ ( 𝐼 ∖ { 𝑎 } ) ) ) , 0 ) ) ) ) )