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

Metamath Proof Explorer

Theorem extvfvv

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
extvfvv.1 ⊢ φ → X ∈ D
Assertion extvfvv Could not format assertion : No typesetting found for |- ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) = 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 extvfvv.1 ⊢ φ → X ∈ D
10 fveq1 ⊢ x = X → x ⁡ A = X ⁡ A
11 10 eqeq1d ⊢ x = X → x ⁡ A = 0 ↔ X ⁡ A = 0
12 reseq1 ⊢ x = X → x ↾ J = X ↾ J
13 12 fveq2d ⊢ x = X → F ⁡ x ↾ J = F ⁡ X ↾ J
14 11 13 ifbieq1d ⊢ x = X → if x ⁡ A = 0 F ⁡ x ↾ J 0 ˙ = if X ⁡ A = 0 F ⁡ X ↾ J 0 ˙
15 1 2 3 4 5 6 7 8 extvfv 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 |-
16 fvexd ⊢ φ → F ⁡ X ↾ J ∈ V
17 2 fvexi ⊢ 0 ˙ ∈ V
18 17 a1i ⊢ φ → 0 ˙ ∈ V
19 16 18 ifcld ⊢ φ → if X ⁡ A = 0 F ⁡ X ↾ J 0 ˙ ∈ V
20 14 15 9 19 fvmptd4 Could not format ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) = if ( ( X ` A ) = 0 , ( F ` ( X |` J ) ) , .0. ) ) : No typesetting found for |- ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) = if ( ( X ` A ) = 0 , ( F ` ( X |` J ) ) , .0. ) ) with typecode |-