aks6d1c1p2 - Mathbox for metakunt

	Mathbox for metakunt		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > aks6d1c1p2		Structured version Visualization version GIF version

Theorem aks6d1c1p2 43160

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

**Hypotheses**
Ref	Expression
aks6d1c1p2.1	⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))}
aks6d1c1p2.2	⊢ 𝑆 = (Poly₁‘𝐾)
aks6d1c1p2.3	⊢ 𝐵 = (Base‘𝑆)
aks6d1c1p2.4	⊢ 𝑋 = (var₁‘𝐾)
aks6d1c1p2.5	⊢ 𝑊 = (mulGrp‘𝑆)
aks6d1c1p2.6	⊢ 𝑉 = (mulGrp‘𝐾)
aks6d1c1p2.7	⊢ ↑ = (._g‘𝑉)
aks6d1c1p2.8	⊢ 𝐶 = (algSc‘𝑆)
aks6d1c1p2.9	⊢ 𝐷 = (._g‘𝑊)
aks6d1c1p2.10	⊢ 𝑃 = (chr‘𝐾)
aks6d1c1p2.11	⊢ 𝑂 = (eval₁‘𝐾)
aks6d1c1p2.12	⊢ + = (+_g‘𝑆)
aks6d1c1p2.13	⊢ (𝜑 → 𝐾 ∈ Field)
aks6d1c1p2.14	⊢ (𝜑 → 𝑃 ∈ ℙ)
aks6d1c1p2.15	⊢ (𝜑 → 𝑅 ∈ ℕ)
aks6d1c1p2.16	⊢ (𝜑 → (𝑁 gcd 𝑅) = 1)
aks6d1c1p2.17	⊢ (𝜑 → 𝑃 ∥ 𝑁)
aks6d1c1p2.18	⊢ 𝐹 = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴)))
aks6d1c1p2.19	⊢ (𝜑 → 𝐴 ∈ ℤ)

**Assertion**
Ref	Expression
aks6d1c1p2	⊢ (𝜑 → 𝑃 ∼ 𝐹)

Distinct variable groups: ↑ ,𝑒,𝑓 𝐵,𝑒,𝑓 𝑒,𝐹,𝑓,𝑦 𝑒,𝑂,𝑓 𝑃,𝑒,𝑓,𝑦 𝑅,𝑒,𝑓 𝑒,𝑉,𝑓 𝜑,𝑦 Allowed substitution hints: 𝜑(𝑒, 𝑓) 𝐴(𝑦, 𝑒, 𝑓) 𝐵(𝑦) 𝐶(𝑦, 𝑒, 𝑓) 𝐷(𝑦, 𝑒, 𝑓) + (𝑦, 𝑒, 𝑓) ∼ (𝑦, 𝑒, 𝑓) 𝑅(𝑦) 𝑆(𝑦, 𝑒, 𝑓) ↑ (𝑦) 𝐾(𝑦, 𝑒, 𝑓) 𝑁(𝑦, 𝑒, 𝑓) 𝑂(𝑦) 𝑉(𝑦) 𝑊(𝑦, 𝑒, 𝑓) 𝑋(𝑦, 𝑒, 𝑓)

