This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) ) )