Metamath Proof Explorer


Theorem mgm2nsgrplem4

Description: Lemma 4 for mgm2nsgrp : M is not a semigroup. (Contributed by AV, 28-Jan-2020) (Proof shortened by AV, 31-Jan-2020)

Ref Expression
Hypotheses mgm2nsgrp.s 𝑆 = { 𝐴 , 𝐵 }
mgm2nsgrp.b ( Base ‘ 𝑀 ) = 𝑆
mgm2nsgrp.o ( +g𝑀 ) = ( 𝑥𝑆 , 𝑦𝑆 ↦ if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) )
Assertion mgm2nsgrplem4 ( ( ♯ ‘ 𝑆 ) = 2 → 𝑀 ∉ Smgrp )

Proof

Step Hyp Ref Expression
1 mgm2nsgrp.s 𝑆 = { 𝐴 , 𝐵 }
2 mgm2nsgrp.b ( Base ‘ 𝑀 ) = 𝑆
3 mgm2nsgrp.o ( +g𝑀 ) = ( 𝑥𝑆 , 𝑦𝑆 ↦ if ( ( 𝑥 = 𝐴𝑦 = 𝐴 ) , 𝐵 , 𝐴 ) )
4 1 hashprdifel ( ( ♯ ‘ 𝑆 ) = 2 → ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) )
5 simp1 ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) → 𝐴𝑆 )
6 simp2 ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) → 𝐵𝑆 )
7 5 5 6 3jca ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) → ( 𝐴𝑆𝐴𝑆𝐵𝑆 ) )
8 4 7 syl ( ( ♯ ‘ 𝑆 ) = 2 → ( 𝐴𝑆𝐴𝑆𝐵𝑆 ) )
9 simp3 ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) → 𝐴𝐵 )
10 eqid ( +g𝑀 ) = ( +g𝑀 )
11 1 2 3 10 mgm2nsgrplem2 ( ( 𝐴𝑆𝐵𝑆 ) → ( ( 𝐴 ( +g𝑀 ) 𝐴 ) ( +g𝑀 ) 𝐵 ) = 𝐴 )
12 11 3adant3 ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) → ( ( 𝐴 ( +g𝑀 ) 𝐴 ) ( +g𝑀 ) 𝐵 ) = 𝐴 )
13 1 2 3 10 mgm2nsgrplem3 ( ( 𝐴𝑆𝐵𝑆 ) → ( 𝐴 ( +g𝑀 ) ( 𝐴 ( +g𝑀 ) 𝐵 ) ) = 𝐵 )
14 13 3adant3 ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) → ( 𝐴 ( +g𝑀 ) ( 𝐴 ( +g𝑀 ) 𝐵 ) ) = 𝐵 )
15 9 12 14 3netr4d ( ( 𝐴𝑆𝐵𝑆𝐴𝐵 ) → ( ( 𝐴 ( +g𝑀 ) 𝐴 ) ( +g𝑀 ) 𝐵 ) ≠ ( 𝐴 ( +g𝑀 ) ( 𝐴 ( +g𝑀 ) 𝐵 ) ) )
16 4 15 syl ( ( ♯ ‘ 𝑆 ) = 2 → ( ( 𝐴 ( +g𝑀 ) 𝐴 ) ( +g𝑀 ) 𝐵 ) ≠ ( 𝐴 ( +g𝑀 ) ( 𝐴 ( +g𝑀 ) 𝐵 ) ) )
17 2 eqcomi 𝑆 = ( Base ‘ 𝑀 )
18 17 10 isnsgrp ( ( 𝐴𝑆𝐴𝑆𝐵𝑆 ) → ( ( ( 𝐴 ( +g𝑀 ) 𝐴 ) ( +g𝑀 ) 𝐵 ) ≠ ( 𝐴 ( +g𝑀 ) ( 𝐴 ( +g𝑀 ) 𝐵 ) ) → 𝑀 ∉ Smgrp ) )
19 8 16 18 sylc ( ( ♯ ‘ 𝑆 ) = 2 → 𝑀 ∉ Smgrp )