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

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 ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ∧ ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑌 ) = 𝑌 ) )