Metamath Proof Explorer


Theorem mgmplusgiopALT

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

Ref Expression
Assertion mgmplusgiopALT M Mgm + M clLaw Base M

Proof

Step Hyp Ref Expression
1 eqid Base M = Base M
2 eqid + M = + M
3 1 2 mgmcl M Mgm x Base M y Base M x + M y Base M
4 3 3expb M Mgm x Base M y Base M x + M y Base M
5 4 ralrimivva M Mgm x Base M y Base M x + M y Base M
6 fvex + M V
7 fvex Base M V
8 6 7 pm3.2i + M V Base M V
9 iscllaw + M V Base M V + M clLaw Base M x Base M y Base M x + M y Base M
10 8 9 mp1i M Mgm + M clLaw Base M x Base M y Base M x + M y Base M
11 5 10 mpbird M Mgm + M clLaw Base M