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 43350

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 21020	. . . . . . . . . . . . . 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 20494	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ CRing → 𝑉 ∈ CMnd)
7	4, 6	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ CMnd)
8		aks6d1c1p2.15	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ ℕ)
9	8	nnnn0d 12691	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
10		aks6d1c1p2.7	. . . . . . . . . . 11 ⊢ ↑ = (._g‘𝑉)
11	7, 9, 10	isprimroot 43334	. . . . . . . . . 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 2763	. . . . . . . . . . . 12 ⊢ (Base‘𝐾) = (Base‘𝐾)
16	5, 15	mgpbas 20392	. . . . . . . . . . 11 ⊢ (Base‘𝐾) = (Base‘𝑉)
17	16	eqcomi 2772	. . . . . . . . . 10 ⊢ (Base‘𝑉) = (Base‘𝐾)
18	17	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (Base‘𝑉) = (Base‘𝐾))
19	18	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (Base‘𝑉) = (Base‘𝐾))
20	19	eleq2d 2850	. . . . . . 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 6909	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑂‘𝐹) = (𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴)))))
26	25	fveq1d 6907	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘𝐹)‘𝑦) = ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦))
27	26	oveq2d 7456	. . . . . . . . . 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 20499	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ CRing → 𝐾 ∈ Ring)
34		aks6d1c1p2.4	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 = (var₁‘𝐾)
35	34, 29, 30	vr1cl 22562	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ Ring → 𝑋 ∈ 𝐵)
36	31, 33, 35	3syl 19	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑋 ∈ 𝐵)
37	28, 34, 15, 29, 30, 31, 32	evl1vard 22682	. . . . . . . . . . . . . . 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 20500	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ Ring)
42		eqid 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℤRHom‘𝐾) = (ℤRHom‘𝐾)
43	42	zrhrhm 21844	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ Ring → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
44		rhmghm 20741	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾) → (ℤRHom‘𝐾) ∈ (ℤ_ring GrpHom 𝐾))
45		zringbas 21786	. . . . . . . . . . . . . . . . . . 19 ⊢ ℤ = (Base‘ℤ_ring)
46	45, 15	ghmf 19460	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℤRHom‘𝐾) ∈ (ℤ_ring GrpHom 𝐾) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
47	41, 43, 44, 46	4syl 20	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
48		aks6d1c1p2.19	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℤ)
49	47, 48	ffvelcdmd 7106	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘𝐴) ∈ (Base‘𝐾))
50		aks6d1c1p2.8	. . . . . . . . . . . . . . . . 17 ⊢ 𝐶 = (algSc‘𝑆)
51	29, 50, 15, 30	ply1sclcl 22632	. . . . . . . . . . . . . . . 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 22680	. . . . . . . . . . . . . . 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 2763	. . . . . . . . . . . . 13 ⊢ (+_g‘𝐾) = (+_g‘𝐾)
60	28, 29, 15, 30, 31, 32, 39, 57, 58, 59	evl1addd 22686	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵 ∧ ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
61	60	simprd 501	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))
62	61	oveq2d 7456	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦)) = (𝑃 ↑ (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
63	27, 62	eqtrd 2798	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = (𝑃 ↑ (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
64	25	fveq1d 6907	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)) = ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘(𝑃 ↑ 𝑦)))
65		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝑉) = (Base‘𝑉)
66	5	ringmgp 20492	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Ring → 𝑉 ∈ Mnd)
67	31, 33, 66	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑉 ∈ Mnd)
68		aks6d1c1p2.14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑃 ∈ ℙ)
69		prmnn 16875	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
70	68, 69	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ∈ ℕ)
71	70	nnnn0d 12691	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
72	71	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑃 ∈ ℕ₀)
73	32, 16	eleqtrdi 2874	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑦 ∈ (Base‘𝑉))
74	65, 10, 67, 72, 73	mulgnn0cld 19331	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ 𝑦) ∈ (Base‘𝑉))
75	74, 17	eleqtrdi 2874	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ 𝑦) ∈ (Base‘𝐾))
76	28, 34, 15, 29, 30, 31, 75	evl1vard 22682	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑋 ∈ 𝐵 ∧ ((𝑂‘𝑋)‘(𝑃 ↑ 𝑦)) = (𝑃 ↑ 𝑦)))
77	28, 29, 15, 50, 30, 31, 54, 75	evl1scad 22680	. . . . . . . . . . . . . . . 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 22686	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵 ∧ ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘(𝑃 ↑ 𝑦)) = ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
81	80	simprd 501	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘(𝑃 ↑ 𝑦)) = ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))
82	64, 81	eqtrd 2798	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)) = ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))
83		aks6d1c1p2.9	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐷 = (._g‘𝑊)
84		aks6d1c1p2.5	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑊 = (mulGrp‘𝑆)
85	84	fveq2i 6908	. . . . . . . . . . . . . . . . . 18 ⊢ (._g‘𝑊) = (._g‘(mulGrp‘𝑆))
86	83, 85	eqtri 2786	. . . . . . . . . . . . . . . . 17 ⊢ 𝐷 = (._g‘(mulGrp‘𝑆))
87	5	fveq2i 6908	. . . . . . . . . . . . . . . . . 18 ⊢ (._g‘𝑉) = (._g‘(mulGrp‘𝐾))
88	10, 87	eqtri 2786	. . . . . . . . . . . . . . . . 17 ⊢ ↑ = (._g‘(mulGrp‘𝐾))
89	28, 29, 15, 30, 31, 32, 37, 86, 88, 72	evl1expd 22690	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑃𝐷𝑋) ∈ 𝐵 ∧ ((𝑂‘(𝑃𝐷𝑋))‘𝑦) = (𝑃 ↑ 𝑦)))
90		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (+_g‘𝑆) = (+_g‘𝑆)
91	28, 29, 15, 30, 31, 32, 89, 57, 90, 59	evl1addd 22686	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵 ∧ ((𝑂‘((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
92	91	simprd 501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))
93		eqidd 2764	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)) = ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))
94	92, 93	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))
95	94	eqcomd 2769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)) = ((𝑂‘((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦))
96		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶‘((ℤRHom‘𝐾)‘𝐴)) = (𝐶‘((ℤRHom‘𝐾)‘𝐴))
97		aks6d1c1p2.10	. . . . . . . . . . . . . . . . 17 ⊢ 𝑃 = (chr‘𝐾)
98	29, 34, 90, 84, 83, 50, 96, 97, 4, 68, 48	ply1fermltlchr 22657	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃𝐷(𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))) = ((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))
99	98	fveq2d 6909	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑂‘(𝑃𝐷(𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))) = (𝑂‘((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))))
100	99	fveq1d 6907	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑂‘(𝑃𝐷(𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))))‘𝑦) = ((𝑂‘((𝑃𝐷𝑋)(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦))
101	100	eqcomd 2769	. . . . . . . . . . . . 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 22686	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵 ∧ ((𝑂‘(𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
104	28, 29, 15, 30, 31, 32, 103, 86, 88, 72	evl1expd 22690	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑃𝐷(𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))) ∈ 𝐵 ∧ ((𝑂‘(𝑃𝐷(𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))))‘𝑦) = (𝑃 ↑ (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))))
105	104	simprd 501	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘(𝑃𝐷(𝑋(+_g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))))‘𝑦) = (𝑃 ↑ (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
106	95, 102, 105	3eqtrd 2802	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑃 ↑ 𝑦)(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴)) = (𝑃 ↑ (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
107	82, 106	eqtrd 2798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)) = (𝑃 ↑ (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))
108	107	eqcomd 2769	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ (𝑦(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐴))) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)))
109	63, 108	eqtrd 2798	. . . . . . . 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 3158	. 2 ⊢ (𝜑 → ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)))
116		aks6d1c1p2.1	. . 3 ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))}
117	29	ply1crng 22543	. . . . . . . . 9 ⊢ (𝐾 ∈ CRing → 𝑆 ∈ CRing)
118	4, 117	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ CRing)
119		crngring 20499	. . . . . . . 8 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring)
120	118, 119	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ Ring)
121	120	ringgrpd 20496	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ Grp)
122	41, 35	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
123	121, 122, 52	3jca 1146	. . . . 5 ⊢ (𝜑 → (𝑆 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ (𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵))
124	30, 58	grpcl 19178	. . . . 5 ⊢ ((𝑆 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ (𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵)
125	123, 124	syl 18	. . . 4 ⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵)
126	23	a1i 11	. . . . 5 ⊢ (𝜑 → 𝐹 = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))
127	126	eleq1d 2849	. . . 4 ⊢ (𝜑 → (𝐹 ∈ 𝐵 ↔ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵))
128	125, 127	mpbird 260	. . 3 ⊢ (𝜑 → 𝐹 ∈ 𝐵)
129	116, 128, 70	aks6d1c1p1 43348	. 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 1570 ∈ wcel 2147 ∀wral 3080 class class class wbr 5106 {copab 5170 ⟶wf 6551 ‘cfv 6555 (class class class)co 7440 1c1 11225 ℕcn 12359 ℕ₀cn0 12630 ℤcz 12717 ∥ cdvds 16448 gcd cgcd 16690 ℙcprime 16872 Basecbs 17413 +_gcplusg 17454 0_gc0g 17636 Mndcmnd 18949 Grpcgrp 19170 ._gcmg 19303 GrpHom cghm 19453 CMndccmn 20021 mulGrpcmgp 20387 Ringcrg 20486 CRingccrg 20487 RingHom crh 20726 DivRingcdr 21007 Fieldcfield 21008 ℤ_ringczring 21779 ℤRHomczrh 21832 chrcchr 21834 algSccascl 22187 var₁cv1 22521 Poly₁cpl1 22522 eval₁ce1 22659 PrimRoots cprimroots 43332

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301 ax-pre-sup 11302 ax-addf 11303 ax-mulf 11304

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-isom 6564 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-of 7714 df-ofr 7715 df-om 7899 df-1st 8022 df-2nd 8023 df-supp 8202 df-tpos 8268 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-1o 8501 df-2o 8502 df-oadd 8505 df-er 8742 df-map 8874 df-pm 8875 df-ixp 8951 df-en 8999 df-dom 9000 df-sdom 9001 df-fin 9002 df-fsupp 9379 df-sup 9458 df-inf 9459 df-oi 9528 df-dju 10006 df-card 10044 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-div 11998 df-nn 12360 df-2 12429 df-3 12430 df-4 12431 df-5 12432 df-6 12433 df-7 12434 df-8 12435 df-9 12436 df-n0 12631 df-xnn0 12704 df-z 12718 df-dec 12839 df-uz 12990 df-rp 13145 df-fz 13664 df-fzo 13813 df-fl 13956 df-mod 14034 df-seq 14169 df-exp 14229 df-fac 14442 df-bc 14471 df-hash 14499 df-cj 15292 df-re 15293 df-im 15294 df-sqrt 15428 df-abs 15429 df-dvds 16449 df-gcd 16691 df-prm 16873 df-phi 16969 df-struct 17351 df-sets 17368 df-slot 17386 df-ndx 17398 df-base 17414 df-ress 17435 df-plusg 17467 df-mulr 17468 df-starv 17469 df-sca 17470 df-vsca 17471 df-ip 17472 df-tset 17473 df-ple 17474 df-ds 17476 df-unif 17477 df-hom 17478 df-cco 17479 df-0g 17638 df-gsum 17639 df-prds 17644 df-pws 17646 df-mre 17782 df-mrc 17783 df-acs 17785 df-mgm 18842 df-sgrp 18934 df-mnd 18950 df-mhm 19004 df-submnd 19005 df-grp 19173 df-minusg 19174 df-sbg 19175 df-mulg 19304 df-subg 19359 df-ghm 19454 df-cntz 19558 df-od 19769 df-cmn 20023 df-abl 20024 df-mgp 20388 df-rng 20402 df-ur 20435 df-srg 20440 df-ring 20488 df-cring 20489 df-oppr 20594 df-dvdsr 20614 df-unit 20615 df-invr 20645 df-dvr 20658 df-rhm 20729 df-subrng 20825 df-subrg 20849 df-drng 21009 df-field 21010 df-lmod 21164 df-lss 21234 df-lsp 21274 df-cnfld 21706 df-zring 21780 df-zrh 21836 df-chr 21838 df-assa 22188 df-asp 22189 df-ascl 22190 df-psr 22244 df-mvr 22245 df-mpl 22246 df-opsr 22248 df-evls 22410 df-evl 22411 df-psr1 22525 df-vr1 22526 df-ply1 22527 df-coe1 22528 df-evl1 22661 df-primroots 43333

This theorem is used by: aks6d1c1 43357

W3C validator