Metamath Proof Explorer


Theorem grpbasex

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 BV
grpstrx.p +˙V
grpstrx.g G=1B2+˙
Assertion grpbasex B=BaseG

Proof

Step Hyp Ref Expression
1 grpstrx.b BV
2 grpstrx.p +˙V
3 grpstrx.g G=1B2+˙
4 basendx Basendx=1
5 4 opeq1i BasendxB=1B
6 plusgndx +ndx=2
7 6 opeq1i +ndx+˙=2+˙
8 5 7 preq12i BasendxB+ndx+˙=1B2+˙
9 3 8 eqtr4i G=BasendxB+ndx+˙
10 9 grpbase BVB=BaseG
11 1 10 ax-mp B=BaseG