| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > subggrp | Structured version Visualization version GIF version | ||
| Description: A subgroup is a group. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| Ref | Expression |
|---|---|
| subggrp.h | ⊢ 𝐻 = (𝐺 ↾s 𝑆) |
| Ref | Expression |
|---|---|
| subggrp | ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | subggrp.h | . 2 ⊢ 𝐻 = (𝐺 ↾s 𝑆) | |
| 2 | eqid 2737 | . . . 4 ⊢ (Base‘𝐺) = (Base‘𝐺) | |
| 3 | 2 | issubg 19091 | . . 3 ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ (Base‘𝐺) ∧ (𝐺 ↾s 𝑆) ∈ Grp)) |
| 4 | 3 | simp3bi 1148 | . 2 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐺 ↾s 𝑆) ∈ Grp) |
| 5 | 1, 4 | eqeltrid 2841 | 1 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 ⊆ wss 3890 ‘cfv 6490 (class class class)co 7358 Basecbs 17168 ↾s cress 17189 Grpcgrp 18898 SubGrpcsubg 19085 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rab 3391 df-v 3432 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5517 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-iota 6446 df-fun 6492 df-fv 6498 df-ov 7361 df-subg 19088 |
| This theorem is referenced by: subg0 19097 subginv 19098 subg0cl 19099 subginvcl 19100 subgcl 19101 issubg2 19106 issubgrpd 19108 subsubg 19114 resghm 19196 resghm2b 19198 subgga 19264 gasubg 19266 odsubdvds 19535 pgp0 19560 subgpgp 19561 sylow2blem2 19585 slwhash 19588 fislw 19589 subglsm 19637 pj1ghm 19667 subgabl 19800 cntrabl 19807 cycsubgcyg 19865 subgdmdprd 20000 subgdprd 20001 ablfacrplem 20031 pgpfaclem1 20047 pgpfaclem3 20049 ablfaclem3 20053 issubrg2 20558 subdrgint 20769 islss3 20943 zringcyg 21457 cnmsgngrp 21567 psgnghm 21568 mplgrp 22004 scmatghm 22507 subgtgp 24079 subgngp 24609 reefgim 26431 subgmulgcld 33124 ressply1sub 33650 amgmlemALT 50275 |
| Copyright terms: Public domain | W3C validator |