Metamath Proof Explorer

Theorem odeq

Description: The oddvds property uniquely defines the group order. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses odcl.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
odid.3 ⊢ · = ( .g ‘ 𝐺 )
odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion odeq ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 = ( 𝑂 ‘ 𝐴 ) ↔ ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 odcl.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odid.3 ⊢ · = ( .g ‘ 𝐺 )
4 odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
5 nn0z ⊢ ( 𝑦 ∈ ℕ0 → 𝑦 ∈ ℤ )
6 1 2 3 4 oddvds ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) )
7 5 6 syl3an3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) )
8 7 3expa ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) )
9 8 ralrimiva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ∀ 𝑦 ∈ ℕ0 ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) )
10 breq1 ⊢ ( 𝑁 = ( 𝑂 ‘ 𝐴 ) → ( 𝑁 ∥ 𝑦 ↔ ( 𝑂 ‘ 𝐴 ) ∥ 𝑦 ) )
11 10 bibi1d ⊢ ( 𝑁 = ( 𝑂 ‘ 𝐴 ) → ( ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ↔ ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) )
12 11 ralbidv ⊢ ( 𝑁 = ( 𝑂 ‘ 𝐴 ) → ( ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ↔ ∀ 𝑦 ∈ ℕ0 ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) )
13 9 12 syl5ibrcom ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 = ( 𝑂 ‘ 𝐴 ) → ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) )
14 13 3adant3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 = ( 𝑂 ‘ 𝐴 ) → ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) )
15 simpl3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) → 𝑁 ∈ ℕ0 )
16 simpl2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) → 𝐴 ∈ 𝑋 )
17 1 2 odcl ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
18 16 17 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
19 1 2 3 4 odid ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 )
20 16 19 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 )
21 17 3ad2ant2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
22 breq2 ⊢ ( 𝑦 = ( 𝑂 ‘ 𝐴 ) → ( 𝑁 ∥ 𝑦 ↔ 𝑁 ∥ ( 𝑂 ‘ 𝐴 ) ) )
23 oveq1 ⊢ ( 𝑦 = ( 𝑂 ‘ 𝐴 ) → ( 𝑦 · 𝐴 ) = ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) )
24 23 eqeq1d ⊢ ( 𝑦 = ( 𝑂 ‘ 𝐴 ) → ( ( 𝑦 · 𝐴 ) = 0 ↔ ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 ) )
25 22 24 bibi12d ⊢ ( 𝑦 = ( 𝑂 ‘ 𝐴 ) → ( ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ↔ ( 𝑁 ∥ ( 𝑂 ‘ 𝐴 ) ↔ ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 ) ) )
26 25 rspcva ⊢ ( ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 ∧ ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) → ( 𝑁 ∥ ( 𝑂 ‘ 𝐴 ) ↔ ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 ) )
27 21 26 sylan ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) → ( 𝑁 ∥ ( 𝑂 ‘ 𝐴 ) ↔ ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 ) )
28 20 27 mpbird ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) → 𝑁 ∥ ( 𝑂 ‘ 𝐴 ) )
29 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
30 iddvds ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∥ 𝑁 )
31 15 29 30 3syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) → 𝑁 ∥ 𝑁 )
32 breq2 ⊢ ( 𝑦 = 𝑁 → ( 𝑁 ∥ 𝑦 ↔ 𝑁 ∥ 𝑁 ) )
33 oveq1 ⊢ ( 𝑦 = 𝑁 → ( 𝑦 · 𝐴 ) = ( 𝑁 · 𝐴 ) )
34 33 eqeq1d ⊢ ( 𝑦 = 𝑁 → ( ( 𝑦 · 𝐴 ) = 0 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
35 32 34 bibi12d ⊢ ( 𝑦 = 𝑁 → ( ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ↔ ( 𝑁 ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) ) )
36 35 rspcva ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) → ( 𝑁 ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
37 36 3ad2antl3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) → ( 𝑁 ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
38 31 37 mpbid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) → ( 𝑁 · 𝐴 ) = 0 )
39 1 2 3 4 oddvds ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
40 29 39 syl3an3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
41 40 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
42 38 41 mpbird ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) → ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 )
43 dvdseq ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 ) ∧ ( 𝑁 ∥ ( 𝑂 ‘ 𝐴 ) ∧ ( 𝑂 ‘ 𝐴 ) ∥ 𝑁 ) ) → 𝑁 = ( 𝑂 ‘ 𝐴 ) )
44 15 18 28 42 43 syl22anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) → 𝑁 = ( 𝑂 ‘ 𝐴 ) )
45 44 ex ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) → 𝑁 = ( 𝑂 ‘ 𝐴 ) ) )
46 14 45 impbid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 = ( 𝑂 ‘ 𝐴 ) ↔ ∀ 𝑦 ∈ ℕ0 ( 𝑁 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) )