Step | Hyp | Ref
| Expression |
1 | | intssuni 4434 |
. . . 4
⊢ (𝑆 ≠ ∅ → ∩ 𝑆
⊆ ∪ 𝑆) |
2 | 1 | adantl 481 |
. . 3
⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) → ∩ 𝑆
⊆ ∪ 𝑆) |
3 | | ssel2 3563 |
. . . . . . 7
⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑔 ∈ 𝑆) → 𝑔 ∈ (SubGrp‘𝐺)) |
4 | 3 | adantlr 747 |
. . . . . 6
⊢ (((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ 𝑔 ∈ 𝑆) → 𝑔 ∈ (SubGrp‘𝐺)) |
5 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝐺) =
(Base‘𝐺) |
6 | 5 | subgss 17418 |
. . . . . 6
⊢ (𝑔 ∈ (SubGrp‘𝐺) → 𝑔 ⊆ (Base‘𝐺)) |
7 | 4, 6 | syl 17 |
. . . . 5
⊢ (((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ 𝑔 ∈ 𝑆) → 𝑔 ⊆ (Base‘𝐺)) |
8 | 7 | ralrimiva 2949 |
. . . 4
⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) → ∀𝑔 ∈ 𝑆 𝑔 ⊆ (Base‘𝐺)) |
9 | | unissb 4405 |
. . . 4
⊢ (∪ 𝑆
⊆ (Base‘𝐺)
↔ ∀𝑔 ∈
𝑆 𝑔 ⊆ (Base‘𝐺)) |
10 | 8, 9 | sylibr 223 |
. . 3
⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) → ∪ 𝑆
⊆ (Base‘𝐺)) |
11 | 2, 10 | sstrd 3578 |
. 2
⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) → ∩ 𝑆
⊆ (Base‘𝐺)) |
12 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
13 | 12 | subg0cl 17425 |
. . . . . 6
⊢ (𝑔 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝑔) |
14 | 4, 13 | syl 17 |
. . . . 5
⊢ (((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ 𝑔 ∈ 𝑆) → (0g‘𝐺) ∈ 𝑔) |
15 | 14 | ralrimiva 2949 |
. . . 4
⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) → ∀𝑔 ∈ 𝑆 (0g‘𝐺) ∈ 𝑔) |
16 | | fvex 6113 |
. . . . 5
⊢
(0g‘𝐺) ∈ V |
17 | 16 | elint2 4417 |
. . . 4
⊢
((0g‘𝐺) ∈ ∩ 𝑆 ↔ ∀𝑔 ∈ 𝑆 (0g‘𝐺) ∈ 𝑔) |
18 | 15, 17 | sylibr 223 |
. . 3
⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) →
(0g‘𝐺)
∈ ∩ 𝑆) |
19 | | ne0i 3880 |
. . 3
⊢
((0g‘𝐺) ∈ ∩ 𝑆 → ∩ 𝑆
≠ ∅) |
20 | 18, 19 | syl 17 |
. 2
⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) → ∩ 𝑆
≠ ∅) |
21 | 4 | adantlr 747 |
. . . . . . . . 9
⊢ ((((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ (𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆)) ∧ 𝑔 ∈ 𝑆) → 𝑔 ∈ (SubGrp‘𝐺)) |
22 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ (𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆)) → 𝑥 ∈ ∩ 𝑆) |
23 | | elinti 4420 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∩ 𝑆
→ (𝑔 ∈ 𝑆 → 𝑥 ∈ 𝑔)) |
24 | 23 | imp 444 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ∩ 𝑆
∧ 𝑔 ∈ 𝑆) → 𝑥 ∈ 𝑔) |
25 | 22, 24 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ (𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆)) ∧ 𝑔 ∈ 𝑆) → 𝑥 ∈ 𝑔) |
26 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ (𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆)) → 𝑦 ∈ ∩ 𝑆) |
27 | | elinti 4420 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ∩ 𝑆
→ (𝑔 ∈ 𝑆 → 𝑦 ∈ 𝑔)) |
28 | 27 | imp 444 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ∩ 𝑆
∧ 𝑔 ∈ 𝑆) → 𝑦 ∈ 𝑔) |
29 | 26, 28 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ (𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆)) ∧ 𝑔 ∈ 𝑆) → 𝑦 ∈ 𝑔) |
30 | | eqid 2610 |
. . . . . . . . . 10
⊢
(+g‘𝐺) = (+g‘𝐺) |
31 | 30 | subgcl 17427 |
. . . . . . . . 9
⊢ ((𝑔 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑔 ∧ 𝑦 ∈ 𝑔) → (𝑥(+g‘𝐺)𝑦) ∈ 𝑔) |
32 | 21, 25, 29, 31 | syl3anc 1318 |
. . . . . . . 8
⊢ ((((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ (𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆)) ∧ 𝑔 ∈ 𝑆) → (𝑥(+g‘𝐺)𝑦) ∈ 𝑔) |
33 | 32 | ralrimiva 2949 |
. . . . . . 7
⊢ (((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ (𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆)) → ∀𝑔 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑔) |
34 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑥(+g‘𝐺)𝑦) ∈ V |
35 | 34 | elint2 4417 |
. . . . . . 7
⊢ ((𝑥(+g‘𝐺)𝑦) ∈ ∩ 𝑆 ↔ ∀𝑔 ∈ 𝑆 (𝑥(+g‘𝐺)𝑦) ∈ 𝑔) |
36 | 33, 35 | sylibr 223 |
. . . . . 6
⊢ (((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ (𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆)) → (𝑥(+g‘𝐺)𝑦) ∈ ∩ 𝑆) |
37 | 36 | anassrs 678 |
. . . . 5
⊢ ((((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝑆) ∧ 𝑦 ∈ ∩ 𝑆) → (𝑥(+g‘𝐺)𝑦) ∈ ∩ 𝑆) |
38 | 37 | ralrimiva 2949 |
. . . 4
⊢ (((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝑆) → ∀𝑦 ∈ ∩ 𝑆(𝑥(+g‘𝐺)𝑦) ∈ ∩ 𝑆) |
39 | 4 | adantlr 747 |
. . . . . . 7
⊢ ((((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝑆) ∧ 𝑔 ∈ 𝑆) → 𝑔 ∈ (SubGrp‘𝐺)) |
40 | 24 | adantll 746 |
. . . . . . 7
⊢ ((((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝑆) ∧ 𝑔 ∈ 𝑆) → 𝑥 ∈ 𝑔) |
41 | | eqid 2610 |
. . . . . . . 8
⊢
(invg‘𝐺) = (invg‘𝐺) |
42 | 41 | subginvcl 17426 |
. . . . . . 7
⊢ ((𝑔 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑔) → ((invg‘𝐺)‘𝑥) ∈ 𝑔) |
43 | 39, 40, 42 | syl2anc 691 |
. . . . . 6
⊢ ((((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝑆) ∧ 𝑔 ∈ 𝑆) → ((invg‘𝐺)‘𝑥) ∈ 𝑔) |
44 | 43 | ralrimiva 2949 |
. . . . 5
⊢ (((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝑆) → ∀𝑔 ∈ 𝑆 ((invg‘𝐺)‘𝑥) ∈ 𝑔) |
45 | | fvex 6113 |
. . . . . 6
⊢
((invg‘𝐺)‘𝑥) ∈ V |
46 | 45 | elint2 4417 |
. . . . 5
⊢
(((invg‘𝐺)‘𝑥) ∈ ∩ 𝑆 ↔ ∀𝑔 ∈ 𝑆 ((invg‘𝐺)‘𝑥) ∈ 𝑔) |
47 | 44, 46 | sylibr 223 |
. . . 4
⊢ (((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝑆) →
((invg‘𝐺)‘𝑥) ∈ ∩ 𝑆) |
48 | 38, 47 | jca 553 |
. . 3
⊢ (((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) ∧ 𝑥 ∈ ∩ 𝑆) → (∀𝑦 ∈ ∩ 𝑆(𝑥(+g‘𝐺)𝑦) ∈ ∩ 𝑆 ∧
((invg‘𝐺)‘𝑥) ∈ ∩ 𝑆)) |
49 | 48 | ralrimiva 2949 |
. 2
⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) → ∀𝑥 ∈ ∩ 𝑆(∀𝑦 ∈ ∩ 𝑆(𝑥(+g‘𝐺)𝑦) ∈ ∩ 𝑆 ∧
((invg‘𝐺)‘𝑥) ∈ ∩ 𝑆)) |
50 | | ssn0 3928 |
. . 3
⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) → (SubGrp‘𝐺) ≠ ∅) |
51 | | n0 3890 |
. . . 4
⊢
((SubGrp‘𝐺)
≠ ∅ ↔ ∃𝑔 𝑔 ∈ (SubGrp‘𝐺)) |
52 | | subgrcl 17422 |
. . . . 5
⊢ (𝑔 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
53 | 52 | exlimiv 1845 |
. . . 4
⊢
(∃𝑔 𝑔 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
54 | 51, 53 | sylbi 206 |
. . 3
⊢
((SubGrp‘𝐺)
≠ ∅ → 𝐺
∈ Grp) |
55 | 5, 30, 41 | issubg2 17432 |
. . 3
⊢ (𝐺 ∈ Grp → (∩ 𝑆
∈ (SubGrp‘𝐺)
↔ (∩ 𝑆 ⊆ (Base‘𝐺) ∧ ∩ 𝑆 ≠ ∅ ∧
∀𝑥 ∈ ∩ 𝑆(∀𝑦 ∈ ∩ 𝑆(𝑥(+g‘𝐺)𝑦) ∈ ∩ 𝑆 ∧
((invg‘𝐺)‘𝑥) ∈ ∩ 𝑆)))) |
56 | 50, 54, 55 | 3syl 18 |
. 2
⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) → (∩ 𝑆
∈ (SubGrp‘𝐺)
↔ (∩ 𝑆 ⊆ (Base‘𝐺) ∧ ∩ 𝑆 ≠ ∅ ∧
∀𝑥 ∈ ∩ 𝑆(∀𝑦 ∈ ∩ 𝑆(𝑥(+g‘𝐺)𝑦) ∈ ∩ 𝑆 ∧
((invg‘𝐺)‘𝑥) ∈ ∩ 𝑆)))) |
57 | 11, 20, 49, 56 | mpbir3and 1238 |
1
⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) → ∩ 𝑆
∈ (SubGrp‘𝐺)) |