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

Metamath Proof Explorer

Theorem evlvar

Description: Simple polynomial evaluation maps variables to projections. (Contributed by AV, 12-Sep-2019)

Ref Expression
Hypotheses evlvar.q ⊢ 𝑄 = ( 𝐼 eval 𝑆 )
evlvar.v ⊢ 𝑉 = ( 𝐼 mVar 𝑆 )
evlvar.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
evlvar.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
evlvar.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evlvar.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion evlvar ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 evlvar.q ⊢ 𝑄 = ( 𝐼 eval 𝑆 )
2 evlvar.v ⊢ 𝑉 = ( 𝐼 mVar 𝑆 )
3 evlvar.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
4 evlvar.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5 evlvar.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
6 evlvar.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
7 eqid ⊢ ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 )
8 eqid ⊢ ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) = ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) )
9 eqid ⊢ ( 𝑆 ↾s 𝐵 ) = ( 𝑆 ↾s 𝐵 )
10 crngring ⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
11 3 subrgid ⊢ ( 𝑆 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
12 5 10 11 3syl ⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
13 7 1 8 9 3 4 5 12 6 evlsvarsrng ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) = ( 𝑄 ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) )
14 7 8 9 3 4 5 12 6 evlsvar ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )
15 2 4 12 9 subrgmvr ⊢ ( 𝜑 → 𝑉 = ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) )
16 15 fveq1d ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) = ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) )
17 16 eqcomd ⊢ ( 𝜑 → ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) = ( 𝑉 ‘ 𝑋 ) )
18 17 fveq2d ⊢ ( 𝜑 → ( 𝑄 ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) = ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) )
19 13 14 18 3eqtr3rd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )