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 ⊢ D = h ∈ ℕ 0 I | finSupp 0 ⁡ h
extvval.1 ⊢ 0 ˙ = 0 R
extvval.i ⊢ φ → I ∈ V
extvval.r ⊢ φ → R ∈ W
extvval.j ⊢ J = I ∖ a
extvval.m ⊢ M = Base J mPoly R
Assertion extvval Could not format assertion : No typesetting found for |- ( ph -> ( I extendVars R ) = ( a e. I |-> ( f e. M |-> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) ) ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 extvval.d ⊢ D = h ∈ ℕ 0 I | finSupp 0 ⁡ h
2 extvval.1 ⊢ 0 ˙ = 0 R
3 extvval.i ⊢ φ → I ∈ V
4 extvval.r ⊢ φ → R ∈ W
5 extvval.j ⊢ J = I ∖ a
6 extvval.m ⊢ M = Base J mPoly R
7 df-extv Could not format extendVars = ( i e. _V , r e. _V |-> ( a e. i |-> ( f e. ( Base ` ( ( i \ { a } ) mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) ) ) ) : No typesetting found for |- extendVars = ( i e. _V , r e. _V |-> ( a e. i |-> ( f e. ( Base ` ( ( i \ { a } ) mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) ) ) ) with typecode |-
8 7 a1i Could not format ( ph -> extendVars = ( i e. _V , r e. _V |-> ( a e. i |-> ( f e. ( Base ` ( ( i \ { a } ) mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) ) ) ) ) : No typesetting found for |- ( ph -> extendVars = ( i e. _V , r e. _V |-> ( a e. i |-> ( f e. ( Base ` ( ( i \ { a } ) mPoly r ) ) |-> ( x e. { h e. ( NN0 ^m i ) | h finSupp 0 } |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( i \ { a } ) ) ) , ( 0g ` r ) ) ) ) ) ) ) with typecode |-
9 simpl ⊢ i = I ∧ r = R → i = I
10 difeq1 ⊢ i = I → i ∖ a = I ∖ a
11 10 5 eqtr4di ⊢ i = I → i ∖ a = J
12 11 adantr ⊢ i = I ∧ r = R → i ∖ a = J
13 simpr ⊢ i = I ∧ r = R → r = R
14 12 13 oveq12d ⊢ i = I ∧ r = R → i ∖ a mPoly r = J mPoly R
15 14 fveq2d ⊢ i = I ∧ r = R → Base i ∖ a mPoly r = Base J mPoly R
16 15 6 eqtr4di ⊢ i = I ∧ r = R → Base i ∖ a mPoly r = M
17 oveq2 ⊢ i = I → ℕ 0 i = ℕ 0 I
18 17 rabeqdv ⊢ i = I → h ∈ ℕ 0 i | finSupp 0 ⁡ h = h ∈ ℕ 0 I | finSupp 0 ⁡ h
19 18 1 eqtr4di ⊢ i = I → h ∈ ℕ 0 i | finSupp 0 ⁡ h = D
20 19 adantr ⊢ i = I ∧ r = R → h ∈ ℕ 0 i | finSupp 0 ⁡ h = D
21 10 reseq2d ⊢ i = I → x ↾ i ∖ a = x ↾ I ∖ a
22 21 fveq2d ⊢ i = I → f ⁡ x ↾ i ∖ a = f ⁡ x ↾ I ∖ a
23 22 adantr ⊢ i = I ∧ r = R → f ⁡ x ↾ i ∖ a = f ⁡ x ↾ I ∖ a
24 fveq2 ⊢ r = R → 0 r = 0 R
25 24 adantl ⊢ i = I ∧ r = R → 0 r = 0 R
26 25 2 eqtr4di ⊢ i = I ∧ r = R → 0 r = 0 ˙
27 23 26 ifeq12d ⊢ i = I ∧ r = R → if x ⁡ a = 0 f ⁡ x ↾ i ∖ a 0 r = if x ⁡ a = 0 f ⁡ x ↾ I ∖ a 0 ˙
28 20 27 mpteq12dv ⊢ i = I ∧ r = R → x ∈ h ∈ ℕ 0 i | finSupp 0 ⁡ h ⟼ if x ⁡ a = 0 f ⁡ x ↾ i ∖ a 0 r = x ∈ D ⟼ if x ⁡ a = 0 f ⁡ x ↾ I ∖ a 0 ˙
29 16 28 mpteq12dv ⊢ i = I ∧ r = R → f ∈ Base i ∖ a mPoly r ⟼ x ∈ h ∈ ℕ 0 i | finSupp 0 ⁡ h ⟼ if x ⁡ a = 0 f ⁡ x ↾ i ∖ a 0 r = f ∈ M ⟼ x ∈ D ⟼ if x ⁡ a = 0 f ⁡ x ↾ I ∖ a 0 ˙
30 9 29 mpteq12dv ⊢ i = I ∧ r = R → a ∈ i ⟼ f ∈ Base i ∖ a mPoly r ⟼ x ∈ h ∈ ℕ 0 i | finSupp 0 ⁡ h ⟼ if x ⁡ a = 0 f ⁡ x ↾ i ∖ a 0 r = a ∈ I ⟼ f ∈ M ⟼ x ∈ D ⟼ if x ⁡ a = 0 f ⁡ x ↾ I ∖ a 0 ˙
31 30 adantl ⊢ φ ∧ i = I ∧ r = R → a ∈ i ⟼ f ∈ Base i ∖ a mPoly r ⟼ x ∈ h ∈ ℕ 0 i | finSupp 0 ⁡ h ⟼ if x ⁡ a = 0 f ⁡ x ↾ i ∖ a 0 r = a ∈ I ⟼ f ∈ M ⟼ x ∈ D ⟼ if x ⁡ a = 0 f ⁡ x ↾ I ∖ a 0 ˙
32 3 elexd ⊢ φ → I ∈ V
33 4 elexd ⊢ φ → R ∈ V
34 3 mptexd ⊢ φ → a ∈ I ⟼ f ∈ M ⟼ x ∈ D ⟼ if x ⁡ a = 0 f ⁡ x ↾ I ∖ a 0 ˙ ∈ V
35 8 31 32 33 34 ovmpod Could not format ( ph -> ( I extendVars R ) = ( a e. I |-> ( f e. M |-> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) ) ) ) ) : No typesetting found for |- ( ph -> ( I extendVars R ) = ( a e. I |-> ( f e. M |-> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) ) ) ) ) with typecode |-