| Step | Hyp | Ref
| Expression |
| 1 | | issubg2.b |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
| 2 | 1 | subgss 19145 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵) |
| 3 | | eqid 2737 |
. . . . 5
⊢ (𝐺 ↾s 𝑆) = (𝐺 ↾s 𝑆) |
| 4 | 3 | subgbas 19148 |
. . . 4
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘(𝐺 ↾s 𝑆))) |
| 5 | 3 | subggrp 19147 |
. . . . 5
⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝑆) ∈ Grp) |
| 6 | | eqid 2737 |
. . . . . 6
⊢
(Base‘(𝐺
↾s 𝑆)) =
(Base‘(𝐺
↾s 𝑆)) |
| 7 | 6 | grpbn0 18984 |
. . . . 5
⊢ ((𝐺 ↾s 𝑆) ∈ Grp →
(Base‘(𝐺
↾s 𝑆))
≠ ∅) |
| 8 | 5, 7 | syl 17 |
. . . 4
⊢ (𝑆 ∈ (SubGrp‘𝐺) → (Base‘(𝐺 ↾s 𝑆)) ≠
∅) |
| 9 | 4, 8 | eqnetrd 3008 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ≠ ∅) |
| 10 | | issubg2.p |
. . . . . . . 8
⊢ + =
(+g‘𝐺) |
| 11 | 10 | subgcl 19154 |
. . . . . . 7
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) |
| 12 | 11 | 3expa 1119 |
. . . . . 6
⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆) |
| 13 | 12 | ralrimiva 3146 |
. . . . 5
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆) → ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) |
| 14 | | issubg2.i |
. . . . . 6
⊢ 𝐼 = (invg‘𝐺) |
| 15 | 14 | subginvcl 19153 |
. . . . 5
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆) → (𝐼‘𝑥) ∈ 𝑆) |
| 16 | 13, 15 | jca 511 |
. . . 4
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑆) → (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)) |
| 17 | 16 | ralrimiva 3146 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)) |
| 18 | 2, 9, 17 | 3jca 1129 |
. 2
⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) |
| 19 | | simpl 482 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → 𝐺 ∈ Grp) |
| 20 | | simpr1 1195 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → 𝑆 ⊆ 𝐵) |
| 21 | 3, 1 | ressbas2 17283 |
. . . . . 6
⊢ (𝑆 ⊆ 𝐵 → 𝑆 = (Base‘(𝐺 ↾s 𝑆))) |
| 22 | 20, 21 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → 𝑆 = (Base‘(𝐺 ↾s 𝑆))) |
| 23 | | fvex 6919 |
. . . . . . 7
⊢
(Base‘(𝐺
↾s 𝑆))
∈ V |
| 24 | 22, 23 | eqeltrdi 2849 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → 𝑆 ∈ V) |
| 25 | 3, 10 | ressplusg 17334 |
. . . . . 6
⊢ (𝑆 ∈ V → + =
(+g‘(𝐺
↾s 𝑆))) |
| 26 | 24, 25 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → + =
(+g‘(𝐺
↾s 𝑆))) |
| 27 | | simpr3 1197 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)) |
| 28 | | simpl 482 |
. . . . . . . . 9
⊢
((∀𝑦 ∈
𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆) → ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) |
| 29 | 28 | ralimi 3083 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) |
| 30 | 27, 29 | syl 17 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) |
| 31 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → (𝑥 + 𝑦) = (𝑢 + 𝑦)) |
| 32 | 31 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑢 + 𝑦) ∈ 𝑆)) |
| 33 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑦 = 𝑣 → (𝑢 + 𝑦) = (𝑢 + 𝑣)) |
| 34 | 33 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑦 = 𝑣 → ((𝑢 + 𝑦) ∈ 𝑆 ↔ (𝑢 + 𝑣) ∈ 𝑆)) |
| 35 | 32, 34 | rspc2v 3633 |
. . . . . . 7
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 → (𝑢 + 𝑣) ∈ 𝑆)) |
| 36 | 30, 35 | syl5com 31 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 + 𝑣) ∈ 𝑆)) |
| 37 | 36 | 3impib 1117 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢 + 𝑣) ∈ 𝑆) |
| 38 | 20 | sseld 3982 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → (𝑢 ∈ 𝑆 → 𝑢 ∈ 𝐵)) |
| 39 | 20 | sseld 3982 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → (𝑣 ∈ 𝑆 → 𝑣 ∈ 𝐵)) |
| 40 | 20 | sseld 3982 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → (𝑤 ∈ 𝑆 → 𝑤 ∈ 𝐵)) |
| 41 | 38, 39, 40 | 3anim123d 1445 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) → (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) |
| 42 | 41 | imp 406 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) |
| 43 | 1, 10 | grpass 18960 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤))) |
| 44 | 43 | adantlr 715 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤))) |
| 45 | 42, 44 | syldan 591 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ((𝑢 + 𝑣) + 𝑤) = (𝑢 + (𝑣 + 𝑤))) |
| 46 | | simpr2 1196 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → 𝑆 ≠ ∅) |
| 47 | | n0 4353 |
. . . . . . 7
⊢ (𝑆 ≠ ∅ ↔
∃𝑢 𝑢 ∈ 𝑆) |
| 48 | 46, 47 | sylib 218 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ∃𝑢 𝑢 ∈ 𝑆) |
| 49 | 20 | sselda 3983 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ 𝐵) |
| 50 | | eqid 2737 |
. . . . . . . . . 10
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 51 | 1, 10, 50, 14 | grplinv 19007 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝐵) → ((𝐼‘𝑢) + 𝑢) = (0g‘𝐺)) |
| 52 | 51 | adantlr 715 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝐵) → ((𝐼‘𝑢) + 𝑢) = (0g‘𝐺)) |
| 53 | 49, 52 | syldan 591 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → ((𝐼‘𝑢) + 𝑢) = (0g‘𝐺)) |
| 54 | | simpr 484 |
. . . . . . . . . . 11
⊢
((∀𝑦 ∈
𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆) → (𝐼‘𝑥) ∈ 𝑆) |
| 55 | 54 | ralimi 3083 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆) → ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆) |
| 56 | 27, 55 | syl 17 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆) |
| 57 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑢 → (𝐼‘𝑥) = (𝐼‘𝑢)) |
| 58 | 57 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑢 → ((𝐼‘𝑥) ∈ 𝑆 ↔ (𝐼‘𝑢) ∈ 𝑆)) |
| 59 | 58 | rspccva 3621 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝑆 (𝐼‘𝑥) ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → (𝐼‘𝑢) ∈ 𝑆) |
| 60 | 56, 59 | sylan 580 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → (𝐼‘𝑢) ∈ 𝑆) |
| 61 | | simpr 484 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → 𝑢 ∈ 𝑆) |
| 62 | 30 | adantr 480 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) |
| 63 | | ovrspc2v 7457 |
. . . . . . . 8
⊢ ((((𝐼‘𝑢) ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆) → ((𝐼‘𝑢) + 𝑢) ∈ 𝑆) |
| 64 | 60, 61, 62, 63 | syl21anc 838 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → ((𝐼‘𝑢) + 𝑢) ∈ 𝑆) |
| 65 | 53, 64 | eqeltrrd 2842 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → (0g‘𝐺) ∈ 𝑆) |
| 66 | 48, 65 | exlimddv 1935 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → (0g‘𝐺) ∈ 𝑆) |
| 67 | 1, 10, 50 | grplid 18985 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝐵) → ((0g‘𝐺) + 𝑢) = 𝑢) |
| 68 | 67 | adantlr 715 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝐵) → ((0g‘𝐺) + 𝑢) = 𝑢) |
| 69 | 49, 68 | syldan 591 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) ∧ 𝑢 ∈ 𝑆) → ((0g‘𝐺) + 𝑢) = 𝑢) |
| 70 | 22, 26, 37, 45, 66, 69, 60, 53 | isgrpd 18976 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → (𝐺 ↾s 𝑆) ∈ Grp) |
| 71 | 1 | issubg 19144 |
. . . 4
⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp)) |
| 72 | 19, 20, 70, 71 | syl3anbrc 1344 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))) → 𝑆 ∈ (SubGrp‘𝐺)) |
| 73 | 72 | ex 412 |
. 2
⊢ (𝐺 ∈ Grp → ((𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)) → 𝑆 ∈ (SubGrp‘𝐺))) |
| 74 | 18, 73 | impbid2 226 |
1
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)))) |