# Metamath Proof Explorer

## Theorem evl1vard

Description: Polynomial evaluation builder for the variable. (Contributed by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses evl1var.q 𝑂 = ( eval1𝑅 )
evl1var.v 𝑋 = ( var1𝑅 )
evl1var.b 𝐵 = ( Base ‘ 𝑅 )
evl1vard.p 𝑃 = ( Poly1𝑅 )
evl1vard.u 𝑈 = ( Base ‘ 𝑃 )
evl1vard.1 ( 𝜑𝑅 ∈ CRing )
evl1vard.2 ( 𝜑𝑌𝐵 )
Assertion evl1vard ( 𝜑 → ( 𝑋𝑈 ∧ ( ( 𝑂𝑋 ) ‘ 𝑌 ) = 𝑌 ) )

### Proof

Step Hyp Ref Expression
1 evl1var.q 𝑂 = ( eval1𝑅 )
2 evl1var.v 𝑋 = ( var1𝑅 )
3 evl1var.b 𝐵 = ( Base ‘ 𝑅 )
4 evl1vard.p 𝑃 = ( Poly1𝑅 )
5 evl1vard.u 𝑈 = ( Base ‘ 𝑃 )
6 evl1vard.1 ( 𝜑𝑅 ∈ CRing )
7 evl1vard.2 ( 𝜑𝑌𝐵 )
8 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
9 2 4 5 vr1cl ( 𝑅 ∈ Ring → 𝑋𝑈 )
10 6 8 9 3syl ( 𝜑𝑋𝑈 )
11 1 2 3 evl1var ( 𝑅 ∈ CRing → ( 𝑂𝑋 ) = ( I ↾ 𝐵 ) )
12 6 11 syl ( 𝜑 → ( 𝑂𝑋 ) = ( I ↾ 𝐵 ) )
13 12 fveq1d ( 𝜑 → ( ( 𝑂𝑋 ) ‘ 𝑌 ) = ( ( I ↾ 𝐵 ) ‘ 𝑌 ) )
14 fvresi ( 𝑌𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑌 ) = 𝑌 )
15 7 14 syl ( 𝜑 → ( ( I ↾ 𝐵 ) ‘ 𝑌 ) = 𝑌 )
16 13 15 eqtrd ( 𝜑 → ( ( 𝑂𝑋 ) ‘ 𝑌 ) = 𝑌 )
17 10 16 jca ( 𝜑 → ( 𝑋𝑈 ∧ ( ( 𝑂𝑋 ) ‘ 𝑌 ) = 𝑌 ) )