Step | Hyp | Ref
| Expression |
1 | | subgrcl 12970 |
. . . . 5
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
2 | | eqger.r |
. . . . . 6
⊢ ∼ =
(𝐺 ~QG
𝑌) |
3 | 2 | releqgg 13011 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ (SubGrp‘𝐺)) → Rel ∼ ) |
4 | 1, 3 | mpancom 422 |
. . . 4
⊢ (𝑌 ∈ (SubGrp‘𝐺) → Rel ∼ ) |
5 | | relelec 6572 |
. . . 4
⊢ (Rel
∼
→ (𝑥 ∈ [ 0 ] ∼ ↔
0 ∼ 𝑥)) |
6 | 4, 5 | syl 14 |
. . 3
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑥 ∈ [ 0 ] ∼ ↔ 0 ∼ 𝑥)) |
7 | 1 | adantr 276 |
. . . . . . . . 9
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → 𝐺 ∈ Grp) |
8 | | eqgid.3 |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝐺) |
9 | | eqid 2177 |
. . . . . . . . . 10
⊢
(invg‘𝐺) = (invg‘𝐺) |
10 | 8, 9 | grpinvid 12862 |
. . . . . . . . 9
⊢ (𝐺 ∈ Grp →
((invg‘𝐺)‘ 0 ) = 0 ) |
11 | 7, 10 | syl 14 |
. . . . . . . 8
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → ((invg‘𝐺)‘ 0 ) = 0 ) |
12 | 11 | oveq1d 5887 |
. . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) = ( 0 (+g‘𝐺)𝑥)) |
13 | | eqger.x |
. . . . . . . . 9
⊢ 𝑋 = (Base‘𝐺) |
14 | | eqid 2177 |
. . . . . . . . 9
⊢
(+g‘𝐺) = (+g‘𝐺) |
15 | 13, 14, 8 | grplid 12838 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → ( 0 (+g‘𝐺)𝑥) = 𝑥) |
16 | 1, 15 | sylan 283 |
. . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → ( 0 (+g‘𝐺)𝑥) = 𝑥) |
17 | 12, 16 | eqtrd 2210 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) = 𝑥) |
18 | 17 | eleq1d 2246 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → ((((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌 ↔ 𝑥 ∈ 𝑌)) |
19 | 18 | pm5.32da 452 |
. . . 4
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ((𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌) ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑌))) |
20 | 13 | subgss 12965 |
. . . . 5
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝑌 ⊆ 𝑋) |
21 | 13, 8 | grpidcl 12836 |
. . . . . 6
⊢ (𝐺 ∈ Grp → 0 ∈ 𝑋) |
22 | 1, 21 | syl 14 |
. . . . 5
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑋) |
23 | 13, 9, 14, 2 | eqgval 13013 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) → ( 0 ∼ 𝑥 ↔ ( 0 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌))) |
24 | | 3anass 982 |
. . . . . . 7
⊢ (( 0 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌) ↔ ( 0 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌))) |
25 | 23, 24 | bitrdi 196 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) → ( 0 ∼ 𝑥 ↔ ( 0 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌)))) |
26 | 25 | baibd 923 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) ∧ 0 ∈ 𝑋) → ( 0 ∼ 𝑥 ↔ (𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌))) |
27 | 1, 20, 22, 26 | syl21anc 1237 |
. . . 4
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ( 0 ∼ 𝑥 ↔ (𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌))) |
28 | 20 | sseld 3154 |
. . . . 5
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑥 ∈ 𝑌 → 𝑥 ∈ 𝑋)) |
29 | 28 | pm4.71rd 394 |
. . . 4
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑥 ∈ 𝑌 ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑌))) |
30 | 19, 27, 29 | 3bitr4d 220 |
. . 3
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ( 0 ∼ 𝑥 ↔ 𝑥 ∈ 𝑌)) |
31 | 6, 30 | bitrd 188 |
. 2
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑥 ∈ [ 0 ] ∼ ↔ 𝑥 ∈ 𝑌)) |
32 | 31 | eqrdv 2175 |
1
⊢ (𝑌 ∈ (SubGrp‘𝐺) → [ 0 ] ∼ = 𝑌) |