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~QGH
Assertion eqg0el ⊢G∈Grp∧H∈SubGrp⁡G→X∼˙=H↔X∈H

Proof

Step Hyp Ref Expression
1 eqg0el.1 ⊢∼˙=G~QGH
2 eqid ⊢BaseG=BaseG
3 2 1 eqger ⊢H∈SubGrp⁡G→∼˙ErBaseG
4 3 adantl ⊢G∈Grp∧H∈SubGrp⁡G→∼˙ErBaseG
5 eqid ⊢0G=0G
6 2 5 grpidcl ⊢G∈Grp→0G∈BaseG
7 6 adantr ⊢G∈Grp∧H∈SubGrp⁡G→0G∈BaseG
8 4 7 erth ⊢G∈Grp∧H∈SubGrp⁡G→0G∼˙X↔0G∼˙=X∼˙
9 2 1 5 eqgid ⊢H∈SubGrp⁡G→0G∼˙=H
10 9 adantl ⊢G∈Grp∧H∈SubGrp⁡G→0G∼˙=H
11 10 eqeq1d ⊢G∈Grp∧H∈SubGrp⁡G→0G∼˙=X∼˙↔H=X∼˙
12 eqcom ⊢H=X∼˙↔X∼˙=H
13 12 a1i ⊢G∈Grp∧H∈SubGrp⁡G→H=X∼˙↔X∼˙=H
14 8 11 13 3bitrrd ⊢G∈Grp∧H∈SubGrp⁡G→X∼˙=H↔0G∼˙X
15 errel ⊢∼˙ErBaseG→Rel⁡∼˙
16 relelec ⊢Rel⁡∼˙→X∈0G∼˙↔0G∼˙X
17 3 15 16 3syl ⊢H∈SubGrp⁡G→X∈0G∼˙↔0G∼˙X
18 17 adantl ⊢G∈Grp∧H∈SubGrp⁡G→X∈0G∼˙↔0G∼˙X
19 10 eleq2d ⊢G∈Grp∧H∈SubGrp⁡G→X∈0G∼˙↔X∈H
20 14 18 19 3bitr2d ⊢G∈Grp∧H∈SubGrp⁡G→X∼˙=H↔X∈H