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