Metamath Proof Explorer

Theorem grpplusg

Description: The operation of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypothesis grpfn.g 
|- G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. }
Assertion grpplusg 
|- ( .+ e. V -> .+ = ( +g ` G ) )

Proof

Step Hyp Ref Expression
1 grpfn.g 
 |-  G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. }
2 df-plusg 
 |-  +g = Slot 2
3 1lt2 
 |-  1 < 2
4 2nn 
 |-  2 e. NN
5 1 2 3 4 2strop 
 |-  ( .+ e. V -> .+ = ( +g ` G ) )