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

Metamath Proof Explorer

Theorem extvfv

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 = h ∈ ℕ 0 I | finSupp 0 ⁡ h
extvval.1 ⊢ 0 ˙ = 0 R
extvval.i ⊢ φ → I ∈ V
extvval.r ⊢ φ → R ∈ W
extvfval.a ⊢ φ → A ∈ I
extvfval.j ⊢ J = I ∖ A
extvfval.m ⊢ M = Base J mPoly R
extvfv.1 ⊢ φ → F ∈ M
Assertion extvfv Could not format assertion : No typesetting found for |- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .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 extvfval.a ⊢ φ → A ∈ I
6 extvfval.j ⊢ J = I ∖ A
7 extvfval.m ⊢ M = Base J mPoly R
8 extvfv.1 ⊢ φ → F ∈ M
9 fveq1 ⊢ f = F → f ⁡ x ↾ J = F ⁡ x ↾ J
10 9 ifeq1d ⊢ f = F → if x ⁡ A = 0 f ⁡ x ↾ J 0 ˙ = if x ⁡ A = 0 F ⁡ x ↾ J 0 ˙
11 10 mpteq2dv ⊢ f = F → x ∈ D ⟼ if x ⁡ A = 0 f ⁡ x ↾ J 0 ˙ = x ∈ D ⟼ if x ⁡ A = 0 F ⁡ x ↾ J 0 ˙
12 1 2 3 4 5 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 |-
13 ovex ⊢ ℕ 0 I ∈ V
14 1 13 rabex2 ⊢ D ∈ V
15 14 a1i ⊢ φ → D ∈ V
16 15 mptexd ⊢ φ → x ∈ D ⟼ if x ⁡ A = 0 F ⁡ x ↾ J 0 ˙ ∈ V
17 11 12 8 16 fvmptd4 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 |-