Metamath Proof Explorer

Theorem sgrp2nmndlem5

Description: Lemma 5 for sgrp2nmnd : M is not a monoid. (Contributed by AV, 29-Jan-2020)

Ref Expression
Hypotheses mgm2nsgrp.s 
|- S = { A , B }
mgm2nsgrp.b 
|- ( Base ` M ) = S
sgrp2nmnd.o 
|- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )
Assertion sgrp2nmndlem5 
|- ( ( # ` S ) = 2 -> M e/ Mnd )

Proof

Step Hyp Ref Expression
1 mgm2nsgrp.s 
 |-  S = { A , B }
2 mgm2nsgrp.b 
 |-  ( Base ` M ) = S
3 sgrp2nmnd.o 
 |-  ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )
4 1 hashprdifel 
 |-  ( ( # ` S ) = 2 -> ( A e. S /\ B e. S /\ A =/= B ) )
5 eqid 
 |-  ( +g ` M ) = ( +g ` M )
6 1 2 3 5 sgrp2nmndlem2 
 |-  ( ( A e. S /\ B e. S ) -> ( A ( +g ` M ) B ) = A )
7 6 3adant3 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( A ( +g ` M ) B ) = A )
8 simp3 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> A =/= B )
9 7 8 eqnetrd 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( A ( +g ` M ) B ) =/= B )
10 9 olcd 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( A ( +g ` M ) A ) =/= A \/ ( A ( +g ` M ) B ) =/= B ) )
11 oveq2 
 |-  ( y = A -> ( A ( +g ` M ) y ) = ( A ( +g ` M ) A ) )
12 id 
 |-  ( y = A -> y = A )
13 11 12 neeq12d 
 |-  ( y = A -> ( ( A ( +g ` M ) y ) =/= y <-> ( A ( +g ` M ) A ) =/= A ) )
14 oveq2 
 |-  ( y = B -> ( A ( +g ` M ) y ) = ( A ( +g ` M ) B ) )
15 id 
 |-  ( y = B -> y = B )
16 14 15 neeq12d 
 |-  ( y = B -> ( ( A ( +g ` M ) y ) =/= y <-> ( A ( +g ` M ) B ) =/= B ) )
17 13 16 rexprg 
 |-  ( ( A e. S /\ B e. S ) -> ( E. y e. { A , B } ( A ( +g ` M ) y ) =/= y <-> ( ( A ( +g ` M ) A ) =/= A \/ ( A ( +g ` M ) B ) =/= B ) ) )
18 17 3adant3 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( E. y e. { A , B } ( A ( +g ` M ) y ) =/= y <-> ( ( A ( +g ` M ) A ) =/= A \/ ( A ( +g ` M ) B ) =/= B ) ) )
19 10 18 mpbird 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> E. y e. { A , B } ( A ( +g ` M ) y ) =/= y )
20 1 2 3 5 sgrp2nmndlem3 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( B ( +g ` M ) A ) = B )
21 necom 
 |-  ( A =/= B <-> B =/= A )
22 df-ne 
 |-  ( B =/= A <-> -. B = A )
23 21 22 sylbb 
 |-  ( A =/= B -> -. B = A )
24 23 3ad2ant3 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> -. B = A )
25 24 adantr 
 |-  ( ( ( A e. S /\ B e. S /\ A =/= B ) /\ ( B ( +g ` M ) A ) = B ) -> -. B = A )
26 eqeq1 
 |-  ( ( B ( +g ` M ) A ) = B -> ( ( B ( +g ` M ) A ) = A <-> B = A ) )
27 26 adantl 
 |-  ( ( ( A e. S /\ B e. S /\ A =/= B ) /\ ( B ( +g ` M ) A ) = B ) -> ( ( B ( +g ` M ) A ) = A <-> B = A ) )
