Theorem ply1fermltlchr

Description: Fermat's little theorem for polynomials in a commutative ring F of characteristic P prime: we have the polynomial equation ( X + A ) ^ P = ( ( X ^ P ) + A ) . (Contributed by Thierry Arnoux, 9-Jan-2025)

	Ref	Expression
Hypotheses	ply1fermltlchr.w	⊢ 𝑊 = ( Poly1 ‘ 𝐹 )
	ply1fermltlchr.x	⊢ 𝑋 = ( var1 ‘ 𝐹 )
	ply1fermltlchr.l	⊢ + = ( +g ‘ 𝑊 )
	ply1fermltlchr.n	⊢ 𝑁 = ( mulGrp ‘ 𝑊 )
	ply1fermltlchr.t	⊢ ↑ = ( .g ‘ 𝑁 )
	ply1fermltlchr.c	⊢ 𝐶 = ( algSc ‘ 𝑊 )
	ply1fermltlchr.a	⊢ 𝐴 = ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) )
	ply1fermltlchr.p	⊢ 𝑃 = ( chr ‘ 𝐹 )
	ply1fermltlchr.f	⊢ ( 𝜑 → 𝐹 ∈ CRing )
	ply1fermltlchr.1	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	ply1fermltlchr.2	⊢ ( 𝜑 → 𝐸 ∈ ℤ )
