Metamath Proof Explorer

Theorem isprimroot

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

Ref Expression
Hypotheses isprimroot.1 ⊢ φ → R ∈ CMnd
isprimroot.2 ⊢ φ → K ∈ ℕ 0
isprimroot.3 ⊢ × ˙ = ⋅ R
Assertion isprimroot ⊢ φ → M ∈ R PrimRoots K ↔ M ∈ Base R ∧ K × ˙ M = 0 R ∧ ∀ l ∈ ℕ 0 l × ˙ M = 0 R → K ∥ l

Proof

Step Hyp Ref Expression
1 isprimroot.1 ⊢ φ → R ∈ CMnd
2 isprimroot.2 ⊢ φ → K ∈ ℕ 0
3 isprimroot.3 ⊢ × ˙ = ⋅ R
4 df-primroots ⊢ PrimRoots = r ∈ CMnd , k ∈ ℕ 0 ⟼ ⦋ Base r / b⦌ x ∈ b | k ⋅ r x = 0 r ∧ ∀ l ∈ ℕ 0 l ⋅ r x = 0 r → k ∥ l
5 4 a1i ⊢ φ → PrimRoots = r ∈ CMnd , k ∈ ℕ 0 ⟼ ⦋ Base r / b⦌ x ∈ b | k ⋅ r x = 0 r ∧ ∀ l ∈ ℕ 0 l ⋅ r x = 0 r → k ∥ l
6 simprl ⊢ φ ∧ r = R ∧ k = K → r = R
7 6 fveq2d ⊢ φ ∧ r = R ∧ k = K → Base r = Base R
8 simplrl ⊢ φ ∧ r = R ∧ k = K ∧ x ∈ b → r = R
9 8 fveq2d ⊢ φ ∧ r = R ∧ k = K ∧ x ∈ b → ⋅ r = ⋅ R
10 simplrr ⊢ φ ∧ r = R ∧ k = K ∧ x ∈ b → k = K
11 eqidd ⊢ φ ∧ r = R ∧ k = K ∧ x ∈ b → x = x
12 9 10 11 oveq123d ⊢ φ ∧ r = R ∧ k = K ∧ x ∈ b → k ⋅ r x = K ⋅ R x
13 8 fveq2d ⊢ φ ∧ r = R ∧ k = K ∧ x ∈ b → 0 r = 0 R
14 12 13 eqeq12d ⊢ φ ∧ r = R ∧ k = K ∧ x ∈ b → k ⋅ r x = 0 r ↔ K ⋅ R x = 0 R
15 6 fveq2d ⊢ φ ∧ r = R ∧ k = K → ⋅ r = ⋅ R
16 15 oveqdr ⊢ φ ∧ r = R ∧ k = K ∧ x ∈ b → l ⋅ r x = l ⋅ R x
17 16 13 eqeq12d ⊢ φ ∧ r = R ∧ k = K ∧ x ∈ b → l ⋅ r x = 0 r ↔ l ⋅ R x = 0 R
18 10 breq1d ⊢ φ ∧ r = R ∧ k = K ∧ x ∈ b → k ∥ l ↔ K ∥ l
19 17 18 imbi12d ⊢ φ ∧ r = R ∧ k = K ∧ x ∈ b → l ⋅ r x = 0 r → k ∥ l ↔ l ⋅ R x = 0 R → K ∥ l
20 19 ralbidv ⊢ φ ∧ r = R ∧ k = K ∧ x ∈ b → ∀ l ∈ ℕ 0 l ⋅ r x = 0 r → k ∥ l ↔ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l
21 14 20 anbi12d ⊢ φ ∧ r = R ∧ k = K ∧ x ∈ b → k ⋅ r x = 0 r ∧ ∀ l ∈ ℕ 0 l ⋅ r x = 0 r → k ∥ l ↔ K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l
22 21 rabbidva ⊢ φ ∧ r = R ∧ k = K → x ∈ b | k ⋅ r x = 0 r ∧ ∀ l ∈ ℕ 0 l ⋅ r x = 0 r → k ∥ l = x ∈ b | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l
23 7 22 csbeq12dv ⊢ φ ∧ r = R ∧ k = K → ⦋ Base r / b⦌ x ∈ b | k ⋅ r x = 0 r ∧ ∀ l ∈ ℕ 0 l ⋅ r x = 0 r → k ∥ l = ⦋ Base R / b⦌ x ∈ b | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l
24 eqid ⊢ x ∈ Base R | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l = x ∈ Base R | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l
25 fvexd ⊢ φ → Base R ∈ V
26 24 25 rabexd ⊢ φ → x ∈ Base R | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l ∈ V
27 simpr ⊢ φ ∧ b = Base R → b = Base R
28 27 rabeqdv ⊢ φ ∧ b = Base R → x ∈ b | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l = x ∈ Base R | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l
29 25 28 csbied ⊢ φ → ⦋ Base R / b⦌ x ∈ b | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l = x ∈ Base R | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l
30 29 eleq1d ⊢ φ → ⦋ Base R / b⦌ x ∈ b | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l ∈ V ↔ x ∈ Base R | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l ∈ V
31 26 30 mpbird ⊢ φ → ⦋ Base R / b⦌ x ∈ b | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l ∈ V
32 5 23 1 2 31 ovmpod ⊢ φ → R PrimRoots K = ⦋ Base R / b⦌ x ∈ b | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l
33 32 29 eqtrd ⊢ φ → R PrimRoots K = x ∈ Base R | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l
34 33 eleq2d ⊢ φ → M ∈ R PrimRoots K ↔ M ∈ x ∈ Base R | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l
35 oveq2 ⊢ x = M → K ⋅ R x = K ⋅ R M
36 35 eqeq1d ⊢ x = M → K ⋅ R x = 0 R ↔ K ⋅ R M = 0 R
37 oveq2 ⊢ x = M → l ⋅ R x = l ⋅ R M
38 37 eqeq1d ⊢ x = M → l ⋅ R x = 0 R ↔ l ⋅ R M = 0 R
39 38 imbi1d ⊢ x = M → l ⋅ R x = 0 R → K ∥ l ↔ l ⋅ R M = 0 R → K ∥ l
40 39 ralbidv ⊢ x = M → ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l ↔ ∀ l ∈ ℕ 0 l ⋅ R M = 0 R → K ∥ l
41 36 40 anbi12d ⊢ x = M → K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l ↔ K ⋅ R M = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R M = 0 R → K ∥ l
42 41 elrab ⊢ M ∈ x ∈ Base R | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l ↔ M ∈ Base R ∧ K ⋅ R M = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R M = 0 R → K ∥ l
43 42 a1i ⊢ φ → M ∈ x ∈ Base R | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l ↔ M ∈ Base R ∧ K ⋅ R M = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R M = 0 R → K ∥ l
44 3anass ⊢ M ∈ Base R ∧ K ⋅ R M = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R M = 0 R → K ∥ l ↔ M ∈ Base R ∧ K ⋅ R M = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R M = 0 R → K ∥ l
45 44 bicomi ⊢ M ∈ Base R ∧ K ⋅ R M = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R M = 0 R → K ∥ l ↔ M ∈ Base R ∧ K ⋅ R M = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R M = 0 R → K ∥ l
46 45 a1i ⊢ φ → M ∈ Base R ∧ K ⋅ R M = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R M = 0 R → K ∥ l ↔ M ∈ Base R ∧ K ⋅ R M = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R M = 0 R → K ∥ l
47 biidd ⊢ φ → M ∈ Base R ↔ M ∈ Base R
48 3 eqcomi ⊢ ⋅ R = × ˙
49 48 a1i ⊢ φ → ⋅ R = × ˙
50 49 oveqd ⊢ φ → K ⋅ R M = K × ˙ M
51 50 eqeq1d ⊢ φ → K ⋅ R M = 0 R ↔ K × ˙ M = 0 R
52 49 oveqd ⊢ φ → l ⋅ R M = l × ˙ M
53 52 eqeq1d ⊢ φ → l ⋅ R M = 0 R ↔ l × ˙ M = 0 R
54 53 imbi1d ⊢ φ → l ⋅ R M = 0 R → K ∥ l ↔ l × ˙ M = 0 R → K ∥ l
55 54 ralbidv ⊢ φ → ∀ l ∈ ℕ 0 l ⋅ R M = 0 R → K ∥ l ↔ ∀ l ∈ ℕ 0 l × ˙ M = 0 R → K ∥ l
56 47 51 55 3anbi123d ⊢ φ → M ∈ Base R ∧ K ⋅ R M = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R M = 0 R → K ∥ l ↔ M ∈ Base R ∧ K × ˙ M = 0 R ∧ ∀ l ∈ ℕ 0 l × ˙ M = 0 R → K ∥ l
57 46 56 bitrd ⊢ φ → M ∈ Base R ∧ K ⋅ R M = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R M = 0 R → K ∥ l ↔ M ∈ Base R ∧ K × ˙ M = 0 R ∧ ∀ l ∈ ℕ 0 l × ˙ M = 0 R → K ∥ l
58 43 57 bitrd ⊢ φ → M ∈ x ∈ Base R | K ⋅ R x = 0 R ∧ ∀ l ∈ ℕ 0 l ⋅ R x = 0 R → K ∥ l ↔ M ∈ Base R ∧ K × ˙ M = 0 R ∧ ∀ l ∈ ℕ 0 l × ˙ M = 0 R → K ∥ l
59 34 58 bitrd ⊢ φ → M ∈ R PrimRoots K ↔ M ∈ Base R ∧ K × ˙ M = 0 R ∧ ∀ l ∈ ℕ 0 l × ˙ M = 0 R → K ∥ l