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

Metamath Proof Explorer

Theorem evlscaval

Description: Polynomial evaluation for scalars. See evlsscaval . (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses evlscafv.1 ⊢ 𝑄 = ( 𝐼 eval 𝑅 )
evlscafv.2 ⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
evlscafv.3 ⊢ 𝐵 = ( Base ‘ 𝑅 )
evlscafv.4 ⊢ 𝐴 = ( algSc ‘ 𝑊 )
evlscafv.5 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
evlscafv.6 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
evlscafv.7 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
evlscafv.8 ⊢ ( 𝜑 → 𝐿 : 𝐼 ⟶ 𝐵 )
Assertion evlscaval ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝐿 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 evlscafv.1 ⊢ 𝑄 = ( 𝐼 eval 𝑅 )
2 evlscafv.2 ⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
3 evlscafv.3 ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 evlscafv.4 ⊢ 𝐴 = ( algSc ‘ 𝑊 )
5 evlscafv.5 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 evlscafv.6 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
7 evlscafv.7 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 evlscafv.8 ⊢ ( 𝜑 → 𝐿 : 𝐼 ⟶ 𝐵 )
9 1 2 3 4 5 6 7 evlsca ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )
10 9 fveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝐿 ) = ( ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) ‘ 𝐿 ) )
11 3 fvexi ⊢ 𝐵 ∈ V
12 11 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
13 12 5 8 elmapdd ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐵 ↑m 𝐼 ) )
14 fvconst2g ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐿 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) ‘ 𝐿 ) = 𝑋 )
15 7 13 14 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) ‘ 𝐿 ) = 𝑋 )
16 10 15 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝐿 ) = 𝑋 )