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