Step | Hyp | Ref
| Expression |
1 | | eqger.r |
. . . . 5
⊢ ∼ =
(𝐺 ~QG
𝑌) |
2 | 1 | releqg 17641 |
. . . 4
⊢ Rel ∼ |
3 | | relelec 7787 |
. . . 4
⊢ (Rel
∼
→ (𝑥 ∈ [ 0 ] ∼ ↔
0 ∼ 𝑥)) |
4 | 2, 3 | ax-mp 5 |
. . 3
⊢ (𝑥 ∈ [ 0 ] ∼ ↔ 0 ∼ 𝑥) |
5 | | subgrcl 17599 |
. . . . . . . . . 10
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
6 | 5 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → 𝐺 ∈ Grp) |
7 | | eqgid.3 |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝐺) |
8 | | eqid 2622 |
. . . . . . . . . 10
⊢
(invg‘𝐺) = (invg‘𝐺) |
9 | 7, 8 | grpinvid 17476 |
. . . . . . . . 9
⊢ (𝐺 ∈ Grp →
((invg‘𝐺)‘ 0 ) = 0 ) |
10 | 6, 9 | syl 17 |
. . . . . . . 8
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → ((invg‘𝐺)‘ 0 ) = 0 ) |
11 | 10 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) = ( 0 (+g‘𝐺)𝑥)) |
12 | | eqger.x |
. . . . . . . . 9
⊢ 𝑋 = (Base‘𝐺) |
13 | | eqid 2622 |
. . . . . . . . 9
⊢
(+g‘𝐺) = (+g‘𝐺) |
14 | 12, 13, 7 | grplid 17452 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → ( 0 (+g‘𝐺)𝑥) = 𝑥) |
15 | 5, 14 | sylan 488 |
. . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → ( 0 (+g‘𝐺)𝑥) = 𝑥) |
16 | 11, 15 | eqtrd 2656 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) = 𝑥) |
17 | 16 | eleq1d 2686 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → ((((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌 ↔ 𝑥 ∈ 𝑌)) |
18 | 17 | pm5.32da 673 |
. . . 4
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ((𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌) ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑌))) |
19 | 12 | subgss 17595 |
. . . . 5
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝑌 ⊆ 𝑋) |
20 | 12, 7 | grpidcl 17450 |
. . . . . 6
⊢ (𝐺 ∈ Grp → 0 ∈ 𝑋) |
21 | 5, 20 | syl 17 |
. . . . 5
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑋) |
22 | 12, 8, 13, 1 | eqgval 17643 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) → ( 0 ∼ 𝑥 ↔ ( 0 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌))) |
23 | | 3anass 1042 |
. . . . . . 7
⊢ (( 0 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌) ↔ ( 0 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌))) |
24 | 22, 23 | syl6bb 276 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) → ( 0 ∼ 𝑥 ↔ ( 0 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌)))) |
25 | 24 | baibd 948 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) ∧ 0 ∈ 𝑋) → ( 0 ∼ 𝑥 ↔ (𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌))) |
26 | 5, 19, 21, 25 | syl21anc 1325 |
. . . 4
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ( 0 ∼ 𝑥 ↔ (𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌))) |
27 | 19 | sseld 3602 |
. . . . 5
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑥 ∈ 𝑌 → 𝑥 ∈ 𝑋)) |
28 | 27 | pm4.71rd 667 |
. . . 4
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑥 ∈ 𝑌 ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑌))) |
29 | 18, 26, 28 | 3bitr4d 300 |
. . 3
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ( 0 ∼ 𝑥 ↔ 𝑥 ∈ 𝑌)) |
30 | 4, 29 | syl5bb 272 |
. 2
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑥 ∈ [ 0 ] ∼ ↔ 𝑥 ∈ 𝑌)) |
31 | 30 | eqrdv 2620 |
1
⊢ (𝑌 ∈ (SubGrp‘𝐺) → [ 0 ] ∼ = 𝑌) |