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

Theorem isprimroot 42052
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.
StepHypRef Expression
1 df-primroots 42051 . . . . . 6 PrimRoots = (𝑟 ∈ CMnd, 𝑘 ∈ ℕ0(Base‘𝑟) / 𝑏{𝑥𝑏 ∣ ((𝑘(.g𝑟)𝑥) = (0g𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑟)𝑥) = (0g𝑟) → 𝑘𝑙))})
21a1i 11 . . . . 5 (𝜑 → PrimRoots = (𝑟 ∈ CMnd, 𝑘 ∈ ℕ0(Base‘𝑟) / 𝑏{𝑥𝑏 ∣ ((𝑘(.g𝑟)𝑥) = (0g𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑟)𝑥) = (0g𝑟) → 𝑘𝑙))}))
3 simprl 770 . . . . . . 7 ((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) → 𝑟 = 𝑅)
43fveq2d 6926 . . . . . 6 ((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) → (Base‘𝑟) = (Base‘𝑅))
5 simplrl 776 . . . . . . . . . . 11 (((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) ∧ 𝑥𝑏) → 𝑟 = 𝑅)
65fveq2d 6926 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) ∧ 𝑥𝑏) → (.g𝑟) = (.g𝑅))
7 simplrr 777 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) ∧ 𝑥𝑏) → 𝑘 = 𝐾)
8 eqidd 2741 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) ∧ 𝑥𝑏) → 𝑥 = 𝑥)
96, 7, 8oveq123d 7471 . . . . . . . . 9 (((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) ∧ 𝑥𝑏) → (𝑘(.g𝑟)𝑥) = (𝐾(.g𝑅)𝑥))
105fveq2d 6926 . . . . . . . . 9 (((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) ∧ 𝑥𝑏) → (0g𝑟) = (0g𝑅))
119, 10eqeq12d 2756 . . . . . . . 8 (((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) ∧ 𝑥𝑏) → ((𝑘(.g𝑟)𝑥) = (0g𝑟) ↔ (𝐾(.g𝑅)𝑥) = (0g𝑅)))
123fveq2d 6926 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) → (.g𝑟) = (.g𝑅))
1312oveqdr 7478 . . . . . . . . . . 11 (((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) ∧ 𝑥𝑏) → (𝑙(.g𝑟)𝑥) = (𝑙(.g𝑅)𝑥))
1413, 10eqeq12d 2756 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) ∧ 𝑥𝑏) → ((𝑙(.g𝑟)𝑥) = (0g𝑟) ↔ (𝑙(.g𝑅)𝑥) = (0g𝑅)))
157breq1d 5176 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) ∧ 𝑥𝑏) → (𝑘𝑙𝐾𝑙))
1614, 15imbi12d 344 . . . . . . . . 9 (((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) ∧ 𝑥𝑏) → (((𝑙(.g𝑟)𝑥) = (0g𝑟) → 𝑘𝑙) ↔ ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙)))
1716ralbidv 3184 . . . . . . . 8 (((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) ∧ 𝑥𝑏) → (∀𝑙 ∈ ℕ0 ((𝑙(.g𝑟)𝑥) = (0g𝑟) → 𝑘𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙)))
1811, 17anbi12d 631 . . . . . . 7 (((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) ∧ 𝑥𝑏) → (((𝑘(.g𝑟)𝑥) = (0g𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑟)𝑥) = (0g𝑟) → 𝑘𝑙)) ↔ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))))
1918rabbidva 3450 . . . . . 6 ((𝜑 ∧ (𝑟 = 𝑅𝑘 = 𝐾)) → {𝑥𝑏 ∣ ((𝑘(.g𝑟)𝑥) = (0g𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑟)𝑥) = (0g𝑟) → 𝑘𝑙))} = {𝑥𝑏 ∣ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))})
204, 19csbeq12dv 3930 . . . . 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 2740 . . . . . . 7 {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))} = {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))}
24 fvexd 6937 . . . . . . 7 (𝜑 → (Base‘𝑅) ∈ V)
2523, 24rabexd 5358 . . . . . 6 (𝜑 → {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))} ∈ V)
26 simpr 484 . . . . . . . . 9 ((𝜑𝑏 = (Base‘𝑅)) → 𝑏 = (Base‘𝑅))
2726rabeqdv 3459 . . . . . . . 8 ((𝜑𝑏 = (Base‘𝑅)) → {𝑥𝑏 ∣ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))} = {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))})
2824, 27csbied 3959 . . . . . . 7 (𝜑(Base‘𝑅) / 𝑏{𝑥𝑏 ∣ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))} = {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))})
2928eleq1d 2829 . . . . . 6 (𝜑 → ((Base‘𝑅) / 𝑏{𝑥𝑏 ∣ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))} ∈ V ↔ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))} ∈ V))
3025, 29mpbird 257 . . . . 5 (𝜑(Base‘𝑅) / 𝑏{𝑥𝑏 ∣ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))} ∈ V)
312, 20, 21, 22, 30ovmpod 7604 . . . 4 (𝜑 → (𝑅 PrimRoots 𝐾) = (Base‘𝑅) / 𝑏{𝑥𝑏 ∣ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))})
3231, 28eqtrd 2780 . . 3 (𝜑 → (𝑅 PrimRoots 𝐾) = {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))})
3332eleq2d 2830 . 2 (𝜑 → (𝑀 ∈ (𝑅 PrimRoots 𝐾) ↔ 𝑀 ∈ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))}))
34 oveq2 7458 . . . . . . 7 (𝑥 = 𝑀 → (𝐾(.g𝑅)𝑥) = (𝐾(.g𝑅)𝑀))
3534eqeq1d 2742 . . . . . 6 (𝑥 = 𝑀 → ((𝐾(.g𝑅)𝑥) = (0g𝑅) ↔ (𝐾(.g𝑅)𝑀) = (0g𝑅)))
36 oveq2 7458 . . . . . . . . 9 (𝑥 = 𝑀 → (𝑙(.g𝑅)𝑥) = (𝑙(.g𝑅)𝑀))
3736eqeq1d 2742 . . . . . . . 8 (𝑥 = 𝑀 → ((𝑙(.g𝑅)𝑥) = (0g𝑅) ↔ (𝑙(.g𝑅)𝑀) = (0g𝑅)))
3837imbi1d 341 . . . . . . 7 (𝑥 = 𝑀 → (((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙) ↔ ((𝑙(.g𝑅)𝑀) = (0g𝑅) → 𝐾𝑙)))
3938ralbidv 3184 . . . . . 6 (𝑥 = 𝑀 → (∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑀) = (0g𝑅) → 𝐾𝑙)))
4035, 39anbi12d 631 . . . . 5 (𝑥 = 𝑀 → (((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙)) ↔ ((𝐾(.g𝑅)𝑀) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑀) = (0g𝑅) → 𝐾𝑙))))
4140elrab 3708 . . . 4 (𝑀 ∈ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))} ↔ (𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g𝑅)𝑀) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑀) = (0g𝑅) → 𝐾𝑙))))
4241a1i 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𝑅) → 𝐾𝑙))))
4443bicomi 224 . . . . 5 ((𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g𝑅)𝑀) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑀) = (0g𝑅) → 𝐾𝑙))) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾(.g𝑅)𝑀) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑀) = (0g𝑅) → 𝐾𝑙)))
4544a1i 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𝑅)
4847eqcomi 2749 . . . . . . . 8 (.g𝑅) =
4948a1i 11 . . . . . . 7 (𝜑 → (.g𝑅) = )
5049oveqd 7467 . . . . . 6 (𝜑 → (𝐾(.g𝑅)𝑀) = (𝐾 𝑀))
5150eqeq1d 2742 . . . . 5 (𝜑 → ((𝐾(.g𝑅)𝑀) = (0g𝑅) ↔ (𝐾 𝑀) = (0g𝑅)))
5249oveqd 7467 . . . . . . . 8 (𝜑 → (𝑙(.g𝑅)𝑀) = (𝑙 𝑀))
5352eqeq1d 2742 . . . . . . 7 (𝜑 → ((𝑙(.g𝑅)𝑀) = (0g𝑅) ↔ (𝑙 𝑀) = (0g𝑅)))
5453imbi1d 341 . . . . . 6 (𝜑 → (((𝑙(.g𝑅)𝑀) = (0g𝑅) → 𝐾𝑙) ↔ ((𝑙 𝑀) = (0g𝑅) → 𝐾𝑙)))
5554ralbidv 3184 . . . . 5 (𝜑 → (∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑀) = (0g𝑅) → 𝐾𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙 𝑀) = (0g𝑅) → 𝐾𝑙)))
5646, 51, 553anbi123d 1436 . . . 4 (𝜑 → ((𝑀 ∈ (Base‘𝑅) ∧ (𝐾(.g𝑅)𝑀) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑀) = (0g𝑅) → 𝐾𝑙)) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 𝑀) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 𝑀) = (0g𝑅) → 𝐾𝑙))))
5745, 56bitrd 279 . . 3 (𝜑 → ((𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g𝑅)𝑀) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑀) = (0g𝑅) → 𝐾𝑙))) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 𝑀) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 𝑀) = (0g𝑅) → 𝐾𝑙))))
5842, 57bitrd 279 . 2 (𝜑 → (𝑀 ∈ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g𝑅)𝑥) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g𝑅)𝑥) = (0g𝑅) → 𝐾𝑙))} ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 𝑀) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 𝑀) = (0g𝑅) → 𝐾𝑙))))
5933, 58bitrd 279 1 (𝜑 → (𝑀 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 𝑀) = (0g𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 𝑀) = (0g𝑅) → 𝐾𝑙))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1537  wcel 2108  wral 3067  {crab 3443  Vcvv 3488  csb 3921   class class class wbr 5166  cfv 6575  (class class class)co 7450  cmpo 7452  0cn0 12555  cdvds 16304  Basecbs 17260  0gc0g 17501  .gcmg 19109  CMndccmn 19824   PrimRoots cprimroots 42050
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-sep 5317  ax-nul 5324  ax-pr 5447
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 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  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-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6527  df-fun 6577  df-fv 6583  df-ov 7453  df-oprab 7454  df-mpo 7455  df-primroots 42051
This theorem is referenced by:  isprimroot2  42053  primrootsunit1  42056  primrootscoprmpow  42058  primrootscoprbij  42061  primrootlekpowne0  42064  primrootspoweq0  42065  aks6d1c1p2  42068  aks6d1c1p3  42069  aks6d1c1p4  42070  aks6d1c1p5  42071  aks6d1c1p7  42072  aks6d1c1p6  42073  aks6d1c1p8  42074  aks6d1c2lem3  42085  aks6d1c2lem4  42086  aks6d1c6lem2  42130  aks6d1c6lem3  42131  aks6d1c6lem4  42132  aks6d1c6isolem1  42133  aks6d1c6isolem2  42134  aks6d1c6lem5  42136  aks5lem2  42146  aks5lem3a  42148
  Copyright terms: Public domain W3C validator