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

Metamath Proof Explorer

Theorem deg1pw

Description: Exact degree of a variable power over a nontrivial ring. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses deg1pw.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
deg1pw.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
deg1pw.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
deg1pw.n ⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
deg1pw.e ⊢ ↑ = ( .g ‘ 𝑁 )
Assertion deg1pw ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( 𝐹 ↑ 𝑋 ) ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 deg1pw.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2 deg1pw.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 deg1pw.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
4 deg1pw.n ⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
5 deg1pw.e ⊢ ↑ = ( .g ‘ 𝑁 )
6 2 ply1sca ⊢ ( 𝑅 ∈ NzRing → 𝑅 = ( Scalar ‘ 𝑃 ) )
7 6 adantr ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
8 7 fveq2d ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
9 8 oveq1d ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) = ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) )
10 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
11 10 adantr ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → 𝑅 ∈ Ring )
12 2 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
13 11 12 syl ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → 𝑃 ∈ LMod )
14 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
15 4 14 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑁 )
16 2 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
17 4 ringmgp ⊢ ( 𝑃 ∈ Ring → 𝑁 ∈ Mnd )
18 11 16 17 3syl ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → 𝑁 ∈ Mnd )
19 simpr ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → 𝐹 ∈ ℕ0 )
20 3 2 14 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
21 11 20 syl ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
22 15 5 18 19 21 mulgnn0cld ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( 𝐹 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
23 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
24 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
25 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) )
26 14 23 24 25 lmodvs1 ⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝐹 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) = ( 𝐹 ↑ 𝑋 ) )
27 13 22 26 syl2anc ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) = ( 𝐹 ↑ 𝑋 ) )
28 9 27 eqtrd ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) = ( 𝐹 ↑ 𝑋 ) )
29 28 fveq2d ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) ) = ( 𝐷 ‘ ( 𝐹 ↑ 𝑋 ) ) )
30 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
31 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
32 30 31 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
33 11 32 syl ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
34 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
35 31 34 nzrnz ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
36 35 adantr ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
37 1 30 2 3 24 4 5 34 deg1tm ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) ) = 𝐹 )
38 11 33 36 19 37 syl121anc ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) ) = 𝐹 )
39 29 38 eqtr3d ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( 𝐹 ↑ 𝑋 ) ) = 𝐹 )