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	$⊢ Z = ℤ / P ℤ$
	ply1fermltl.w	$⊢ W = {Poly}_{1} (Z)$
	ply1fermltl.x	$⊢ X = {var}_{1} (Z)$
	ply1fermltl.l	$⊢ \underset{˙}{+} = +_{W}$
	ply1fermltl.n	$⊢ N = {mulGrp}_{W}$
	ply1fermltl.t	$⊢ \underset{˙}{\times} = \cdot_{N}$
	ply1fermltl.c	$⊢ C = algSc (W)$
	ply1fermltl.a	$⊢ A = C (ℤRHom (Z) (E))$
	ply1fermltl.p	$⊢ φ \to P \in ℙ$
	ply1fermltl.1	$⊢ φ \to E \in ℤ$
Assertion	ply1fermltl	$⊢ φ \to P \underset{˙}{\times} (X \underset{˙}{+} A) = (P \underset{˙}{\times} X) \underset{˙}{+} A$

Proof

Step	Hyp	Ref	Expression
1		ply1fermltl.z	$⊢ Z = ℤ / P ℤ$
2		ply1fermltl.w	$⊢ W = {Poly}_{1} (Z)$
3		ply1fermltl.x	$⊢ X = {var}_{1} (Z)$
4		ply1fermltl.l	$⊢ \underset{˙}{+} = +_{W}$
5		ply1fermltl.n	$⊢ N = {mulGrp}_{W}$
6		ply1fermltl.t	$⊢ \underset{˙}{\times} = \cdot_{N}$
7		ply1fermltl.c	$⊢ C = algSc (W)$
8		ply1fermltl.a	$⊢ A = C (ℤRHom (Z) (E))$
9		ply1fermltl.p	$⊢ φ \to P \in ℙ$
10		ply1fermltl.1	$⊢ φ \to E \in ℤ$
11		eqid	$⊢ chr (Z) = chr (Z)$
12		prmnn	$⊢ P \in ℙ \to P \in ℕ$
13		nnnn0	$⊢ P \in ℕ \to P \in ℕ_{0}$
14	1	zncrng	$⊢ P \in ℕ_{0} \to Z \in CRing$
15	9 12 13 14	4syl	$⊢ φ \to Z \in CRing$
16	1	znchr	$⊢ P \in ℕ_{0} \to chr (Z) = P$
17	9 12 13 16	4syl	$⊢ φ \to chr (Z) = P$
18	17 9	eqeltrd	$⊢ φ \to chr (Z) \in ℙ$
19	2 3 4 5 6 7 8 11 15 18 10	ply1fermltlchr	$⊢ φ \to chr (Z) \underset{˙}{\times} (X \underset{˙}{+} A) = (chr (Z) \underset{˙}{\times} X) \underset{˙}{+} A$
20	17	oveq1d	$⊢ φ \to chr (Z) \underset{˙}{\times} (X \underset{˙}{+} A) = P \underset{˙}{\times} (X \underset{˙}{+} A)$
21	17	oveq1d	$⊢ φ \to chr (Z) \underset{˙}{\times} X = P \underset{˙}{\times} X$
22	21	oveq1d	$⊢ φ \to (chr (Z) \underset{˙}{\times} X) \underset{˙}{+} A = (P \underset{˙}{\times} X) \underset{˙}{+} A$
23	19 20 22	3eqtr3d	$⊢ φ \to P \underset{˙}{\times} (X \underset{˙}{+} A) = (P \underset{˙}{\times} X) \underset{˙}{+} A$

Metamath Proof Explorer

Theorem ply1fermltl

Proof