Metamath Proof Explorer

Theorem aks6d1c1p1

Description: Definition of the introspective relation. (Contributed by metakunt, 25-Apr-2025)

Ref Expression
Hypotheses aks6d1c1p1.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 𝐷 𝑦 ) ) ) }
aks6d1c1p1.2 ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
aks6d1c1p1.3 ⊢ ( 𝜑 → 𝐸 ∈ ℕ )
Assertion aks6d1c1p1 ( 𝜑 → ( 𝐸 ∼ 𝐹 ↔ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1c1p1.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 𝐷 𝑦 ) ) ) }
2 aks6d1c1p1.2 ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
3 aks6d1c1p1.3 ⊢ ( 𝜑 → 𝐸 ∈ ℕ )
4 simpl ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → 𝑒 = 𝐸 )
5 4 eleq1d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 ∈ ℕ ↔ 𝐸 ∈ ℕ ) )
6 simpr ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
7 6 eleq1d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑓 ∈ 𝐵 ↔ 𝐹 ∈ 𝐵 ) )
8 6 fveq2d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑂 ‘ 𝑓 ) = ( 𝑂 ‘ 𝐹 ) )
9 8 fveq1d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) = ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) )
10 4 9 oveq12d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) )
11 4 oveq1d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( 𝑒 𝐷 𝑦 ) = ( 𝐸 𝐷 𝑦 ) )
12 8 11 fveq12d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 𝐷 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) )
13 10 12 eqeq12d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 𝐷 𝑦 ) ) ↔ ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) )
14 13 ralbidv ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 𝐷 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) )
15 5 7 14 3anbi123d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝑒 ↑ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝑓 ) ‘ ( 𝑒 𝐷 𝑦 ) ) ) ↔ ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) ) )
16 15 1 brabga ⊢ ( ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) → ( 𝐸 ∼ 𝐹 ↔ ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) ) )
17 3 2 16 syl2anc ⊢ ( 𝜑 → ( 𝐸 ∼ 𝐹 ↔ ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) ) )
18 17 biimpd ⊢ ( 𝜑 → ( 𝐸 ∼ 𝐹 → ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) ) )
19 18 imp ⊢ ( ( 𝜑 ∧ 𝐸 ∼ 𝐹 ) → ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) )
20 19 simp3d ⊢ ( ( 𝜑 ∧ 𝐸 ∼ 𝐹 ) → ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) )
21 20 ex ⊢ ( 𝜑 → ( 𝐸 ∼ 𝐹 → ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) )
22 3 2 jca ⊢ ( 𝜑 → ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) )
23 df-3an ⊢ ( ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) ↔ ( ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) )
24 23 bicomi ⊢ ( ( ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) ↔ ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) )
25 24 a1i ⊢ ( 𝜑 → ( ( ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) ↔ ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) ) )
26 17 biimprd ⊢ ( 𝜑 → ( ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) → 𝐸 ∼ 𝐹 ) )
27 25 26 sylbid ⊢ ( 𝜑 → ( ( ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) → 𝐸 ∼ 𝐹 ) )
28 27 imp ⊢ ( ( 𝜑 ∧ ( ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) ) → 𝐸 ∼ 𝐹 )
29 28 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) ) ∧ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) → 𝐸 ∼ 𝐹 )
30 29 ex ⊢ ( ( 𝜑 ∧ ( 𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵 ) ) → ( ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) → 𝐸 ∼ 𝐹 ) )
31 22 30 mpdan ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) → 𝐸 ∼ 𝐹 ) )
32 21 31 impbid ⊢ ( 𝜑 → ( 𝐸 ∼ 𝐹 ↔ ∀ 𝑦 ∈ ( 𝐾 PrimRoots 𝑅 ) ( 𝐸 ↑ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑂 ‘ 𝐹 ) ‘ ( 𝐸 𝐷 𝑦 ) ) ) )