odcl2

Description: The order of an element of a finite group is finite. (Contributed by Mario Carneiro, 14-Jan-2015)

	Ref	Expression
Hypotheses	odcl2.1	\|- X = ( Base ` G )
	odcl2.2	\|- O = ( od ` G )
Assertion	odcl2	\|- ( ( G e. Grp /\ X e. Fin /\ A e. X ) -> ( O ` A ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		odcl2.1	\|- X = ( Base ` G )
2		odcl2.2	\|- O = ( od ` G )
3	1 2	odcl	\|- ( A e. X -> ( O ` A ) e. NN0 )
4	3	adantl	\|- ( ( G e. Grp /\ A e. X ) -> ( O ` A ) e. NN0 )
5		elnn0	\|- ( ( O ` A ) e. NN0 <-> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
6	4 5	sylib	\|- ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
7	6	ord	\|- ( ( G e. Grp /\ A e. X ) -> ( -. ( O ` A ) e. NN -> ( O ` A ) = 0 ) )
8		eqid	\|- ( .g ` G ) = ( .g ` G )
9		eqid	\|- ( x e. ZZ \|-> ( x ( .g ` G ) A ) ) = ( x e. ZZ \|-> ( x ( .g ` G ) A ) )
10	1 2 8 9	odinf	\|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> -. ran ( x e. ZZ \|-> ( x ( .g ` G ) A ) ) e. Fin )
11	1 2 8 9	odf1	\|- ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) = 0 <-> ( x e. ZZ \|-> ( x ( .g ` G ) A ) ) : ZZ -1-1-> X ) )
12	11	biimp3a	\|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( x e. ZZ \|-> ( x ( .g ` G ) A ) ) : ZZ -1-1-> X )
13		f1f	\|- ( ( x e. ZZ \|-> ( x ( .g ` G ) A ) ) : ZZ -1-1-> X -> ( x e. ZZ \|-> ( x ( .g ` G ) A ) ) : ZZ --> X )
14		frn	\|- ( ( x e. ZZ \|-> ( x ( .g ` G ) A ) ) : ZZ --> X -> ran ( x e. ZZ \|-> ( x ( .g ` G ) A ) ) C_ X )
15		ssfi	\|- ( ( X e. Fin /\ ran ( x e. ZZ \|-> ( x ( .g ` G ) A ) ) C_ X ) -> ran ( x e. ZZ \|-> ( x ( .g ` G ) A ) ) e. Fin )
16	15	expcom	\|- ( ran ( x e. ZZ \|-> ( x ( .g ` G ) A ) ) C_ X -> ( X e. Fin -> ran ( x e. ZZ \|-> ( x ( .g ` G ) A ) ) e. Fin ) )
17	12 13 14 16	4syl	\|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> ( X e. Fin -> ran ( x e. ZZ \|-> ( x ( .g ` G ) A ) ) e. Fin ) )
18	10 17	mtod	\|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) = 0 ) -> -. X e. Fin )
19	18	3expia	\|- ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) = 0 -> -. X e. Fin ) )
20	7 19	syld	\|- ( ( G e. Grp /\ A e. X ) -> ( -. ( O ` A ) e. NN -> -. X e. Fin ) )
21	20	con4d	\|- ( ( G e. Grp /\ A e. X ) -> ( X e. Fin -> ( O ` A ) e. NN ) )
22	21	3impia	\|- ( ( G e. Grp /\ A e. X /\ X e. Fin ) -> ( O ` A ) e. NN )
23	22	3com23	\|- ( ( G e. Grp /\ X e. Fin /\ A e. X ) -> ( O ` A ) e. NN )

Metamath Proof Explorer

Theorem odcl2

Proof