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

Metamath Proof Explorer

Theorem extvfval

Description: The "variable extension" function evaluated for 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
Assertion extvfval Could not format assertion : 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 |-

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 sneq ⊢ a = A → a = A
9 8 difeq2d ⊢ a = A → I ∖ a = I ∖ A
10 9 6 eqtr4di ⊢ a = A → I ∖ a = J
11 10 fvoveq1d ⊢ a = A → Base I ∖ a mPoly R = Base J mPoly R
12 11 7 eqtr4di ⊢ a = A → Base I ∖ a mPoly R = M
13 fveqeq2 ⊢ a = A → x ⁡ a = 0 ↔ x ⁡ A = 0
14 10 reseq2d ⊢ a = A → x ↾ I ∖ a = x ↾ J
15 14 fveq2d ⊢ a = A → f ⁡ x ↾ I ∖ a = f ⁡ x ↾ J
16 13 15 ifbieq1d ⊢ a = A → if x ⁡ a = 0 f ⁡ x ↾ I ∖ a 0 ˙ = if x ⁡ A = 0 f ⁡ x ↾ J 0 ˙
17 16 mpteq2dv ⊢ a = A → x ∈ D ⟼ if x ⁡ a = 0 f ⁡ x ↾ I ∖ a 0 ˙ = x ∈ D ⟼ if x ⁡ A = 0 f ⁡ x ↾ J 0 ˙
18 12 17 mpteq12dv ⊢ a = A → f ∈ Base I ∖ a mPoly R ⟼ x ∈ D ⟼ if x ⁡ a = 0 f ⁡ x ↾ I ∖ a 0 ˙ = f ∈ M ⟼ x ∈ D ⟼ if x ⁡ A = 0 f ⁡ x ↾ J 0 ˙
19 eqid ⊢ I ∖ a = I ∖ a
20 eqid ⊢ Base I ∖ a mPoly R = Base I ∖ a mPoly R
21 1 2 3 4 19 20 extvval Could not format ( ph -> ( I extendVars R ) = ( a e. I |-> ( f e. ( Base ` ( ( I \ { a } ) mPoly R ) ) |-> ( 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. ( Base ` ( ( I \ { a } ) mPoly R ) ) |-> ( x e. D |-> if ( ( x ` a ) = 0 , ( f ` ( x |` ( I \ { a } ) ) ) , .0. ) ) ) ) ) with typecode |-
22 7 fvexi ⊢ M ∈ V
23 22 mptex ⊢ f ∈ M ⟼ x ∈ D ⟼ if x ⁡ A = 0 f ⁡ x ↾ J 0 ˙ ∈ V
24 23 a1i ⊢ φ → f ∈ M ⟼ x ∈ D ⟼ if x ⁡ A = 0 f ⁡ x ↾ J 0 ˙ ∈ V
25 18 21 5 24 fvmptd4 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 |-