Metamath Proof Explorer


Theorem mgm2nsgrplem1

Description: Lemma 1 for mgm2nsgrp : M is a magma, even if A = B ( M is the trivial magma in this case, see mgmb1mgm1 ). (Contributed by AV, 27-Jan-2020)

Ref Expression
Hypotheses mgm2nsgrp.s S=AB
mgm2nsgrp.b BaseM=S
mgm2nsgrp.o +M=xS,ySifx=Ay=ABA
Assertion mgm2nsgrplem1 AVBWMMgm

Proof

Step Hyp Ref Expression
1 mgm2nsgrp.s S=AB
2 mgm2nsgrp.b BaseM=S
3 mgm2nsgrp.o +M=xS,ySifx=Ay=ABA
4 prid1g AVAAB
5 4 1 eleqtrrdi AVAS
6 prid2g BWBAB
7 6 1 eleqtrrdi BWBS
8 2 eqcomi S=BaseM
9 ne0i ASS
10 9 adantr ASBSS
11 simplr ASBSxSySBS
12 simpll ASBSxSySAS
13 8 3 10 11 12 opifismgm ASBSMMgm
14 5 7 13 syl2an AVBWMMgm