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	2	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
15	4	ringmgp	⊢ ( 𝑃 ∈ Ring → 𝑁 ∈ Mnd )
16	11 14 15	3syl	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → 𝑁 ∈ Mnd )
17		simpr	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → 𝐹 ∈ ℕ0 )
18		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
19	3 2 18	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
20	11 19	syl	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
21	4 18	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑁 )
22	21 5	mulgnn0cl	⊢ ( ( 𝑁 ∈ Mnd ∧ 𝐹 ∈ ℕ0 ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( 𝐹 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
23	16 17 20 22	syl3anc	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( 𝐹 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
24		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
25		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
26		eqid	⊢ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) )
27	18 24 25 26	lmodvs1	⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝐹 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) = ( 𝐹 ↑ 𝑋 ) )
28	13 23 27	syl2anc	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) = ( 𝐹 ↑ 𝑋 ) )
29	9 28	eqtrd	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) = ( 𝐹 ↑ 𝑋 ) )
30	29	fveq2d	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) ) = ( 𝐷 ‘ ( 𝐹 ↑ 𝑋 ) ) )
31		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
32		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
33	31 32	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
34	11 33	syl	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
35		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
36	32 35	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
37	36	adantr	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
38	1 31 2 3 25 4 5 35	deg1tm	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) ) = 𝐹 )
39	11 34 37 17 38	syl121anc	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↑ 𝑋 ) ) ) = 𝐹 )
40	30 39	eqtr3d	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0 ) → ( 𝐷 ‘ ( 𝐹 ↑ 𝑋 ) ) = 𝐹 )