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

Metamath Proof Explorer

Theorem evls1varpwval

Description: Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. See evl1varpwval . (Contributed by Thierry Arnoux, 24-Jan-2025)

Ref Expression
Hypotheses evls1varpwval.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
evls1varpwval.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
evls1varpwval.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
evls1varpwval.x ⊢ 𝑋 = ( var1 ‘ 𝑈 )
evls1varpwval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
evls1varpwval.e ⊢ ∧ = ( .g ‘ ( mulGrp ‘ 𝑊 ) )
evls1varpwval.f ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
evls1varpwval.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evls1varpwval.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evls1varpwval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
evls1varpwval.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
Assertion evls1varpwval ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ∧ 𝑋 ) ) ‘ 𝐶 ) = ( 𝑁 ↑ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 evls1varpwval.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2 evls1varpwval.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
3 evls1varpwval.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
4 evls1varpwval.x ⊢ 𝑋 = ( var1 ‘ 𝑈 )
5 evls1varpwval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
6 evls1varpwval.e ⊢ ∧ = ( .g ‘ ( mulGrp ‘ 𝑊 ) )
7 evls1varpwval.f ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
8 evls1varpwval.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
9 evls1varpwval.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
10 evls1varpwval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
11 evls1varpwval.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
12 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
13 2 subrgring ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
14 4 3 12 vr1cl ⊢ ( 𝑈 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑊 ) )
15 9 13 14 3syl ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑊 ) )
16 1 5 3 2 12 8 9 6 7 10 15 11 evls1expd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ∧ 𝑋 ) ) ‘ 𝐶 ) = ( 𝑁 ↑ ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐶 ) ) )
17 1 4 2 5 8 9 evls1var ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑋 ) = ( I ↾ 𝐵 ) )
18 17 fveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐶 ) = ( ( I ↾ 𝐵 ) ‘ 𝐶 ) )
19 fvresi ⊢ ( 𝐶 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝐶 ) = 𝐶 )
20 11 19 syl ⊢ ( 𝜑 → ( ( I ↾ 𝐵 ) ‘ 𝐶 ) = 𝐶 )
21 18 20 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐶 ) = 𝐶 )
22 21 oveq2d ⊢ ( 𝜑 → ( 𝑁 ↑ ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐶 ) ) = ( 𝑁 ↑ 𝐶 ) )
23 16 22 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ∧ 𝑋 ) ) ‘ 𝐶 ) = ( 𝑁 ↑ 𝐶 ) )