Metamath Proof Explorer

Theorem 0cyg

Description: The trivial group is cyclic. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypothesis cygctb.1 
|- B = ( Base ` G )
Assertion 0cyg 
|- ( ( G e. Grp /\ B ~~ 1o ) -> G e. CycGrp )

Proof

Step Hyp Ref Expression
1 cygctb.1 
 |-  B = ( Base ` G )
2 eqid 
 |-  ( .g ` G ) = ( .g ` G )
3 simpl 
 |-  ( ( G e. Grp /\ B ~~ 1o ) -> G e. Grp )
4 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
5 1 4 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. B )
6 5 adantr 
 |-  ( ( G e. Grp /\ B ~~ 1o ) -> ( 0g ` G ) e. B )
7 0z 
 |-  0 e. ZZ
8 en1eqsn 
 |-  ( ( ( 0g ` G ) e. B /\ B ~~ 1o ) -> B = { ( 0g ` G ) } )
9 5 8 sylan 
 |-  ( ( G e. Grp /\ B ~~ 1o ) -> B = { ( 0g ` G ) } )
10 9 eleq2d 
 |-  ( ( G e. Grp /\ B ~~ 1o ) -> ( x e. B <-> x e. { ( 0g ` G ) } ) )
11 10 biimpa 
 |-  ( ( ( G e. Grp /\ B ~~ 1o ) /\ x e. B ) -> x e. { ( 0g ` G ) } )
12 velsn 
 |-  ( x e. { ( 0g ` G ) } <-> x = ( 0g ` G ) )
13 11 12 sylib 
 |-  ( ( ( G e. Grp /\ B ~~ 1o ) /\ x e. B ) -> x = ( 0g ` G ) )
14 1 4 2 mulg0 
 |-  ( ( 0g ` G ) e. B -> ( 0 ( .g ` G ) ( 0g ` G ) ) = ( 0g ` G ) )
15 6 14 syl 
 |-  ( ( G e. Grp /\ B ~~ 1o ) -> ( 0 ( .g ` G ) ( 0g ` G ) ) = ( 0g ` G ) )
16 15 adantr 
 |-  ( ( ( G e. Grp /\ B ~~ 1o ) /\ x e. B ) -> ( 0 ( .g ` G ) ( 0g ` G ) ) = ( 0g ` G ) )
17 13 16 eqtr4d 
 |-  ( ( ( G e. Grp /\ B ~~ 1o ) /\ x e. B ) -> x = ( 0 ( .g ` G ) ( 0g ` G ) ) )
18 oveq1 
 |-  ( n = 0 -> ( n ( .g ` G ) ( 0g ` G ) ) = ( 0 ( .g ` G ) ( 0g ` G ) ) )
19 18 rspceeqv 
 |-  ( ( 0 e. ZZ /\ x = ( 0 ( .g ` G ) ( 0g ` G ) ) ) -> E. n e. ZZ x = ( n ( .g ` G ) ( 0g ` G ) ) )
20 7 17 19 sylancr 
 |-  ( ( ( G e. Grp /\ B ~~ 1o ) /\ x e. B ) -> E. n e. ZZ x = ( n ( .g ` G ) ( 0g ` G ) ) )
21 1 2 3 6 20 iscygd 
 |-  ( ( G e. Grp /\ B ~~ 1o ) -> G e. CycGrp )