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 Grp H SubGrp G X ˙ = H X H

Proof

Step Hyp Ref Expression
1 eqg0el.1 ˙ = G ~ QG H
2 eqid Base G = Base G
3 2 1 eqger H SubGrp G ˙ Er Base G
4 3 adantl G Grp H SubGrp G ˙ Er Base G
5 eqid 0 G = 0 G
6 2 5 grpidcl G Grp 0 G Base G
7 6 adantr G Grp H SubGrp G 0 G Base G
8 4 7 erth G Grp H SubGrp G 0 G ˙ X 0 G ˙ = X ˙
9 2 1 5 eqgid H SubGrp G 0 G ˙ = H
10 9 adantl G Grp H SubGrp G 0 G ˙ = H
11 10 eqeq1d G Grp H SubGrp G 0 G ˙ = 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 0 G ˙ X
15 errel ˙ Er Base G Rel ˙
16 relelec Rel ˙ X 0 G ˙ 0 G ˙ X
17 3 15 16 3syl H SubGrp G X 0 G ˙ 0 G ˙ X
18 17 adantl G Grp H SubGrp G X 0 G ˙ 0 G ˙ X
19 10 eleq2d G Grp H SubGrp G X 0 G ˙ X H
20 14 18 19 3bitr2d G Grp H SubGrp G X ˙ = H X H