| Step | Hyp | Ref
| Expression |
| 1 | | eqger.r |
. . . . 5
⊢ ∼ =
(𝐺 ~QG
𝑌) |
| 2 | 1 | releqg 19193 |
. . . 4
⊢ Rel ∼ |
| 3 | | relelec 8792 |
. . . 4
⊢ (Rel
∼
→ (𝑥 ∈ [ 0 ] ∼ ↔
0 ∼ 𝑥)) |
| 4 | 2, 3 | ax-mp 5 |
. . 3
⊢ (𝑥 ∈ [ 0 ] ∼ ↔ 0 ∼ 𝑥) |
| 5 | | subgrcl 19149 |
. . . . . . . . . 10
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
| 6 | 5 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → 𝐺 ∈ Grp) |
| 7 | | eqgid.3 |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝐺) |
| 8 | | eqid 2737 |
. . . . . . . . . 10
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 9 | 7, 8 | grpinvid 19017 |
. . . . . . . . 9
⊢ (𝐺 ∈ Grp →
((invg‘𝐺)‘ 0 ) = 0 ) |
| 10 | 6, 9 | syl 17 |
. . . . . . . 8
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → ((invg‘𝐺)‘ 0 ) = 0 ) |
| 11 | 10 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) = ( 0 (+g‘𝐺)𝑥)) |
| 12 | | eqger.x |
. . . . . . . . 9
⊢ 𝑋 = (Base‘𝐺) |
| 13 | | eqid 2737 |
. . . . . . . . 9
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 14 | 12, 13, 7 | grplid 18985 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → ( 0 (+g‘𝐺)𝑥) = 𝑥) |
| 15 | 5, 14 | sylan 580 |
. . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → ( 0 (+g‘𝐺)𝑥) = 𝑥) |
| 16 | 11, 15 | eqtrd 2777 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) = 𝑥) |
| 17 | 16 | eleq1d 2826 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑋) → ((((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌 ↔ 𝑥 ∈ 𝑌)) |
| 18 | 17 | pm5.32da 579 |
. . . 4
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ((𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌) ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑌))) |
| 19 | 12 | subgss 19145 |
. . . . 5
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝑌 ⊆ 𝑋) |
| 20 | 12, 7 | grpidcl 18983 |
. . . . . 6
⊢ (𝐺 ∈ Grp → 0 ∈ 𝑋) |
| 21 | 5, 20 | syl 17 |
. . . . 5
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑋) |
| 22 | 12, 8, 13, 1 | eqgval 19195 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) → ( 0 ∼ 𝑥 ↔ ( 0 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌))) |
| 23 | | 3anass 1095 |
. . . . . . 7
⊢ (( 0 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌) ↔ ( 0 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌))) |
| 24 | 22, 23 | bitrdi 287 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) → ( 0 ∼ 𝑥 ↔ ( 0 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌)))) |
| 25 | 24 | baibd 539 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋) ∧ 0 ∈ 𝑋) → ( 0 ∼ 𝑥 ↔ (𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌))) |
| 26 | 5, 19, 21, 25 | syl21anc 838 |
. . . 4
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ( 0 ∼ 𝑥 ↔ (𝑥 ∈ 𝑋 ∧ (((invg‘𝐺)‘ 0
)(+g‘𝐺)𝑥) ∈ 𝑌))) |
| 27 | 19 | sseld 3982 |
. . . . 5
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑥 ∈ 𝑌 → 𝑥 ∈ 𝑋)) |
| 28 | 27 | pm4.71rd 562 |
. . . 4
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑥 ∈ 𝑌 ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑌))) |
| 29 | 18, 26, 28 | 3bitr4d 311 |
. . 3
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ( 0 ∼ 𝑥 ↔ 𝑥 ∈ 𝑌)) |
| 30 | 4, 29 | bitrid 283 |
. 2
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑥 ∈ [ 0 ] ∼ ↔ 𝑥 ∈ 𝑌)) |
| 31 | 30 | eqrdv 2735 |
1
⊢ (𝑌 ∈ (SubGrp‘𝐺) → [ 0 ] ∼ = 𝑌) |