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

Metamath Proof Explorer

Theorem eqg0subgecsn

Description: The equivalence classes modulo the coset equivalence relation for the trivial (zero) subgroup of a group are singletons. (Contributed by AV, 26-Feb-2025)

Ref Expression
Hypotheses eqg0subg.0 
|- .0. = ( 0g ` G )
eqg0subg.s 
|- S = { .0. }
eqg0subg.b 
|- B = ( Base ` G )
eqg0subg.r 
|- R = ( G ~QG S )
Assertion eqg0subgecsn 
|- ( ( G e. Grp /\ X e. B ) -> [ X ] R = { X } )

Proof

Step Hyp Ref Expression
1 eqg0subg.0 
 |-  .0. = ( 0g ` G )
2 eqg0subg.s 
 |-  S = { .0. }
3 eqg0subg.b 
 |-  B = ( Base ` G )
4 eqg0subg.r 
 |-  R = ( G ~QG S )
5 df-ec 
 |-  [ X ] R = ( R " { X } )
6 1 2 3 4 eqg0subg 
 |-  ( G e. Grp -> R = ( _I |` B ) )
7 6 adantr 
 |-  ( ( G e. Grp /\ X e. B ) -> R = ( _I |` B ) )
8 7 imaeq1d 
 |-  ( ( G e. Grp /\ X e. B ) -> ( R " { X } ) = ( ( _I |` B ) " { X } ) )
9 snssi 
 |-  ( X e. B -> { X } C_ B )
10 9 adantl 
 |-  ( ( G e. Grp /\ X e. B ) -> { X } C_ B )
11 resima2 
 |-  ( { X } C_ B -> ( ( _I |` B ) " { X } ) = ( _I " { X } ) )
12 10 11 syl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( _I |` B ) " { X } ) = ( _I " { X } ) )
13 imai 
 |-  ( _I " { X } ) = { X }
14 12 13 eqtrdi 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( _I |` B ) " { X } ) = { X } )
15 8 14 eqtrd 
 |-  ( ( G e. Grp /\ X e. B ) -> ( R " { X } ) = { X } )
16 5 15 eqtrid 
 |-  ( ( G e. Grp /\ X e. B ) -> [ X ] R = { X } )