Description: Properties that determine a group. N (negative) is normally dependent on x i.e. read it as N ( x ) . (Contributed by NM, 3-Sep-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isgrpi.b | |
|
isgrpi.p | |
||
isgrpi.c | |
||
isgrpi.a | |
||
isgrpi.z | |
||
isgrpi.i | |
||
isgrpi.n | |
||
isgrpi.j | |
||
Assertion | isgrpi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isgrpi.b | |
|
2 | isgrpi.p | |
|
3 | isgrpi.c | |
|
4 | isgrpi.a | |
|
5 | isgrpi.z | |
|
6 | isgrpi.i | |
|
7 | isgrpi.n | |
|
8 | isgrpi.j | |
|
9 | 1 | a1i | |
10 | 2 | a1i | |
11 | 3 | 3adant1 | |
12 | 4 | adantl | |
13 | 5 | a1i | |
14 | 6 | adantl | |
15 | 7 | adantl | |
16 | 8 | adantl | |
17 | 9 10 11 12 13 14 15 16 | isgrpd | |
18 | 17 | mptru | |