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 ) → ( 𝐷 ‘ ( 𝐹 ↑ 𝑋 ) ) ≤ 𝐹 )