Metamath Proof Explorer

Theorem 0subg

Description: The zero subgroup of an arbitrary group. (Contributed by Stefan O'Rear, 10-Dec-2014) (Proof shortened by SN, 31-Jan-2025)

Ref Expression
Hypothesis 0subg.z 
|- .0. = ( 0g ` G )
Assertion 0subg 
|- ( G e. Grp -> { .0. } e. ( SubGrp ` G ) )

Proof

Step Hyp Ref Expression
1 0subg.z 
 |-  .0. = ( 0g ` G )
2 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
3 1 0subm 
 |-  ( G e. Mnd -> { .0. } e. ( SubMnd ` G ) )
4 2 3 syl 
 |-  ( G e. Grp -> { .0. } e. ( SubMnd ` G ) )
5 eqid 
 |-  ( invg ` G ) = ( invg ` G )
6 1 5 grpinvid 
 |-  ( G e. Grp -> ( ( invg ` G ) ` .0. ) = .0. )
7 fvex 
 |-  ( ( invg ` G ) ` .0. ) e. _V
8 7 elsn 
 |-  ( ( ( invg ` G ) ` .0. ) e. { .0. } <-> ( ( invg ` G ) ` .0. ) = .0. )
9 6 8 sylibr 
 |-  ( G e. Grp -> ( ( invg ` G ) ` .0. ) e. { .0. } )
10 1 fvexi 
 |-  .0. e. _V
11 fveq2 
 |-  ( a = .0. -> ( ( invg ` G ) ` a ) = ( ( invg ` G ) ` .0. ) )
12 11 eleq1d 
 |-  ( a = .0. -> ( ( ( invg ` G ) ` a ) e. { .0. } <-> ( ( invg ` G ) ` .0. ) e. { .0. } ) )
13 10 12 ralsn 
 |-  ( A. a e. { .0. } ( ( invg ` G ) ` a ) e. { .0. } <-> ( ( invg ` G ) ` .0. ) e. { .0. } )
14 9 13 sylibr 
 |-  ( G e. Grp -> A. a e. { .0. } ( ( invg ` G ) ` a ) e. { .0. } )
15 5 issubg3 
 |-  ( G e. Grp -> ( { .0. } e. ( SubGrp ` G ) <-> ( { .0. } e. ( SubMnd ` G ) /\ A. a e. { .0. } ( ( invg ` G ) ` a ) e. { .0. } ) ) )
16 4 14 15 mpbir2and 
 |-  ( G e. Grp -> { .0. } e. ( SubGrp ` G ) )