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

Metamath Proof Explorer

Theorem evl1scvarpwval

Description: Value of a univariate polynomial evaluation mapping a multiple of an exponentiation of a variable to the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-Sep-2019)

Ref Expression
Hypotheses evl1varpw.q ⊢ 𝑄 = ( eval1 ‘ 𝑅 )
evl1varpw.w ⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
evl1varpw.g ⊢ 𝐺 = ( mulGrp ‘ 𝑊 )
evl1varpw.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
evl1varpw.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
evl1varpw.e ⊢ ↑ = ( .g ‘ 𝐺 )
evl1varpw.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
evl1varpw.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
evl1scvarpw.t1 ⊢ × = ( ·𝑠 ‘ 𝑊 )
evl1scvarpw.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
evl1scvarpwval.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
evl1scvarpwval.h ⊢ 𝐻 = ( mulGrp ‘ 𝑅 )
evl1scvarpwval.e ⊢ 𝐸 = ( .g ‘ 𝐻 )
evl1scvarpwval.t ⊢ · = ( .r ‘ 𝑅 )
Assertion evl1scvarpwval ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ‘ 𝐶 ) = ( 𝐴 · ( 𝑁 𝐸 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 evl1varpw.q ⊢ 𝑄 = ( eval1 ‘ 𝑅 )
2 evl1varpw.w ⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
3 evl1varpw.g ⊢ 𝐺 = ( mulGrp ‘ 𝑊 )
4 evl1varpw.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
5 evl1varpw.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
6 evl1varpw.e ⊢ ↑ = ( .g ‘ 𝐺 )
7 evl1varpw.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
8 evl1varpw.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9 evl1scvarpw.t1 ⊢ × = ( ·𝑠 ‘ 𝑊 )
10 evl1scvarpw.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
11 evl1scvarpwval.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
12 evl1scvarpwval.h ⊢ 𝐻 = ( mulGrp ‘ 𝑅 )
13 evl1scvarpwval.e ⊢ 𝐸 = ( .g ‘ 𝐻 )
14 evl1scvarpwval.t ⊢ · = ( .r ‘ 𝑅 )
15 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
16 3 15 mgpbas ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝐺 )
17 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
18 7 17 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
19 2 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑊 ∈ Ring )
20 18 19 syl ⊢ ( 𝜑 → 𝑊 ∈ Ring )
21 3 ringmgp ⊢ ( 𝑊 ∈ Ring → 𝐺 ∈ Mnd )
22 20 21 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
23 4 2 15 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑊 ) )
24 18 23 syl ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑊 ) )
25 16 6 22 8 24 mulgnn0cld ⊢ ( 𝜑 → ( 𝑁 ↑ 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
26 1 2 3 4 5 6 7 8 11 12 13 evl1varpwval ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) ‘ 𝐶 ) = ( 𝑁 𝐸 𝐶 ) )
27 25 26 jca ⊢ ( 𝜑 → ( ( 𝑁 ↑ 𝑋 ) ∈ ( Base ‘ 𝑊 ) ∧ ( ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) ‘ 𝐶 ) = ( 𝑁 𝐸 𝐶 ) ) )
28 1 2 5 15 7 11 27 10 9 14 evl1vsd ⊢ ( 𝜑 → ( ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) ∧ ( ( 𝑄 ‘ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ‘ 𝐶 ) = ( 𝐴 · ( 𝑁 𝐸 𝐶 ) ) ) )
29 28 simprd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) ‘ 𝐶 ) = ( 𝐴 · ( 𝑁 𝐸 𝐶 ) ) )