Theorem ply1fermltl

Description: Fermat's little theorem for polynomials. If P is prime, Then ( X + A ) ^ P = ( ( X ^ P ) + A ) modulo P . (Contributed by Thierry Arnoux, 24-Jul-2024)

	Ref	Expression
Hypotheses	ply1fermltl.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑃 )
	ply1fermltl.w	⊢ 𝑊 = ( Poly1 ‘ 𝑍 )
	ply1fermltl.x	⊢ 𝑋 = ( var1 ‘ 𝑍 )
	ply1fermltl.l	⊢ + = ( +g ‘ 𝑊 )
	ply1fermltl.n	⊢ 𝑁 = ( mulGrp ‘ 𝑊 )
	ply1fermltl.t	⊢ ↑ = ( .g ‘ 𝑁 )
	ply1fermltl.c	⊢ 𝐶 = ( algSc ‘ 𝑊 )
	ply1fermltl.a	⊢ 𝐴 = ( 𝐶 ‘ ( ( ℤRHom ‘ 𝑍 ) ‘ 𝐸 ) )
	ply1fermltl.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	ply1fermltl.1	⊢ ( 𝜑 → 𝐸 ∈ ℤ )
Assertion	ply1fermltl	⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑋 + 𝐴 ) ) = ( ( 𝑃 ↑ 𝑋 ) + 𝐴 ) )

Proof

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