![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-subg | Structured version Visualization version Unicode version |
Description: Define a subgroup of a group as a set of elements that is a group in its own right. Equivalently (issubg2 16910), a subgroup is a subset of the group that is closed for the group internal operation (see subgcl 16905), contains the neutral element of the group (see subg0 16901) and contains the inverses for all of its elements (see subginvcl 16904). (Contributed by Mario Carneiro, 2-Dec-2014.) |
Ref | Expression |
---|---|
df-subg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csubg 16889 |
. 2
![]() | |
2 | vw |
. . 3
![]() ![]() | |
3 | cgrp 16747 |
. . 3
![]() ![]() | |
4 | 2 | cv 1451 |
. . . . . 6
![]() ![]() |
5 | vs |
. . . . . . 7
![]() ![]() | |
6 | 5 | cv 1451 |
. . . . . 6
![]() ![]() |
7 | cress 15200 |
. . . . . 6
![]() | |
8 | 4, 6, 7 | co 6308 |
. . . . 5
![]() ![]() ![]() ![]() ![]() |
9 | 8, 3 | wcel 1904 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | cbs 15199 |
. . . . . 6
![]() ![]() | |
11 | 4, 10 | cfv 5589 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
12 | 11 | cpw 3942 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 9, 5, 12 | crab 2760 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 2, 3, 13 | cmpt 4454 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 1, 14 | wceq 1452 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: issubg 16895 |
Copyright terms: Public domain | W3C validator |