Theorem odeq

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

	Ref	Expression
Hypotheses	odcl.1	$$⊢X={\mathrm{Base}}_G$$
	odcl.2	$$⊢O=\mathrm{od}\left(G\right)$$
	odid.3	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	odid.4	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	odeq	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\to \left(N=O\left(A\right)\leftrightarrow \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		odcl.1	$$⊢X={\mathrm{Base}}_G$$
2		odcl.2	$$⊢O=\mathrm{od}\left(G\right)$$
3		odid.3	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
4		odid.4	$$⊢\underset{\dot{}}{0}=0_G$$
5		nn0z	$$⊢y\in {\mathbb{N}}_0\to y\in \mathbb{Z}$$
6	1 2 3 4	oddvds	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\wedge y\in \mathbb{Z}\right)\to \left(O\left(A\right)\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
7	5 6	syl3an3	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\wedge y\in {\mathbb{N}}_0\right)\to \left(O\left(A\right)\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
8	7	3expa	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\in X\right)\wedge y\in {\mathbb{N}}_0\right)\to \left(O\left(A\right)\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
9	8	ralrimiva	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to \forall y\in {\mathbb{N}}_0\left(O\left(A\right)\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
10		breq1	$$⊢N=O\left(A\right)\to \left(N\parallel y\leftrightarrow O\left(A\right)\parallel y\right)$$
11	10	bibi1d	$$⊢N=O\left(A\right)\to \left(\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\leftrightarrow \left(O\left(A\right)\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)$$
12	11	ralbidv	$$⊢N=O\left(A\right)\to \left(\forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\leftrightarrow \forall y\in {\mathbb{N}}_0\left(O\left(A\right)\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)$$
13	9 12	syl5ibrcom	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to \left(N=O\left(A\right)\to \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)$$
14	13	3adant3	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\to \left(N=O\left(A\right)\to \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)$$
15		simpl3	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\wedge \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)\to N\in {\mathbb{N}}_0$$
16		simpl2	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\wedge \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)\to A\in X$$
17	1 2	odcl	$$⊢A\in X\to O\left(A\right)\in {\mathbb{N}}_0$$
18	16 17	syl	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\wedge \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)\to O\left(A\right)\in {\mathbb{N}}_0$$
19	1 2 3 4	odid	$$⊢A\in X\to O\left(A\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
20	16 19	syl	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\wedge \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)\to O\left(A\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
21	17	3ad2ant2	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\to O\left(A\right)\in {\mathbb{N}}_0$$
22		breq2	$$⊢y=O\left(A\right)\to \left(N\parallel y\leftrightarrow N\parallel O\left(A\right)\right)$$
23		oveq1	$$⊢y=O\left(A\right)\to y\underset{\dot{}}{·}A=O\left(A\right)\underset{\dot{}}{·}A$$
24	23	eqeq1d	$$⊢y=O\left(A\right)\to \left(y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\leftrightarrow O\left(A\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
25	22 24	bibi12d	$$⊢y=O\left(A\right)\to \left(\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\leftrightarrow \left(N\parallel O\left(A\right)\leftrightarrow O\left(A\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)$$
26	25	rspcva	$$⊢\left(O\left(A\right)\in {\mathbb{N}}_0\wedge \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)\to \left(N\parallel O\left(A\right)\leftrightarrow O\left(A\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
27	21 26	sylan	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\wedge \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)\to \left(N\parallel O\left(A\right)\leftrightarrow O\left(A\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
28	20 27	mpbird	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\wedge \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)\to N\parallel O\left(A\right)$$
29		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
30		iddvds	$$⊢N\in \mathbb{Z}\to N\parallel N$$
31	15 29 30	3syl	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\wedge \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)\to N\parallel N$$
32		breq2	$$⊢y=N\to \left(N\parallel y\leftrightarrow N\parallel N\right)$$
33		oveq1	$$⊢y=N\to y\underset{\dot{}}{·}A=N\underset{\dot{}}{·}A$$
34	33	eqeq1d	$$⊢y=N\to \left(y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\leftrightarrow N\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
35	32 34	bibi12d	$$⊢y=N\to \left(\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\leftrightarrow \left(N\parallel N\leftrightarrow N\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)$$
36	35	rspcva	$$⊢\left(N\in {\mathbb{N}}_0\wedge \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)\to \left(N\parallel N\leftrightarrow N\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
37	36	3ad2antl3	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\wedge \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)\to \left(N\parallel N\leftrightarrow N\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
38	31 37	mpbid	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\wedge \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)\to N\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
39	1 2 3 4	oddvds	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in \mathbb{Z}\right)\to \left(O\left(A\right)\parallel N\leftrightarrow N\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
40	29 39	syl3an3	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\to \left(O\left(A\right)\parallel N\leftrightarrow N\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
41	40	adantr	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\wedge \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)\to \left(O\left(A\right)\parallel N\leftrightarrow N\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
42	38 41	mpbird	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\wedge \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)\to O\left(A\right)\parallel N$$
43		dvdseq	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge O\left(A\right)\in {\mathbb{N}}_0\right)\wedge \left(N\parallel O\left(A\right)\wedge O\left(A\right)\parallel N\right)\right)\to N=O\left(A\right)$$
44	15 18 28 42 43	syl22anc	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\wedge \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)\to N=O\left(A\right)$$
45	44	ex	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\to \left(\forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\to N=O\left(A\right)\right)$$
46	14 45	impbid	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in {\mathbb{N}}_0\right)\to \left(N=O\left(A\right)\leftrightarrow \forall y\in {\mathbb{N}}_0\left(N\parallel y\leftrightarrow y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)\right)$$