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