Assertion	ply1fermltlchr	⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑋 + 𝐴 ) ) = ( ( 𝑃 ↑ 𝑋 ) + 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1fermltlchr.w	⊢ 𝑊 = ( Poly1 ‘ 𝐹 )
2		ply1fermltlchr.x	⊢ 𝑋 = ( var1 ‘ 𝐹 )
3		ply1fermltlchr.l	⊢ + = ( +g ‘ 𝑊 )
4		ply1fermltlchr.n	⊢ 𝑁 = ( mulGrp ‘ 𝑊 )
5		ply1fermltlchr.t	⊢ ↑ = ( .g ‘ 𝑁 )
6		ply1fermltlchr.c	⊢ 𝐶 = ( algSc ‘ 𝑊 )
7		ply1fermltlchr.a	⊢ 𝐴 = ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) )
8		ply1fermltlchr.p	⊢ 𝑃 = ( chr ‘ 𝐹 )
9		ply1fermltlchr.f	⊢ ( 𝜑 → 𝐹 ∈ CRing )
10		ply1fermltlchr.1	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
11		ply1fermltlchr.2	⊢ ( 𝜑 → 𝐸 ∈ ℤ )
12		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
13	4	fveq2i	⊢ ( .g ‘ 𝑁 ) = ( .g ‘ ( mulGrp ‘ 𝑊 ) )
14	5 13	eqtri	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑊 ) )
15		eqid	⊢ ( chr ‘ 𝑊 ) = ( chr ‘ 𝑊 )
16	1	ply1crng	⊢ ( 𝐹 ∈ CRing → 𝑊 ∈ CRing )
17	9 16	syl	⊢ ( 𝜑 → 𝑊 ∈ CRing )
18	1	ply1chr	⊢ ( 𝐹 ∈ CRing → ( chr ‘ 𝑊 ) = ( chr ‘ 𝐹 ) )
19	9 18	syl	⊢ ( 𝜑 → ( chr ‘ 𝑊 ) = ( chr ‘ 𝐹 ) )
20	19 8	eqtr4di	⊢ ( 𝜑 → ( chr ‘ 𝑊 ) = 𝑃 )
21	20 10	eqeltrd	⊢ ( 𝜑 → ( chr ‘ 𝑊 ) ∈ ℙ )
22	9	crngringd	⊢ ( 𝜑 → 𝐹 ∈ Ring )
23	2 1 12	vr1cl	⊢ ( 𝐹 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑊 ) )
24	22 23	syl	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑊 ) )
25		eqid	⊢ ( ℤRHom ‘ 𝐹 ) = ( ℤRHom ‘ 𝐹 )
26	25	zrhrhm	⊢ ( 𝐹 ∈ Ring → ( ℤRHom ‘ 𝐹 ) ∈ ( ℤring RingHom 𝐹 ) )
27		zringbas	⊢ ℤ = ( Base ‘ ℤring )
28		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
29	27 28	rhmf	⊢ ( ( ℤRHom ‘ 𝐹 ) ∈ ( ℤring RingHom 𝐹 ) → ( ℤRHom ‘ 𝐹 ) : ℤ ⟶ ( Base ‘ 𝐹 ) )
30	22 26 29	3syl	⊢ ( 𝜑 → ( ℤRHom ‘ 𝐹 ) : ℤ ⟶ ( Base ‘ 𝐹 ) )
31	30 11	ffvelcdmd	⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ∈ ( Base ‘ 𝐹 ) )
32	1 6 28 12	ply1sclcl	⊢ ( ( 𝐹 ∈ Ring ∧ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ∈ ( Base ‘ 𝐹 ) ) → ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ∈ ( Base ‘ 𝑊 ) )
33	22 31 32	syl2anc	⊢ ( 𝜑 → ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ∈ ( Base ‘ 𝑊 ) )
34	7 33	eqeltrid	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝑊 ) )
35	12 3 14 15 17 21 24 34	freshmansdream	⊢ ( 𝜑 → ( ( chr ‘ 𝑊 ) ↑ ( 𝑋 + 𝐴 ) ) = ( ( ( chr ‘ 𝑊 ) ↑ 𝑋 ) + ( ( chr ‘ 𝑊 ) ↑ 𝐴 ) ) )
36	20	oveq1d	⊢ ( 𝜑 → ( ( chr ‘ 𝑊 ) ↑ ( 𝑋 + 𝐴 ) ) = ( 𝑃 ↑ ( 𝑋 + 𝐴 ) ) )
37	20	oveq1d	⊢ ( 𝜑 → ( ( chr ‘ 𝑊 ) ↑ 𝑋 ) = ( 𝑃 ↑ 𝑋 ) )
38	20	oveq1d	⊢ ( 𝜑 → ( ( chr ‘ 𝑊 ) ↑ 𝐴 ) = ( 𝑃 ↑ 𝐴 ) )
39	1	ply1assa	⊢ ( 𝐹 ∈ CRing → 𝑊 ∈ AssAlg )
40		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
41	6 40	asclrhm	⊢ ( 𝑊 ∈ AssAlg → 𝐶 ∈ ( ( Scalar ‘ 𝑊 ) RingHom 𝑊 ) )
42	9 39 41	3syl	⊢ ( 𝜑 → 𝐶 ∈ ( ( Scalar ‘ 𝑊 ) RingHom 𝑊 ) )
43	9	crnggrpd	⊢ ( 𝜑 → 𝐹 ∈ Grp )
44	1	ply1sca	⊢ ( 𝐹 ∈ Grp → 𝐹 = ( Scalar ‘ 𝑊 ) )
45	43 44	syl	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝑊 ) )
46	45	oveq1d	⊢ ( 𝜑 → ( 𝐹 RingHom 𝑊 ) = ( ( Scalar ‘ 𝑊 ) RingHom 𝑊 ) )
47	42 46	eleqtrrd	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐹 RingHom 𝑊 ) )
48		eqid	⊢ ( mulGrp ‘ 𝐹 ) = ( mulGrp ‘ 𝐹 )
49	48 4	rhmmhm	⊢ ( 𝐶 ∈ ( 𝐹 RingHom 𝑊 ) → 𝐶 ∈ ( ( mulGrp ‘ 𝐹 ) MndHom 𝑁 ) )
50	47 49	syl	⊢ ( 𝜑 → 𝐶 ∈ ( ( mulGrp ‘ 𝐹 ) MndHom 𝑁 ) )
51		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
52		nnnn0	⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℕ0 )
53	10 51 52	3syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
54	48 28	mgpbas	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ ( mulGrp ‘ 𝐹 ) )
55		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝐹 ) ) = ( .g ‘ ( mulGrp ‘ 𝐹 ) )
56	54 55 5	mhmmulg	⊢ ( ( 𝐶 ∈ ( ( mulGrp ‘ 𝐹 ) MndHom 𝑁 ) ∧ 𝑃 ∈ ℕ0 ∧ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ∈ ( Base ‘ 𝐹 ) ) → ( 𝐶 ‘ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐹 ) ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ) = ( 𝑃 ↑ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ) )
57	50 53 31 56	syl3anc	⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐹 ) ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ) = ( 𝑃 ↑ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ) )
58	7	a1i	⊢ ( 𝜑 → 𝐴 = ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) )
59	58	oveq2d	⊢ ( 𝜑 → ( 𝑃 ↑ 𝐴 ) = ( 𝑃 ↑ ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ) )
60	57 59	eqtr4d	⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐹 ) ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ) = ( 𝑃 ↑ 𝐴 ) )
61		eqid	⊢ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 )
62	8 28 55 61 10 11 9	fermltlchr	⊢ ( 𝜑 → ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐹 ) ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) = ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) )
63	62	fveq2d	⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐹 ) ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ) = ( 𝐶 ‘ ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) )
64	63 7	eqtr4di	⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐹 ) ) ( ( ℤRHom ‘ 𝐹 ) ‘ 𝐸 ) ) ) = 𝐴 )
65	38 60 64	3eqtr2d	⊢ ( 𝜑 → ( ( chr ‘ 𝑊 ) ↑ 𝐴 ) = 𝐴 )
66	37 65	oveq12d	⊢ ( 𝜑 → ( ( ( chr ‘ 𝑊 ) ↑ 𝑋 ) + ( ( chr ‘ 𝑊 ) ↑ 𝐴 ) ) = ( ( 𝑃 ↑ 𝑋 ) + 𝐴 ) )
67	35 36 66	3eqtr3d	⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑋 + 𝐴 ) ) = ( ( 𝑃 ↑ 𝑋 ) + 𝐴 ) )