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