Metamath Proof Explorer


Theorem sgrpplusgaopALT

Description: Slot 2 (group operation) of a semigroup as extensible structure is an associative operation on the base set. (Contributed by AV, 13-Jan-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion sgrpplusgaopALT Could not format assertion : No typesetting found for |- ( G e. Smgrp -> ( +g ` G ) assLaw ( Base ` G ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 simpr G Mgm x Base G y Base G z Base G x + G y + G z = x + G y + G z x Base G y Base G z Base G x + G y + G z = x + G y + G z
2 eqid Base G = Base G
3 eqid + G = + G
4 2 3 issgrp Could not format ( G e. Smgrp <-> ( G e. Mgm /\ A. x e. ( Base ` G ) A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) ) ) : No typesetting found for |- ( G e. Smgrp <-> ( G e. Mgm /\ A. x e. ( Base ` G ) A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) ) ) with typecode |-
5 fvex + G V
6 fvex Base G V
7 isasslaw + G V Base G V + G assLaw Base G x Base G y Base G z Base G x + G y + G z = x + G y + G z
8 5 6 7 mp2an + G assLaw Base G x Base G y Base G z Base G x + G y + G z = x + G y + G z
9 1 4 8 3imtr4i Could not format ( G e. Smgrp -> ( +g ` G ) assLaw ( Base ` G ) ) : No typesetting found for |- ( G e. Smgrp -> ( +g ` G ) assLaw ( Base ` G ) ) with typecode |-