| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 2 | 1 | subg0cl 19152 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝑆) |
| 3 | 2 | a1i 11 |
. 2
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝑆)) |
| 4 | 1 | subm0cl 18824 |
. . . 4
⊢ (𝑆 ∈ (SubMnd‘𝐺) →
(0g‘𝐺)
∈ 𝑆) |
| 5 | 4 | adantr 480 |
. . 3
⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆) → (0g‘𝐺) ∈ 𝑆) |
| 6 | 5 | a1i 11 |
. 2
⊢ (𝐺 ∈ Grp → ((𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆) → (0g‘𝐺) ∈ 𝑆)) |
| 7 | | ne0i 4341 |
. . . . . . . 8
⊢
((0g‘𝐺) ∈ 𝑆 → 𝑆 ≠ ∅) |
| 8 | | id 22 |
. . . . . . . 8
⊢
((0g‘𝐺) ∈ 𝑆 → (0g‘𝐺) ∈ 𝑆) |
| 9 | 7, 8 | 2thd 265 |
. . . . . . 7
⊢
((0g‘𝐺) ∈ 𝑆 → (𝑆 ≠ ∅ ↔
(0g‘𝐺)
∈ 𝑆)) |
| 10 | 9 | adantl 481 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧
(0g‘𝐺)
∈ 𝑆) → (𝑆 ≠ ∅ ↔
(0g‘𝐺)
∈ 𝑆)) |
| 11 | | r19.26 3111 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆) ↔ (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)) |
| 12 | 11 | a1i 11 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧
(0g‘𝐺)
∈ 𝑆) →
(∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆) ↔ (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) |
| 13 | 10, 12 | 3anbi23d 1441 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧
(0g‘𝐺)
∈ 𝑆) → ((𝑆 ⊆ (Base‘𝐺) ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)) ↔ (𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆 ∧ (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)))) |
| 14 | | anass 468 |
. . . . . 6
⊢ ((((𝑆 ⊆ (Base‘𝐺) ∧
(0g‘𝐺)
∈ 𝑆) ∧
∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆) ↔ ((𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆) ∧ (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) |
| 15 | | df-3an 1089 |
. . . . . . 7
⊢ ((𝑆 ⊆ (Base‘𝐺) ∧
(0g‘𝐺)
∈ 𝑆 ∧
∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) ↔ ((𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆)) |
| 16 | 15 | anbi1i 624 |
. . . . . 6
⊢ (((𝑆 ⊆ (Base‘𝐺) ∧
(0g‘𝐺)
∈ 𝑆 ∧
∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆) ↔ (((𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)) |
| 17 | | df-3an 1089 |
. . . . . 6
⊢ ((𝑆 ⊆ (Base‘𝐺) ∧
(0g‘𝐺)
∈ 𝑆 ∧
(∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)) ↔ ((𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆) ∧ (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) |
| 18 | 14, 16, 17 | 3bitr4ri 304 |
. . . . 5
⊢ ((𝑆 ⊆ (Base‘𝐺) ∧
(0g‘𝐺)
∈ 𝑆 ∧
(∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)) ↔ ((𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)) |
| 19 | 13, 18 | bitrdi 287 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧
(0g‘𝐺)
∈ 𝑆) → ((𝑆 ⊆ (Base‘𝐺) ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)) ↔ ((𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) |
| 20 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 21 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 22 | | issubg3.i |
. . . . . 6
⊢ 𝐼 = (invg‘𝐺) |
| 23 | 20, 21, 22 | issubg2 19159 |
. . . . 5
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ (Base‘𝐺) ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)))) |
| 24 | 23 | adantr 480 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧
(0g‘𝐺)
∈ 𝑆) → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ (Base‘𝐺) ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)))) |
| 25 | | grpmnd 18958 |
. . . . . . 7
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
| 26 | 20, 1, 21 | issubm 18816 |
. . . . . . 7
⊢ (𝐺 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝐺) ↔ (𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆))) |
| 27 | 25, 26 | syl 17 |
. . . . . 6
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubMnd‘𝐺) ↔ (𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆))) |
| 28 | 27 | anbi1d 631 |
. . . . 5
⊢ (𝐺 ∈ Grp → ((𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆) ↔ ((𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) |
| 29 | 28 | adantr 480 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧
(0g‘𝐺)
∈ 𝑆) → ((𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆) ↔ ((𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) |
| 30 | 19, 24, 29 | 3bitr4d 311 |
. . 3
⊢ ((𝐺 ∈ Grp ∧
(0g‘𝐺)
∈ 𝑆) → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) |
| 31 | 30 | ex 412 |
. 2
⊢ (𝐺 ∈ Grp →
((0g‘𝐺)
∈ 𝑆 → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)))) |
| 32 | 3, 6, 31 | pm5.21ndd 379 |
1
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) |