aks6d1c1p6

Description: If a polynomials F is introspective to E , then so are its powers. (Contributed by metakunt, 30-Apr-2025)

	Ref	Expression
Hypotheses	aks6d1c1.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))\}$
	aks6d1c1.2	$⊢ S = {Poly}_{1} (K)$
	aks6d1c1.3	$⊢ B = {Base}_{S}$
	aks6d1c1.4	$⊢ X = {var}_{1} (K)$
	aks6d1c1.5	$⊢ W = {mulGrp}_{S}$
	aks6d1c1.6	$⊢ V = {mulGrp}_{K}$
	aks6d1c1.7	$⊢ \underset{˙}{\times} = \cdot_{V}$
	aks6d1c1.8	$⊢ C = algSc (S)$
	aks6d1c1.9	$⊢ D = \cdot_{W}$
	aks6d1c1.10	$⊢ P = chr (K)$
	aks6d1c1.11	$⊢ O = {eval}_{1} (K)$
	aks6d1c1.12	$⊢ \underset{˙}{+} = +_{S}$
	aks6d1c1.13	$⊢ φ \to K \in Field$
	aks6d1c1.14	$⊢ φ \to P \in ℙ$
	aks6d1c1.15	$⊢ φ \to R \in ℕ$
	aks6d1c1.16	$⊢ φ \to N \in ℕ$
	aks6d1c1.17	$⊢ φ \to P ∥ N$
	aks6d1c1.18	$⊢ φ \to N \gcd R = 1$
	aks6d1c1p6.1	$⊢ φ \to E \underset{˙}{\sim} F$
	aks6d1c1p6.2	$⊢ φ \to L \in ℕ_{0}$
