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 ) ) )