aks6d1c1p2

Description: P and linear factors are introspective. (Contributed by metakunt, 25-Apr-2025)

	Ref	Expression
Hypotheses	aks6d1c1p2.1	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in B \land \forall y \in (V PrimRoots R) e \underset{˙}{\times} O (f) (y) = O (f) (e \underset{˙}{\times} y))\}$
	aks6d1c1p2.2	$⊢ S = {Poly}_{1} (K)$
	aks6d1c1p2.3	$⊢ B = {Base}_{S}$
	aks6d1c1p2.4	$⊢ X = {var}_{1} (K)$
	aks6d1c1p2.5	$⊢ W = {mulGrp}_{S}$
	aks6d1c1p2.6	$⊢ V = {mulGrp}_{K}$
	aks6d1c1p2.7	$⊢ \underset{˙}{\times} = \cdot_{V}$
	aks6d1c1p2.8	$⊢ C = algSc (S)$
	aks6d1c1p2.9	$⊢ D = \cdot_{W}$
	aks6d1c1p2.10	$⊢ P = chr (K)$
	aks6d1c1p2.11	$⊢ O = {eval}_{1} (K)$
	aks6d1c1p2.12	$⊢ \underset{˙}{+} = +_{S}$
	aks6d1c1p2.13	$⊢ φ \to K \in Field$
	aks6d1c1p2.14	$⊢ φ \to P \in ℙ$
	aks6d1c1p2.15	$⊢ φ \to R \in ℕ$
	aks6d1c1p2.16	$⊢ φ \to N \gcd R = 1$
	aks6d1c1p2.17	$⊢ φ \to P ∥ N$
	aks6d1c1p2.18	$⊢ F = X \underset{˙}{+} C (ℤRHom (K) (A))$
	aks6d1c1p2.19	$⊢ φ \to A \in ℤ$
