Metamath Proof Explorer


Theorem evls1varpw

Description: Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-Sep-2019)

Ref Expression
Hypotheses evls1varpw.q 𝑄 = ( 𝑆 evalSub1 𝑅 )
evls1varpw.u 𝑈 = ( 𝑆s 𝑅 )
evls1varpw.w 𝑊 = ( Poly1𝑈 )
evls1varpw.g 𝐺 = ( mulGrp ‘ 𝑊 )
evls1varpw.x 𝑋 = ( var1𝑈 )
evls1varpw.b 𝐵 = ( Base ‘ 𝑆 )
evls1varpw.e = ( .g𝐺 )
evls1varpw.s ( 𝜑𝑆 ∈ CRing )
evls1varpw.r ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evls1varpw.n ( 𝜑𝑁 ∈ ℕ0 )
Assertion evls1varpw ( 𝜑 → ( 𝑄 ‘ ( 𝑁 𝑋 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑆s 𝐵 ) ) ) ( 𝑄𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 evls1varpw.q 𝑄 = ( 𝑆 evalSub1 𝑅 )
2 evls1varpw.u 𝑈 = ( 𝑆s 𝑅 )
3 evls1varpw.w 𝑊 = ( Poly1𝑈 )
4 evls1varpw.g 𝐺 = ( mulGrp ‘ 𝑊 )
5 evls1varpw.x 𝑋 = ( var1𝑈 )
6 evls1varpw.b 𝐵 = ( Base ‘ 𝑆 )
7 evls1varpw.e = ( .g𝐺 )
8 evls1varpw.s ( 𝜑𝑆 ∈ CRing )
9 evls1varpw.r ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
10 evls1varpw.n ( 𝜑𝑁 ∈ ℕ0 )
11 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
12 2 subrgring ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
13 5 3 11 vr1cl ( 𝑈 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑊 ) )
14 9 12 13 3syl ( 𝜑𝑋 ∈ ( Base ‘ 𝑊 ) )
15 1 2 3 4 6 11 7 8 9 10 14 evls1pw ( 𝜑 → ( 𝑄 ‘ ( 𝑁 𝑋 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑆s 𝐵 ) ) ) ( 𝑄𝑋 ) ) )