Metamath Proof Explorer

Theorem odval2

Description: A non-conditional definition of 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 odval2 
|- ( ( G e. Grp /\ A e. X ) -> ( O ` A ) = ( iota_ x e. NN0 A. y e. NN0 ( x || 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 1 2 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
6 5 adantl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( O ` A ) e. NN0 )
7 1 2 3 4 odeq 
 |-  ( ( G e. Grp /\ A e. X /\ x e. NN0 ) -> ( x = ( O ` A ) <-> A. y e. NN0 ( x || y <-> ( y .x. A ) = .0. ) ) )
8 7 3expa 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ x e. NN0 ) -> ( x = ( O ` A ) <-> A. y e. NN0 ( x || y <-> ( y .x. A ) = .0. ) ) )
9 8 bicomd 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ x e. NN0 ) -> ( A. y e. NN0 ( x || y <-> ( y .x. A ) = .0. ) <-> x = ( O ` A ) ) )
10 6 9 riota5 
 |-  ( ( G e. Grp /\ A e. X ) -> ( iota_ x e. NN0 A. y e. NN0 ( x || y <-> ( y .x. A ) = .0. ) ) = ( O ` A ) )
11 10 eqcomd 
 |-  ( ( G e. Grp /\ A e. X ) -> ( O ` A ) = ( iota_ x e. NN0 A. y e. NN0 ( x || y <-> ( y .x. A ) = .0. ) ) )