Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . 4
⊢
(0g‘𝐺) = (0g‘𝐺) |
2 | 1 | subg0cl 18398 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝑆) |
3 | 2 | a1i 11 |
. 2
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝑆)) |
4 | 1 | subm0cl 18085 |
. . . 4
⊢ (𝑆 ∈ (SubMnd‘𝐺) →
(0g‘𝐺)
∈ 𝑆) |
5 | 4 | adantr 484 |
. . 3
⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆) → (0g‘𝐺) ∈ 𝑆) |
6 | 5 | a1i 11 |
. 2
⊢ (𝐺 ∈ Grp → ((𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆) → (0g‘𝐺) ∈ 𝑆)) |
7 | | ne0i 4221 |
. . . . . . . 8
⊢
((0g‘𝐺) ∈ 𝑆 → 𝑆 ≠ ∅) |
8 | | id 22 |
. . . . . . . 8
⊢
((0g‘𝐺) ∈ 𝑆 → (0g‘𝐺) ∈ 𝑆) |
9 | 7, 8 | 2thd 268 |
. . . . . . 7
⊢
((0g‘𝐺) ∈ 𝑆 → (𝑆 ≠ ∅ ↔
(0g‘𝐺)
∈ 𝑆)) |
10 | 9 | adantl 485 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧
(0g‘𝐺)
∈ 𝑆) → (𝑆 ≠ ∅ ↔
(0g‘𝐺)
∈ 𝑆)) |
11 | | r19.26 3084 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆) ↔ (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)) |
12 | 11 | a1i 11 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧
(0g‘𝐺)
∈ 𝑆) →
(∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆) ↔ (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) |
13 | 10, 12 | 3anbi23d 1440 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧
(0g‘𝐺)
∈ 𝑆) → ((𝑆 ⊆ (Base‘𝐺) ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)) ↔ (𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆 ∧ (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)))) |
14 | | anass 472 |
. . . . . 6
⊢ ((((𝑆 ⊆ (Base‘𝐺) ∧
(0g‘𝐺)
∈ 𝑆) ∧
∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆) ↔ ((𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆) ∧ (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) |
15 | | df-3an 1090 |
. . . . . . 7
⊢ ((𝑆 ⊆ (Base‘𝐺) ∧
(0g‘𝐺)
∈ 𝑆 ∧
∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) ↔ ((𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆)) |
16 | 15 | anbi1i 627 |
. . . . . 6
⊢ (((𝑆 ⊆ (Base‘𝐺) ∧
(0g‘𝐺)
∈ 𝑆 ∧
∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆) ↔ (((𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)) |
17 | | df-3an 1090 |
. . . . . 6
⊢ ((𝑆 ⊆ (Base‘𝐺) ∧
(0g‘𝐺)
∈ 𝑆 ∧
(∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)) ↔ ((𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆) ∧ (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) |
18 | 14, 16, 17 | 3bitr4ri 307 |
. . . . 5
⊢ ((𝑆 ⊆ (Base‘𝐺) ∧
(0g‘𝐺)
∈ 𝑆 ∧
(∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)) ↔ ((𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)) |
19 | 13, 18 | bitrdi 290 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧
(0g‘𝐺)
∈ 𝑆) → ((𝑆 ⊆ (Base‘𝐺) ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)) ↔ ((𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) |
20 | | eqid 2738 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
21 | | eqid 2738 |
. . . . . 6
⊢
(+g‘𝐺) = (+g‘𝐺) |
22 | | issubg3.i |
. . . . . 6
⊢ 𝐼 = (invg‘𝐺) |
23 | 20, 21, 22 | issubg2 18405 |
. . . . 5
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ (Base‘𝐺) ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)))) |
24 | 23 | adantr 484 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧
(0g‘𝐺)
∈ 𝑆) → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ (Base‘𝐺) ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆)))) |
25 | | grpmnd 18219 |
. . . . . . 7
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
26 | 20, 1, 21 | issubm 18077 |
. . . . . . 7
⊢ (𝐺 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝐺) ↔ (𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆))) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubMnd‘𝐺) ↔ (𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆))) |
28 | 27 | anbi1d 633 |
. . . . 5
⊢ (𝐺 ∈ Grp → ((𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆) ↔ ((𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) |
29 | 28 | adantr 484 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧
(0g‘𝐺)
∈ 𝑆) → ((𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆) ↔ ((𝑆 ⊆ (Base‘𝐺) ∧ (0g‘𝐺) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) |
30 | 19, 24, 29 | 3bitr4d 314 |
. . 3
⊢ ((𝐺 ∈ Grp ∧
(0g‘𝐺)
∈ 𝑆) → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) |
31 | 30 | ex 416 |
. 2
⊢ (𝐺 ∈ Grp →
((0g‘𝐺)
∈ 𝑆 → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)))) |
32 | 3, 6, 31 | pm5.21ndd 384 |
1
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆))) |