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 𝐼 ) ↦ ( 𝑔𝑋 ) ) )