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 
|- X = ( Base ` G )
odcl.2 
|- O = ( od ` G )
odid.3 
|- .x. = ( .g ` G )
odid.4 
|- .0. = ( 0g ` G )
Assertion odeq 
|- ( ( G e. Grp /\ A e. X /\ N e. NN0 ) -> ( N = ( O ` A ) <-> A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) )

Proof

Step Hyp Ref Expression
1 odcl.1 
 |-  X = ( Base ` G )
2 odcl.2 
 |-  O = ( od ` G )
3 odid.3 
 |-  .x. = ( .g ` G )
4 odid.4 
 |-  .0. = ( 0g ` G )
5 nn0z 
 |-  ( y e. NN0 -> y e. ZZ )
6 1 2 3 4 oddvds 
 |-  ( ( G e. Grp /\ A e. X /\ y e. ZZ ) -> ( ( O ` A ) || y <-> ( y .x. A ) = .0. ) )
7 5 6 syl3an3 
 |-  ( ( G e. Grp /\ A e. X /\ y e. NN0 ) -> ( ( O ` A ) || y <-> ( y .x. A ) = .0. ) )
8 7 3expa 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ y e. NN0 ) -> ( ( O ` A ) || y <-> ( y .x. A ) = .0. ) )
9 8 ralrimiva 
 |-  ( ( G e. Grp /\ A e. X ) -> A. y e. NN0 ( ( O ` A ) || y <-> ( y .x. A ) = .0. ) )
10 breq1 
 |-  ( N = ( O ` A ) -> ( N || y <-> ( O ` A ) || y ) )
11 10 bibi1d 
 |-  ( N = ( O ` A ) -> ( ( N || y <-> ( y .x. A ) = .0. ) <-> ( ( O ` A ) || y <-> ( y .x. A ) = .0. ) ) )
12 11 ralbidv 
 |-  ( N = ( O ` A ) -> ( A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) <-> A. y e. NN0 ( ( O ` A ) || y <-> ( y .x. A ) = .0. ) ) )
13 9 12 syl5ibrcom 
 |-  ( ( G e. Grp /\ A e. X ) -> ( N = ( O ` A ) -> A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) )
14 13 3adant3 
 |-  ( ( G e. Grp /\ A e. X /\ N e. NN0 ) -> ( N = ( O ` A ) -> A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) )
15 simpl3 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. NN0 ) /\ A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) -> N e. NN0 )
16 simpl2 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. NN0 ) /\ A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) -> A e. X )
17 1 2 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
18 16 17 syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. NN0 ) /\ A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) -> ( O ` A ) e. NN0 )
19 1 2 3 4 odid 
 |-  ( A e. X -> ( ( O ` A ) .x. A ) = .0. )
20 16 19 syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. NN0 ) /\ A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) -> ( ( O ` A ) .x. A ) = .0. )
21 17 3ad2ant2 
 |-  ( ( G e. Grp /\ A e. X /\ N e. NN0 ) -> ( O ` A ) e. NN0 )
22 breq2 
 |-  ( y = ( O ` A ) -> ( N || y <-> N || ( O ` A ) ) )
23 oveq1 
 |-  ( y = ( O ` A ) -> ( y .x. A ) = ( ( O ` A ) .x. A ) )
24 23 eqeq1d 
 |-  ( y = ( O ` A ) -> ( ( y .x. A ) = .0. <-> ( ( O ` A ) .x. A ) = .0. ) )
25 22 24 bibi12d 
 |-  ( y = ( O ` A ) -> ( ( N || y <-> ( y .x. A ) = .0. ) <-> ( N || ( O ` A ) <-> ( ( O ` A ) .x. A ) = .0. ) ) )
26 25 rspcva 
 |-  ( ( ( O ` A ) e. NN0 /\ A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) -> ( N || ( O ` A ) <-> ( ( O ` A ) .x. A ) = .0. ) )
27 21 26 sylan 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. NN0 ) /\ A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) -> ( N || ( O ` A ) <-> ( ( O ` A ) .x. A ) = .0. ) )
28 20 27 mpbird 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. NN0 ) /\ A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) -> N || ( O ` A ) )
29 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
30 iddvds 
 |-  ( N e. ZZ -> N || N )
31 15 29 30 3syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. NN0 ) /\ A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) -> N || N )
32 breq2 
 |-  ( y = N -> ( N || y <-> N || N ) )
33 oveq1 
 |-  ( y = N -> ( y .x. A ) = ( N .x. A ) )
34 33 eqeq1d 
 |-  ( y = N -> ( ( y .x. A ) = .0. <-> ( N .x. A ) = .0. ) )
35 32 34 bibi12d 
 |-  ( y = N -> ( ( N || y <-> ( y .x. A ) = .0. ) <-> ( N || N <-> ( N .x. A ) = .0. ) ) )
36 35 rspcva 
 |-  ( ( N e. NN0 /\ A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) -> ( N || N <-> ( N .x. A ) = .0. ) )
37 36 3ad2antl3 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. NN0 ) /\ A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) -> ( N || N <-> ( N .x. A ) = .0. ) )
38 31 37 mpbid 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. NN0 ) /\ A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) -> ( N .x. A ) = .0. )
39 1 2 3 4 oddvds 
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) )
40 29 39 syl3an3 
 |-  ( ( G e. Grp /\ A e. X /\ N e. NN0 ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) )
41 40 adantr 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. NN0 ) /\ A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) )
42 38 41 mpbird 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. NN0 ) /\ A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) -> ( O ` A ) || N )
43 dvdseq 
 |-  ( ( ( N e. NN0 /\ ( O ` A ) e. NN0 ) /\ ( N || ( O ` A ) /\ ( O ` A ) || N ) ) -> N = ( O ` A ) )
44 15 18 28 42 43 syl22anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. NN0 ) /\ A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) -> N = ( O ` A ) )
45 44 ex 
 |-  ( ( G e. Grp /\ A e. X /\ N e. NN0 ) -> ( A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) -> N = ( O ` A ) ) )
46 14 45 impbid 
 |-  ( ( G e. Grp /\ A e. X /\ N e. NN0 ) -> ( N = ( O ` A ) <-> A. y e. NN0 ( N || y <-> ( y .x. A ) = .0. ) ) )