Metamath Proof Explorer

Theorem 0subg

Description: The zero subgroup of an arbitrary group. (Contributed by Stefan O'Rear, 10-Dec-2014)

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 eqid 
 |-  ( Base ` G ) = ( Base ` G )
3 2 1 grpidcl 
 |-  ( G e. Grp -> .0. e. ( Base ` G ) )
4 3 snssd 
 |-  ( G e. Grp -> { .0. } C_ ( Base ` G ) )
5 1 fvexi 
 |-  .0. e. _V
6 5 snnz 
 |-  { .0. } =/= (/)
7 6 a1i 
 |-  ( G e. Grp -> { .0. } =/= (/) )
8 eqid 
 |-  ( +g ` G ) = ( +g ` G )
9 2 8 1 grplid 
 |-  ( ( G e. Grp /\ .0. e. ( Base ` G ) ) -> ( .0. ( +g ` G ) .0. ) = .0. )
10 3 9 mpdan 
 |-  ( G e. Grp -> ( .0. ( +g ` G ) .0. ) = .0. )
11 ovex 
 |-  ( .0. ( +g ` G ) .0. ) e. _V
12 11 elsn 
 |-  ( ( .0. ( +g ` G ) .0. ) e. { .0. } <-> ( .0. ( +g ` G ) .0. ) = .0. )
13 10 12 sylibr 
 |-  ( G e. Grp -> ( .0. ( +g ` G ) .0. ) e. { .0. } )
14 eqid 
 |-  ( invg ` G ) = ( invg ` G )
15 1 14 grpinvid 
 |-  ( G e. Grp -> ( ( invg ` G ) ` .0. ) = .0. )
16 fvex 
 |-  ( ( invg ` G ) ` .0. ) e. _V
17 16 elsn 
 |-  ( ( ( invg ` G ) ` .0. ) e. { .0. } <-> ( ( invg ` G ) ` .0. ) = .0. )
18 15 17 sylibr 
 |-  ( G e. Grp -> ( ( invg ` G ) ` .0. ) e. { .0. } )
19 oveq1 
 |-  ( a = .0. -> ( a ( +g ` G ) b ) = ( .0. ( +g ` G ) b ) )
20 19 eleq1d 
 |-  ( a = .0. -> ( ( a ( +g ` G ) b ) e. { .0. } <-> ( .0. ( +g ` G ) b ) e. { .0. } ) )
21 20 ralbidv 
 |-  ( a = .0. -> ( A. b e. { .0. } ( a ( +g ` G ) b ) e. { .0. } <-> A. b e. { .0. } ( .0. ( +g ` G ) b ) e. { .0. } ) )
22 oveq2 
 |-  ( b = .0. -> ( .0. ( +g ` G ) b ) = ( .0. ( +g ` G ) .0. ) )
23 22 eleq1d 
 |-  ( b = .0. -> ( ( .0. ( +g ` G ) b ) e. { .0. } <-> ( .0. ( +g ` G ) .0. ) e. { .0. } ) )
24 5 23 ralsn 
 |-  ( A. b e. { .0. } ( .0. ( +g ` G ) b ) e. { .0. } <-> ( .0. ( +g ` G ) .0. ) e. { .0. } )
25 21 24 bitrdi 
 |-  ( a = .0. -> ( A. b e. { .0. } ( a ( +g ` G ) b ) e. { .0. } <-> ( .0. ( +g ` G ) .0. ) e. { .0. } ) )
26 fveq2 
 |-  ( a = .0. -> ( ( invg ` G ) ` a ) = ( ( invg ` G ) ` .0. ) )
27 26 eleq1d 
 |-  ( a = .0. -> ( ( ( invg ` G ) ` a ) e. { .0. } <-> ( ( invg ` G ) ` .0. ) e. { .0. } ) )
28 25 27 anbi12d 
 |-  ( a = .0. -> ( ( A. b e. { .0. } ( a ( +g ` G ) b ) e. { .0. } /\ ( ( invg ` G ) ` a ) e. { .0. } ) <-> ( ( .0. ( +g ` G ) .0. ) e. { .0. } /\ ( ( invg ` G ) ` .0. ) e. { .0. } ) ) )
29 5 28 ralsn 
 |-  ( A. a e. { .0. } ( A. b e. { .0. } ( a ( +g ` G ) b ) e. { .0. } /\ ( ( invg ` G ) ` a ) e. { .0. } ) <-> ( ( .0. ( +g ` G ) .0. ) e. { .0. } /\ ( ( invg ` G ) ` .0. ) e. { .0. } ) )
30 13 18 29 sylanbrc 
 |-  ( G e. Grp -> A. a e. { .0. } ( A. b e. { .0. } ( a ( +g ` G ) b ) e. { .0. } /\ ( ( invg ` G ) ` a ) e. { .0. } ) )
31 2 8 14 issubg2 
 |-  ( G e. Grp -> ( { .0. } e. ( SubGrp ` G ) <-> ( { .0. } C_ ( Base ` G ) /\ { .0. } =/= (/) /\ A. a e. { .0. } ( A. b e. { .0. } ( a ( +g ` G ) b ) e. { .0. } /\ ( ( invg ` G ) ` a ) e. { .0. } ) ) ) )
32 4 7 30 31 mpbir3and 
 |-  ( G e. Grp -> { .0. } e. ( SubGrp ` G ) )