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

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 𝐵 ) ) ) ( 𝑄 ‘ 𝑋 ) ) )