Step |
Hyp |
Ref |
Expression |
1 |
|
eqg0el.1 |
⊢ ∼ = ( 𝐺 ~QG 𝐻 ) |
2 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
3 |
2 1
|
eqger |
⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → ∼ Er ( Base ‘ 𝐺 ) ) |
4 |
3
|
adantl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ∼ Er ( Base ‘ 𝐺 ) ) |
5 |
|
eqid |
⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) |
6 |
2 5
|
grpidcl |
⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) ) |
7 |
6
|
adantr |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) ) |
8 |
4 7
|
erth |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 0g ‘ 𝐺 ) ∼ 𝑋 ↔ [ ( 0g ‘ 𝐺 ) ] ∼ = [ 𝑋 ] ∼ ) ) |
9 |
2 1 5
|
eqgid |
⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → [ ( 0g ‘ 𝐺 ) ] ∼ = 𝐻 ) |
10 |
9
|
adantl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → [ ( 0g ‘ 𝐺 ) ] ∼ = 𝐻 ) |
11 |
10
|
eqeq1d |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( [ ( 0g ‘ 𝐺 ) ] ∼ = [ 𝑋 ] ∼ ↔ 𝐻 = [ 𝑋 ] ∼ ) ) |
12 |
|
eqcom |
⊢ ( 𝐻 = [ 𝑋 ] ∼ ↔ [ 𝑋 ] ∼ = 𝐻 ) |
13 |
12
|
a1i |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐻 = [ 𝑋 ] ∼ ↔ [ 𝑋 ] ∼ = 𝐻 ) ) |
14 |
8 11 13
|
3bitrrd |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( [ 𝑋 ] ∼ = 𝐻 ↔ ( 0g ‘ 𝐺 ) ∼ 𝑋 ) ) |
15 |
|
errel |
⊢ ( ∼ Er ( Base ‘ 𝐺 ) → Rel ∼ ) |
16 |
|
relelec |
⊢ ( Rel ∼ → ( 𝑋 ∈ [ ( 0g ‘ 𝐺 ) ] ∼ ↔ ( 0g ‘ 𝐺 ) ∼ 𝑋 ) ) |
17 |
3 15 16
|
3syl |
⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑋 ∈ [ ( 0g ‘ 𝐺 ) ] ∼ ↔ ( 0g ‘ 𝐺 ) ∼ 𝑋 ) ) |
18 |
17
|
adantl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑋 ∈ [ ( 0g ‘ 𝐺 ) ] ∼ ↔ ( 0g ‘ 𝐺 ) ∼ 𝑋 ) ) |
19 |
10
|
eleq2d |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑋 ∈ [ ( 0g ‘ 𝐺 ) ] ∼ ↔ 𝑋 ∈ 𝐻 ) ) |
20 |
14 18 19
|
3bitr2d |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( [ 𝑋 ] ∼ = 𝐻 ↔ 𝑋 ∈ 𝐻 ) ) |