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	⊢ 𝑆 = { 𝐴 , 𝐵 }
	mgm2nsgrp.b	⊢ ( Base ‘ 𝑀 ) = 𝑆
	mgm2nsgrp.o	⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) )
Assertion	mgm2nsgrplem1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝑀 ∈ Mgm )

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	⊢ 𝑆 = { 𝐴 , 𝐵 }
2		mgm2nsgrp.b	⊢ ( Base ‘ 𝑀 ) = 𝑆
3		mgm2nsgrp.o	⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) )
4		prid1g	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 , 𝐵 } )
5	4 1	eleqtrrdi	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑆 )
6		prid2g	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ { 𝐴 , 𝐵 } )
7	6 1	eleqtrrdi	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ 𝑆 )
8	2	eqcomi	⊢ 𝑆 = ( Base ‘ 𝑀 )
9		ne0i	⊢ ( 𝐴 ∈ 𝑆 → 𝑆 ≠ ∅ )
10	9	adantr	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝑆 ≠ ∅ )
11		simplr	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝐵 ∈ 𝑆 )
12		simpll	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝐴 ∈ 𝑆 )
13	8 3 10 11 12	opifismgm	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝑀 ∈ Mgm )
14	5 7 13	syl2an	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝑀 ∈ Mgm )