Description: The operation of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013) (Revised by Mario Carneiro, 30-Apr-2015) (Revised by AV, 27-Oct-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | grpfn.g | |- G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } |
|
| Assertion | grpplusg | |- ( .+ e. V -> .+ = ( +g ` G ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | grpfn.g | |- G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } |
|
| 2 | basendxltplusgndx | |- ( Base ` ndx ) < ( +g ` ndx ) |
|
| 3 | plusgndxnn | |- ( +g ` ndx ) e. NN |
|
| 4 | plusgid | |- +g = Slot ( +g ` ndx ) |
|
| 5 | 1 2 3 4 | 2strop1 | |- ( .+ e. V -> .+ = ( +g ` G ) ) |