| 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 19097 | . . 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 6494 (class class class)co 7362 Basecbs 17174 ↾s cress 17195 Grpcgrp 18904 SubGrpcsubg 19091 |
| 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 5232 ax-nul 5242 ax-pow 5304 ax-pr 5372 |
| 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 5521 df-xp 5632 df-rel 5633 df-cnv 5634 df-co 5635 df-dm 5636 df-rn 5637 df-res 5638 df-ima 5639 df-iota 6450 df-fun 6496 df-fv 6502 df-ov 7365 df-subg 19094 |
| This theorem is referenced by: subg0 19103 subginv 19104 subg0cl 19105 subginvcl 19106 subgcl 19107 issubg2 19112 issubgrpd 19114 subsubg 19120 resghm 19202 resghm2b 19204 subgga 19270 gasubg 19272 odsubdvds 19541 pgp0 19566 subgpgp 19567 sylow2blem2 19591 slwhash 19594 fislw 19595 subglsm 19643 pj1ghm 19673 subgabl 19806 cntrabl 19813 cycsubgcyg 19871 subgdmdprd 20006 subgdprd 20007 ablfacrplem 20037 pgpfaclem1 20053 pgpfaclem3 20055 ablfaclem3 20059 issubrg2 20564 subdrgint 20775 islss3 20949 zringcyg 21463 cnmsgngrp 21573 psgnghm 21574 mplgrp 22009 scmatghm 22512 subgtgp 24084 subgngp 24614 reefgim 26432 subgmulgcld 33123 ressply1sub 33649 amgmlemALT 50294 |
| Copyright terms: Public domain | W3C validator |