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