Theorem aks6d1c1p5 42069

Description: The product of exponents is introspective. (Contributed by metakunt, 26-Apr-2025.)

Hypotheses

Ref	Expression
aks6d1c1p5.1	⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))}
aks6d1c1p5.2	⊢ 𝑆 = (Poly1‘𝐾)
aks6d1c1p5.3	⊢ 𝐵 = (Base‘𝑆)
aks6d1c1p5.4	⊢ 𝑋 = (var1‘𝐾)
aks6d1c1p5.5	⊢ 𝑊 = (mulGrp‘𝑆)
aks6d1c1p5.6	⊢ 𝑉 = (mulGrp‘𝐾)
aks6d1c1p5.7	⊢ ↑ = (.g‘𝑉)
aks6d1c1p5.8	⊢ 𝐶 = (algSc‘𝑆)
aks6d1c1p5.10	⊢ 𝑃 = (chr‘𝐾)
aks6d1c1p5.11	⊢ 𝑂 = (eval1‘𝐾)
aks6d1c1p5.12	⊢ + = (+g‘𝑆)
aks6d1c1p5.13	⊢ (𝜑 → 𝐾 ∈ Field)
aks6d1c1p5.14	⊢ (𝜑 → 𝑃 ∈ ℙ)
aks6d1c1p5.15	⊢ (𝜑 → 𝑅 ∈ ℕ)
aks6d1c1p5.16	⊢ (𝜑 → (𝐸 gcd 𝑅) = 1)
aks6d1c1p5.17	⊢ (𝜑 → 𝑃 ∥ 𝑁)
aks6d1c1p5.18	⊢ (𝜑 → 𝐷 ∼ 𝐹)
aks6d1c1p5.19	⊢ (𝜑 → 𝐸 ∼ 𝐹)

Assertion

Ref	Expression
aks6d1c1p5	⊢ (𝜑 → (𝐷 · 𝐸) ∼ 𝐹)

Distinct variable groups:   ↑ ,𝑒,𝑓,𝑦   𝐵,𝑒,𝑓   𝐷,𝑒,𝑓,𝑦   𝑒,𝐸,𝑓,𝑦   𝑒,𝐹,𝑓,𝑦   𝑒,𝑂,𝑓,𝑦   𝑅,𝑒,𝑓,𝑦   𝑒,𝑉,𝑓,𝑦   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑒,𝑓)   𝐵(𝑦)   𝐶(𝑦,𝑒,𝑓)   𝑃(𝑦,𝑒,𝑓)   + (𝑦,𝑒,𝑓)   ∼ (𝑦,𝑒,𝑓)   𝑆(𝑦,𝑒,𝑓)   𝐾(𝑦,𝑒,𝑓)   𝑁(𝑦,𝑒,𝑓)   𝑊(𝑦,𝑒,𝑓)   𝑋(𝑦,𝑒,𝑓)

Proof of Theorem aks6d1c1p5

