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

Metamath Proof Explorer

Theorem extvfvvcl

Description: Closure for 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 extvfvvcl.d ⊢ D = h ∈ ℕ 0 I | finSupp 0 ⁡ h
extvfvvcl.3 ⊢ 0 ˙ = 0 R
extvfvvcl.i ⊢ φ → I ∈ V
extvfvvcl.r ⊢ φ → R ∈ Ring
extvfvvcl.b ⊢ B = Base R
extvfvvcl.j ⊢ J = I ∖ A
extvfvvcl.m ⊢ M = Base J mPoly R
extvfvvcl.1 ⊢ φ → A ∈ I
extvfvvcl.f ⊢ φ → F ∈ M
extvfvvcl.x ⊢ φ → X ∈ D
Assertion extvfvvcl Could not format assertion : No typesetting found for |- ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) e. B ) with typecode |-

Proof

Step Hyp Ref Expression
1 extvfvvcl.d ⊢ D = h ∈ ℕ 0 I | finSupp 0 ⁡ h
2 extvfvvcl.3 ⊢ 0 ˙ = 0 R
3 extvfvvcl.i ⊢ φ → I ∈ V
4 extvfvvcl.r ⊢ φ → R ∈ Ring
5 extvfvvcl.b ⊢ B = Base R
6 extvfvvcl.j ⊢ J = I ∖ A
7 extvfvvcl.m ⊢ M = Base J mPoly R
8 extvfvvcl.1 ⊢ φ → A ∈ I
9 extvfvvcl.f ⊢ φ → F ∈ M
10 extvfvvcl.x ⊢ φ → X ∈ D
11 1 2 3 4 8 6 7 9 10 extvfvv 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 |-
12 eqid ⊢ J mPoly R = J mPoly R
13 eqid ⊢ h ∈ ℕ 0 J | finSupp 0 ⁡ h = h ∈ ℕ 0 J | finSupp 0 ⁡ h
14 13 psrbasfsupp ⊢ h ∈ ℕ 0 J | finSupp 0 ⁡ h = h ∈ ℕ 0 J | h -1 ℕ ∈ Fin
15 12 5 7 14 9 mplelf ⊢ φ → F : h ∈ ℕ 0 J | finSupp 0 ⁡ h ⟶ B
16 breq1 ⊢ h = X ↾ J → finSupp 0 ⁡ h ↔ finSupp 0 ⁡ X ↾ J
17 nn0ex ⊢ ℕ 0 ∈ V
18 17 a1i ⊢ φ → ℕ 0 ∈ V
19 3 difexd ⊢ φ → I ∖ A ∈ V
20 6 19 eqeltrid ⊢ φ → J ∈ V
21 1 ssrab3 ⊢ D ⊆ ℕ 0 I
22 21 10 sselid ⊢ φ → X ∈ ℕ 0 I
23 3 18 22 elmaprd ⊢ φ → X : I ⟶ ℕ 0
24 difssd ⊢ φ → I ∖ A ⊆ I
25 6 24 eqsstrid ⊢ φ → J ⊆ I
26 23 25 fssresd ⊢ φ → X ↾ J : J ⟶ ℕ 0
27 18 20 26 elmapdd ⊢ φ → X ↾ J ∈ ℕ 0 J
28 breq1 ⊢ h = X → finSupp 0 ⁡ h ↔ finSupp 0 ⁡ X
29 10 1 eleqtrdi ⊢ φ → X ∈ h ∈ ℕ 0 I | finSupp 0 ⁡ h
30 28 29 elrabrd ⊢ φ → finSupp 0 ⁡ X
31 c0ex ⊢ 0 ∈ V
32 31 a1i ⊢ φ → 0 ∈ V
33 30 32 fsuppres ⊢ φ → finSupp 0 ⁡ X ↾ J
34 16 27 33 elrabd ⊢ φ → X ↾ J ∈ h ∈ ℕ 0 J | finSupp 0 ⁡ h
35 15 34 ffvelcdmd ⊢ φ → F ⁡ X ↾ J ∈ B
36 5 2 ring0cl ⊢ R ∈ Ring → 0 ˙ ∈ B
37 4 36 syl ⊢ φ → 0 ˙ ∈ B
38 35 37 ifcld ⊢ φ → if X ⁡ A = 0 F ⁡ X ↾ J 0 ˙ ∈ B
39 11 38 eqeltrd Could not format ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) e. B ) : No typesetting found for |- ( ph -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` X ) e. B ) with typecode |-