28 25 27 mtbird 
 |-  ( ( ( A e. S /\ B e. S /\ A =/= B ) /\ ( B ( +g ` M ) A ) = B ) -> -. ( B ( +g ` M ) A ) = A )
29 20 28 mpdan 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> -. ( B ( +g ` M ) A ) = A )
30 29 neqned 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( B ( +g ` M ) A ) =/= A )
31 30 orcd 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( B ( +g ` M ) A ) =/= A \/ ( B ( +g ` M ) B ) =/= B ) )
32 oveq2 
 |-  ( y = A -> ( B ( +g ` M ) y ) = ( B ( +g ` M ) A ) )
33 32 12 neeq12d 
 |-  ( y = A -> ( ( B ( +g ` M ) y ) =/= y <-> ( B ( +g ` M ) A ) =/= A ) )
34 oveq2 
 |-  ( y = B -> ( B ( +g ` M ) y ) = ( B ( +g ` M ) B ) )
35 34 15 neeq12d 
 |-  ( y = B -> ( ( B ( +g ` M ) y ) =/= y <-> ( B ( +g ` M ) B ) =/= B ) )
36 33 35 rexprg 
 |-  ( ( A e. S /\ B e. S ) -> ( E. y e. { A , B } ( B ( +g ` M ) y ) =/= y <-> ( ( B ( +g ` M ) A ) =/= A \/ ( B ( +g ` M ) B ) =/= B ) ) )
37 36 3adant3 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( E. y e. { A , B } ( B ( +g ` M ) y ) =/= y <-> ( ( B ( +g ` M ) A ) =/= A \/ ( B ( +g ` M ) B ) =/= B ) ) )
38 31 37 mpbird 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> E. y e. { A , B } ( B ( +g ` M ) y ) =/= y )
39 oveq1 
 |-  ( x = A -> ( x ( +g ` M ) y ) = ( A ( +g ` M ) y ) )
40 39 neeq1d 
 |-  ( x = A -> ( ( x ( +g ` M ) y ) =/= y <-> ( A ( +g ` M ) y ) =/= y ) )
41 40 rexbidv 
 |-  ( x = A -> ( E. y e. { A , B } ( x ( +g ` M ) y ) =/= y <-> E. y e. { A , B } ( A ( +g ` M ) y ) =/= y ) )
42 oveq1 
 |-  ( x = B -> ( x ( +g ` M ) y ) = ( B ( +g ` M ) y ) )
43 42 neeq1d 
 |-  ( x = B -> ( ( x ( +g ` M ) y ) =/= y <-> ( B ( +g ` M ) y ) =/= y ) )
44 43 rexbidv 
 |-  ( x = B -> ( E. y e. { A , B } ( x ( +g ` M ) y ) =/= y <-> E. y e. { A , B } ( B ( +g ` M ) y ) =/= y ) )
45 41 44 ralprg 
 |-  ( ( A e. S /\ B e. S ) -> ( A. x e. { A , B } E. y e. { A , B } ( x ( +g ` M ) y ) =/= y <-> ( E. y e. { A , B } ( A ( +g ` M ) y ) =/= y /\ E. y e. { A , B } ( B ( +g ` M ) y ) =/= y ) ) )
46 45 3adant3 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( A. x e. { A , B } E. y e. { A , B } ( x ( +g ` M ) y ) =/= y <-> ( E. y e. { A , B } ( A ( +g ` M ) y ) =/= y /\ E. y e. { A , B } ( B ( +g ` M ) y ) =/= y ) ) )
47 19 38 46 mpbir2and 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> A. x e. { A , B } E. y e. { A , B } ( x ( +g ` M ) y ) =/= y )
48 2 1 eqtr2i 
 |-  { A , B } = ( Base ` M )
49 48 5 isnmnd 
 |-  ( A. x e. { A , B } E. y e. { A , B } ( x ( +g ` M ) y ) =/= y -> M e/ Mnd )
50 4 47 49 3syl 
 |-  ( ( # ` S ) = 2 -> M e/ Mnd )