Description: Properties that determine a group operation. Read N as N ( x ) . (Contributed by NM, 4-Nov-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isgrpoi.1 | |
|
isgrpoi.2 | |
||
isgrpoi.3 | |
||
isgrpoi.4 | |
||
isgrpoi.5 | |
||
isgrpoi.6 | |
||
isgrpoi.7 | |
||
Assertion | isgrpoi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isgrpoi.1 | |
|
2 | isgrpoi.2 | |
|
3 | isgrpoi.3 | |
|
4 | isgrpoi.4 | |
|
5 | isgrpoi.5 | |
|
6 | isgrpoi.6 | |
|
7 | isgrpoi.7 | |
|
8 | 3 | rgen3 | |
9 | oveq1 | |
|
10 | 9 | eqeq1d | |
11 | 10 | rspcev | |
12 | 6 7 11 | syl2anc | |
13 | 5 12 | jca | |
14 | 13 | rgen | |
15 | oveq1 | |
|
16 | 15 | eqeq1d | |
17 | eqeq2 | |
|
18 | 17 | rexbidv | |
19 | 16 18 | anbi12d | |
20 | 19 | ralbidv | |
21 | 20 | rspcev | |
22 | 4 14 21 | mp2an | |
23 | 1 1 | xpex | |
24 | fex | |
|
25 | 2 23 24 | mp2an | |
26 | 5 | eqcomd | |
27 | rspceov | |
|
28 | 4 27 | mp3an1 | |
29 | 26 28 | mpdan | |
30 | 29 | rgen | |
31 | foov | |
|
32 | 2 30 31 | mpbir2an | |
33 | forn | |
|
34 | 32 33 | ax-mp | |
35 | 34 | eqcomi | |
36 | 35 | isgrpo | |
37 | 25 36 | ax-mp | |
38 | 2 8 22 37 | mpbir3an | |