Metamath Proof Explorer

Theorem eqg0subg

Description: The coset equivalence relation for the trivial (zero) subgroup of a group is the identity relation restricted to the base set of the group. (Contributed by AV, 25-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 eqg0subg 
|- ( G e. Grp -> R = ( _I |` B ) )

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 1 0subg 
 |-  ( G e. Grp -> { .0. } e. ( SubGrp ` G ) )
6 3 subgss 
 |-  ( { .0. } e. ( SubGrp ` G ) -> { .0. } C_ B )
7 5 6 syl 
 |-  ( G e. Grp -> { .0. } C_ B )
8 2 7 eqsstrid 
 |-  ( G e. Grp -> S C_ B )
9 eqid 
 |-  ( invg ` G ) = ( invg ` G )
10 eqid 
 |-  ( +g ` G ) = ( +g ` G )
11 3 9 10 4 eqgfval 
 |-  ( ( G e. Grp /\ S C_ B ) -> R = { <. x , y >. | ( { x , y } C_ B /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. S ) } )
12 8 11 mpdan 
 |-  ( G e. Grp -> R = { <. x , y >. | ( { x , y } C_ B /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. S ) } )
13 opabresid 
 |-  ( _I |` B ) = { <. x , y >. | ( x e. B /\ y = x ) }
14 simpl 
 |-  ( ( x e. B /\ y = x ) -> x e. B )
15 eleq1w 
 |-  ( x = y -> ( x e. B <-> y e. B ) )
16 15 equcoms 
 |-  ( y = x -> ( x e. B <-> y e. B ) )
17 16 biimpac 
 |-  ( ( x e. B /\ y = x ) -> y e. B )
18 simpr 
 |-  ( ( x e. B /\ y = x ) -> y = x )
19 14 17 18 jca31 
 |-  ( ( x e. B /\ y = x ) -> ( ( x e. B /\ y e. B ) /\ y = x ) )
20 simpl 
 |-  ( ( x e. B /\ y e. B ) -> x e. B )
21 20 anim1i 
 |-  ( ( ( x e. B /\ y e. B ) /\ y = x ) -> ( x e. B /\ y = x ) )
22 21 a1i 
 |-  ( G e. Grp -> ( ( ( x e. B /\ y e. B ) /\ y = x ) -> ( x e. B /\ y = x ) ) )
23 19 22 impbid2 
 |-  ( G e. Grp -> ( ( x e. B /\ y = x ) <-> ( ( x e. B /\ y e. B ) /\ y = x ) ) )
24 simpl 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> G e. Grp )
25 simpr 
 |-  ( ( x e. B /\ y e. B ) -> y e. B )
26 25 adantl 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> y e. B )
27 20 adantl 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> x e. B )
28 3 9 24 26 27 grpinv11 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( ( invg ` G ) ` y ) = ( ( invg ` G ) ` x ) <-> y = x ) )
29 3 9 grpinvcl 
 |-  ( ( G e. Grp /\ x e. B ) -> ( ( invg ` G ) ` x ) e. B )
30 29 adantrr 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( invg ` G ) ` x ) e. B )
31 3 10 1 9 grpinvid2 
 |-  ( ( G e. Grp /\ y e. B /\ ( ( invg ` G ) ` x ) e. B ) -> ( ( ( invg ` G ) ` y ) = ( ( invg ` G ) ` x ) <-> ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) = .0. ) )
32 24 26 30 31 syl3anc 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( ( invg ` G ) ` y ) = ( ( invg ` G ) ` x ) <-> ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) = .0. ) )
33 28 32 bitr3d 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( y = x <-> ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) = .0. ) )
34 33 pm5.32da 
 |-  ( G e. Grp -> ( ( ( x e. B /\ y e. B ) /\ y = x ) <-> ( ( x e. B /\ y e. B ) /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) = .0. ) ) )
35 vex 
 |-  x e. _V
36 vex 
 |-  y e. _V
37 35 36 prss 
 |-  ( ( x e. B /\ y e. B ) <-> { x , y } C_ B )
38 37 a1i 
 |-  ( G e. Grp -> ( ( x e. B /\ y e. B ) <-> { x , y } C_ B ) )
39 2 eleq2i 
 |-  ( ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. S <-> ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. { .0. } )
40 ovex 
 |-  ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. _V
41 40 elsn 
 |-  ( ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. { .0. } <-> ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) = .0. )
42 39 41 bitr2i 
 |-  ( ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) = .0. <-> ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. S )
43 42 a1i 
 |-  ( G e. Grp -> ( ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) = .0. <-> ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. S ) )
44 38 43 anbi12d 
 |-  ( G e. Grp -> ( ( ( x e. B /\ y e. B ) /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) = .0. ) <-> ( { x , y } C_ B /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. S ) ) )
45 23 34 44 3bitrd 
 |-  ( G e. Grp -> ( ( x e. B /\ y = x ) <-> ( { x , y } C_ B /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. S ) ) )
46 45 opabbidv 
 |-  ( G e. Grp -> { <. x , y >. | ( x e. B /\ y = x ) } = { <. x , y >. | ( { x , y } C_ B /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. S ) } )
47 13 46 eqtr2id 
 |-  ( G e. Grp -> { <. x , y >. | ( { x , y } C_ B /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. S ) } = ( _I |` B ) )
48 12 47 eqtrd 
 |-  ( G e. Grp -> R = ( _I |` B ) )