Assertion	aks6d1c1p2	$⊢ φ \to P \underset{˙}{\sim} F$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c1p2.1	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in B \land \forall y \in (V PrimRoots R) e \underset{˙}{\times} O (f) (y) = O (f) (e \underset{˙}{\times} y))\}$
2		aks6d1c1p2.2	$⊢ S = {Poly}_{1} (K)$
3		aks6d1c1p2.3	$⊢ B = {Base}_{S}$
4		aks6d1c1p2.4	$⊢ X = {var}_{1} (K)$
5		aks6d1c1p2.5	$⊢ W = {mulGrp}_{S}$
6		aks6d1c1p2.6	$⊢ V = {mulGrp}_{K}$
7		aks6d1c1p2.7	$⊢ \underset{˙}{\times} = \cdot_{V}$
8		aks6d1c1p2.8	$⊢ C = algSc (S)$
9		aks6d1c1p2.9	$⊢ D = \cdot_{W}$
10		aks6d1c1p2.10	$⊢ P = chr (K)$
11		aks6d1c1p2.11	$⊢ O = {eval}_{1} (K)$
12		aks6d1c1p2.12	$⊢ \underset{˙}{+} = +_{S}$
13		aks6d1c1p2.13	$⊢ φ \to K \in Field$
14		aks6d1c1p2.14	$⊢ φ \to P \in ℙ$
15		aks6d1c1p2.15	$⊢ φ \to R \in ℕ$
16		aks6d1c1p2.16	$⊢ φ \to N \gcd R = 1$
17		aks6d1c1p2.17	$⊢ φ \to P ∥ N$
18		aks6d1c1p2.18	$⊢ F = X \underset{˙}{+} C (ℤRHom (K) (A))$
19		aks6d1c1p2.19	$⊢ φ \to A \in ℤ$
20		isfld	$⊢ K \in Field \leftrightarrow (K \in DivRing \land K \in CRing)$
21	13 20	sylib	$⊢ φ \to (K \in DivRing \land K \in CRing)$
22	21	simprd	$⊢ φ \to K \in CRing$
23	6	crngmgp	$⊢ K \in CRing \to V \in CMnd$
24	22 23	syl	$⊢ φ \to V \in CMnd$
25	15	nnnn0d	$⊢ φ \to R \in ℕ_{0}$
26	24 25 7	isprimroot	$⊢ φ \to (y \in (V PrimRoots R) \leftrightarrow (y \in {Base}_{V} \land R \underset{˙}{\times} y = 0_{V} \land \forall l \in ℕ_{0} (l \underset{˙}{\times} y = 0_{V} \to R ∥ l)))$
27	26	biimpd	$⊢ φ \to (y \in (V PrimRoots R) \to (y \in {Base}_{V} \land R \underset{˙}{\times} y = 0_{V} \land \forall l \in ℕ_{0} (l \underset{˙}{\times} y = 0_{V} \to R ∥ l)))$
28	27	imp	$⊢ (φ \land y \in (V PrimRoots R)) \to (y \in {Base}_{V} \land R \underset{˙}{\times} y = 0_{V} \land \forall l \in ℕ_{0} (l \underset{˙}{\times} y = 0_{V} \to R ∥ l))$
29	28	simp1d	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in {Base}_{V}$
30		eqid	$⊢ {Base}_{K} = {Base}_{K}$
31	6 30	mgpbas	$⊢ {Base}_{K} = {Base}_{V}$
32	31	eqcomi	$⊢ {Base}_{V} = {Base}_{K}$
33	32	a1i	$⊢ φ \to {Base}_{V} = {Base}_{K}$
34	33	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to {Base}_{V} = {Base}_{K}$
35	34	eleq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to (y \in {Base}_{V} \leftrightarrow y \in {Base}_{K})$
36	29 35	mpbid	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in {Base}_{K}$
37	36	ex	$⊢ φ \to (y \in (V PrimRoots R) \to y \in {Base}_{K})$
38	18	a1i	$⊢ (φ \land y \in {Base}_{K}) \to F = X \underset{˙}{+} C (ℤRHom (K) (A))$
39	38	fveq2d	$⊢ (φ \land y \in {Base}_{K}) \to O (F) = O (X \underset{˙}{+} C (ℤRHom (K) (A)))$
40	39	fveq1d	$⊢ (φ \land y \in {Base}_{K}) \to O (F) (y) = O (X \underset{˙}{+} C (ℤRHom (K) (A))) (y)$
41	40	oveq2d	$⊢ (φ \land y \in {Base}_{K}) \to P \underset{˙}{\times} O (F) (y) = P \underset{˙}{\times} O (X \underset{˙}{+} C (ℤRHom (K) (A))) (y)$
42	22	adantr	$⊢ (φ \land y \in {Base}_{K}) \to K \in CRing$
43		simpr	$⊢ (φ \land y \in {Base}_{K}) \to y \in {Base}_{K}$
44		crngring	$⊢ K \in CRing \to K \in Ring$
45	4 2 3	vr1cl	$⊢ K \in Ring \to X \in B$
46	42 44 45	3syl	$⊢ (φ \land y \in {Base}_{K}) \to X \in B$
47	11 4 30 2 3 42 43	evl1vard	$⊢ (φ \land y \in {Base}_{K}) \to (X \in B \land O (X) (y) = y)$
48	47	simprd	$⊢ (φ \land y \in {Base}_{K}) \to O (X) (y) = y$
49	46 48	jca	$⊢ (φ \land y \in {Base}_{K}) \to (X \in B \land O (X) (y) = y)$
50	22 44	syl	$⊢ φ \to K \in Ring$
51	22	crngringd	$⊢ φ \to K \in Ring$
52		eqid	$⊢ ℤRHom (K) = ℤRHom (K)$
53	52	zrhrhm	$⊢ K \in Ring \to ℤRHom (K) \in (ℤ_{ring} RingHom K)$
54		rhmghm	$⊢ ℤRHom (K) \in (ℤ_{ring} RingHom K) \to ℤRHom (K) \in (ℤ_{ring} GrpHom K)$
55		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
56	55 30	ghmf	$⊢ ℤRHom (K) \in (ℤ_{ring} GrpHom K) \to ℤRHom (K) : ℤ ⟶ {Base}_{K}$
57	51 53 54 56	4syl	$⊢ φ \to ℤRHom (K) : ℤ ⟶ {Base}_{K}$
58	57 19	ffvelcdmd	$⊢ φ \to ℤRHom (K) (A) \in {Base}_{K}$
59	2 8 30 3	ply1sclcl	$⊢ (K \in Ring \land ℤRHom (K) (A) \in {Base}_{K}) \to C (ℤRHom (K) (A)) \in B$
60	50 58 59	syl2anc	$⊢ φ \to C (ℤRHom (K) (A)) \in B$
61	60	adantr	$⊢ (φ \land y \in {Base}_{K}) \to C (ℤRHom (K) (A)) \in B$
62	58	adantr	$⊢ (φ \land y \in {Base}_{K}) \to ℤRHom (K) (A) \in {Base}_{K}$
63	11 2 30 8 3 42 62 43	evl1scad	$⊢ (φ \land y \in {Base}_{K}) \to (C (ℤRHom (K) (A)) \in B \land O (C (ℤRHom (K) (A))) (y) = ℤRHom (K) (A))$
64	63	simprd	$⊢ (φ \land y \in {Base}_{K}) \to O (C (ℤRHom (K) (A))) (y) = ℤRHom (K) (A)$
65	61 64	jca	$⊢ (φ \land y \in {Base}_{K}) \to (C (ℤRHom (K) (A)) \in B \land O (C (ℤRHom (K) (A))) (y) = ℤRHom (K) (A))$
66		eqid	$⊢ +_{K} = +_{K}$
67	11 2 30 3 42 43 49 65 12 66	evl1addd	$⊢ (φ \land y \in {Base}_{K}) \to (X \underset{˙}{+} C (ℤRHom (K) (A)) \in B \land O (X \underset{˙}{+} C (ℤRHom (K) (A))) (y) = y +_{K} ℤRHom (K) (A))$
68	67	simprd	$⊢ (φ \land y \in {Base}_{K}) \to O (X \underset{˙}{+} C (ℤRHom (K) (A))) (y) = y +_{K} ℤRHom (K) (A)$
69	68	oveq2d	$⊢ (φ \land y \in {Base}_{K}) \to P \underset{˙}{\times} O (X \underset{˙}{+} C (ℤRHom (K) (A))) (y) = P \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))$
70	41 69	eqtrd	$⊢ (φ \land y \in {Base}_{K}) \to P \underset{˙}{\times} O (F) (y) = P \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))$
71	39	fveq1d	$⊢ (φ \land y \in {Base}_{K}) \to O (F) (P \underset{˙}{\times} y) = O (X \underset{˙}{+} C (ℤRHom (K) (A))) (P \underset{˙}{\times} y)$
72		eqid	$⊢ {Base}_{V} = {Base}_{V}$
73	6	ringmgp	$⊢ K \in Ring \to V \in Mnd$
74	42 44 73	3syl	$⊢ (φ \land y \in {Base}_{K}) \to V \in Mnd$
75		prmnn	$⊢ P \in ℙ \to P \in ℕ$
76	14 75	syl	$⊢ φ \to P \in ℕ$
77	76	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
78	77	adantr	$⊢ (φ \land y \in {Base}_{K}) \to P \in ℕ_{0}$
79	43 31	eleqtrdi	$⊢ (φ \land y \in {Base}_{K}) \to y \in {Base}_{V}$
80	72 7 74 78 79	mulgnn0cld	$⊢ (φ \land y \in {Base}_{K}) \to P \underset{˙}{\times} y \in {Base}_{V}$
81	80 32	eleqtrdi	$⊢ (φ \land y \in {Base}_{K}) \to P \underset{˙}{\times} y \in {Base}_{K}$
82	11 4 30 2 3 42 81	evl1vard	$⊢ (φ \land y \in {Base}_{K}) \to (X \in B \land O (X) (P \underset{˙}{\times} y) = P \underset{˙}{\times} y)$
83	11 2 30 8 3 42 62 81	evl1scad	$⊢ (φ \land y \in {Base}_{K}) \to (C (ℤRHom (K) (A)) \in B \land O (C (ℤRHom (K) (A))) (P \underset{˙}{\times} y) = ℤRHom (K) (A))$
84	83	simprd	$⊢ (φ \land y \in {Base}_{K}) \to O (C (ℤRHom (K) (A))) (P \underset{˙}{\times} y) = ℤRHom (K) (A)$
85	61 84	jca	$⊢ (φ \land y \in {Base}_{K}) \to (C (ℤRHom (K) (A)) \in B \land O (C (ℤRHom (K) (A))) (P \underset{˙}{\times} y) = ℤRHom (K) (A))$
86	11 2 30 3 42 81 82 85 12 66	evl1addd	$⊢ (φ \land y \in {Base}_{K}) \to (X \underset{˙}{+} C (ℤRHom (K) (A)) \in B \land O (X \underset{˙}{+} C (ℤRHom (K) (A))) (P \underset{˙}{\times} y) = (P \underset{˙}{\times} y) +_{K} ℤRHom (K) (A))$
87	86	simprd	$⊢ (φ \land y \in {Base}_{K}) \to O (X \underset{˙}{+} C (ℤRHom (K) (A))) (P \underset{˙}{\times} y) = (P \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
88	71 87	eqtrd	$⊢ (φ \land y \in {Base}_{K}) \to O (F) (P \underset{˙}{\times} y) = (P \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
89	5	fveq2i	$⊢ \cdot_{W} = \cdot_{{mulGrp}_{S}}$
90	9 89	eqtri	$⊢ D = \cdot_{{mulGrp}_{S}}$
91	6	fveq2i	$⊢ \cdot_{V} = \cdot_{{mulGrp}_{K}}$
92	7 91	eqtri	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{K}}$
93	11 2 30 3 42 43 47 90 92 78	evl1expd	$⊢ (φ \land y \in {Base}_{K}) \to (P D X \in B \land O (P D X) (y) = P \underset{˙}{\times} y)$
94		eqid	$⊢ +_{S} = +_{S}$
95	11 2 30 3 42 43 93 65 94 66	evl1addd	$⊢ (φ \land y \in {Base}_{K}) \to ((P D X) +_{S} C (ℤRHom (K) (A)) \in B \land O ((P D X) +_{S} C (ℤRHom (K) (A))) (y) = (P \underset{˙}{\times} y) +_{K} ℤRHom (K) (A))$
96	95	simprd	$⊢ (φ \land y \in {Base}_{K}) \to O ((P D X) +_{S} C (ℤRHom (K) (A))) (y) = (P \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
97		eqidd	$⊢ (φ \land y \in {Base}_{K}) \to (P \underset{˙}{\times} y) +_{K} ℤRHom (K) (A) = (P \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
98	96 97	eqtrd	$⊢ (φ \land y \in {Base}_{K}) \to O ((P D X) +_{S} C (ℤRHom (K) (A))) (y) = (P \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
99	98	eqcomd	$⊢ (φ \land y \in {Base}_{K}) \to (P \underset{˙}{\times} y) +_{K} ℤRHom (K) (A) = O ((P D X) +_{S} C (ℤRHom (K) (A))) (y)$
100		eqid	$⊢ C (ℤRHom (K) (A)) = C (ℤRHom (K) (A))$
101	2 4 94 5 9 8 100 10 22 14 19	ply1fermltlchr	$⊢ φ \to P D (X +_{S} C (ℤRHom (K) (A))) = (P D X) +_{S} C (ℤRHom (K) (A))$
102	101	fveq2d	$⊢ φ \to O (P D (X +_{S} C (ℤRHom (K) (A)))) = O ((P D X) +_{S} C (ℤRHom (K) (A)))$
103	102	fveq1d	$⊢ φ \to O (P D (X +_{S} C (ℤRHom (K) (A)))) (y) = O ((P D X) +_{S} C (ℤRHom (K) (A))) (y)$
104	103	eqcomd	$⊢ φ \to O ((P D X) +_{S} C (ℤRHom (K) (A))) (y) = O (P D (X +_{S} C (ℤRHom (K) (A)))) (y)$
105	104	adantr	$⊢ (φ \land y \in {Base}_{K}) \to O ((P D X) +_{S} C (ℤRHom (K) (A))) (y) = O (P D (X +_{S} C (ℤRHom (K) (A)))) (y)$
106	11 2 30 3 42 43 47 63 94 66	evl1addd	$⊢ (φ \land y \in {Base}_{K}) \to (X +_{S} C (ℤRHom (K) (A)) \in B \land O (X +_{S} C (ℤRHom (K) (A))) (y) = y +_{K} ℤRHom (K) (A))$
107	11 2 30 3 42 43 106 90 92 78	evl1expd	$⊢ (φ \land y \in {Base}_{K}) \to (P D (X +_{S} C (ℤRHom (K) (A))) \in B \land O (P D (X +_{S} C (ℤRHom (K) (A)))) (y) = P \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)))$
108	107	simprd	$⊢ (φ \land y \in {Base}_{K}) \to O (P D (X +_{S} C (ℤRHom (K) (A)))) (y) = P \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))$
109	99 105 108	3eqtrd	$⊢ (φ \land y \in {Base}_{K}) \to (P \underset{˙}{\times} y) +_{K} ℤRHom (K) (A) = P \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))$
110	88 109	eqtrd	$⊢ (φ \land y \in {Base}_{K}) \to O (F) (P \underset{˙}{\times} y) = P \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))$
111	110	eqcomd	$⊢ (φ \land y \in {Base}_{K}) \to P \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)) = O (F) (P \underset{˙}{\times} y)$
112	70 111	eqtrd	$⊢ (φ \land y \in {Base}_{K}) \to P \underset{˙}{\times} O (F) (y) = O (F) (P \underset{˙}{\times} y)$
113	112	adantlr	$⊢ ((φ \land y \in (V PrimRoots R)) \land y \in {Base}_{K}) \to P \underset{˙}{\times} O (F) (y) = O (F) (P \underset{˙}{\times} y)$
114	113	ex	$⊢ (φ \land y \in (V PrimRoots R)) \to (y \in {Base}_{K} \to P \underset{˙}{\times} O (F) (y) = O (F) (P \underset{˙}{\times} y))$
115	114	ex	$⊢ φ \to (y \in (V PrimRoots R) \to (y \in {Base}_{K} \to P \underset{˙}{\times} O (F) (y) = O (F) (P \underset{˙}{\times} y)))$
116	37 115	mpdd	$⊢ φ \to (y \in (V PrimRoots R) \to P \underset{˙}{\times} O (F) (y) = O (F) (P \underset{˙}{\times} y))$
117	116	imp	$⊢ (φ \land y \in (V PrimRoots R)) \to P \underset{˙}{\times} O (F) (y) = O (F) (P \underset{˙}{\times} y)$
118	117	ralrimiva	$⊢ φ \to \forall y \in (V PrimRoots R) P \underset{˙}{\times} O (F) (y) = O (F) (P \underset{˙}{\times} y)$
119	2	ply1crng	$⊢ K \in CRing \to S \in CRing$
120	22 119	syl	$⊢ φ \to S \in CRing$
121		crngring	$⊢ S \in CRing \to S \in Ring$
122	120 121	syl	$⊢ φ \to S \in Ring$
123	122	ringgrpd	$⊢ φ \to S \in Grp$
124	51 45	syl	$⊢ φ \to X \in B$
125	123 124 60	3jca	$⊢ φ \to (S \in Grp \land X \in B \land C (ℤRHom (K) (A)) \in B)$
126	3 12	grpcl	$⊢ (S \in Grp \land X \in B \land C (ℤRHom (K) (A)) \in B) \to X \underset{˙}{+} C (ℤRHom (K) (A)) \in B$
127	125 126	syl	$⊢ φ \to X \underset{˙}{+} C (ℤRHom (K) (A)) \in B$
128	18	a1i	$⊢ φ \to F = X \underset{˙}{+} C (ℤRHom (K) (A))$
129	128	eleq1d	$⊢ φ \to (F \in B \leftrightarrow X \underset{˙}{+} C (ℤRHom (K) (A)) \in B)$
130	127 129	mpbird	$⊢ φ \to F \in B$
131	1 130 76	aks6d1c1p1	$⊢ φ \to (P \underset{˙}{\sim} F \leftrightarrow \forall y \in (V PrimRoots R) P \underset{˙}{\times} O (F) (y) = O (F) (P \underset{˙}{\times} y))$
132	118 131	mpbird	$⊢ φ \to P \underset{˙}{\sim} F$

Metamath Proof Explorer

Theorem aks6d1c1p2

Proof