Theorem isprimroot 41998

Description: The value of a primitive root. (Contributed by metakunt, 25-Apr-2025.)

Hypotheses

Ref	Expression
isprimroot.1	⊢ (𝜑 → 𝑅 ∈ CMnd)
isprimroot.2	⊢ (𝜑 → 𝐾 ∈ ℕ0)
isprimroot.3	⊢ ↑ = (.g‘𝑅)

Assertion

Ref	Expression
isprimroot	⊢ (𝜑 → (𝑀 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 ↑ 𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))

Distinct variable groups:   𝐾,𝑙   𝑀,𝑙   𝑅,𝑙   𝜑,𝑙

Allowed substitution hint:   ↑ (𝑙)

Proof of Theorem isprimroot

Dummy variables 𝑏 𝑘 𝑟 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-primroots 41997	. . . . . 6 ⊢ PrimRoots = (𝑟 ∈ CMnd, 𝑘 ∈ ℕ0 ↦ ⦋(Base‘𝑟) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝑘(.g‘𝑟)𝑥) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙))})
2	1	a1i 11	. . . . 5 ⊢ (𝜑 → PrimRoots = (𝑟 ∈ CMnd, 𝑘 ∈ ℕ0 ↦ ⦋(Base‘𝑟) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝑘(.g‘𝑟)𝑥) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙))}))
3		simprl 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) → 𝑟 = 𝑅)
4	3	fveq2d 6923	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) → (Base‘𝑟) = (Base‘𝑅))
5		simplrl 776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → 𝑟 = 𝑅)
6	5	fveq2d 6923	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (.g‘𝑟) = (.g‘𝑅))
7		simplrr 777	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → 𝑘 = 𝐾)
8		eqidd 2735	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → 𝑥 = 𝑥)
9	6, 7, 8	oveq123d 7466	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (𝑘(.g‘𝑟)𝑥) = (𝐾(.g‘𝑅)𝑥))
10	5	fveq2d 6923	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (0g‘𝑟) = (0g‘𝑅))
11	9, 10	eqeq12d 2750	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → ((𝑘(.g‘𝑟)𝑥) = (0g‘𝑟) ↔ (𝐾(.g‘𝑅)𝑥) = (0g‘𝑅)))
12	3	fveq2d 6923	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) → (.g‘𝑟) = (.g‘𝑅))
13	12	oveqdr 7473	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (𝑙(.g‘𝑟)𝑥) = (𝑙(.g‘𝑅)𝑥))
14	13, 10	eqeq12d 2750	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) ↔ (𝑙(.g‘𝑅)𝑥) = (0g‘𝑅)))
15	7	breq1d 5179	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (𝑘 ∥ 𝑙 ↔ 𝐾 ∥ 𝑙))
16	14, 15	imbi12d 344	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙) ↔ ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
17	16	ralbidv 3180	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
18	11, 17	anbi12d 631	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (((𝑘(.g‘𝑟)𝑥) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙)) ↔ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
19	18	rabbidva 3445	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) → {𝑥 ∈ 𝑏 ∣ ((𝑘(.g‘𝑟)𝑥) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙))} = {𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
20	4, 19	csbeq12dv 3924	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) → ⦋(Base‘𝑟) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝑘(.g‘𝑟)𝑥) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙))} = ⦋(Base‘𝑅) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
21		isprimroot.1	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ CMnd)
22		isprimroot.2	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
23		eqid 2734	. . . . . . 7 ⊢ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} = {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))}
24		fvexd 6934	. . . . . . 7 ⊢ (𝜑 → (Base‘𝑅) ∈ V)
25	23, 24	rabexd 5361	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ∈ V)
26		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 = (Base‘𝑅)) → 𝑏 = (Base‘𝑅))
27	26	rabeqdv 3454	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 = (Base‘𝑅)) → {𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} = {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
28	24, 27	csbied 3953	. . . . . . 7 ⊢ (𝜑 → ⦋(Base‘𝑅) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} = {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
29	28	eleq1d 2823	. . . . . 6 ⊢ (𝜑 → (⦋(Base‘𝑅) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ∈ V ↔ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ∈ V))
30	25, 29	mpbird 257	. . . . 5 ⊢ (𝜑 → ⦋(Base‘𝑅) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ∈ V)
31	2, 20, 21, 22, 30	ovmpod 7598	. . . 4 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = ⦋(Base‘𝑅) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
32	31, 28	eqtrd 2774	. . 3 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
33	32	eleq2d 2824	. 2 ⊢ (𝜑 → (𝑀 ∈ (𝑅 PrimRoots 𝐾) ↔ 𝑀 ∈ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))}))
34		oveq2 7453	. . . . . . 7 ⊢ (𝑥 = 𝑀 → (𝐾(.g‘𝑅)𝑥) = (𝐾(.g‘𝑅)𝑀))
35	34	eqeq1d 2736	. . . . . 6 ⊢ (𝑥 = 𝑀 → ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ↔ (𝐾(.g‘𝑅)𝑀) = (0g‘𝑅)))
36		oveq2 7453	. . . . . . . . 9 ⊢ (𝑥 = 𝑀 → (𝑙(.g‘𝑅)𝑥) = (𝑙(.g‘𝑅)𝑀))
37	36	eqeq1d 2736	. . . . . . . 8 ⊢ (𝑥 = 𝑀 → ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) ↔ (𝑙(.g‘𝑅)𝑀) = (0g‘𝑅)))
38	37	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = 𝑀 → (((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
39	38	ralbidv 3180	. . . . . 6 ⊢ (𝑥 = 𝑀 → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
40	35, 39	anbi12d 631	. . . . 5 ⊢ (𝑥 = 𝑀 → (((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙)) ↔ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
41	40	elrab 3703	. . . 4 ⊢ (𝑀 ∈ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ↔ (𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
42	41	a1i 11	. . 3 ⊢ (𝜑 → (𝑀 ∈ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ↔ (𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))))
43		3anass 1095	. . . . . 6 ⊢ ((𝑀 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)) ↔ (𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
44	43	bicomi 224	. . . . 5 ⊢ ((𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
45	44	a1i 11	. . . 4 ⊢ (𝜑 → ((𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
46		biidd 262	. . . . 5 ⊢ (𝜑 → (𝑀 ∈ (Base‘𝑅) ↔ 𝑀 ∈ (Base‘𝑅)))
47		isprimroot.3	. . . . . . . . 9 ⊢ ↑ = (.g‘𝑅)
48	47	eqcomi 2743	. . . . . . . 8 ⊢ (.g‘𝑅) = ↑
49	48	a1i 11	. . . . . . 7 ⊢ (𝜑 → (.g‘𝑅) = ↑ )
50	49	oveqd 7462	. . . . . 6 ⊢ (𝜑 → (𝐾(.g‘𝑅)𝑀) = (𝐾 ↑ 𝑀))
51	50	eqeq1d 2736	. . . . 5 ⊢ (𝜑 → ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ↔ (𝐾 ↑ 𝑀) = (0g‘𝑅)))
52	49	oveqd 7462	. . . . . . . 8 ⊢ (𝜑 → (𝑙(.g‘𝑅)𝑀) = (𝑙 ↑ 𝑀))
53	52	eqeq1d 2736	. . . . . . 7 ⊢ (𝜑 → ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) ↔ (𝑙 ↑ 𝑀) = (0g‘𝑅)))
54	53	imbi1d 341	. . . . . 6 ⊢ (𝜑 → (((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
55	54	ralbidv 3180	. . . . 5 ⊢ (𝜑 → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
56	46, 51, 55	3anbi123d 1436	. . . 4 ⊢ (𝜑 → ((𝑀 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 ↑ 𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
57	45, 56	bitrd 279	. . 3 ⊢ (𝜑 → ((𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 ↑ 𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
58	42, 57	bitrd 279	. 2 ⊢ (𝜑 → (𝑀 ∈ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 ↑ 𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
59	33, 58	bitrd 279	1 ⊢ (𝜑 → (𝑀 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 ↑ 𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2103  ∀wral 3063  {crab 3438  Vcvv 3482  ⦋csb 3915   class class class wbr 5169  ‘cfv 6572  (class class class)co 7445   ∈ cmpo 7447  ℕ₀cn0 12549   ∥ cdvds 16296  Basecbs 17253  0_gc0g 17494  ._gcmg 19102  CMndccmn 19817   PrimRoots cprimroots 41996

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 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-sep 5320  ax-nul 5327  ax-pr 5450

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ne 2943  df-ral 3064  df-rex 3073  df-rab 3439  df-v 3484  df-sbc 3799  df-csb 3916  df-dif 3973  df-un 3975  df-in 3977  df-ss 3987  df-nul 4348  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5170  df-opab 5232  df-id 5597  df-xp 5705  df-rel 5706  df-cnv 5707  df-co 5708  df-dm 5709  df-iota 6524  df-fun 6574  df-fv 6580  df-ov 7448  df-oprab 7449  df-mpo 7450  df-primroots 41997

This theorem is referenced by:  isprimroot2  41999  primrootsunit1  42002  primrootscoprmpow  42004  primrootscoprbij  42007  primrootlekpowne0  42010  primrootspoweq0  42011  aks6d1c1p2  42014  aks6d1c1p3  42015  aks6d1c1p4  42016  aks6d1c1p5  42017  aks6d1c1p7  42018  aks6d1c1p6  42019  aks6d1c1p8  42020  aks6d1c2lem3  42031  aks6d1c2lem4  42032  aks6d1c6lem2  42076  aks6d1c6lem3  42077  aks6d1c6lem4  42078  aks6d1c6isolem1  42079  aks6d1c6isolem2  42080  aks6d1c6lem5  42082  aks5lem2  42092  aks5lem3a  42094