Proof of Theorem aks6d1c1p2 Dummy variable 𝑙 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		aks6d1c1p2.13	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ Field)
2		isfld 20993	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ Field ↔ (𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing))
3	1, 2	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing))
4	3	simprd 501	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ CRing)
5		aks6d1c1p2.6	. . . . . . . . . . . . 13 ⊢ 𝑉 = (mulGrp‘𝐾)
6	5	crngmgp 20467	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ CRing → 𝑉 ∈ CMnd)
7	4, 6	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ CMnd)
8		aks6d1c1p2.15	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ ℕ)
9	8	nnnn0d 12667	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
10		aks6d1c1p2.7	. . . . . . . . . . 11 ⊢ ↑ = (._g‘𝑉)
11	7, 9, 10	isprimroot 43144	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ (𝑉 PrimRoots 𝑅) ↔ (𝑦 ∈ (Base‘𝑉) ∧ (𝑅 ↑ 𝑦) = (0_g‘𝑉) ∧ ∀𝑙 ∈ ℕ₀ ((𝑙 ↑ 𝑦) = (0_g‘𝑉) → 𝑅 ∥ 𝑙))))
12	11	biimpd 232	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ (𝑉 PrimRoots 𝑅) → (𝑦 ∈ (Base‘𝑉) ∧ (𝑅 ↑ 𝑦) = (0_g‘𝑉) ∧ ∀𝑙 ∈ ℕ₀ ((𝑙 ↑ 𝑦) = (0_g‘𝑉) → 𝑅 ∥ 𝑙))))
13	12	imp 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝑦 ∈ (Base‘𝑉) ∧ (𝑅 ↑ 𝑦) = (0_g‘𝑉) ∧ ∀𝑙 ∈ ℕ₀ ((𝑙 ↑ 𝑦) = (0_g‘𝑉) → 𝑅 ∥ 𝑙)))
14	13	simp1d 1160	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝑦 ∈ (Base‘𝑉))
15		eqid 2760	. . . . . . . . . . . 12 ⊢ (Base‘𝐾) = (Base‘𝐾)
16	5, 15	mgpbas 20365	. . . . . . . . . . 11 ⊢ (Base‘𝐾) = (Base‘𝑉)
17	16	eqcomi 2769	. . . . . . . . . 10 ⊢ (Base‘𝑉) = (Base‘𝐾)
18	17	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (Base‘𝑉) = (Base‘𝐾))
19	18	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (Base‘𝑉) = (Base‘𝐾))
20	19	eleq2d 2846	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝑦 ∈ (Base‘𝑉) ↔ 𝑦 ∈ (Base‘𝐾)))
21	14, 20	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝑦 ∈ (Base‘𝐾))
22	21	ex 418	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ (𝑉 PrimRoots 𝑅) → 𝑦 ∈ (Base‘𝐾)))
23		aks6d1c1p2.18	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴)))
24	23	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝐹 = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))
25	24	fveq2d 6889	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑂‘𝐹) = (𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴)))))
26	25	fveq1d 6887	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘𝐹)‘𝑦) = ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦))
27	26	oveq2d 7436	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = (𝑃 ↑ ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦)))
28		aks6d1c1p2.11	. . . . . . . . . . . . 13 ⊢ 𝑂 = (eval₁‘𝐾)
29		aks6d1c1p2.2	. . . . . . . . . . . . 13 ⊢ 𝑆 = (Poly₁‘𝐾)
30		aks6d1c1p2.3	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝑆)
31	4	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝐾 ∈ CRing)
32		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑦 ∈ (Base‘𝐾))
33		crngring 20472	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ CRing → 𝐾 ∈ Ring)
34		aks6d1c1p2.4	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 = (var₁‘𝐾)
35	34, 29, 30	vr1cl 22535	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ Ring → 𝑋 ∈ 𝐵)
36	31, 33, 35	3syl 19	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑋 ∈ 𝐵)
37	28, 34, 15, 29, 30, 31, 32	evl1vard 22655	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑋 ∈ 𝐵 ∧ ((𝑂‘𝑋)‘𝑦) = 𝑦))
38	37	simprd 501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘𝑋)‘𝑦) = 𝑦)
39	36, 38	jca 521	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑋 ∈ 𝐵 ∧ ((𝑂‘𝑋)‘𝑦) = 𝑦))
40	4, 33	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ Ring)
41	4	crngringd 20473	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ Ring)
42		eqid 2760	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℤRHom‘𝐾) = (ℤRHom‘𝐾)
43	42	zrhrhm 21817	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ Ring → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
44		rhmghm 20714	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾) → (ℤRHom‘𝐾) ∈ (ℤ_ring GrpHom 𝐾))
45		zringbas 21759	. . . . . . . . . . . . . . . . . . 19 ⊢ ℤ = (Base‘ℤ_ring)
46	45, 15	ghmf 19434	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℤRHom‘𝐾) ∈ (ℤ_ring GrpHom 𝐾) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
47	41, 43, 44, 46	4syl 20	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
48		aks6d1c1p2.19	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℤ)
49	47, 48	ffvelcdmd 7085	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘𝐴) ∈ (Base‘𝐾))
50		aks6d1c1p2.8	. . . . . . . . . . . . . . . . 17 ⊢ 𝐶 = (algSc‘𝑆)
51	29, 50, 15, 30	ply1sclcl 22605	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Ring ∧ ((ℤRHom‘𝐾)‘𝐴) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵)
52	40, 49, 51	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵)
53	52	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵)
54	49	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((ℤRHom‘𝐾)‘𝐴) ∈ (Base‘𝐾))
55	28, 29, 15, 50, 30, 31, 54, 32	evl1scad 22653	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵 ∧ ((𝑂‘(𝐶‘((ℤRHom‘𝐾)‘𝐴)))‘𝑦) = ((ℤRHom‘𝐾)‘𝐴)))
56	55	simprd 501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘(𝐶‘((ℤRHom‘𝐾)‘𝐴)))‘𝑦) = ((ℤRHom‘𝐾)‘𝐴))
57	53, 56	jca 521	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵 ∧ ((𝑂‘(𝐶‘((ℤRHom‘𝐾)‘𝐴)))‘𝑦) = ((ℤRHom‘𝐾)‘𝐴)))
58		aks6d1c1p2.12	. . . . . . . . . . . . 13 ⊢ + = (+_g‘𝑆)
59		eqid 2760	. . . . . . . . . . . . 13 ⊢ (+_g‘𝐾) = (+_g‘𝐾)
60	28, 29, 15, 30, 31, 32, 39, 57, 58, 59	evl1addd 22659	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵 ∧ ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
61	60	simprd 501	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))
62	61	oveq2d 7436	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦)) = (𝑃 ↑ (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
63	27, 62	eqtrd 2795	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = (𝑃 ↑ (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
64	25	fveq1d 6887	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)) = ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘(𝑃 ↑ 𝑦)))
65		eqid 2760	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝑉) = (Base‘𝑉)
66	5	ringmgp 20465	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Ring → 𝑉 ∈ Mnd)
67	31, 33, 66	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑉 ∈ Mnd)
68		aks6d1c1p2.14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑃 ∈ ℙ)
69		prmnn 16849	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
70	68, 69	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ∈ ℕ)
71	70	nnnn0d 12667	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
72	71	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑃 ∈ ℕ₀)
73	32, 16	eleqtrdi 2870	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑦 ∈ (Base‘𝑉))
74	65, 10, 67, 72, 73	mulgnn0cld 19305	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ 𝑦) ∈ (Base‘𝑉))
75	74, 17	eleqtrdi 2870	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ 𝑦) ∈ (Base‘𝐾))
76	28, 34, 15, 29, 30, 31, 75	evl1vard 22655	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑋 ∈ 𝐵 ∧ ((𝑂‘𝑋)‘(𝑃 ↑ 𝑦)) = (𝑃 ↑ 𝑦)))
77	28, 29, 15, 50, 30, 31, 54, 75	evl1scad 22653	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵 ∧ ((𝑂‘(𝐶‘((ℤRHom‘𝐾)‘𝐴)))‘(𝑃 ↑ 𝑦)) = ((ℤRHom‘𝐾)‘𝐴)))
78	77	simprd 501	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘(𝐶‘((ℤRHom‘𝐾)‘𝐴)))‘(𝑃 ↑ 𝑦)) = ((ℤRHom‘𝐾)‘𝐴))
79	53, 78	jca 521	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵 ∧ ((𝑂‘(𝐶‘((ℤRHom‘𝐾)‘𝐴)))‘(𝑃 ↑ 𝑦)) = ((ℤRHom‘𝐾)‘𝐴)))
80	28, 29, 15, 30, 31, 75, 76, 79, 58, 59	evl1addd 22659	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵 ∧ ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘(𝑃 ↑ 𝑦)) = ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
81	80	simprd 501	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘(𝑃 ↑ 𝑦)) = ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))
82	64, 81	eqtrd 2795	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)) = ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))
83		aks6d1c1p2.9	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐷 = (._g‘𝑊)
84		aks6d1c1p2.5	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑊 = (mulGrp‘𝑆)
85	84	fveq2i 6888	. . . . . . . . . . . . . . . . . 18 ⊢ (._g‘𝑊) = (._g‘(mulGrp‘𝑆))
86	83, 85	eqtri 2783	. . . . . . . . . . . . . . . . 17 ⊢ 𝐷 = (._g‘(mulGrp‘𝑆))
87	5	fveq2i 6888	. . . . . . . . . . . . . . . . . 18 ⊢ (._g‘𝑉) = (._g‘(mulGrp‘𝐾))
88	10, 87	eqtri 2783	. . . . . . . . . . . . . . . . 17 ⊢ ↑ = (._g‘(mulGrp‘𝐾))
89	28, 29, 15, 30, 31, 32, 37, 86, 88, 72	evl1expd 22663	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑃𝐷𝑋) ∈ 𝐵 ∧ ((𝑂‘(𝑃𝐷𝑋))‘𝑦) = (𝑃 ↑ 𝑦)))
90		eqid 2760	. . . . . . . . . . . . . . . 16 ⊢ (+_g‘𝑆) = (+_g‘𝑆)
91	28, 29, 15, 30, 31, 32, 89, 57, 90, 59	evl1addd 22659	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵 ∧ ((𝑂‘((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
92	91	simprd 501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))
93		eqidd 2761	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)) = ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))
94	92, 93	eqtrd 2795	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))
95	94	eqcomd 2766	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)) = ((𝑂‘((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦))
96		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶‘((ℤRHom‘𝐾)‘𝐴)) = (𝐶‘((ℤRHom‘𝐾)‘𝐴))
97		aks6d1c1p2.10	. . . . . . . . . . . . . . . . 17 ⊢ 𝑃 = (chr‘𝐾)
98	29, 34, 90, 84, 83, 50, 96, 97, 4, 68, 48	ply1fermltlchr 22630	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃𝐷(𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))) = ((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))
99	98	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑂‘(𝑃𝐷(𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))) = (𝑂‘((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))))
100	99	fveq1d 6887	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑂‘(𝑃𝐷(𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))))‘𝑦) = ((𝑂‘((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦))
101	100	eqcomd 2766	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑂‘((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = ((𝑂‘(𝑃𝐷(𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))))‘𝑦))
102	101	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = ((𝑂‘(𝑃𝐷(𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))))‘𝑦))
103	28, 29, 15, 30, 31, 32, 37, 55, 90, 59	evl1addd 22659	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵 ∧ ((𝑂‘(𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
104	28, 29, 15, 30, 31, 32, 103, 86, 88, 72	evl1expd 22663	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑃𝐷(𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))) ∈ 𝐵 ∧ ((𝑂‘(𝑃𝐷(𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))))‘𝑦) = (𝑃 ↑ (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))))
105	104	simprd 501	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘(𝑃𝐷(𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))))‘𝑦) = (𝑃 ↑ (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
106	95, 102, 105	3eqtrd 2799	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)) = (𝑃 ↑ (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
107	82, 106	eqtrd 2795	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)) = (𝑃 ↑ (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
108	107	eqcomd 2766	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)))
109	63, 108	eqtrd 2795	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)))
110	109	adantlr 728	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)))
111	110	ex 418	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝑦 ∈ (Base‘𝐾) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦))))
112	111	ex 418	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ (𝑉 PrimRoots 𝑅) → (𝑦 ∈ (Base‘𝐾) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)))))
113	22, 112	mpdd 44	. . . 4 ⊢ (𝜑 → (𝑦 ∈ (𝑉 PrimRoots 𝑅) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦))))
114	113	imp 412	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)))
115	114	ralrimiva 3154	. 2 ⊢ (𝜑 → ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)))
116		aks6d1c1p2.1	. . 3 ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))}
117	29	ply1crng 22516	. . . . . . . . 9 ⊢ (𝐾 ∈ CRing → 𝑆 ∈ CRing)
118	4, 117	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ CRing)
119		crngring 20472	. . . . . . . 8 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring)
120	118, 119	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ Ring)
121	120	ringgrpd 20469	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ Grp)
122	41, 35	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
123	121, 122, 52	3jca 1146	. . . . 5 ⊢ (𝜑 → (𝑆 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ (𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵))
124	30, 58	grpcl 19152	. . . . 5 ⊢ ((𝑆 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ (𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵)
125	123, 124	syl 18	. . . 4 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵)
126	23	a1i 11	. . . . 5 ⊢ (𝜑 → 𝐹 = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))
127	126	eleq1d 2845	. . . 4 ⊢ (𝜑 → (𝐹 ∈ 𝐵 ↔ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵))
128	125, 127	mpbird 260	. . 3 ⊢ (𝜑 → 𝐹 ∈ 𝐵)
129	116, 128, 70	aks6d1c1p1 43158	. 2 ⊢ (𝜑 → (𝑃 ∼ 𝐹 ↔ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦))))
130	115, 129	mpbird 260	1 ⊢ (𝜑 → 𝑃 ∼ 𝐹)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∀wral 3076 class class class wbr 5102 {copab 5166 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 1c1 11201 ℕcn 12335 ℕ₀cn0 12606 ℤcz 12693 ∥ cdvds 16422 gcd cgcd 16664 ℙcprime 16846 Basecbs 17387 +_gcplusg 17428 0_gc0g 17610 Mndcmnd 18923 Grpcgrp 19144 ._gcmg 19277 GrpHom cghm 19427 CMndccmn 19994 mulGrpcmgp 20360 Ringcrg 20459 CRingccrg 20460 RingHom crh 20699 DivRingcdr 20980 Fieldcfield 20981 ℤ_ringczring 21752 ℤRHomczrh 21805 chrcchr 21807 algSccascl 22160 var₁cv1 22494 Poly₁cpl1 22495 eval₁ce1 22632 PrimRoots cprimroots 43142

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278 ax-addf 11279 ax-mulf 11280

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-ofr 7694 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8178 df-tpos 8243 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-2o 8477 df-oadd 8480 df-er 8717 df-map 8849 df-pm 8850 df-ixp 8926 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-fsupp 9354 df-sup 9434 df-inf 9435 df-oi 9504 df-dju 9982 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-5 12408 df-6 12409 df-7 12410 df-8 12411 df-9 12412 df-n0 12607 df-xnn0 12680 df-z 12694 df-dec 12815 df-uz 12966 df-rp 13121 df-fz 13640 df-fzo 13789 df-fl 13932 df-mod 14010 df-seq 14145 df-exp 14205 df-fac 14418 df-bc 14447 df-hash 14475 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-dvds 16423 df-gcd 16665 df-prm 16847 df-phi 16943 df-struct 17325 df-sets 17342 df-slot 17360 df-ndx 17372 df-base 17388 df-ress 17409 df-plusg 17441 df-mulr 17442 df-starv 17443 df-sca 17444 df-vsca 17445 df-ip 17446 df-tset 17447 df-ple 17448 df-ds 17450 df-unif 17451 df-hom 17452 df-cco 17453 df-0g 17612 df-gsum 17613 df-prds 17618 df-pws 17620 df-mre 17756 df-mrc 17757 df-acs 17759 df-mgm 18816 df-sgrp 18908 df-mnd 18924 df-mhm 18978 df-submnd 18979 df-grp 19147 df-minusg 19148 df-sbg 19149 df-mulg 19278 df-subg 19333 df-ghm 19428 df-cntz 19531 df-od 19742 df-cmn 19996 df-abl 19997 df-mgp 20361 df-rng 20375 df-ur 20408 df-srg 20413 df-ring 20461 df-cring 20462 df-oppr 20567 df-dvdsr 20587 df-unit 20588 df-invr 20618 df-dvr 20631 df-rhm 20702 df-subrng 20798 df-subrg 20822 df-drng 20982 df-field 20983 df-lmod 21137 df-lss 21207 df-lsp 21247 df-cnfld 21679 df-zring 21753 df-zrh 21809 df-chr 21811 df-assa 22161 df-asp 22162 df-ascl 22163 df-psr 22217 df-mvr 22218 df-mpl 22219 df-opsr 22221 df-evls 22383 df-evl 22384 df-psr1 22498 df-vr1 22499 df-ply1 22500 df-coe1 22501 df-evl1 22634 df-primroots 43143

This theorem is used by: aks6d1c1 43167

W3C validator