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

Metamath Proof Explorer

Theorem deg1pwle

Description: Limiting degree of a variable power. (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 deg1pwle ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ℕ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 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
7 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
8 2 3 4 5 7 ply1moncl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ℕ0 ) → ( 𝐹 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
9 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
10 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
11 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) )
12 7 9 10 11 lmodvs1 ⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝐹 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) = ( 𝐹 ↑ 𝑋 ) )
13 6 8 12 syl2an2r ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ℕ0 ) → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) = ( 𝐹 ↑ 𝑋 ) )
14 13 fveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) ) = ( 𝐷 ‘ ( 𝐹 ↑ 𝑋 ) ) )
15 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ℕ0 ) → 𝑅 ∈ Ring )
16 2 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
17 16 fveq2d ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
18 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
19 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
20 18 19 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
21 17 20 eqeltrrd ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ∈ ( Base ‘ 𝑅 ) )
22 21 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ℕ0 ) → ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ∈ ( Base ‘ 𝑅 ) )
23 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ℕ0 ) → 𝐹 ∈ ℕ0 )
24 1 18 2 3 10 4 5 deg1tmle ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ∈ ( Base ‘ 𝑅 ) ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) ) ≤ 𝐹 )
25 15 22 23 24 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) ) ≤ 𝐹 )
26 14 25 eqbrtrrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( 𝐹 ↑ 𝑋 ) ) ≤ 𝐹 )