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	|- S = { A , B }
	mgm2nsgrp.b	|- ( Base ` M ) = S
	mgm2nsgrp.o	|- ( +g ` M ) = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) )
Assertion	mgm2nsgrplem4	|- ( ( # ` S ) = 2 -> M e/ Smgrp )

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	|- S = { A , B }
2		mgm2nsgrp.b	|- ( Base ` M ) = S
3		mgm2nsgrp.o	|- ( +g ` M ) = ( x e. S , y e. S |-> if ( ( x = A /\ y = A ) , B , A ) )
4	1	hashprdifel	|- ( ( # ` S ) = 2 -> ( A e. S /\ B e. S /\ A =/= B ) )
5		simp1	|- ( ( A e. S /\ B e. S /\ A =/= B ) -> A e. S )
6		simp2	|- ( ( A e. S /\ B e. S /\ A =/= B ) -> B e. S )
7	5 5 6	3jca	|- ( ( A e. S /\ B e. S /\ A =/= B ) -> ( A e. S /\ A e. S /\ B e. S ) )
8	4 7	syl	|- ( ( # ` S ) = 2 -> ( A e. S /\ A e. S /\ B e. S ) )
9		simp3	|- ( ( A e. S /\ B e. S /\ A =/= B ) -> A =/= B )
10		eqid	|- ( +g ` M ) = ( +g ` M )
11	1 2 3 10	mgm2nsgrplem2	|- ( ( A e. S /\ B e. S ) -> ( ( A ( +g ` M ) A ) ( +g ` M ) B ) = A )
12	11	3adant3	|- ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( A ( +g ` M ) A ) ( +g ` M ) B ) = A )
13	1 2 3 10	mgm2nsgrplem3	|- ( ( A e. S /\ B e. S ) -> ( A ( +g ` M ) ( A ( +g ` M ) B ) ) = B )
14	13	3adant3	|- ( ( A e. S /\ B e. S /\ A =/= B ) -> ( A ( +g ` M ) ( A ( +g ` M ) B ) ) = B )
15	9 12 14	3netr4d	|- ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( A ( +g ` M ) A ) ( +g ` M ) B ) =/= ( A ( +g ` M ) ( A ( +g ` M ) B ) ) )
16	4 15	syl	|- ( ( # ` S ) = 2 -> ( ( A ( +g ` M ) A ) ( +g ` M ) B ) =/= ( A ( +g ` M ) ( A ( +g ` M ) B ) ) )
17	2	eqcomi	|- S = ( Base ` M )
18	17 10	isnsgrp	|- ( ( A e. S /\ A e. S /\ B e. S ) -> ( ( ( A ( +g ` M ) A ) ( +g ` M ) B ) =/= ( A ( +g ` M ) ( A ( +g ` M ) B ) ) -> M e/ Smgrp ) )
19	8 16 18	sylc	|- ( ( # ` S ) = 2 -> M e/ Smgrp )