Step |
Hyp |
Ref |
Expression |
1 |
|
eqger.x |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
2 |
|
eqger.r |
⊢ ∼ = ( 𝐺 ~QG 𝑌 ) |
3 |
|
eqgid.3 |
⊢ 0 = ( 0g ‘ 𝐺 ) |
4 |
2
|
releqg |
⊢ Rel ∼ |
5 |
|
relelec |
⊢ ( Rel ∼ → ( 𝑥 ∈ [ 0 ] ∼ ↔ 0 ∼ 𝑥 ) ) |
6 |
4 5
|
ax-mp |
⊢ ( 𝑥 ∈ [ 0 ] ∼ ↔ 0 ∼ 𝑥 ) |
7 |
|
subgrcl |
⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp ) |
8 |
7
|
adantr |
⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐺 ∈ Grp ) |
9 |
|
eqid |
⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 ) |
10 |
3 9
|
grpinvid |
⊢ ( 𝐺 ∈ Grp → ( ( invg ‘ 𝐺 ) ‘ 0 ) = 0 ) |
11 |
8 10
|
syl |
⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 0 ) = 0 ) |
12 |
11
|
oveq1d |
⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 0 ) ( +g ‘ 𝐺 ) 𝑥 ) = ( 0 ( +g ‘ 𝐺 ) 𝑥 ) ) |
13 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
14 |
1 13 3
|
grplid |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( 0 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ) |
15 |
7 14
|
sylan |
⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → ( 0 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ) |
16 |
12 15
|
eqtrd |
⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 0 ) ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ) |
17 |
16
|
eleq1d |
⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 0 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑌 ↔ 𝑥 ∈ 𝑌 ) ) |
18 |
17
|
pm5.32da |
⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 0 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑌 ) ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑌 ) ) ) |
19 |
1
|
subgss |
⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝑌 ⊆ 𝑋 ) |
20 |
1 3
|
grpidcl |
⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝑋 ) |
21 |
7 20
|
syl |
⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ 𝑋 ) |
22 |
1 9 13 2
|
eqgval |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ) → ( 0 ∼ 𝑥 ↔ ( 0 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 0 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑌 ) ) ) |
23 |
|
3anass |
⊢ ( ( 0 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 0 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑌 ) ↔ ( 0 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 0 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑌 ) ) ) |
24 |
22 23
|
bitrdi |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ) → ( 0 ∼ 𝑥 ↔ ( 0 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 0 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑌 ) ) ) ) |
25 |
24
|
baibd |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ) ∧ 0 ∈ 𝑋 ) → ( 0 ∼ 𝑥 ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 0 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑌 ) ) ) |
26 |
7 19 21 25
|
syl21anc |
⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 0 ∼ 𝑥 ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 0 ) ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑌 ) ) ) |
27 |
19
|
sseld |
⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑥 ∈ 𝑌 → 𝑥 ∈ 𝑋 ) ) |
28 |
27
|
pm4.71rd |
⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑥 ∈ 𝑌 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑌 ) ) ) |
29 |
18 26 28
|
3bitr4d |
⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 0 ∼ 𝑥 ↔ 𝑥 ∈ 𝑌 ) ) |
30 |
6 29
|
syl5bb |
⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑥 ∈ [ 0 ] ∼ ↔ 𝑥 ∈ 𝑌 ) ) |
31 |
30
|
eqrdv |
⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → [ 0 ] ∼ = 𝑌 ) |