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

Metamath Proof Explorer

Theorem gexid

Description: Any element to the power of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses gexcl.1 
|- X = ( Base ` G )
gexcl.2 
|- E = ( gEx ` G )
gexid.3 
|- .x. = ( .g ` G )
gexid.4 
|- .0. = ( 0g ` G )
Assertion gexid 
|- ( A e. X -> ( E .x. A ) = .0. )

Proof

Step Hyp Ref Expression
1 gexcl.1 
 |-  X = ( Base ` G )
2 gexcl.2 
 |-  E = ( gEx ` G )
3 gexid.3 
 |-  .x. = ( .g ` G )
4 gexid.4 
 |-  .0. = ( 0g ` G )
5 oveq1 
 |-  ( E = 0 -> ( E .x. A ) = ( 0 .x. A ) )
6 1 4 3 mulg0 
 |-  ( A e. X -> ( 0 .x. A ) = .0. )
7 5 6 sylan9eqr 
 |-  ( ( A e. X /\ E = 0 ) -> ( E .x. A ) = .0. )
8 7 adantrr 
 |-  ( ( A e. X /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> ( E .x. A ) = .0. )
9 oveq1 
 |-  ( y = E -> ( y .x. x ) = ( E .x. x ) )
10 9 eqeq1d 
 |-  ( y = E -> ( ( y .x. x ) = .0. <-> ( E .x. x ) = .0. ) )
11 10 ralbidv 
 |-  ( y = E -> ( A. x e. X ( y .x. x ) = .0. <-> A. x e. X ( E .x. x ) = .0. ) )
12 11 elrab 
 |-  ( E e. { y e. NN | A. x e. X ( y .x. x ) = .0. } <-> ( E e. NN /\ A. x e. X ( E .x. x ) = .0. ) )
13 12 simprbi 
 |-  ( E e. { y e. NN | A. x e. X ( y .x. x ) = .0. } -> A. x e. X ( E .x. x ) = .0. )
14 oveq2 
 |-  ( x = A -> ( E .x. x ) = ( E .x. A ) )
15 14 eqeq1d 
 |-  ( x = A -> ( ( E .x. x ) = .0. <-> ( E .x. A ) = .0. ) )
16 15 rspcva 
 |-  ( ( A e. X /\ A. x e. X ( E .x. x ) = .0. ) -> ( E .x. A ) = .0. )
17 13 16 sylan2 
 |-  ( ( A e. X /\ E e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> ( E .x. A ) = .0. )
18 elfvex 
 |-  ( A e. ( Base ` G ) -> G e. _V )
19 18 1 eleq2s 
 |-  ( A e. X -> G e. _V )
20 eqid 
 |-  { y e. NN | A. x e. X ( y .x. x ) = .0. } = { y e. NN | A. x e. X ( y .x. x ) = .0. }
21 1 3 4 2 20 gexlem1 
 |-  ( G e. _V -> ( ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) \/ E e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) )
22 19 21 syl 
 |-  ( A e. X -> ( ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) \/ E e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) )
23 8 17 22 mpjaodan 
 |-  ( A e. X -> ( E .x. A ) = .0. )