Dummy variables 𝑖 𝑙 𝑧 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		aks6d1c1p5.13	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ Field)
2	1	fldcrngd 20764	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ CRing)
3		aks6d1c1p5.6	. . . . . . . . 9 ⊢ 𝑉 = (mulGrp‘𝐾)
4	3	crngmgp 20268	. . . . . . . 8 ⊢ (𝐾 ∈ CRing → 𝑉 ∈ CMnd)
5	2, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑉 ∈ CMnd)
6	5	cmnmndd 19846	. . . . . 6 ⊢ (𝜑 → 𝑉 ∈ Mnd)
7	6	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝑉 ∈ Mnd)
8		aks6d1c1p5.1	. . . . . . . . . 10 ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))}
9		aks6d1c1p5.18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∼ 𝐹)
10	8, 9	aks6d1c1p1rcl 42065	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 ∈ ℕ ∧ 𝐹 ∈ 𝐵))
11	10	simpld 494	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℕ)
12	11	nnnn0d 12613	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℕ0)
13	12	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝐷 ∈ ℕ0)
14		aks6d1c1p5.19	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∼ 𝐹)
15	8, 14	aks6d1c1p1rcl 42065	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵))
16	15	simpld 494	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ ℕ)
17	16	nnnn0d 12613	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ℕ0)
18	17	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝐸 ∈ ℕ0)
19		aks6d1c1p5.11	. . . . . . . 8 ⊢ 𝑂 = (eval1‘𝐾)
20		aks6d1c1p5.2	. . . . . . . 8 ⊢ 𝑆 = (Poly1‘𝐾)
21		eqid 2740	. . . . . . . 8 ⊢ (Base‘𝐾) = (Base‘𝐾)
22		aks6d1c1p5.3	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑆)
23	2	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝐾 ∈ CRing)
24		aks6d1c1p5.15	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ ℕ)
25	24	nnnn0d 12613	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ ℕ0)
26		aks6d1c1p5.7	. . . . . . . . . . . . 13 ⊢ ↑ = (.g‘𝑉)
27	5, 25, 26	isprimroot 42050	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ (𝑉 PrimRoots 𝑅) ↔ (𝑦 ∈ (Base‘𝑉) ∧ (𝑅 ↑ 𝑦) = (0g‘𝑉) ∧ ∀𝑞 ∈ ℕ0 ((𝑞 ↑ 𝑦) = (0g‘𝑉) → 𝑅 ∥ 𝑞))))
28	27	biimpd 229	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝑉 PrimRoots 𝑅) → (𝑦 ∈ (Base‘𝑉) ∧ (𝑅 ↑ 𝑦) = (0g‘𝑉) ∧ ∀𝑞 ∈ ℕ0 ((𝑞 ↑ 𝑦) = (0g‘𝑉) → 𝑅 ∥ 𝑞))))
29	28	imp 406	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝑦 ∈ (Base‘𝑉) ∧ (𝑅 ↑ 𝑦) = (0g‘𝑉) ∧ ∀𝑞 ∈ ℕ0 ((𝑞 ↑ 𝑦) = (0g‘𝑉) → 𝑅 ∥ 𝑞)))
30	29	simp1d 1142	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝑦 ∈ (Base‘𝑉))
31	3, 21	mgpbas 20167	. . . . . . . . . . . 12 ⊢ (Base‘𝐾) = (Base‘𝑉)
32	31	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝐾) = (Base‘𝑉))
33	32	eqcomd 2746	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝑉) = (Base‘𝐾))
34	33	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (Base‘𝑉) = (Base‘𝐾))
35	30, 34	eleqtrd 2846	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝑦 ∈ (Base‘𝐾))
36	10	simprd 495	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ 𝐵)
37	36	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝐹 ∈ 𝐵)
38	19, 20, 21, 22, 23, 35, 37	fveval1fvcl 22358	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘𝐹)‘𝑦) ∈ (Base‘𝐾))
39	34	eleq2d 2830	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (((𝑂‘𝐹)‘𝑦) ∈ (Base‘𝑉) ↔ ((𝑂‘𝐹)‘𝑦) ∈ (Base‘𝐾)))
40	38, 39	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘𝐹)‘𝑦) ∈ (Base‘𝑉))
41	13, 18, 40	3jca 1128	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ∧ ((𝑂‘𝐹)‘𝑦) ∈ (Base‘𝑉)))
42		eqid 2740	. . . . . 6 ⊢ (Base‘𝑉) = (Base‘𝑉)
43	42, 26	mulgnn0ass 19150	. . . . 5 ⊢ ((𝑉 ∈ Mnd ∧ (𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ∧ ((𝑂‘𝐹)‘𝑦) ∈ (Base‘𝑉))) → ((𝐷 · 𝐸) ↑ ((𝑂‘𝐹)‘𝑦)) = (𝐷 ↑ (𝐸 ↑ ((𝑂‘𝐹)‘𝑦))))
44	7, 41, 43	syl2anc 583	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝐷 · 𝐸) ↑ ((𝑂‘𝐹)‘𝑦)) = (𝐷 ↑ (𝐸 ↑ ((𝑂‘𝐹)‘𝑦))))
45		eqidd 2741	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙)) = (𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙)))
46		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) ∧ 𝑙 = 𝑦) → 𝑙 = 𝑦)
47	46	oveq2d 7464	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) ∧ 𝑙 = 𝑦) → (𝐸 ↑ 𝑙) = (𝐸 ↑ 𝑦))
48		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝑦 ∈ (𝑉 PrimRoots 𝑅))
49	42, 26, 7, 18, 30	mulgnn0cld 19135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑ 𝑦) ∈ (Base‘𝑉))
50	45, 47, 48, 49	fvmptd 7036	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑦) = (𝐸 ↑ 𝑦))
51	50	fveq2d 6924	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦)))
52	51	oveq2d 7464	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐷 ↑ ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑦))) = (𝐷 ↑ ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))))
53	52	eqcomd 2746	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐷 ↑ ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))) = (𝐷 ↑ ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑦))))
54		2fveq3 6925	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑦 → ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖)) = ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑦)))
55	54	oveq2d 7464	. . . . . . . . . 10 ⊢ (𝑖 = 𝑦 → (𝐷 ↑ ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖))) = (𝐷 ↑ ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑦))))
56		fveq2 6920	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑦 → ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖) = ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑦))
57	56	oveq2d 7464	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑦 → (𝐷 ↑ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖)) = (𝐷 ↑ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑦)))
58	57	fveq2d 6924	. . . . . . . . . 10 ⊢ (𝑖 = 𝑦 → ((𝑂‘𝐹)‘(𝐷 ↑ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖))) = ((𝑂‘𝐹)‘(𝐷 ↑ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑦))))
59	55, 58	eqeq12d 2756	. . . . . . . . 9 ⊢ (𝑖 = 𝑦 → ((𝐷 ↑ ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖))) = ((𝑂‘𝐹)‘(𝐷 ↑ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖))) ↔ (𝐷 ↑ ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑦))) = ((𝑂‘𝐹)‘(𝐷 ↑ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑦)))))
60	8, 36, 11	aks6d1c1p1 42064	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 ∼ 𝐹 ↔ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐷 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐷 ↑ 𝑦))))
61	60	biimpd 229	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷 ∼ 𝐹 → ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐷 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐷 ↑ 𝑦))))
62	9, 61	mpd 15	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐷 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐷 ↑ 𝑦)))
63	26	oveqi 7461	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 ↑ 𝑙) = (𝐸(.g‘𝑉)𝑙)
64	63	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑙 ∈ (𝑉 PrimRoots 𝑅) → (𝐸 ↑ 𝑙) = (𝐸(.g‘𝑉)𝑙))
65	64	mpteq2ia 5269	. . . . . . . . . . . . . 14 ⊢ (𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙)) = (𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸(.g‘𝑉)𝑙))
66		aks6d1c1p5.16	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸 gcd 𝑅) = 1)
67	65, 5, 24, 16, 66	primrootscoprbij2 42060	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙)):(𝑉 PrimRoots 𝑅)–1-1-onto→(𝑉 PrimRoots 𝑅))
68		f1ofo 6869	. . . . . . . . . . . . 13 ⊢ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙)):(𝑉 PrimRoots 𝑅)–1-1-onto→(𝑉 PrimRoots 𝑅) → (𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙)):(𝑉 PrimRoots 𝑅)–onto→(𝑉 PrimRoots 𝑅))
69	67, 68	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙)):(𝑉 PrimRoots 𝑅)–onto→(𝑉 PrimRoots 𝑅))
70		fveq2 6920	. . . . . . . . . . . . . . 15 ⊢ (((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖) = 𝑦 → ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖)) = ((𝑂‘𝐹)‘𝑦))
71	70	oveq2d 7464	. . . . . . . . . . . . . 14 ⊢ (((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖) = 𝑦 → (𝐷 ↑ ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖))) = (𝐷 ↑ ((𝑂‘𝐹)‘𝑦)))
72		oveq2 7456	. . . . . . . . . . . . . . 15 ⊢ (((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖) = 𝑦 → (𝐷 ↑ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖)) = (𝐷 ↑ 𝑦))
73	72	fveq2d 6924	. . . . . . . . . . . . . 14 ⊢ (((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖) = 𝑦 → ((𝑂‘𝐹)‘(𝐷 ↑ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖))) = ((𝑂‘𝐹)‘(𝐷 ↑ 𝑦)))
74	71, 73	eqeq12d 2756	. . . . . . . . . . . . 13 ⊢ (((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖) = 𝑦 → ((𝐷 ↑ ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖))) = ((𝑂‘𝐹)‘(𝐷 ↑ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖))) ↔ (𝐷 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐷 ↑ 𝑦))))
75	74	cbvfo 7325	. . . . . . . . . . . 12 ⊢ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙)):(𝑉 PrimRoots 𝑅)–onto→(𝑉 PrimRoots 𝑅) → (∀𝑖 ∈ (𝑉 PrimRoots 𝑅)(𝐷 ↑ ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖))) = ((𝑂‘𝐹)‘(𝐷 ↑ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖))) ↔ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐷 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐷 ↑ 𝑦))))
76	69, 75	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (∀𝑖 ∈ (𝑉 PrimRoots 𝑅)(𝐷 ↑ ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖))) = ((𝑂‘𝐹)‘(𝐷 ↑ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖))) ↔ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐷 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐷 ↑ 𝑦))))
77	62, 76	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑖 ∈ (𝑉 PrimRoots 𝑅)(𝐷 ↑ ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖))) = ((𝑂‘𝐹)‘(𝐷 ↑ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖))))
78	77	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ∀𝑖 ∈ (𝑉 PrimRoots 𝑅)(𝐷 ↑ ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖))) = ((𝑂‘𝐹)‘(𝐷 ↑ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑖))))
79	59, 78, 48	rspcdva 3636	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐷 ↑ ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑦))) = ((𝑂‘𝐹)‘(𝐷 ↑ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑦))))
80	50	oveq2d 7464	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐷 ↑ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑦)) = (𝐷 ↑ (𝐸 ↑ 𝑦)))
81	80	fveq2d 6924	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘𝐹)‘(𝐷 ↑ ((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑦))) = ((𝑂‘𝐹)‘(𝐷 ↑ (𝐸 ↑ 𝑦))))
82	79, 81	eqtrd 2780	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐷 ↑ ((𝑂‘𝐹)‘((𝑙 ∈ (𝑉 PrimRoots 𝑅) ↦ (𝐸 ↑ 𝑙))‘𝑦))) = ((𝑂‘𝐹)‘(𝐷 ↑ (𝐸 ↑ 𝑦))))
83	53, 82	eqtr2d 2781	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘𝐹)‘(𝐷 ↑ (𝐸 ↑ 𝑦))) = (𝐷 ↑ ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))))
84		fveq2 6920	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → ((𝑂‘𝐹)‘𝑧) = ((𝑂‘𝐹)‘𝑦))
85	84	oveq2d 7464	. . . . . . . . . 10 ⊢ (𝑧 = 𝑦 → (𝐸 ↑ ((𝑂‘𝐹)‘𝑧)) = (𝐸 ↑ ((𝑂‘𝐹)‘𝑦)))
86		oveq2 7456	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → (𝐸 ↑ 𝑧) = (𝐸 ↑ 𝑦))
87	86	fveq2d 6924	. . . . . . . . . 10 ⊢ (𝑧 = 𝑦 → ((𝑂‘𝐹)‘(𝐸 ↑ 𝑧)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦)))
88	85, 87	eqeq12d 2756	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → ((𝐸 ↑ ((𝑂‘𝐹)‘𝑧)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑧)) ↔ (𝐸 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))))
89	8, 36, 16	aks6d1c1p1 42064	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ∼ 𝐹 ↔ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))))
90	89	biimpd 229	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∼ 𝐹 → ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))))
91	14, 90	mpd 15	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦)))
92		nfv 1913	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝐸 ↑ ((𝑂‘𝐹)‘𝑧)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑧))
93		nfv 1913	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧(𝐸 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))
94	92, 93, 88	cbvralw 3312	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐹)‘𝑧)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑧)) ↔ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦)))
95	91, 94	sylibr 234	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑧 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐹)‘𝑧)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑧)))
96	95	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ∀𝑧 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐹)‘𝑧)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑧)))
97	88, 96, 48	rspcdva 3636	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦)))
98	97	eqcomd 2746	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦)) = (𝐸 ↑ ((𝑂‘𝐹)‘𝑦)))
99	98	oveq2d 7464	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐷 ↑ ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))) = (𝐷 ↑ (𝐸 ↑ ((𝑂‘𝐹)‘𝑦))))
100	83, 99	eqtrd 2780	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘𝐹)‘(𝐷 ↑ (𝐸 ↑ 𝑦))) = (𝐷 ↑ (𝐸 ↑ ((𝑂‘𝐹)‘𝑦))))
101	100	eqcomd 2746	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐷 ↑ (𝐸 ↑ ((𝑂‘𝐹)‘𝑦))) = ((𝑂‘𝐹)‘(𝐷 ↑ (𝐸 ↑ 𝑦))))
102	13, 18, 30	3jca 1128	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ∧ 𝑦 ∈ (Base‘𝑉)))
103	42, 26	mulgnn0ass 19150	. . . . . . 7 ⊢ ((𝑉 ∈ Mnd ∧ (𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ∧ 𝑦 ∈ (Base‘𝑉))) → ((𝐷 · 𝐸) ↑ 𝑦) = (𝐷 ↑ (𝐸 ↑ 𝑦)))
104	103	eqcomd 2746	. . . . . 6 ⊢ ((𝑉 ∈ Mnd ∧ (𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ∧ 𝑦 ∈ (Base‘𝑉))) → (𝐷 ↑ (𝐸 ↑ 𝑦)) = ((𝐷 · 𝐸) ↑ 𝑦))
105	7, 102, 104	syl2anc 583	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐷 ↑ (𝐸 ↑ 𝑦)) = ((𝐷 · 𝐸) ↑ 𝑦))
106	105	fveq2d 6924	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘𝐹)‘(𝐷 ↑ (𝐸 ↑ 𝑦))) = ((𝑂‘𝐹)‘((𝐷 · 𝐸) ↑ 𝑦)))
107	44, 101, 106	3eqtrd 2784	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝐷 · 𝐸) ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘((𝐷 · 𝐸) ↑ 𝑦)))
108	107	ralrimiva 3152	. 2 ⊢ (𝜑 → ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)((𝐷 · 𝐸) ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘((𝐷 · 𝐸) ↑ 𝑦)))
109	11, 16	nnmulcld 12346	. . 3 ⊢ (𝜑 → (𝐷 · 𝐸) ∈ ℕ)
110	8, 36, 109	aks6d1c1p1 42064	. 2 ⊢ (𝜑 → ((𝐷 · 𝐸) ∼ 𝐹 ↔ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)((𝐷 · 𝐸) ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘((𝐷 · 𝐸) ↑ 𝑦))))
111	108, 110	mpbird 257	1 ⊢ (𝜑 → (𝐷 · 𝐸) ∼ 𝐹)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  ∀wral 3067   class class class wbr 5166  {copab 5228   ↦ cmpt 5249  –onto→wfo 6571  –1-1-onto→wf1o 6572  ‘cfv 6573  (class class class)co 7448  1c1 11185   · cmul 11189  ℕcn 12293  ℕ₀cn0 12553   ∥ cdvds 16302   gcd cgcd 16540  ℙcprime 16718  Basecbs 17258  +_gcplusg 17311  0_gc0g 17499  Mndcmnd 18772  ._gcmg 19107  CMndccmn 19822  mulGrpcmgp 20161  CRingccrg 20261  Fieldcfield 20752  chrcchr 21535  algSccascl 21895  var₁cv1 22198  Poly₁cpl1 22199  eval₁ce1 22339   PrimRoots cprimroots 42048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-iin 5018  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-of 7714  df-ofr 7715  df-om 7904  df-1st 8030  df-2nd 8031  df-supp 8202  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-er 8763  df-map 8886  df-pm 8887  df-ixp 8956  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-fsupp 9432  df-sup 9511  df-inf 9512  df-oi 9579  df-card 10008  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362  df-9 12363  df-n0 12554  df-z 12640  df-dec 12759  df-uz 12904  df-rp 13058  df-fz 13568  df-fzo 13712  df-fl 13843  df-mod 13921  df-seq 14053  df-exp 14113  df-hash 14380  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285  df-dvds 16303  df-gcd 16541  df-struct 17194  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-mulr 17325  df-sca 17327  df-vsca 17328  df-ip 17329  df-tset 17330  df-ple 17331  df-ds 17333  df-hom 17335  df-cco 17336  df-0g 17501  df-gsum 17502  df-prds 17507  df-pws 17509  df-mre 17644  df-mrc 17645  df-acs 17647  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-mhm 18818  df-submnd 18819  df-grp 18976  df-minusg 18977  df-sbg 18978  df-mulg 19108  df-subg 19163  df-ghm 19253  df-cntz 19357  df-cmn 19824  df-abl 19825  df-mgp 20162  df-rng 20180  df-ur 20209  df-srg 20214  df-ring 20262  df-cring 20263  df-rhm 20498  df-subrng 20572  df-subrg 20597  df-field 20754  df-lmod 20882  df-lss 20953  df-lsp 20993  df-assa 21896  df-asp 21897  df-ascl 21898  df-psr 21952  df-mvr 21953  df-mpl 21954  df-opsr 21956  df-evls 22121  df-evl 22122  df-psr1 22202  df-ply1 22204  df-evl1 22341  df-primroots 42049

This theorem is referenced by:  aks6d1c1p8  42072  aks6d1c1  42073