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

Metamath Proof Explorer

Theorem evlvarval

Description: Polynomial evaluation builder for a variable. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses evlvarval.1 ⊢ 𝑄 = ( 𝐼 eval 𝑆 )
evlvarval.2 ⊢ 𝑃 = ( 𝐼 mPoly 𝑆 )
evlvarval.3 ⊢ 𝐾 = ( Base ‘ 𝑆 )
evlvarval.4 ⊢ 𝐵 = ( Base ‘ 𝑃 )
evlvarval.5 ⊢ ∙ = ( .r ‘ 𝑃 )
evlvarval.6 ⊢ · = ( .r ‘ 𝑆 )
evlvarval.7 ⊢ ( 𝜑 → 𝐼 ∈ 𝑍 )
evlvarval.8 ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evlvarval.9 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
evlvarval.10 ⊢ 𝑉 = ( 𝐼 mVar 𝑆 )
evlvarval.11 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion evlvarval ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) ‘ 𝐴 ) = ( 𝐴 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 evlvarval.1 ⊢ 𝑄 = ( 𝐼 eval 𝑆 )
2 evlvarval.2 ⊢ 𝑃 = ( 𝐼 mPoly 𝑆 )
3 evlvarval.3 ⊢ 𝐾 = ( Base ‘ 𝑆 )
4 evlvarval.4 ⊢ 𝐵 = ( Base ‘ 𝑃 )
5 evlvarval.5 ⊢ ∙ = ( .r ‘ 𝑃 )
6 evlvarval.6 ⊢ · = ( .r ‘ 𝑆 )
7 evlvarval.7 ⊢ ( 𝜑 → 𝐼 ∈ 𝑍 )
8 evlvarval.8 ⊢ ( 𝜑 → 𝑆 ∈ CRing )
9 evlvarval.9 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
10 evlvarval.10 ⊢ 𝑉 = ( 𝐼 mVar 𝑆 )
11 evlvarval.11 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
12 8 crngringd ⊢ ( 𝜑 → 𝑆 ∈ Ring )
13 2 10 4 7 12 11 mvrcl ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 )
14 fveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ‘ 𝑋 ) = ( 𝐴 ‘ 𝑋 ) )
15 1 10 3 7 8 11 evlvar ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑎 ‘ 𝑋 ) ) )
16 3 fvexi ⊢ 𝐾 ∈ V
17 16 a1i ⊢ ( 𝜑 → 𝐾 ∈ V )
18 7 17 9 elmaprd ⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐾 )
19 18 11 ffvelcdmd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ 𝐾 )
20 14 15 9 19 fvmptd4 ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) ‘ 𝐴 ) = ( 𝐴 ‘ 𝑋 ) )
21 13 20 jca ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) ‘ 𝐴 ) = ( 𝐴 ‘ 𝑋 ) ) )