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

Metamath Proof Explorer

Theorem evls1scafv

Description: Value of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 21-Jan-2025)

Ref Expression
Hypotheses evls1scafv.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
evls1scafv.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
evls1scafv.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
evls1scafv.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
evls1scafv.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
evls1scafv.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evls1scafv.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evls1scafv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
evls1scafv.1 ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
Assertion evls1scafv ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝐶 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 evls1scafv.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2 evls1scafv.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
3 evls1scafv.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
4 evls1scafv.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
5 evls1scafv.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
6 evls1scafv.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
7 evls1scafv.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
8 evls1scafv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
9 evls1scafv.1 ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
10 1 2 3 4 5 6 7 8 evls1sca ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐵 × { 𝑋 } ) )
11 10 fveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝐶 ) = ( ( 𝐵 × { 𝑋 } ) ‘ 𝐶 ) )
12 fvconst2g ⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐵 × { 𝑋 } ) ‘ 𝐶 ) = 𝑋 )
13 8 9 12 syl2anc ⊢ ( 𝜑 → ( ( 𝐵 × { 𝑋 } ) ‘ 𝐶 ) = 𝑋 )
14 11 13 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝐶 ) = 𝑋 )