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

Metamath Proof Explorer

Theorem evlsvarval

Description: Polynomial evaluation builder for a variable. (Contributed by SN, 27-Jul-2024)

Ref Expression
Hypotheses evlsvarval.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
evlsvarval.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
evlsvarval.v ⊢ 𝑉 = ( 𝐼 mVar 𝑈 )
evlsvarval.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
evlsvarval.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
evlsvarval.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
evlsvarval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
evlsvarval.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evlsvarval.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evlsvarval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
evlsvarval.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
Assertion evlsvarval ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) ‘ 𝐴 ) = ( 𝐴 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 evlsvarval.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 evlsvarval.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
3 evlsvarval.v ⊢ 𝑉 = ( 𝐼 mVar 𝑈 )
4 evlsvarval.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5 evlsvarval.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
6 evlsvarval.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
7 evlsvarval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
8 evlsvarval.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
9 evlsvarval.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
10 evlsvarval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
11 evlsvarval.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
12 4 subrgring ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
13 9 12 syl ⊢ ( 𝜑 → 𝑈 ∈ Ring )
14 2 3 6 7 13 10 mvrcl ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 )
15 fveq1 ⊢ ( 𝑔 = 𝐴 → ( 𝑔 ‘ 𝑋 ) = ( 𝐴 ‘ 𝑋 ) )
16 1 3 4 5 7 8 9 10 evlsvar ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑔 ∈ ( 𝐾 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )
17 fvexd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ V )
18 15 16 11 17 fvmptd4 ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) ‘ 𝐴 ) = ( 𝐴 ‘ 𝑋 ) )
19 14 18 jca ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) ‘ 𝐴 ) = ( 𝐴 ‘ 𝑋 ) ) )