Metamath Proof Explorer

Theorem eqg0el

Description: Equivalence class of a quotient group for a subgroup. (Contributed by Thierry Arnoux, 15-Jan-2024)

Ref Expression
Hypothesis eqg0el.1 
|- .~ = ( G ~QG H )
Assertion eqg0el 
|- ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> ( [ X ] .~ = H <-> X e. H ) )

Proof

Step Hyp Ref Expression
1 eqg0el.1 
 |-  .~ = ( G ~QG H )
2 eqid 
 |-  ( Base ` G ) = ( Base ` G )
3 2 1 eqger 
 |-  ( H e. ( SubGrp ` G ) -> .~ Er ( Base ` G ) )
4 3 adantl 
 |-  ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> .~ Er ( Base ` G ) )
5 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
6 2 5 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. ( Base ` G ) )
7 6 adantr 
 |-  ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> ( 0g ` G ) e. ( Base ` G ) )
8 4 7 erth 
 |-  ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> ( ( 0g ` G ) .~ X <-> [ ( 0g ` G ) ] .~ = [ X ] .~ ) )
9 2 1 5 eqgid 
 |-  ( H e. ( SubGrp ` G ) -> [ ( 0g ` G ) ] .~ = H )
10 9 adantl 
 |-  ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> [ ( 0g ` G ) ] .~ = H )
11 10 eqeq1d 
 |-  ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> ( [ ( 0g ` G ) ] .~ = [ X ] .~ <-> H = [ X ] .~ ) )
12 eqcom 
 |-  ( H = [ X ] .~ <-> [ X ] .~ = H )
13 12 a1i 
 |-  ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> ( H = [ X ] .~ <-> [ X ] .~ = H ) )
14 8 11 13 3bitrrd 
 |-  ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> ( [ X ] .~ = H <-> ( 0g ` G ) .~ X ) )
15 errel 
 |-  ( .~ Er ( Base ` G ) -> Rel .~ )
16 relelec 
 |-  ( Rel .~ -> ( X e. [ ( 0g ` G ) ] .~ <-> ( 0g ` G ) .~ X ) )
17 3 15 16 3syl 
 |-  ( H e. ( SubGrp ` G ) -> ( X e. [ ( 0g ` G ) ] .~ <-> ( 0g ` G ) .~ X ) )
18 17 adantl 
 |-  ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> ( X e. [ ( 0g ` G ) ] .~ <-> ( 0g ` G ) .~ X ) )
19 10 eleq2d 
 |-  ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> ( X e. [ ( 0g ` G ) ] .~ <-> X e. H ) )
20 14 18 19 3bitr2d 
 |-  ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> ( [ X ] .~ = H <-> X e. H ) )