This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem odhash3

Description: An element which generates a finite subgroup has order the size of that subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Hypotheses odhash.x 
|- X = ( Base ` G )
odhash.o 
|- O = ( od ` G )
odhash.k 
|- K = ( mrCls ` ( SubGrp ` G ) )
Assertion odhash3 
|- ( ( G e. Grp /\ A e. X /\ ( K ` { A } ) e. Fin ) -> ( O ` A ) = ( # ` ( K ` { A } ) ) )

Proof

Step Hyp Ref Expression
1 odhash.x 
 |-  X = ( Base ` G )
2 odhash.o 
 |-  O = ( od ` G )
3 odhash.k 
 |-  K = ( mrCls ` ( SubGrp ` G ) )
4 1 2 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
5 4 3ad2ant2 
 |-  ( ( G e. Grp /\ A e. X /\ ( K ` { A } ) e. Fin ) -> ( O ` A ) e. NN0 )
6 hashcl 
 |-  ( ( K ` { A } ) e. Fin -> ( # ` ( K ` { A } ) ) e. NN0 )
7 6 nn0red 
 |-  ( ( K ` { A } ) e. Fin -> ( # ` ( K ` { A } ) ) e. RR )
8 pnfnre 
 |-  +oo e/ RR
9 8 neli 
 |-  -. +oo e. RR
10 1 2 3 odhash 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( # ` ( K ` { A } ) ) = +oo )
11 10 eleq1d 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( ( # ` ( K ` { A } ) ) e. RR <-> +oo e. RR ) )
12 9 11 mtbiri 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> -. ( # ` ( K ` { A } ) ) e. RR )
13 12 3expia 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) = 0 -> -. ( # ` ( K ` { A } ) ) e. RR ) )
14 13 necon2ad 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( # ` ( K ` { A } ) ) e. RR -> ( O ` A ) =/= 0 ) )
15 7 14 syl5 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( K ` { A } ) e. Fin -> ( O ` A ) =/= 0 ) )
16 15 3impia 
 |-  ( ( G e. Grp /\ A e. X /\ ( K ` { A } ) e. Fin ) -> ( O ` A ) =/= 0 )
17 elnnne0 
 |-  ( ( O ` A ) e. NN <-> ( ( O ` A ) e. NN0 /\ ( O ` A ) =/= 0 ) )
18 5 16 17 sylanbrc 
 |-  ( ( G e. Grp /\ A e. X /\ ( K ` { A } ) e. Fin ) -> ( O ` A ) e. NN )
19 1 2 3 odhash2 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> ( # ` ( K ` { A } ) ) = ( O ` A ) )
20 18 19 syld3an3 
 |-  ( ( G e. Grp /\ A e. X /\ ( K ` { A } ) e. Fin ) -> ( # ` ( K ` { A } ) ) = ( O ` A ) )
21 20 eqcomd 
 |-  ( ( G e. Grp /\ A e. X /\ ( K ` { A } ) e. Fin ) -> ( O ` A ) = ( # ` ( K ` { A } ) ) )