Description: The base of an explicitly given group. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use grpbase instead. (New usage is discouraged.) (Contributed by NM, 17-Oct-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | grpstrx.b | |
|
grpstrx.p | |
||
grpstrx.g | |
||
Assertion | grpbasex | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grpstrx.b | |
|
2 | grpstrx.p | |
|
3 | grpstrx.g | |
|
4 | basendx | |
|
5 | 4 | opeq1i | |
6 | plusgndx | |
|
7 | 6 | opeq1i | |
8 | 5 7 | preq12i | |
9 | 3 8 | eqtr4i | |
10 | 9 | grpbase | |
11 | 1 10 | ax-mp | |