aks6d1c1p4 - Mathbox for metakunt

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

Theorem aks6d1c1p4 42550

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

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

**Assertion**
Ref	Expression
aks6d1c1p4	⊢ (𝜑 → 𝐸 ∼ (𝐹(+_g‘𝑊)𝐺))

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

Proof of Theorem aks6d1c1p4 Dummy variables 𝑧 𝑙 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		aks6d1c1p4.11	. . . . . . 7 ⊢ 𝑂 = (eval₁‘𝐾)
2		aks6d1c1p4.2	. . . . . . 7 ⊢ 𝑆 = (Poly₁‘𝐾)
3		eqid 2736	. . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾)
4		aks6d1c1p4.3	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑆)
5		aks6d1c1p4.13	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ Field)
6	5	fldcrngd 20719	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ CRing)
7	6	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝐾 ∈ CRing)
8		aks6d1c1p4.6	. . . . . . . . 9 ⊢ 𝑉 = (mulGrp‘𝐾)
9	8, 3	mgpbas 20126	. . . . . . . 8 ⊢ (Base‘𝐾) = (Base‘𝑉)
10		aks6d1c1p4.7	. . . . . . . 8 ⊢ ↑ = (._g‘𝑉)
11	8	crngmgp 20222	. . . . . . . . . . 11 ⊢ (𝐾 ∈ CRing → 𝑉 ∈ CMnd)
12	6, 11	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ CMnd)
13	12	cmnmndd 19779	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ Mnd)
14	13	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝑉 ∈ Mnd)
15		aks6d1c1p4.1	. . . . . . . . . . . 12 ⊢ ∼ = {⟨𝑒, 𝑓⟩ ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))}
16		aks6d1c1p4.18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∼ 𝐹)
17	15, 16	aks6d1c1p1rcl 42547	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵))
18	17	simpld 494	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ ℕ)
19	18	nnnn0d 12498	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ ℕ₀)
20	19	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝐸 ∈ ℕ₀)
21		aks6d1c1p4.15	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ ℕ)
22	21	nnnn0d 12498	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
23		eqid 2736	. . . . . . . . . . . . 13 ⊢ (._g‘𝑉) = (._g‘𝑉)
24	12, 22, 23	isprimroot 42532	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ (𝑉 PrimRoots 𝑅) ↔ (𝑦 ∈ (Base‘𝑉) ∧ (𝑅(._g‘𝑉)𝑦) = (0_g‘𝑉) ∧ ∀𝑙 ∈ ℕ₀ ((𝑙(._g‘𝑉)𝑦) = (0_g‘𝑉) → 𝑅 ∥ 𝑙))))
25	24	biimpd 229	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑦 ∈ (𝑉 PrimRoots 𝑅) → (𝑦 ∈ (Base‘𝑉) ∧ (𝑅(._g‘𝑉)𝑦) = (0_g‘𝑉) ∧ ∀𝑙 ∈ ℕ₀ ((𝑙(._g‘𝑉)𝑦) = (0_g‘𝑉) → 𝑅 ∥ 𝑙))))
26	25	imp 406	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝑦 ∈ (Base‘𝑉) ∧ (𝑅(._g‘𝑉)𝑦) = (0_g‘𝑉) ∧ ∀𝑙 ∈ ℕ₀ ((𝑙(._g‘𝑉)𝑦) = (0_g‘𝑉) → 𝑅 ∥ 𝑙)))
27	26	simp1d 1143	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝑦 ∈ (Base‘𝑉))
28	27, 9	eleqtrrdi 2847	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝑦 ∈ (Base‘𝐾))
29	9, 10, 14, 20, 28	mulgnn0cld 19071	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑ 𝑦) ∈ (Base‘𝐾))
30	17	simprd 495	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ 𝐵)
31	30	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝐹 ∈ 𝐵)
32		eqidd 2737	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦)))
33	31, 32	jca 511	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐹 ∈ 𝐵 ∧ ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))))
34		aks6d1c1p4.19	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∼ 𝐺)
35	15, 34	aks6d1c1p1rcl 42547	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 ∈ ℕ ∧ 𝐺 ∈ 𝐵))
36	35	simprd 495	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ 𝐵)
37	36	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝐺 ∈ 𝐵)
38		eqidd 2737	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘𝐺)‘(𝐸 ↑ 𝑦)) = ((𝑂‘𝐺)‘(𝐸 ↑ 𝑦)))
39	37, 38	jca 511	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐺 ∈ 𝐵 ∧ ((𝑂‘𝐺)‘(𝐸 ↑ 𝑦)) = ((𝑂‘𝐺)‘(𝐸 ↑ 𝑦))))
40		aks6d1c1p4.5	. . . . . . . . 9 ⊢ 𝑊 = (mulGrp‘𝑆)
41		eqid 2736	. . . . . . . . 9 ⊢ (._r‘𝑆) = (._r‘𝑆)
42	40, 41	mgpplusg 20125	. . . . . . . 8 ⊢ (._r‘𝑆) = (+_g‘𝑊)
43	42	eqcomi 2745	. . . . . . 7 ⊢ (+_g‘𝑊) = (._r‘𝑆)
44		eqid 2736	. . . . . . 7 ⊢ (._r‘𝐾) = (._r‘𝐾)
45	1, 2, 3, 4, 7, 29, 33, 39, 43, 44	evl1muld 22308	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝐹(+_g‘𝑊)𝐺) ∈ 𝐵 ∧ ((𝑂‘(𝐹(+_g‘𝑊)𝐺))‘(𝐸 ↑ 𝑦)) = (((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))(._r‘𝐾)((𝑂‘𝐺)‘(𝐸 ↑ 𝑦)))))
46	45	simprd 495	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘(𝐹(+_g‘𝑊)𝐺))‘(𝐸 ↑ 𝑦)) = (((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))(._r‘𝐾)((𝑂‘𝐺)‘(𝐸 ↑ 𝑦))))
47	12	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝑉 ∈ CMnd)
48	1, 2, 3, 4, 7, 28, 31	fveval1fvcl 22298	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘𝐹)‘𝑦) ∈ (Base‘𝐾))
49	8	eqcomi 2745	. . . . . . . . . . . . . . 15 ⊢ (mulGrp‘𝐾) = 𝑉
50	49	fveq2i 6843	. . . . . . . . . . . . . 14 ⊢ (Base‘(mulGrp‘𝐾)) = (Base‘𝑉)
51	9, 50	eqtr4i 2762	. . . . . . . . . . . . 13 ⊢ (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
52	51	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (Base‘𝐾) = (Base‘(mulGrp‘𝐾)))
53	52	eleq2d 2822	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (((𝑂‘𝐹)‘𝑦) ∈ (Base‘𝐾) ↔ ((𝑂‘𝐹)‘𝑦) ∈ (Base‘(mulGrp‘𝐾))))
54	48, 53	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘𝐹)‘𝑦) ∈ (Base‘(mulGrp‘𝐾)))
55	1, 2, 3, 4, 7, 28, 37	fveval1fvcl 22298	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘𝐺)‘𝑦) ∈ (Base‘𝐾))
56	52	eleq2d 2822	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (((𝑂‘𝐺)‘𝑦) ∈ (Base‘𝐾) ↔ ((𝑂‘𝐺)‘𝑦) ∈ (Base‘(mulGrp‘𝐾))))
57	55, 56	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘𝐺)‘𝑦) ∈ (Base‘(mulGrp‘𝐾)))
58	20, 54, 57	3jca 1129	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ∈ ℕ₀ ∧ ((𝑂‘𝐹)‘𝑦) ∈ (Base‘(mulGrp‘𝐾)) ∧ ((𝑂‘𝐺)‘𝑦) ∈ (Base‘(mulGrp‘𝐾))))
59	49	fveq2i 6843	. . . . . . . . . 10 ⊢ (+_g‘(mulGrp‘𝐾)) = (+_g‘𝑉)
60	50, 10, 59	mulgnn0di 19800	. . . . . . . . 9 ⊢ ((𝑉 ∈ CMnd ∧ (𝐸 ∈ ℕ₀ ∧ ((𝑂‘𝐹)‘𝑦) ∈ (Base‘(mulGrp‘𝐾)) ∧ ((𝑂‘𝐺)‘𝑦) ∈ (Base‘(mulGrp‘𝐾)))) → (𝐸 ↑ (((𝑂‘𝐹)‘𝑦)(+_g‘(mulGrp‘𝐾))((𝑂‘𝐺)‘𝑦))) = ((𝐸 ↑ ((𝑂‘𝐹)‘𝑦))(+_g‘(mulGrp‘𝐾))(𝐸 ↑ ((𝑂‘𝐺)‘𝑦))))
61	47, 58, 60	syl2anc 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑ (((𝑂‘𝐹)‘𝑦)(+_g‘(mulGrp‘𝐾))((𝑂‘𝐺)‘𝑦))) = ((𝐸 ↑ ((𝑂‘𝐹)‘𝑦))(+_g‘(mulGrp‘𝐾))(𝐸 ↑ ((𝑂‘𝐺)‘𝑦))))
62	8, 44	mgpplusg 20125	. . . . . . . . . . . 12 ⊢ (._r‘𝐾) = (+_g‘𝑉)
63	8	fveq2i 6843	. . . . . . . . . . . 12 ⊢ (+_g‘𝑉) = (+_g‘(mulGrp‘𝐾))
64	62, 63	eqtri 2759	. . . . . . . . . . 11 ⊢ (._r‘𝐾) = (+_g‘(mulGrp‘𝐾))
65	64	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (._r‘𝐾) = (+_g‘(mulGrp‘𝐾)))
66	65	eqcomd 2742	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (+_g‘(mulGrp‘𝐾)) = (._r‘𝐾))
67		fveq2 6840	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ((𝑂‘𝐹)‘𝑧) = ((𝑂‘𝐹)‘𝑦))
68	67	oveq2d 7383	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → (𝐸 ↑ ((𝑂‘𝐹)‘𝑧)) = (𝐸 ↑ ((𝑂‘𝐹)‘𝑦)))
69		oveq2 7375	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → (𝐸 ↑ 𝑧) = (𝐸 ↑ 𝑦))
70	69	fveq2d 6844	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → ((𝑂‘𝐹)‘(𝐸 ↑ 𝑧)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦)))
71	68, 70	eqeq12d 2752	. . . . . . . . . 10 ⊢ (𝑧 = 𝑦 → ((𝐸 ↑ ((𝑂‘𝐹)‘𝑧)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑧)) ↔ (𝐸 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))))
72	15, 30, 18	aks6d1c1p1 42546	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ∼ 𝐹 ↔ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))))
73	16, 72	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦)))
74		fveq2 6840	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → ((𝑂‘𝐹)‘𝑦) = ((𝑂‘𝐹)‘𝑧))
75	74	oveq2d 7383	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (𝐸 ↑ ((𝑂‘𝐹)‘𝑦)) = (𝐸 ↑ ((𝑂‘𝐹)‘𝑧)))
76		oveq2 7375	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → (𝐸 ↑ 𝑦) = (𝐸 ↑ 𝑧))
77	76	fveq2d 6844	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑧)))
78	75, 77	eqeq12d 2752	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → ((𝐸 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦)) ↔ (𝐸 ↑ ((𝑂‘𝐹)‘𝑧)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑧))))
79	78	cbvralvw 3215	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦)) ↔ ∀𝑧 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐹)‘𝑧)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑧)))
80	73, 79	sylib 218	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑧 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐹)‘𝑧)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑧)))
81	80	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ∀𝑧 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐹)‘𝑧)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑧)))
82		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝑦 ∈ (𝑉 PrimRoots 𝑅))
83	71, 81, 82	rspcdva 3565	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝐸 ↑ 𝑦)))
84		fveq2 6840	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ((𝑂‘𝐺)‘𝑧) = ((𝑂‘𝐺)‘𝑦))
85	84	oveq2d 7383	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → (𝐸 ↑ ((𝑂‘𝐺)‘𝑧)) = (𝐸 ↑ ((𝑂‘𝐺)‘𝑦)))
86	69	fveq2d 6844	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → ((𝑂‘𝐺)‘(𝐸 ↑ 𝑧)) = ((𝑂‘𝐺)‘(𝐸 ↑ 𝑦)))
87	85, 86	eqeq12d 2752	. . . . . . . . . 10 ⊢ (𝑧 = 𝑦 → ((𝐸 ↑ ((𝑂‘𝐺)‘𝑧)) = ((𝑂‘𝐺)‘(𝐸 ↑ 𝑧)) ↔ (𝐸 ↑ ((𝑂‘𝐺)‘𝑦)) = ((𝑂‘𝐺)‘(𝐸 ↑ 𝑦))))
88	15, 36, 18	aks6d1c1p1 42546	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ∼ 𝐺 ↔ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐺)‘𝑦)) = ((𝑂‘𝐺)‘(𝐸 ↑ 𝑦))))
89	34, 88	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐺)‘𝑦)) = ((𝑂‘𝐺)‘(𝐸 ↑ 𝑦)))
90		fveq2 6840	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → ((𝑂‘𝐺)‘𝑦) = ((𝑂‘𝐺)‘𝑧))
91	90	oveq2d 7383	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (𝐸 ↑ ((𝑂‘𝐺)‘𝑦)) = (𝐸 ↑ ((𝑂‘𝐺)‘𝑧)))
92	76	fveq2d 6844	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → ((𝑂‘𝐺)‘(𝐸 ↑ 𝑦)) = ((𝑂‘𝐺)‘(𝐸 ↑ 𝑧)))
93	91, 92	eqeq12d 2752	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → ((𝐸 ↑ ((𝑂‘𝐺)‘𝑦)) = ((𝑂‘𝐺)‘(𝐸 ↑ 𝑦)) ↔ (𝐸 ↑ ((𝑂‘𝐺)‘𝑧)) = ((𝑂‘𝐺)‘(𝐸 ↑ 𝑧))))
94	93	cbvralvw 3215	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐺)‘𝑦)) = ((𝑂‘𝐺)‘(𝐸 ↑ 𝑦)) ↔ ∀𝑧 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐺)‘𝑧)) = ((𝑂‘𝐺)‘(𝐸 ↑ 𝑧)))
95	89, 94	sylib 218	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑧 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐺)‘𝑧)) = ((𝑂‘𝐺)‘(𝐸 ↑ 𝑧)))
96	95	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ∀𝑧 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘𝐺)‘𝑧)) = ((𝑂‘𝐺)‘(𝐸 ↑ 𝑧)))
97	87, 96, 82	rspcdva 3565	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑ ((𝑂‘𝐺)‘𝑦)) = ((𝑂‘𝐺)‘(𝐸 ↑ 𝑦)))
98	66, 83, 97	oveq123d 7388	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝐸 ↑ ((𝑂‘𝐹)‘𝑦))(+_g‘(mulGrp‘𝐾))(𝐸 ↑ ((𝑂‘𝐺)‘𝑦))) = (((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))(._r‘𝐾)((𝑂‘𝐺)‘(𝐸 ↑ 𝑦))))
99	61, 98	eqtr2d 2772	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))(._r‘𝐾)((𝑂‘𝐺)‘(𝐸 ↑ 𝑦))) = (𝐸 ↑ (((𝑂‘𝐹)‘𝑦)(+_g‘(mulGrp‘𝐾))((𝑂‘𝐺)‘𝑦))))
100	64	eqcomi 2745	. . . . . . . . . 10 ⊢ (+_g‘(mulGrp‘𝐾)) = (._r‘𝐾)
101	100	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (+_g‘(mulGrp‘𝐾)) = (._r‘𝐾))
102	101	oveqd 7384	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (((𝑂‘𝐹)‘𝑦)(+_g‘(mulGrp‘𝐾))((𝑂‘𝐺)‘𝑦)) = (((𝑂‘𝐹)‘𝑦)(._r‘𝐾)((𝑂‘𝐺)‘𝑦)))
103	102	oveq2d 7383	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑ (((𝑂‘𝐹)‘𝑦)(+_g‘(mulGrp‘𝐾))((𝑂‘𝐺)‘𝑦))) = (𝐸 ↑ (((𝑂‘𝐹)‘𝑦)(._r‘𝐾)((𝑂‘𝐺)‘𝑦))))
104	99, 103	eqtrd 2771	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))(._r‘𝐾)((𝑂‘𝐺)‘(𝐸 ↑ 𝑦))) = (𝐸 ↑ (((𝑂‘𝐹)‘𝑦)(._r‘𝐾)((𝑂‘𝐺)‘𝑦))))
105		eqidd 2737	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘𝐹)‘𝑦) = ((𝑂‘𝐹)‘𝑦))
106	31, 105	jca 511	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐹 ∈ 𝐵 ∧ ((𝑂‘𝐹)‘𝑦) = ((𝑂‘𝐹)‘𝑦)))
107		eqidd 2737	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘𝐺)‘𝑦) = ((𝑂‘𝐺)‘𝑦))
108	37, 107	jca 511	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐺 ∈ 𝐵 ∧ ((𝑂‘𝐺)‘𝑦) = ((𝑂‘𝐺)‘𝑦)))
109	1, 2, 3, 4, 7, 28, 106, 108, 43, 44	evl1muld 22308	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝐹(+_g‘𝑊)𝐺) ∈ 𝐵 ∧ ((𝑂‘(𝐹(+_g‘𝑊)𝐺))‘𝑦) = (((𝑂‘𝐹)‘𝑦)(._r‘𝐾)((𝑂‘𝐺)‘𝑦))))
110	109	simprd 495	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘(𝐹(+_g‘𝑊)𝐺))‘𝑦) = (((𝑂‘𝐹)‘𝑦)(._r‘𝐾)((𝑂‘𝐺)‘𝑦)))
111	110	eqcomd 2742	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (((𝑂‘𝐹)‘𝑦)(._r‘𝐾)((𝑂‘𝐺)‘𝑦)) = ((𝑂‘(𝐹(+_g‘𝑊)𝐺))‘𝑦))
112	111	oveq2d 7383	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑ (((𝑂‘𝐹)‘𝑦)(._r‘𝐾)((𝑂‘𝐺)‘𝑦))) = (𝐸 ↑ ((𝑂‘(𝐹(+_g‘𝑊)𝐺))‘𝑦)))
113	104, 112	eqtrd 2771	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (((𝑂‘𝐹)‘(𝐸 ↑ 𝑦))(._r‘𝐾)((𝑂‘𝐺)‘(𝐸 ↑ 𝑦))) = (𝐸 ↑ ((𝑂‘(𝐹(+_g‘𝑊)𝐺))‘𝑦)))
114	46, 113	eqtrd 2771	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘(𝐹(+_g‘𝑊)𝐺))‘(𝐸 ↑ 𝑦)) = (𝐸 ↑ ((𝑂‘(𝐹(+_g‘𝑊)𝐺))‘𝑦)))
115	114	eqcomd 2742	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑ ((𝑂‘(𝐹(+_g‘𝑊)𝐺))‘𝑦)) = ((𝑂‘(𝐹(+_g‘𝑊)𝐺))‘(𝐸 ↑ 𝑦)))
116	115	ralrimiva 3129	. 2 ⊢ (𝜑 → ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘(𝐹(+_g‘𝑊)𝐺))‘𝑦)) = ((𝑂‘(𝐹(+_g‘𝑊)𝐺))‘(𝐸 ↑ 𝑦)))
117	2	ply1crng 22162	. . . . . 6 ⊢ (𝐾 ∈ CRing → 𝑆 ∈ CRing)
118	6, 117	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ CRing)
119	118	crngringd 20227	. . . 4 ⊢ (𝜑 → 𝑆 ∈ Ring)
120	4, 43, 119, 30, 36	ringcld 20241	. . 3 ⊢ (𝜑 → (𝐹(+_g‘𝑊)𝐺) ∈ 𝐵)
121	15, 120, 18	aks6d1c1p1 42546	. 2 ⊢ (𝜑 → (𝐸 ∼ (𝐹(+_g‘𝑊)𝐺) ↔ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘(𝐹(+_g‘𝑊)𝐺))‘𝑦)) = ((𝑂‘(𝐹(+_g‘𝑊)𝐺))‘(𝐸 ↑ 𝑦))))
122	116, 121	mpbird 257	1 ⊢ (𝜑 → 𝐸 ∼ (𝐹(+_g‘𝑊)𝐺))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∀wral 3051 class class class wbr 5085 {copab 5147 ‘cfv 6498 (class class class)co 7367 1c1 11039 ℕcn 12174 ℕ₀cn0 12437 ∥ cdvds 16221 gcd cgcd 16463 ℙcprime 16640 Basecbs 17179 +_gcplusg 17220 ._rcmulr 17221 0_gc0g 17402 Mndcmnd 18702 ._gcmg 19043 CMndccmn 19755 mulGrpcmgp 20121 CRingccrg 20215 Fieldcfield 20707 chrcchr 21481 algSccascl 21832 var₁cv1 22139 Poly₁cpl1 22140 eval₁ce1 22279 PrimRoots cprimroots 42530

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-iin 4936 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-isom 6507 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-of 7631 df-ofr 7632 df-om 7818 df-1st 7942 df-2nd 7943 df-supp 8111 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-2o 8406 df-er 8643 df-map 8775 df-pm 8776 df-ixp 8846 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-fsupp 9275 df-sup 9355 df-oi 9425 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-nn 12175 df-2 12244 df-3 12245 df-4 12246 df-5 12247 df-6 12248 df-7 12249 df-8 12250 df-9 12251 df-n0 12438 df-z 12525 df-dec 12645 df-uz 12789 df-fz 13462 df-fzo 13609 df-seq 13964 df-hash 14293 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-hom 17244 df-cco 17245 df-0g 17404 df-gsum 17405 df-prds 17410 df-pws 17412 df-mre 17548 df-mrc 17549 df-acs 17551 df-mgm 18608 df-sgrp 18687 df-mnd 18703 df-mhm 18751 df-submnd 18752 df-grp 18912 df-minusg 18913 df-sbg 18914 df-mulg 19044 df-subg 19099 df-ghm 19188 df-cntz 19292 df-cmn 19757 df-abl 19758 df-mgp 20122 df-rng 20134 df-ur 20163 df-srg 20168 df-ring 20216 df-cring 20217 df-rhm 20452 df-subrng 20523 df-subrg 20547 df-field 20709 df-lmod 20857 df-lss 20927 df-lsp 20967 df-assa 21833 df-asp 21834 df-ascl 21835 df-psr 21889 df-mvr 21890 df-mpl 21891 df-opsr 21893 df-evls 22052 df-evl 22053 df-psr1 22143 df-ply1 22145 df-evl1 22281 df-primroots 42531

This theorem is referenced by: aks6d1c1p6 42553 aks6d1c1 42555

W3C validator