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

Metamath Proof Explorer

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