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

Metamath Proof Explorer

Theorem gex1

Description: A group or monoid has exponent 1 iff it is trivial. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses gexcl2.1 
|- X = ( Base ` G )
gexcl2.2 
|- E = ( gEx ` G )
Assertion gex1 
|- ( G e. Mnd -> ( E = 1 <-> X ~~ 1o ) )

Proof

Step Hyp Ref Expression
1 gexcl2.1 
 |-  X = ( Base ` G )
2 gexcl2.2 
 |-  E = ( gEx ` G )
3 simplr 
 |-  ( ( ( G e. Mnd /\ E = 1 ) /\ x e. X ) -> E = 1 )
4 3 oveq1d 
 |-  ( ( ( G e. Mnd /\ E = 1 ) /\ x e. X ) -> ( E ( .g ` G ) x ) = ( 1 ( .g ` G ) x ) )
5 eqid 
 |-  ( .g ` G ) = ( .g ` G )
6 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
7 1 2 5 6 gexid 
 |-  ( x e. X -> ( E ( .g ` G ) x ) = ( 0g ` G ) )
8 7 adantl 
 |-  ( ( ( G e. Mnd /\ E = 1 ) /\ x e. X ) -> ( E ( .g ` G ) x ) = ( 0g ` G ) )
9 1 5 mulg1 
 |-  ( x e. X -> ( 1 ( .g ` G ) x ) = x )
10 9 adantl 
 |-  ( ( ( G e. Mnd /\ E = 1 ) /\ x e. X ) -> ( 1 ( .g ` G ) x ) = x )
11 4 8 10 3eqtr3rd 
 |-  ( ( ( G e. Mnd /\ E = 1 ) /\ x e. X ) -> x = ( 0g ` G ) )
12 velsn 
 |-  ( x e. { ( 0g ` G ) } <-> x = ( 0g ` G ) )
13 11 12 sylibr 
 |-  ( ( ( G e. Mnd /\ E = 1 ) /\ x e. X ) -> x e. { ( 0g ` G ) } )
14 13 ex 
 |-  ( ( G e. Mnd /\ E = 1 ) -> ( x e. X -> x e. { ( 0g ` G ) } ) )
15 14 ssrdv 
 |-  ( ( G e. Mnd /\ E = 1 ) -> X C_ { ( 0g ` G ) } )
16 1 6 mndidcl 
 |-  ( G e. Mnd -> ( 0g ` G ) e. X )
17 16 adantr 
 |-  ( ( G e. Mnd /\ E = 1 ) -> ( 0g ` G ) e. X )
18 17 snssd 
 |-  ( ( G e. Mnd /\ E = 1 ) -> { ( 0g ` G ) } C_ X )
19 15 18 eqssd 
 |-  ( ( G e. Mnd /\ E = 1 ) -> X = { ( 0g ` G ) } )
20 fvex 
 |-  ( 0g ` G ) e. _V
21 20 ensn1 
 |-  { ( 0g ` G ) } ~~ 1o
22 19 21 eqbrtrdi 
 |-  ( ( G e. Mnd /\ E = 1 ) -> X ~~ 1o )
23 simpl 
 |-  ( ( G e. Mnd /\ X ~~ 1o ) -> G e. Mnd )
24 1nn 
 |-  1 e. NN
25 24 a1i 
 |-  ( ( G e. Mnd /\ X ~~ 1o ) -> 1 e. NN )
26 9 adantl 
 |-  ( ( ( G e. Mnd /\ X ~~ 1o ) /\ x e. X ) -> ( 1 ( .g ` G ) x ) = x )
27 en1eqsn 
 |-  ( ( ( 0g ` G ) e. X /\ X ~~ 1o ) -> X = { ( 0g ` G ) } )
28 16 27 sylan 
 |-  ( ( G e. Mnd /\ X ~~ 1o ) -> X = { ( 0g ` G ) } )
29 28 eleq2d 
 |-  ( ( G e. Mnd /\ X ~~ 1o ) -> ( x e. X <-> x e. { ( 0g ` G ) } ) )
30 29 biimpa 
 |-  ( ( ( G e. Mnd /\ X ~~ 1o ) /\ x e. X ) -> x e. { ( 0g ` G ) } )
31 30 12 sylib 
 |-  ( ( ( G e. Mnd /\ X ~~ 1o ) /\ x e. X ) -> x = ( 0g ` G ) )
32 26 31 eqtrd 
 |-  ( ( ( G e. Mnd /\ X ~~ 1o ) /\ x e. X ) -> ( 1 ( .g ` G ) x ) = ( 0g ` G ) )
33 32 ralrimiva 
 |-  ( ( G e. Mnd /\ X ~~ 1o ) -> A. x e. X ( 1 ( .g ` G ) x ) = ( 0g ` G ) )
34 1 2 5 6 gexlem2 
 |-  ( ( G e. Mnd /\ 1 e. NN /\ A. x e. X ( 1 ( .g ` G ) x ) = ( 0g ` G ) ) -> E e. ( 1 ... 1 ) )
35 23 25 33 34 syl3anc 
 |-  ( ( G e. Mnd /\ X ~~ 1o ) -> E e. ( 1 ... 1 ) )
36 elfz1eq 
 |-  ( E e. ( 1 ... 1 ) -> E = 1 )
37 35 36 syl 
 |-  ( ( G e. Mnd /\ X ~~ 1o ) -> E = 1 )
38 22 37 impbida 
 |-  ( G e. Mnd -> ( E = 1 <-> X ~~ 1o ) )