![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > subgbas | Structured version Unicode version |
Description: The base of the restricted group in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
Ref | Expression |
---|---|
subggrp.h |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
subgbas |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2454 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | subgss 15800 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | subggrp.h |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3, 1 | ressbas2 14347 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | syl 16 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-sep 4520 ax-nul 4528 ax-pow 4577 ax-pr 4638 ax-un 6481 ax-cnex 9448 ax-resscn 9449 ax-1cn 9450 ax-icn 9451 ax-addcl 9452 ax-addrcl 9453 ax-mulcl 9454 ax-mulrcl 9455 ax-i2m1 9460 ax-1ne0 9461 ax-rrecex 9464 ax-cnre 9465 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2649 df-ral 2803 df-rex 2804 df-reu 2805 df-rab 2807 df-v 3078 df-sbc 3293 df-csb 3395 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-pss 3451 df-nul 3745 df-if 3899 df-pw 3969 df-sn 3985 df-pr 3987 df-tp 3989 df-op 3991 df-uni 4199 df-iun 4280 df-br 4400 df-opab 4458 df-mpt 4459 df-tr 4493 df-eprel 4739 df-id 4743 df-po 4748 df-so 4749 df-fr 4786 df-we 4788 df-ord 4829 df-on 4830 df-lim 4831 df-suc 4832 df-xp 4953 df-rel 4954 df-cnv 4955 df-co 4956 df-dm 4957 df-rn 4958 df-res 4959 df-ima 4960 df-iota 5488 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-ov 6202 df-oprab 6203 df-mpt2 6204 df-om 6586 df-recs 6941 df-rdg 6975 df-nn 10433 df-ndx 14294 df-slot 14295 df-base 14296 df-sets 14297 df-ress 14298 df-subg 15796 |
This theorem is referenced by: subg0 15805 subginv 15806 subg0cl 15807 subginvcl 15808 subgcl 15809 subgsub 15811 subgmulg 15813 issubg2 15814 subsubg 15822 nmznsg 15843 subgga 15936 gasubg 15938 odsubdvds 16190 pgp0 16215 subgpgp 16216 sylow2blem2 16240 sylow2blem3 16241 slwhash 16243 fislw 16244 sylow3lem4 16249 sylow3lem6 16251 subglsm 16290 pj1ghm 16320 subgabl 16440 cycsubgcyg 16497 subgdmdprd 16652 ablfacrplem 16687 ablfac1c 16693 pgpfaclem1 16703 pgpfaclem2 16704 pgpfaclem3 16705 ablfaclem3 16709 ablfac2 16711 subrgbas 16996 issubrg2 17007 pj1lmhm 17303 zcyg 18036 subgtgp 19807 subgnm 20350 subgngp 20352 lssnlm 20412 reefgim 22047 scmatsgrp1 31054 |
Copyright terms: Public domain | W3C validator |