Metamath Proof Explorer


Theorem sgrp2nmndlem1

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

Ref Expression
Hypotheses mgm2nsgrp.s S = A B
mgm2nsgrp.b Base M = S
sgrp2nmnd.o + M = x S , y S if x = A A B
Assertion sgrp2nmndlem1 A V B W M Mgm

Proof

Step Hyp Ref Expression
1 mgm2nsgrp.s S = A B
2 mgm2nsgrp.b Base M = S
3 sgrp2nmnd.o + M = x S , y S if x = A A B
4 prid1g A V A A B
5 4 1 eleqtrrdi A V A S
6 prid2g B W B A B
7 6 1 eleqtrrdi B W B S
8 2 eqcomi S = Base M
9 ne0i A S S
10 9 adantr A S B S S
11 simpll A S B S x S y S A S
12 simplr A S B S x S y S B S
13 8 3 10 11 12 opifismgm A S B S M Mgm
14 5 7 13 syl2an A V B W M Mgm