Assertion	aks6d1c1p6	$⊢ φ \to E \underset{˙}{\sim} (L D F)$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c1.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		aks6d1c1.2	$⊢ S = {Poly}_{1} (K)$
3		aks6d1c1.3	$⊢ B = {Base}_{S}$
4		aks6d1c1.4	$⊢ X = {var}_{1} (K)$
5		aks6d1c1.5	$⊢ W = {mulGrp}_{S}$
6		aks6d1c1.6	$⊢ V = {mulGrp}_{K}$
7		aks6d1c1.7	$⊢ \underset{˙}{\times} = \cdot_{V}$
8		aks6d1c1.8	$⊢ C = algSc (S)$
9		aks6d1c1.9	$⊢ D = \cdot_{W}$
10		aks6d1c1.10	$⊢ P = chr (K)$
11		aks6d1c1.11	$⊢ O = {eval}_{1} (K)$
12		aks6d1c1.12	$⊢ \underset{˙}{+} = +_{S}$
13		aks6d1c1.13	$⊢ φ \to K \in Field$
14		aks6d1c1.14	$⊢ φ \to P \in ℙ$
15		aks6d1c1.15	$⊢ φ \to R \in ℕ$
16		aks6d1c1.16	$⊢ φ \to N \in ℕ$
17		aks6d1c1.17	$⊢ φ \to P ∥ N$
18		aks6d1c1.18	$⊢ φ \to N \gcd R = 1$
19		aks6d1c1p6.1	$⊢ φ \to E \underset{˙}{\sim} F$
20		aks6d1c1p6.2	$⊢ φ \to L \in ℕ_{0}$
21		oveq1	$⊢ h = 0 \to h D F = 0 D F$
22	21	breq2d	$⊢ h = 0 \to (E \underset{˙}{\sim} (h D F) \leftrightarrow E \underset{˙}{\sim} (0 D F))$
23		oveq1	$⊢ h = i \to h D F = i D F$
24	23	breq2d	$⊢ h = i \to (E \underset{˙}{\sim} (h D F) \leftrightarrow E \underset{˙}{\sim} (i D F))$
25		oveq1	$⊢ h = i + 1 \to h D F = (i + 1) D F$
26	25	breq2d	$⊢ h = i + 1 \to (E \underset{˙}{\sim} (h D F) \leftrightarrow E \underset{˙}{\sim} ((i + 1) D F))$
27		oveq1	$⊢ h = L \to h D F = L D F$
28	27	breq2d	$⊢ h = L \to (E \underset{˙}{\sim} (h D F) \leftrightarrow E \underset{˙}{\sim} (L D F))$
29	1 19	aks6d1c1p1rcl	$⊢ φ \to (E \in ℕ \land F \in B)$
30	29	simprd	$⊢ φ \to F \in B$
31	30 3	eleqtrdi	$⊢ φ \to F \in {Base}_{S}$
32		eqid	$⊢ {Base}_{S} = {Base}_{S}$
33	5 32	mgpbas	$⊢ {Base}_{S} = {Base}_{W}$
34	31 33	eleqtrdi	$⊢ φ \to F \in {Base}_{W}$
35		eqid	$⊢ {Base}_{W} = {Base}_{W}$
36		eqid	$⊢ 0_{W} = 0_{W}$
37	35 36 9	mulg0	$⊢ F \in {Base}_{W} \to 0 D F = 0_{W}$
38	34 37	syl	$⊢ φ \to 0 D F = 0_{W}$
39		eqid	$⊢ 1_{S} = 1_{S}$
40	5 39	ringidval	$⊢ 1_{S} = 0_{W}$
41	40	eqcomi	$⊢ 0_{W} = 1_{S}$
42	38 41	eqtrdi	$⊢ φ \to 0 D F = 1_{S}$
43	42	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to 0 D F = 1_{S}$
44	43	fveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (0 D F) = O (1_{S})$
45	44	fveq1d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (0 D F) (y) = O (1_{S}) (y)$
46	45	oveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} O (0 D F) (y) = E \underset{˙}{\times} O (1_{S}) (y)$
47	13	fldcrngd	$⊢ φ \to K \in CRing$
48		crngring	$⊢ K \in CRing \to K \in Ring$
49	47 48	syl	$⊢ φ \to K \in Ring$
50		eqid	$⊢ 1_{K} = 1_{K}$
51	2 8 50 39	ply1scl1	$⊢ K \in Ring \to C (1_{K}) = 1_{S}$
52	49 51	syl	$⊢ φ \to C (1_{K}) = 1_{S}$
53	52	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to C (1_{K}) = 1_{S}$
54	53	eqcomd	$⊢ (φ \land y \in (V PrimRoots R)) \to 1_{S} = C (1_{K})$
55	54	fveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (1_{S}) = O (C (1_{K}))$
56	55	fveq1d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (1_{S}) (y) = O (C (1_{K})) (y)$
57	56	oveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} O (1_{S}) (y) = E \underset{˙}{\times} O (C (1_{K})) (y)$
58		eqid	$⊢ {Base}_{K} = {Base}_{K}$
59	47	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to K \in CRing$
60	58 50	ringidcl	$⊢ K \in Ring \to 1_{K} \in {Base}_{K}$
61	49 60	syl	$⊢ φ \to 1_{K} \in {Base}_{K}$
62	61	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to 1_{K} \in {Base}_{K}$
63	6	crngmgp	$⊢ K \in CRing \to V \in CMnd$
64	47 63	syl	$⊢ φ \to V \in CMnd$
65	15	nnnn0d	$⊢ φ \to R \in ℕ_{0}$
66		eqid	$⊢ \cdot_{V} = \cdot_{V}$
67	64 65 66	isprimroot	$⊢ φ \to (y \in (V PrimRoots R) \leftrightarrow (y \in {Base}_{V} \land R \cdot_{V} y = 0_{V} \land \forall z \in ℕ_{0} (z \cdot_{V} y = 0_{V} \to R ∥ z)))$
68	67	biimpd	$⊢ φ \to (y \in (V PrimRoots R) \to (y \in {Base}_{V} \land R \cdot_{V} y = 0_{V} \land \forall z \in ℕ_{0} (z \cdot_{V} y = 0_{V} \to R ∥ z)))$
69	68	imp	$⊢ (φ \land y \in (V PrimRoots R)) \to (y \in {Base}_{V} \land R \cdot_{V} y = 0_{V} \land \forall z \in ℕ_{0} (z \cdot_{V} y = 0_{V} \to R ∥ z))$
70	69	simp1d	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in {Base}_{V}$
71	6 58	mgpbas	$⊢ {Base}_{K} = {Base}_{V}$
72	71	eqcomi	$⊢ {Base}_{V} = {Base}_{K}$
73	70 72	eleqtrdi	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in {Base}_{K}$
74	11 2 58 8 3 59 62 73	evl1scad	$⊢ (φ \land y \in (V PrimRoots R)) \to (C (1_{K}) \in B \land O (C (1_{K})) (y) = 1_{K})$
75	74	simprd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (C (1_{K})) (y) = 1_{K}$
76	75	oveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} O (C (1_{K})) (y) = E \underset{˙}{\times} 1_{K}$
77	64	cmnmndd	$⊢ φ \to V \in Mnd$
78	29	simpld	$⊢ φ \to E \in ℕ$
79	78	nnnn0d	$⊢ φ \to E \in ℕ_{0}$
80		eqid	$⊢ {Base}_{V} = {Base}_{V}$
81	6 50	ringidval	$⊢ 1_{K} = 0_{V}$
82	80 7 81	mulgnn0z	$⊢ (V \in Mnd \land E \in ℕ_{0}) \to E \underset{˙}{\times} 1_{K} = 1_{K}$
83	77 79 82	syl2anc	$⊢ φ \to E \underset{˙}{\times} 1_{K} = 1_{K}$
84	83	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} 1_{K} = 1_{K}$
85	77	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to V \in Mnd$
86	79	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to E \in ℕ_{0}$
87	71 7	mulgnn0cl	$⊢ (V \in Mnd \land E \in ℕ_{0} \land y \in {Base}_{K}) \to E \underset{˙}{\times} y \in {Base}_{K}$
88	85 86 73 87	syl3anc	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} y \in {Base}_{K}$
89	11 2 58 8 3 59 62 88	evl1scad	$⊢ (φ \land y \in (V PrimRoots R)) \to (C (1_{K}) \in B \land O (C (1_{K})) (E \underset{˙}{\times} y) = 1_{K})$
90	89	simprd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (C (1_{K})) (E \underset{˙}{\times} y) = 1_{K}$
91	90	eqcomd	$⊢ (φ \land y \in (V PrimRoots R)) \to 1_{K} = O (C (1_{K})) (E \underset{˙}{\times} y)$
92	76 84 91	3eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} O (C (1_{K})) (y) = O (C (1_{K})) (E \underset{˙}{\times} y)$
93	53	fveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (C (1_{K})) = O (1_{S})$
94	93	fveq1d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (C (1_{K})) (E \underset{˙}{\times} y) = O (1_{S}) (E \underset{˙}{\times} y)$
95	57 92 94	3eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} O (1_{S}) (y) = O (1_{S}) (E \underset{˙}{\times} y)$
96	43	eqcomd	$⊢ (φ \land y \in (V PrimRoots R)) \to 1_{S} = 0 D F$
97	96	fveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (1_{S}) = O (0 D F)$
98	97	fveq1d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (1_{S}) (E \underset{˙}{\times} y) = O (0 D F) (E \underset{˙}{\times} y)$
99	46 95 98	3eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} O (0 D F) (y) = O (0 D F) (E \underset{˙}{\times} y)$
100	99	ralrimiva	$⊢ φ \to \forall y \in (V PrimRoots R) E \underset{˙}{\times} O (0 D F) (y) = O (0 D F) (E \underset{˙}{\times} y)$
101	2	ply1ring	$⊢ K \in Ring \to S \in Ring$
102	49 101	syl	$⊢ φ \to S \in Ring$
103	32 39	ringidcl	$⊢ S \in Ring \to 1_{S} \in {Base}_{S}$
104	102 103	syl	$⊢ φ \to 1_{S} \in {Base}_{S}$
105	42	eqcomd	$⊢ φ \to 1_{S} = 0 D F$
106	3	a1i	$⊢ φ \to B = {Base}_{S}$
107	106	eqcomd	$⊢ φ \to {Base}_{S} = B$
108	105 107	eleq12d	$⊢ φ \to (1_{S} \in {Base}_{S} \leftrightarrow 0 D F \in B)$
109	104 108	mpbid	$⊢ φ \to 0 D F \in B$
110	1 109 78	aks6d1c1p1	$⊢ φ \to (E \underset{˙}{\sim} (0 D F) \leftrightarrow \forall y \in (V PrimRoots R) E \underset{˙}{\times} O (0 D F) (y) = O (0 D F) (E \underset{˙}{\times} y))$
111	100 110	mpbird	$⊢ φ \to E \underset{˙}{\sim} (0 D F)$
112	13	ad2antrr	$⊢ ((φ \land i \in ℕ_{0}) \land E \underset{˙}{\sim} (i D F)) \to K \in Field$
113	14	ad2antrr	$⊢ ((φ \land i \in ℕ_{0}) \land E \underset{˙}{\sim} (i D F)) \to P \in ℙ$
114	15	ad2antrr	$⊢ ((φ \land i \in ℕ_{0}) \land E \underset{˙}{\sim} (i D F)) \to R \in ℕ$
115	18	ad2antrr	$⊢ ((φ \land i \in ℕ_{0}) \land E \underset{˙}{\sim} (i D F)) \to N \gcd R = 1$
116	17	ad2antrr	$⊢ ((φ \land i \in ℕ_{0}) \land E \underset{˙}{\sim} (i D F)) \to P ∥ N$
117		simpr	$⊢ ((φ \land i \in ℕ_{0}) \land E \underset{˙}{\sim} (i D F)) \to E \underset{˙}{\sim} (i D F)$
118	19	ad2antrr	$⊢ ((φ \land i \in ℕ_{0}) \land E \underset{˙}{\sim} (i D F)) \to E \underset{˙}{\sim} F$
119	1 2 3 4 5 6 7 8 9 10 11 12 112 113 114 115 116 117 118	aks6d1c1p4	$⊢ ((φ \land i \in ℕ_{0}) \land E \underset{˙}{\sim} (i D F)) \to E \underset{˙}{\sim} ((i D F) +_{W} F)$
120	5	ringmgp	$⊢ S \in Ring \to W \in Mnd$
121	102 120	syl	$⊢ φ \to W \in Mnd$
122	121	adantr	$⊢ (φ \land i \in ℕ_{0}) \to W \in Mnd$
123	122	adantr	$⊢ ((φ \land i \in ℕ_{0}) \land E \underset{˙}{\sim} (i D F)) \to W \in Mnd$
124		simplr	$⊢ ((φ \land i \in ℕ_{0}) \land E \underset{˙}{\sim} (i D F)) \to i \in ℕ_{0}$
125	33	a1i	$⊢ φ \to {Base}_{S} = {Base}_{W}$
126	106 125	eqtrd	$⊢ φ \to B = {Base}_{W}$
127	126	eleq2d	$⊢ φ \to (F \in B \leftrightarrow F \in {Base}_{W})$
128	30 127	mpbid	$⊢ φ \to F \in {Base}_{W}$
129	128	adantr	$⊢ (φ \land i \in ℕ_{0}) \to F \in {Base}_{W}$
130	129	adantr	$⊢ ((φ \land i \in ℕ_{0}) \land E \underset{˙}{\sim} (i D F)) \to F \in {Base}_{W}$
131		eqid	$⊢ +_{W} = +_{W}$
132	35 9 131	mulgnn0p1	$⊢ (W \in Mnd \land i \in ℕ_{0} \land F \in {Base}_{W}) \to (i + 1) D F = (i D F) +_{W} F$
133	123 124 130 132	syl3anc	$⊢ ((φ \land i \in ℕ_{0}) \land E \underset{˙}{\sim} (i D F)) \to (i + 1) D F = (i D F) +_{W} F$
134	119 133	breqtrrd	$⊢ ((φ \land i \in ℕ_{0}) \land E \underset{˙}{\sim} (i D F)) \to E \underset{˙}{\sim} ((i + 1) D F)$
135	22 24 26 28 111 134	nn0indd	$⊢ (φ \land L \in ℕ_{0}) \to E \underset{˙}{\sim} (L D F)$
136	20 135	mpdan	$⊢ φ \to E \underset{˙}{\sim} (L D F)$

Metamath Proof Explorer

Theorem aks6d1c1p6

Proof