Metamath Proof Explorer

Theorem isprimroot

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

Ref Expression
Hypotheses isprimroot.1 ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
isprimroot.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
isprimroot.3 ⊢ ↑ = ( .g ‘ 𝑅 )
Assertion isprimroot ( 𝜑 → ( 𝑀 ∈ ( 𝑅 PrimRoots 𝐾 ) ↔ ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ↑ 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) )

Proof

Step Hyp Ref Expression
1 isprimroot.1 ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
2 isprimroot.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 isprimroot.3 ⊢ ↑ = ( .g ‘ 𝑅 )
4 df-primroots ⊢ PrimRoots = ( 𝑟 ∈ CMnd , 𝑘 ∈ ℕ0 ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑏 ⦌ { 𝑥 ∈ 𝑏 ∣ ( ( 𝑘 ( .g ‘ 𝑟 ) 𝑥 ) = ( 0g ‘ 𝑟 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑟 ) 𝑥 ) = ( 0g ‘ 𝑟 ) → 𝑘 ∥ 𝑙 ) ) } )
5 4 a1i ⊢ ( 𝜑 → PrimRoots = ( 𝑟 ∈ CMnd , 𝑘 ∈ ℕ0 ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑏 ⦌ { 𝑥 ∈ 𝑏 ∣ ( ( 𝑘 ( .g ‘ 𝑟 ) 𝑥 ) = ( 0g ‘ 𝑟 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑟 ) 𝑥 ) = ( 0g ‘ 𝑟 ) → 𝑘 ∥ 𝑙 ) ) } ) )
6 simprl ⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) → 𝑟 = 𝑅 )
7 6 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
8 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) ∧ 𝑥 ∈ 𝑏 ) → 𝑟 = 𝑅 )
9 8 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( .g ‘ 𝑟 ) = ( .g ‘ 𝑅 ) )
10 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) ∧ 𝑥 ∈ 𝑏 ) → 𝑘 = 𝐾 )
11 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) ∧ 𝑥 ∈ 𝑏 ) → 𝑥 = 𝑥 )
12 9 10 11 oveq123d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( 𝑘 ( .g ‘ 𝑟 ) 𝑥 ) = ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) )
13 8 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
14 12 13 eqeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( ( 𝑘 ( .g ‘ 𝑟 ) 𝑥 ) = ( 0g ‘ 𝑟 ) ↔ ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
15 6 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) → ( .g ‘ 𝑟 ) = ( .g ‘ 𝑅 ) )
16 15 oveqdr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( 𝑙 ( .g ‘ 𝑟 ) 𝑥 ) = ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) )
17 16 13 eqeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( ( 𝑙 ( .g ‘ 𝑟 ) 𝑥 ) = ( 0g ‘ 𝑟 ) ↔ ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
18 10 breq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( 𝑘 ∥ 𝑙 ↔ 𝐾 ∥ 𝑙 ) )
19 17 18 imbi12d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( ( ( 𝑙 ( .g ‘ 𝑟 ) 𝑥 ) = ( 0g ‘ 𝑟 ) → 𝑘 ∥ 𝑙 ) ↔ ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) )
20 19 ralbidv ⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑟 ) 𝑥 ) = ( 0g ‘ 𝑟 ) → 𝑘 ∥ 𝑙 ) ↔ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) )
21 14 20 anbi12d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) ∧ 𝑥 ∈ 𝑏 ) → ( ( ( 𝑘 ( .g ‘ 𝑟 ) 𝑥 ) = ( 0g ‘ 𝑟 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑟 ) 𝑥 ) = ( 0g ‘ 𝑟 ) → 𝑘 ∥ 𝑙 ) ) ↔ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) )
22 21 rabbidva ⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) → { 𝑥 ∈ 𝑏 ∣ ( ( 𝑘 ( .g ‘ 𝑟 ) 𝑥 ) = ( 0g ‘ 𝑟 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑟 ) 𝑥 ) = ( 0g ‘ 𝑟 ) → 𝑘 ∥ 𝑙 ) ) } = { 𝑥 ∈ 𝑏 ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } )
23 7 22 csbeq12dv ⊢ ( ( 𝜑 ∧ ( 𝑟 = 𝑅 ∧ 𝑘 = 𝐾 ) ) → ⦋ ( Base ‘ 𝑟 ) / 𝑏 ⦌ { 𝑥 ∈ 𝑏 ∣ ( ( 𝑘 ( .g ‘ 𝑟 ) 𝑥 ) = ( 0g ‘ 𝑟 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑟 ) 𝑥 ) = ( 0g ‘ 𝑟 ) → 𝑘 ∥ 𝑙 ) ) } = ⦋ ( Base ‘ 𝑅 ) / 𝑏 ⦌ { 𝑥 ∈ 𝑏 ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } )
24 eqid ⊢ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } = { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) }
25 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ V )
26 24 25 rabexd ⊢ ( 𝜑 → { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } ∈ V )
27 simpr ⊢ ( ( 𝜑 ∧ 𝑏 = ( Base ‘ 𝑅 ) ) → 𝑏 = ( Base ‘ 𝑅 ) )
28 27 rabeqdv ⊢ ( ( 𝜑 ∧ 𝑏 = ( Base ‘ 𝑅 ) ) → { 𝑥 ∈ 𝑏 ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } = { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } )
29 25 28 csbied ⊢ ( 𝜑 → ⦋ ( Base ‘ 𝑅 ) / 𝑏 ⦌ { 𝑥 ∈ 𝑏 ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } = { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } )
30 29 eleq1d ⊢ ( 𝜑 → ( ⦋ ( Base ‘ 𝑅 ) / 𝑏 ⦌ { 𝑥 ∈ 𝑏 ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } ∈ V ↔ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } ∈ V ) )
31 26 30 mpbird ⊢ ( 𝜑 → ⦋ ( Base ‘ 𝑅 ) / 𝑏 ⦌ { 𝑥 ∈ 𝑏 ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } ∈ V )
32 5 23 1 2 31 ovmpod ⊢ ( 𝜑 → ( 𝑅 PrimRoots 𝐾 ) = ⦋ ( Base ‘ 𝑅 ) / 𝑏 ⦌ { 𝑥 ∈ 𝑏 ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } )
33 32 29 eqtrd ⊢ ( 𝜑 → ( 𝑅 PrimRoots 𝐾 ) = { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } )
34 33 eleq2d ⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝑅 PrimRoots 𝐾 ) ↔ 𝑀 ∈ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } ) )
35 oveq2 ⊢ ( 𝑥 = 𝑀 → ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) )
36 35 eqeq1d ⊢ ( 𝑥 = 𝑀 → ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ) )
37 oveq2 ⊢ ( 𝑥 = 𝑀 → ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) )
38 37 eqeq1d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ) )
39 38 imbi1d ⊢ ( 𝑥 = 𝑀 → ( ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ↔ ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) )
40 39 ralbidv ⊢ ( 𝑥 = 𝑀 → ( ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ↔ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) )
41 36 40 anbi12d ⊢ ( 𝑥 = 𝑀 → ( ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ↔ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) )
42 41 elrab ⊢ ( 𝑀 ∈ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } ↔ ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) )
43 42 a1i ⊢ ( 𝜑 → ( 𝑀 ∈ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } ↔ ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) ) )
44 3anass ⊢ ( ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ↔ ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) )
45 44 bicomi ⊢ ( ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) ↔ ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) )
46 45 a1i ⊢ ( 𝜑 → ( ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) ↔ ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) )
47 biidd ⊢ ( 𝜑 → ( 𝑀 ∈ ( Base ‘ 𝑅 ) ↔ 𝑀 ∈ ( Base ‘ 𝑅 ) ) )
48 3 eqcomi ⊢ ( .g ‘ 𝑅 ) = ↑
49 48 a1i ⊢ ( 𝜑 → ( .g ‘ 𝑅 ) = ↑ )
50 49 oveqd ⊢ ( 𝜑 → ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 𝐾 ↑ 𝑀 ) )
51 50 eqeq1d ⊢ ( 𝜑 → ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝐾 ↑ 𝑀 ) = ( 0g ‘ 𝑅 ) ) )
52 49 oveqd ⊢ ( 𝜑 → ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 𝑙 ↑ 𝑀 ) )
53 52 eqeq1d ⊢ ( 𝜑 → ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑙 ↑ 𝑀 ) = ( 0g ‘ 𝑅 ) ) )
54 53 imbi1d ⊢ ( 𝜑 → ( ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ↔ ( ( 𝑙 ↑ 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) )
55 54 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ↔ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) )
56 47 51 55 3anbi123d ⊢ ( 𝜑 → ( ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ↔ ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ↑ 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) )
57 46 56 bitrd ⊢ ( 𝜑 → ( ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) ↔ ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ↑ 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) )
58 43 57 bitrd ⊢ ( 𝜑 → ( 𝑀 ∈ { 𝑥 ∈ ( Base ‘ 𝑅 ) ∣ ( ( 𝐾 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) } ↔ ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ↑ 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) )
59 34 58 bitrd ⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝑅 PrimRoots 𝐾 ) ↔ ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ↑ 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) )