Metamath Proof Explorer

Theorem aks6d1c1p7

Description: X is introspective to all positive integers. (Contributed by metakunt, 30-Apr-2025)

Ref Expression
Hypotheses aks6d1c1p7.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 ↑ 𝑦 ) ) ) }
aks6d1c1p7.2 ⊢ 𝑆 = ( Poly1 ‘ 𝐾 )
aks6d1c1p7.3 ⊢ 𝐵 = ( Base ‘ 𝑆 )
aks6d1c1p7.4 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
aks6d1c1p7.5 ⊢ 𝑉 = ( mulGrp ‘ 𝐾 )
aks6d1c1p7.6 ⊢ ↑ = ( .g ‘ 𝑉 )
aks6d1c1p7.7 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks6d1c1p7.8 ⊢ 𝑂 = ( eval1 ‘ 𝐾 )
aks6d1c1p7.9 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks6d1c1p7.10 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c1p7.11 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks6d1c1p7.12 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
aks6d1c1p7.13 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
aks6d1c1p7.14 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
aks6d1c1p7.15 ⊢ ( 𝜑 → 𝐿 ∈ ℕ )
Assertion aks6d1c1p7 ( 𝜑 → 𝐿 ∼ 𝑋 )

Proof

Step Hyp Ref Expression
1 aks6d1c1p7.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 ↑ 𝑦 ) ) ) }
2 aks6d1c1p7.2 ⊢ 𝑆 = ( Poly1 ‘ 𝐾 )
3 aks6d1c1p7.3 ⊢ 𝐵 = ( Base ‘ 𝑆 )
4 aks6d1c1p7.4 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
5 aks6d1c1p7.5 ⊢ 𝑉 = ( mulGrp ‘ 𝐾 )
6 aks6d1c1p7.6 ⊢ ↑ = ( .g ‘ 𝑉 )
7 aks6d1c1p7.7 ⊢ 𝑃 = ( chr ‘ 𝐾 )
8 aks6d1c1p7.8 ⊢ 𝑂 = ( eval1 ‘ 𝐾 )
9 aks6d1c1p7.9 ⊢ ( 𝜑 → 𝐾 ∈ Field )
10 aks6d1c1p7.10 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
11 aks6d1c1p7.11 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
12 aks6d1c1p7.12 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
13 aks6d1c1p7.13 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
14 aks6d1c1p7.14 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
15 aks6d1c1p7.15 ⊢ ( 𝜑 → 𝐿 ∈ ℕ )
16 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17 9 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐾 ∈ CRing )
19 5 crngmgp ⊢ ( 𝐾 ∈ CRing → 𝑉 ∈ CMnd )
20 17 19 syl ⊢ ( 𝜑 → 𝑉 ∈ CMnd )
21 11 nnnn0d ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
22 20 21 6 isprimroot ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ↔ ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑙 ) ) ) )
23 22 biimpd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) → ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑙 ) ) ) )
24 23 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑦 ∈ ( Base ‘ 𝑉 ) ∧ ( 𝑅 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ↑ 𝑦 ) = ( 0g ‘ 𝑉 ) → 𝑅 ∥ 𝑙 ) ) )
25 24 simp1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝑉 ) )
26 5 16 mgpbas ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝑉 )
27 25 26 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
28 8 4 16 2 3 18 27 evl1vard ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑦 ) = 𝑦 ) )
29 28 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑦 ) = 𝑦 )
30 29 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐿 ↑ ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑦 ) ) = ( 𝐿 ↑ 𝑦 ) )
31 20 cmnmndd ⊢ ( 𝜑 → 𝑉 ∈ Mnd )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑉 ∈ Mnd )
33 15 nnnn0d ⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝐿 ∈ ℕ0 )
35 27 26 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → 𝑦 ∈ ( Base ‘ 𝑉 ) )
36 eqid ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
37 36 6 mulgnn0cl ⊢ ( ( 𝑉 ∈ Mnd ∧ 𝐿 ∈ ℕ0 ∧ 𝑦 ∈ ( Base ‘ 𝑉 ) ) → ( 𝐿 ↑ 𝑦 ) ∈ ( Base ‘ 𝑉 ) )
38 32 34 35 37 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐿 ↑ 𝑦 ) ∈ ( Base ‘ 𝑉 ) )
39 38 26 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐿 ↑ 𝑦 ) ∈ ( Base ‘ 𝐾 ) )
40 8 4 16 2 3 18 39 evl1vard ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑋 ) ‘ ( 𝐿 ↑ 𝑦 ) ) = ( 𝐿 ↑ 𝑦 ) ) )
41 40 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( ( 𝑂 ‘ 𝑋 ) ‘ ( 𝐿 ↑ 𝑦 ) ) = ( 𝐿 ↑ 𝑦 ) )
42 eqidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐿 ↑ 𝑦 ) = ( 𝐿 ↑ 𝑦 ) )
43 41 42 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐿 ↑ 𝑦 ) = ( ( 𝑂 ‘ 𝑋 ) ‘ ( 𝐿 ↑ 𝑦 ) ) )
44 30 43 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ) → ( 𝐿 ↑ ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑋 ) ‘ ( 𝐿 ↑ 𝑦 ) ) )
45 44 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐿 ↑ ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑋 ) ‘ ( 𝐿 ↑ 𝑦 ) ) )
46 crngring ⊢ ( 𝐾 ∈ CRing → 𝐾 ∈ Ring )
47 17 46 syl ⊢ ( 𝜑 → 𝐾 ∈ Ring )
48 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
49 4 2 48 vr1cl ⊢ ( 𝐾 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑆 ) )
50 47 49 syl ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑆 ) )
51 50 3 eleqtrrdi ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
52 1 51 15 aks6d1c1p1 ⊢ ( 𝜑 → ( 𝐿 ∼ 𝑋 ↔ ∀ 𝑦 ∈ ( 𝑉 PrimRoots 𝑅 ) ( 𝐿 ↑ ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑋 ) ‘ ( 𝐿 ↑ 𝑦 ) ) ) )
53 45 52 mpbird ⊢ ( 𝜑 → 𝐿 ∼ 𝑋 )