Theorem odid

Description: Any element to the power of its order is the identity. (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Stefan O'Rear, 5-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	odid	|- ( A e. X -> ( ( O ` A ) .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		oveq1	|- ( ( O ` A ) = 0 -> ( ( O ` A ) .x. A ) = ( 0 .x. A ) )
6	1 4 3	mulg0	|- ( A e. X -> ( 0 .x. A ) = .0. )
7	5 6	sylan9eqr	|- ( ( A e. X /\ ( O ` A ) = 0 ) -> ( ( O ` A ) .x. A ) = .0. )
8	7	adantrr	|- ( ( A e. X /\ ( ( O ` A ) = 0 /\ { y e. NN | ( y .x. A ) = .0. } = (/) ) ) -> ( ( O ` A ) .x. A ) = .0. )
9		oveq1	|- ( y = ( O ` A ) -> ( y .x. A ) = ( ( O ` A ) .x. A ) )
10	9	eqeq1d	|- ( y = ( O ` A ) -> ( ( y .x. A ) = .0. <-> ( ( O ` A ) .x. A ) = .0. ) )
11	10	elrab	|- ( ( O ` A ) e. { y e. NN | ( y .x. A ) = .0. } <-> ( ( O ` A ) e. NN /\ ( ( O ` A ) .x. A ) = .0. ) )
12	11	simprbi	|- ( ( O ` A ) e. { y e. NN | ( y .x. A ) = .0. } -> ( ( O ` A ) .x. A ) = .0. )
13	12	adantl	|- ( ( A e. X /\ ( O ` A ) e. { y e. NN | ( y .x. A ) = .0. } ) -> ( ( O ` A ) .x. A ) = .0. )
14		eqid	|- { y e. NN | ( y .x. A ) = .0. } = { y e. NN | ( y .x. A ) = .0. }
15	1 3 4 2 14	odlem1	|- ( A e. X -> ( ( ( O ` A ) = 0 /\ { y e. NN | ( y .x. A ) = .0. } = (/) ) \/ ( O ` A ) e. { y e. NN | ( y .x. A ) = .0. } ) )
16	8 13 15	mpjaodan	|- ( A e. X -> ( ( O ` A ) .x. A ) = .0. )