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 )