Metamath Proof Explorer

Theorem sgrp2nmndlem4

Description: Lemma 4 for sgrp2nmnd : M is a semigroup. (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 sgrp2nmndlem4 
|- ( ( # ` S ) = 2 -> M e. Smgrp )

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 3simpa 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( A e. S /\ B e. S ) )
6 1 2 3 sgrp2nmndlem1 
 |-  ( ( A e. S /\ B e. S ) -> M e. Mgm )
7 4 5 6 3syl 
 |-  ( ( # ` S ) = 2 -> M e. Mgm )
8 eqid 
 |-  ( +g ` M ) = ( +g ` M )
9 1 2 3 8 sgrp2nmndlem2 
 |-  ( ( A e. S /\ A e. S ) -> ( A ( +g ` M ) A ) = A )
10 9 oveq1d 
 |-  ( ( A e. S /\ A e. S ) -> ( ( A ( +g ` M ) A ) ( +g ` M ) A ) = ( A ( +g ` M ) A ) )
11 9 oveq2d 
 |-  ( ( A e. S /\ A e. S ) -> ( A ( +g ` M ) ( A ( +g ` M ) A ) ) = ( A ( +g ` M ) A ) )
12 10 11 eqtr4d 
 |-  ( ( A e. S /\ A e. S ) -> ( ( A ( +g ` M ) A ) ( +g ` M ) A ) = ( A ( +g ` M ) ( A ( +g ` M ) A ) ) )
13 12 anidms 
 |-  ( A e. S -> ( ( A ( +g ` M ) A ) ( +g ` M ) A ) = ( A ( +g ` M ) ( A ( +g ` M ) A ) ) )
14 13 3ad2ant1 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( A ( +g ` M ) A ) ( +g ` M ) A ) = ( A ( +g ` M ) ( A ( +g ` M ) A ) ) )
15 9 anidms 
 |-  ( A e. S -> ( A ( +g ` M ) A ) = A )
16 15 adantr 
 |-  ( ( A e. S /\ B e. S ) -> ( A ( +g ` M ) A ) = A )
17 16 oveq1d 
 |-  ( ( A e. S /\ B e. S ) -> ( ( A ( +g ` M ) A ) ( +g ` M ) B ) = ( A ( +g ` M ) B ) )
18 1 2 3 8 sgrp2nmndlem2 
 |-  ( ( A e. S /\ B e. S ) -> ( A ( +g ` M ) B ) = A )
19 18 oveq2d 
 |-  ( ( A e. S /\ B e. S ) -> ( A ( +g ` M ) ( A ( +g ` M ) B ) ) = ( A ( +g ` M ) A ) )
20 16 19 18 3eqtr4rd 
 |-  ( ( A e. S /\ B e. S ) -> ( A ( +g ` M ) B ) = ( A ( +g ` M ) ( A ( +g ` M ) B ) ) )
21 17 20 eqtrd 
 |-  ( ( A e. S /\ B e. S ) -> ( ( A ( +g ` M ) A ) ( +g ` M ) B ) = ( A ( +g ` M ) ( A ( +g ` M ) B ) ) )
22 21 3adant3 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( A ( +g ` M ) A ) ( +g ` M ) B ) = ( A ( +g ` M ) ( A ( +g ` M ) B ) ) )
23 14 22 jca 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( ( A ( +g ` M ) A ) ( +g ` M ) A ) = ( A ( +g ` M ) ( A ( +g ` M ) A ) ) /\ ( ( A ( +g ` M ) A ) ( +g ` M ) B ) = ( A ( +g ` M ) ( A ( +g ` M ) B ) ) ) )
24 18 3adant3 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( A ( +g ` M ) B ) = A )
25 1 2 3 8 sgrp2nmndlem3 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( B ( +g ` M ) A ) = B )
26 25 oveq2d 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( A ( +g ` M ) ( B ( +g ` M ) A ) ) = ( A ( +g ` M ) B ) )
27 24 oveq1d 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( A ( +g ` M ) B ) ( +g ` M ) A ) = ( A ( +g ` M ) A ) )
28 15 3ad2ant1 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( A ( +g ` M ) A ) = A )
29 27 28 eqtrd 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( A ( +g ` M ) B ) ( +g ` M ) A ) = A )
30 24 26 29 3eqtr4rd 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( A ( +g ` M ) B ) ( +g ` M ) A ) = ( A ( +g ` M ) ( B ( +g ` M ) A ) ) )
31 simp2 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> B e. S )
32 1 2 3 8 sgrp2nmndlem3 
 |-  ( ( B e. S /\ B e. S /\ A =/= B ) -> ( B ( +g ` M ) B ) = B )
33 31 32 syld3an1 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( B ( +g ` M ) B ) = B )
34 33 oveq2d 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( A ( +g ` M ) ( B ( +g ` M ) B ) ) = ( A ( +g ` M ) B ) )
35 18 oveq1d 
 |-  ( ( A e. S /\ B e. S ) -> ( ( A ( +g ` M ) B ) ( +g ` M ) B ) = ( A ( +g ` M ) B ) )
36 35 18 eqtrd 
 |-  ( ( A e. S /\ B e. S ) -> ( ( A ( +g ` M ) B ) ( +g ` M ) B ) = A )
37 36 3adant3 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( A ( +g ` M ) B ) ( +g ` M ) B ) = A )
38 24 34 37 3eqtr4rd 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( A ( +g ` M ) B ) ( +g ` M ) B ) = ( A ( +g ` M ) ( B ( +g ` M ) B ) ) )
39 23 30 38 jca32 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( ( ( A ( +g ` M ) A ) ( +g ` M ) A ) = ( A ( +g ` M ) ( A ( +g ` M ) A ) ) /\ ( ( A ( +g ` M ) A ) ( +g ` M ) B ) = ( A ( +g ` M ) ( A ( +g ` M ) B ) ) ) /\ ( ( ( A ( +g ` M ) B ) ( +g ` M ) A ) = ( A ( +g ` M ) ( B ( +g ` M ) A ) ) /\ ( ( A ( +g ` M ) B ) ( +g ` M ) B ) = ( A ( +g ` M ) ( B ( +g ` M ) B ) ) ) ) )
40 25 oveq1d 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( B ( +g ` M ) A ) ( +g ` M ) A ) = ( B ( +g ` M ) A ) )
41 28 oveq2d 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( B ( +g ` M ) ( A ( +g ` M ) A ) ) = ( B ( +g ` M ) A ) )
42 40 41 eqtr4d 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( B ( +g ` M ) A ) ( +g ` M ) A ) = ( B ( +g ` M ) ( A ( +g ` M ) A ) ) )
43 24 oveq2d 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( B ( +g ` M ) ( A ( +g ` M ) B ) ) = ( B ( +g ` M ) A ) )
44 25 oveq1d 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( B ( +g ` M ) A ) ( +g ` M ) B ) = ( B ( +g ` M ) B ) )
45 44 33 eqtrd 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( B ( +g ` M ) A ) ( +g ` M ) B ) = B )
46 25 43 45 3eqtr4rd 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( B ( +g ` M ) A ) ( +g ` M ) B ) = ( B ( +g ` M ) ( A ( +g ` M ) B ) ) )
47 42 46 jca 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( ( B ( +g ` M ) A ) ( +g ` M ) A ) = ( B ( +g ` M ) ( A ( +g ` M ) A ) ) /\ ( ( B ( +g ` M ) A ) ( +g ` M ) B ) = ( B ( +g ` M ) ( A ( +g ` M ) B ) ) ) )
48 25 oveq2d 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( B ( +g ` M ) ( B ( +g ` M ) A ) ) = ( B ( +g ` M ) B ) )
49 33 oveq1d 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( B ( +g ` M ) B ) ( +g ` M ) A ) = ( B ( +g ` M ) A ) )
50 49 25 eqtrd 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( B ( +g ` M ) B ) ( +g ` M ) A ) = B )
51 33 48 50 3eqtr4rd 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( B ( +g ` M ) B ) ( +g ` M ) A ) = ( B ( +g ` M ) ( B ( +g ` M ) A ) ) )
52 32 oveq1d 
 |-  ( ( B e. S /\ B e. S /\ A =/= B ) -> ( ( B ( +g ` M ) B ) ( +g ` M ) B ) = ( B ( +g ` M ) B ) )
53 32 oveq2d 
 |-  ( ( B e. S /\ B e. S /\ A =/= B ) -> ( B ( +g ` M ) ( B ( +g ` M ) B ) ) = ( B ( +g ` M ) B ) )
54 52 53 eqtr4d 
 |-  ( ( B e. S /\ B e. S /\ A =/= B ) -> ( ( B ( +g ` M ) B ) ( +g ` M ) B ) = ( B ( +g ` M ) ( B ( +g ` M ) B ) ) )
55 31 54 syld3an1 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( B ( +g ` M ) B ) ( +g ` M ) B ) = ( B ( +g ` M ) ( B ( +g ` M ) B ) ) )
56 47 51 55 jca32 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( ( ( ( B ( +g ` M ) A ) ( +g ` M ) A ) = ( B ( +g ` M ) ( A ( +g ` M ) A ) ) /\ ( ( B ( +g ` M ) A ) ( +g ` M ) B ) = ( B ( +g ` M ) ( A ( +g ` M ) B ) ) ) /\ ( ( ( B ( +g ` M ) B ) ( +g ` M ) A ) = ( B ( +g ` M ) ( B ( +g ` M ) A ) ) /\ ( ( B ( +g ` M ) B ) ( +g ` M ) B ) = ( B ( +g ` M ) ( B ( +g ` M ) B ) ) ) ) )
57 oveq1 
 |-  ( a = A -> ( a ( +g ` M ) b ) = ( A ( +g ` M ) b ) )
58 57 oveq1d 
 |-  ( a = A -> ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( ( A ( +g ` M ) b ) ( +g ` M ) c ) )
59 oveq1 
 |-  ( a = A -> ( a ( +g ` M ) ( b ( +g ` M ) c ) ) = ( A ( +g ` M ) ( b ( +g ` M ) c ) ) )
60 58 59 eqeq12d 
 |-  ( a = A -> ( ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) <-> ( ( A ( +g ` M ) b ) ( +g ` M ) c ) = ( A ( +g ` M ) ( b ( +g ` M ) c ) ) ) )
61 60 2ralbidv 
 |-  ( a = A -> ( A. b e. { A , B } A. c e. { A , B } ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) <-> A. b e. { A , B } A. c e. { A , B } ( ( A ( +g ` M ) b ) ( +g ` M ) c ) = ( A ( +g ` M ) ( b ( +g ` M ) c ) ) ) )
62 oveq1 
 |-  ( a = B -> ( a ( +g ` M ) b ) = ( B ( +g ` M ) b ) )
63 62 oveq1d 
 |-  ( a = B -> ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( ( B ( +g ` M ) b ) ( +g ` M ) c ) )
64 oveq1 
 |-  ( a = B -> ( a ( +g ` M ) ( b ( +g ` M ) c ) ) = ( B ( +g ` M ) ( b ( +g ` M ) c ) ) )
65 63 64 eqeq12d 
 |-  ( a = B -> ( ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) <-> ( ( B ( +g ` M ) b ) ( +g ` M ) c ) = ( B ( +g ` M ) ( b ( +g ` M ) c ) ) ) )
66 65 2ralbidv 
 |-  ( a = B -> ( A. b e. { A , B } A. c e. { A , B } ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) <-> A. b e. { A , B } A. c e. { A , B } ( ( B ( +g ` M ) b ) ( +g ` M ) c ) = ( B ( +g ` M ) ( b ( +g ` M ) c ) ) ) )
67 61 66 ralprg 
 |-  ( ( A e. S /\ B e. S ) -> ( A. a e. { A , B } A. b e. { A , B } A. c e. { A , B } ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) <-> ( A. b e. { A , B } A. c e. { A , B } ( ( A ( +g ` M ) b ) ( +g ` M ) c ) = ( A ( +g ` M ) ( b ( +g ` M ) c ) ) /\ A. b e. { A , B } A. c e. { A , B } ( ( B ( +g ` M ) b ) ( +g ` M ) c ) = ( B ( +g ` M ) ( b ( +g ` M ) c ) ) ) ) )
68 oveq2 
 |-  ( b = A -> ( A ( +g ` M ) b ) = ( A ( +g ` M ) A ) )
69 68 oveq1d 
 |-  ( b = A -> ( ( A ( +g ` M ) b ) ( +g ` M ) c ) = ( ( A ( +g ` M ) A ) ( +g ` M ) c ) )
70 oveq1 
 |-  ( b = A -> ( b ( +g ` M ) c ) = ( A ( +g ` M ) c ) )
71 70 oveq2d 
 |-  ( b = A -> ( A ( +g ` M ) ( b ( +g ` M ) c ) ) = ( A ( +g ` M ) ( A ( +g ` M ) c ) ) )
72 69 71 eqeq12d 
 |-  ( b = A -> ( ( ( A ( +g ` M ) b ) ( +g ` M ) c ) = ( A ( +g ` M ) ( b ( +g ` M ) c ) ) <-> ( ( A ( +g ` M ) A ) ( +g ` M ) c ) = ( A ( +g ` M ) ( A ( +g ` M ) c ) ) ) )
73 72 ralbidv 
 |-  ( b = A -> ( A. c e. { A , B } ( ( A ( +g ` M ) b ) ( +g ` M ) c ) = ( A ( +g ` M ) ( b ( +g ` M ) c ) ) <-> A. c e. { A , B } ( ( A ( +g ` M ) A ) ( +g ` M ) c ) = ( A ( +g ` M ) ( A ( +g ` M ) c ) ) ) )
74 oveq2 
 |-  ( b = B -> ( A ( +g ` M ) b ) = ( A ( +g ` M ) B ) )
75 74 oveq1d 
 |-  ( b = B -> ( ( A ( +g ` M ) b ) ( +g ` M ) c ) = ( ( A ( +g ` M ) B ) ( +g ` M ) c ) )
76 oveq1 
 |-  ( b = B -> ( b ( +g ` M ) c ) = ( B ( +g ` M ) c ) )
77 76 oveq2d 
 |-  ( b = B -> ( A ( +g ` M ) ( b ( +g ` M ) c ) ) = ( A ( +g ` M ) ( B ( +g ` M ) c ) ) )
78 75 77 eqeq12d 
 |-  ( b = B -> ( ( ( A ( +g ` M ) b ) ( +g ` M ) c ) = ( A ( +g ` M ) ( b ( +g ` M ) c ) ) <-> ( ( A ( +g ` M ) B ) ( +g ` M ) c ) = ( A ( +g ` M ) ( B ( +g ` M ) c ) ) ) )
79 78 ralbidv 
 |-  ( b = B -> ( A. c e. { A , B } ( ( A ( +g ` M ) b ) ( +g ` M ) c ) = ( A ( +g ` M ) ( b ( +g ` M ) c ) ) <-> A. c e. { A , B } ( ( A ( +g ` M ) B ) ( +g ` M ) c ) = ( A ( +g ` M ) ( B ( +g ` M ) c ) ) ) )
80 73 79 ralprg 
 |-  ( ( A e. S /\ B e. S ) -> ( A. b e. { A , B } A. c e. { A , B } ( ( A ( +g ` M ) b ) ( +g ` M ) c ) = ( A ( +g ` M ) ( b ( +g ` M ) c ) ) <-> ( A. c e. { A , B } ( ( A ( +g ` M ) A ) ( +g ` M ) c ) = ( A ( +g ` M ) ( A ( +g ` M ) c ) ) /\ A. c e. { A , B } ( ( A ( +g ` M ) B ) ( +g ` M ) c ) = ( A ( +g ` M ) ( B ( +g ` M ) c ) ) ) ) )
81 oveq2 
 |-  ( b = A -> ( B ( +g ` M ) b ) = ( B ( +g ` M ) A ) )
82 81 oveq1d 
 |-  ( b = A -> ( ( B ( +g ` M ) b ) ( +g ` M ) c ) = ( ( B ( +g ` M ) A ) ( +g ` M ) c ) )
83 70 oveq2d 
 |-  ( b = A -> ( B ( +g ` M ) ( b ( +g ` M ) c ) ) = ( B ( +g ` M ) ( A ( +g ` M ) c ) ) )
84 82 83 eqeq12d 
 |-  ( b = A -> ( ( ( B ( +g ` M ) b ) ( +g ` M ) c ) = ( B ( +g ` M ) ( b ( +g ` M ) c ) ) <-> ( ( B ( +g ` M ) A ) ( +g ` M ) c ) = ( B ( +g ` M ) ( A ( +g ` M ) c ) ) ) )
85 84 ralbidv 
 |-  ( b = A -> ( A. c e. { A , B } ( ( B ( +g ` M ) b ) ( +g ` M ) c ) = ( B ( +g ` M ) ( b ( +g ` M ) c ) ) <-> A. c e. { A , B } ( ( B ( +g ` M ) A ) ( +g ` M ) c ) = ( B ( +g ` M ) ( A ( +g ` M ) c ) ) ) )
86 oveq2 
 |-  ( b = B -> ( B ( +g ` M ) b ) = ( B ( +g ` M ) B ) )
87 86 oveq1d 
 |-  ( b = B -> ( ( B ( +g ` M ) b ) ( +g ` M ) c ) = ( ( B ( +g ` M ) B ) ( +g ` M ) c ) )
88 76 oveq2d 
 |-  ( b = B -> ( B ( +g ` M ) ( b ( +g ` M ) c ) ) = ( B ( +g ` M ) ( B ( +g ` M ) c ) ) )
89 87 88 eqeq12d 
 |-  ( b = B -> ( ( ( B ( +g ` M ) b ) ( +g ` M ) c ) = ( B ( +g ` M ) ( b ( +g ` M ) c ) ) <-> ( ( B ( +g ` M ) B ) ( +g ` M ) c ) = ( B ( +g ` M ) ( B ( +g ` M ) c ) ) ) )
90 89 ralbidv 
 |-  ( b = B -> ( A. c e. { A , B } ( ( B ( +g ` M ) b ) ( +g ` M ) c ) = ( B ( +g ` M ) ( b ( +g ` M ) c ) ) <-> A. c e. { A , B } ( ( B ( +g ` M ) B ) ( +g ` M ) c ) = ( B ( +g ` M ) ( B ( +g ` M ) c ) ) ) )
91 85 90 ralprg 
 |-  ( ( A e. S /\ B e. S ) -> ( A. b e. { A , B } A. c e. { A , B } ( ( B ( +g ` M ) b ) ( +g ` M ) c ) = ( B ( +g ` M ) ( b ( +g ` M ) c ) ) <-> ( A. c e. { A , B } ( ( B ( +g ` M ) A ) ( +g ` M ) c ) = ( B ( +g ` M ) ( A ( +g ` M ) c ) ) /\ A. c e. { A , B } ( ( B ( +g ` M ) B ) ( +g ` M ) c ) = ( B ( +g ` M ) ( B ( +g ` M ) c ) ) ) ) )
92 80 91 anbi12d 
 |-  ( ( A e. S /\ B e. S ) -> ( ( A. b e. { A , B } A. c e. { A , B } ( ( A ( +g ` M ) b ) ( +g ` M ) c ) = ( A ( +g ` M ) ( b ( +g ` M ) c ) ) /\ A. b e. { A , B } A. c e. { A , B } ( ( B ( +g ` M ) b ) ( +g ` M ) c ) = ( B ( +g ` M ) ( b ( +g ` M ) c ) ) ) <-> ( ( A. c e. { A , B } ( ( A ( +g ` M ) A ) ( +g ` M ) c ) = ( A ( +g ` M ) ( A ( +g ` M ) c ) ) /\ A. c e. { A , B } ( ( A ( +g ` M ) B ) ( +g ` M ) c ) = ( A ( +g ` M ) ( B ( +g ` M ) c ) ) ) /\ ( A. c e. { A , B } ( ( B ( +g ` M ) A ) ( +g ` M ) c ) = ( B ( +g ` M ) ( A ( +g ` M ) c ) ) /\ A. c e. { A , B } ( ( B ( +g ` M ) B ) ( +g ` M ) c ) = ( B ( +g ` M ) ( B ( +g ` M ) c ) ) ) ) ) )
93 oveq2 
 |-  ( c = A -> ( ( A ( +g ` M ) A ) ( +g ` M ) c ) = ( ( A ( +g ` M ) A ) ( +g ` M ) A ) )
94 oveq2 
 |-  ( c = A -> ( A ( +g ` M ) c ) = ( A ( +g ` M ) A ) )
95 94 oveq2d 
 |-  ( c = A -> ( A ( +g ` M ) ( A ( +g ` M ) c ) ) = ( A ( +g ` M ) ( A ( +g ` M ) A ) ) )
96 93 95 eqeq12d 
 |-  ( c = A -> ( ( ( A ( +g ` M ) A ) ( +g ` M ) c ) = ( A ( +g ` M ) ( A ( +g ` M ) c ) ) <-> ( ( A ( +g ` M ) A ) ( +g ` M ) A ) = ( A ( +g ` M ) ( A ( +g ` M ) A ) ) ) )
97 oveq2 
 |-  ( c = B -> ( ( A ( +g ` M ) A ) ( +g ` M ) c ) = ( ( A ( +g ` M ) A ) ( +g ` M ) B ) )
98 oveq2 
 |-  ( c = B -> ( A ( +g ` M ) c ) = ( A ( +g ` M ) B ) )
99 98 oveq2d 
 |-  ( c = B -> ( A ( +g ` M ) ( A ( +g ` M ) c ) ) = ( A ( +g ` M ) ( A ( +g ` M ) B ) ) )
100 97 99 eqeq12d 
 |-  ( c = B -> ( ( ( A ( +g ` M ) A ) ( +g ` M ) c ) = ( A ( +g ` M ) ( A ( +g ` M ) c ) ) <-> ( ( A ( +g ` M ) A ) ( +g ` M ) B ) = ( A ( +g ` M ) ( A ( +g ` M ) B ) ) ) )
101 96 100 ralprg 
 |-  ( ( A e. S /\ B e. S ) -> ( A. c e. { A , B } ( ( A ( +g ` M ) A ) ( +g ` M ) c ) = ( A ( +g ` M ) ( A ( +g ` M ) c ) ) <-> ( ( ( A ( +g ` M ) A ) ( +g ` M ) A ) = ( A ( +g ` M ) ( A ( +g ` M ) A ) ) /\ ( ( A ( +g ` M ) A ) ( +g ` M ) B ) = ( A ( +g ` M ) ( A ( +g ` M ) B ) ) ) ) )
102 oveq2 
 |-  ( c = A -> ( ( A ( +g ` M ) B ) ( +g ` M ) c ) = ( ( A ( +g ` M ) B ) ( +g ` M ) A ) )
103 oveq2 
 |-  ( c = A -> ( B ( +g ` M ) c ) = ( B ( +g ` M ) A ) )
104 103 oveq2d 
 |-  ( c = A -> ( A ( +g ` M ) ( B ( +g ` M ) c ) ) = ( A ( +g ` M ) ( B ( +g ` M ) A ) ) )
105 102 104 eqeq12d 
 |-  ( c = A -> ( ( ( A ( +g ` M ) B ) ( +g ` M ) c ) = ( A ( +g ` M ) ( B ( +g ` M ) c ) ) <-> ( ( A ( +g ` M ) B ) ( +g ` M ) A ) = ( A ( +g ` M ) ( B ( +g ` M ) A ) ) ) )
106 oveq2 
 |-  ( c = B -> ( ( A ( +g ` M ) B ) ( +g ` M ) c ) = ( ( A ( +g ` M ) B ) ( +g ` M ) B ) )
107 oveq2 
 |-  ( c = B -> ( B ( +g ` M ) c ) = ( B ( +g ` M ) B ) )
108 107 oveq2d 
 |-  ( c = B -> ( A ( +g ` M ) ( B ( +g ` M ) c ) ) = ( A ( +g ` M ) ( B ( +g ` M ) B ) ) )
109 106 108 eqeq12d 
 |-  ( c = B -> ( ( ( A ( +g ` M ) B ) ( +g ` M ) c ) = ( A ( +g ` M ) ( B ( +g ` M ) c ) ) <-> ( ( A ( +g ` M ) B ) ( +g ` M ) B ) = ( A ( +g ` M ) ( B ( +g ` M ) B ) ) ) )
110 105 109 ralprg 
 |-  ( ( A e. S /\ B e. S ) -> ( A. c e. { A , B } ( ( A ( +g ` M ) B ) ( +g ` M ) c ) = ( A ( +g ` M ) ( B ( +g ` M ) c ) ) <-> ( ( ( A ( +g ` M ) B ) ( +g ` M ) A ) = ( A ( +g ` M ) ( B ( +g ` M ) A ) ) /\ ( ( A ( +g ` M ) B ) ( +g ` M ) B ) = ( A ( +g ` M ) ( B ( +g ` M ) B ) ) ) ) )
111 101 110 anbi12d 
 |-  ( ( A e. S /\ B e. S ) -> ( ( A. c e. { A , B } ( ( A ( +g ` M ) A ) ( +g ` M ) c ) = ( A ( +g ` M ) ( A ( +g ` M ) c ) ) /\ A. c e. { A , B } ( ( A ( +g ` M ) B ) ( +g ` M ) c ) = ( A ( +g ` M ) ( B ( +g ` M ) c ) ) ) <-> ( ( ( ( A ( +g ` M ) A ) ( +g ` M ) A ) = ( A ( +g ` M ) ( A ( +g ` M ) A ) ) /\ ( ( A ( +g ` M ) A ) ( +g ` M ) B ) = ( A ( +g ` M ) ( A ( +g ` M ) B ) ) ) /\ ( ( ( A ( +g ` M ) B ) ( +g ` M ) A ) = ( A ( +g ` M ) ( B ( +g ` M ) A ) ) /\ ( ( A ( +g ` M ) B ) ( +g ` M ) B ) = ( A ( +g ` M ) ( B ( +g ` M ) B ) ) ) ) ) )
112 oveq2 
 |-  ( c = A -> ( ( B ( +g ` M ) A ) ( +g ` M ) c ) = ( ( B ( +g ` M ) A ) ( +g ` M ) A ) )
113 94 oveq2d 
 |-  ( c = A -> ( B ( +g ` M ) ( A ( +g ` M ) c ) ) = ( B ( +g ` M ) ( A ( +g ` M ) A ) ) )
114 112 113 eqeq12d 
 |-  ( c = A -> ( ( ( B ( +g ` M ) A ) ( +g ` M ) c ) = ( B ( +g ` M ) ( A ( +g ` M ) c ) ) <-> ( ( B ( +g ` M ) A ) ( +g ` M ) A ) = ( B ( +g ` M ) ( A ( +g ` M ) A ) ) ) )
115 oveq2 
 |-  ( c = B -> ( ( B ( +g ` M ) A ) ( +g ` M ) c ) = ( ( B ( +g ` M ) A ) ( +g ` M ) B ) )
116 98 oveq2d 
 |-  ( c = B -> ( B ( +g ` M ) ( A ( +g ` M ) c ) ) = ( B ( +g ` M ) ( A ( +g ` M ) B ) ) )
117 115 116 eqeq12d 
 |-  ( c = B -> ( ( ( B ( +g ` M ) A ) ( +g ` M ) c ) = ( B ( +g ` M ) ( A ( +g ` M ) c ) ) <-> ( ( B ( +g ` M ) A ) ( +g ` M ) B ) = ( B ( +g ` M ) ( A ( +g ` M ) B ) ) ) )
118 114 117 ralprg 
 |-  ( ( A e. S /\ B e. S ) -> ( A. c e. { A , B } ( ( B ( +g ` M ) A ) ( +g ` M ) c ) = ( B ( +g ` M ) ( A ( +g ` M ) c ) ) <-> ( ( ( B ( +g ` M ) A ) ( +g ` M ) A ) = ( B ( +g ` M ) ( A ( +g ` M ) A ) ) /\ ( ( B ( +g ` M ) A ) ( +g ` M ) B ) = ( B ( +g ` M ) ( A ( +g ` M ) B ) ) ) ) )
119 oveq2 
 |-  ( c = A -> ( ( B ( +g ` M ) B ) ( +g ` M ) c ) = ( ( B ( +g ` M ) B ) ( +g ` M ) A ) )
120 103 oveq2d 
 |-  ( c = A -> ( B ( +g ` M ) ( B ( +g ` M ) c ) ) = ( B ( +g ` M ) ( B ( +g ` M ) A ) ) )
121 119 120 eqeq12d 
 |-  ( c = A -> ( ( ( B ( +g ` M ) B ) ( +g ` M ) c ) = ( B ( +g ` M ) ( B ( +g ` M ) c ) ) <-> ( ( B ( +g ` M ) B ) ( +g ` M ) A ) = ( B ( +g ` M ) ( B ( +g ` M ) A ) ) ) )
122 oveq2 
 |-  ( c = B -> ( ( B ( +g ` M ) B ) ( +g ` M ) c ) = ( ( B ( +g ` M ) B ) ( +g ` M ) B ) )
123 107 oveq2d 
 |-  ( c = B -> ( B ( +g ` M ) ( B ( +g ` M ) c ) ) = ( B ( +g ` M ) ( B ( +g ` M ) B ) ) )
124 122 123 eqeq12d 
 |-  ( c = B -> ( ( ( B ( +g ` M ) B ) ( +g ` M ) c ) = ( B ( +g ` M ) ( B ( +g ` M ) c ) ) <-> ( ( B ( +g ` M ) B ) ( +g ` M ) B ) = ( B ( +g ` M ) ( B ( +g ` M ) B ) ) ) )
125 121 124 ralprg 
 |-  ( ( A e. S /\ B e. S ) -> ( A. c e. { A , B } ( ( B ( +g ` M ) B ) ( +g ` M ) c ) = ( B ( +g ` M ) ( B ( +g ` M ) c ) ) <-> ( ( ( B ( +g ` M ) B ) ( +g ` M ) A ) = ( B ( +g ` M ) ( B ( +g ` M ) A ) ) /\ ( ( B ( +g ` M ) B ) ( +g ` M ) B ) = ( B ( +g ` M ) ( B ( +g ` M ) B ) ) ) ) )
126 118 125 anbi12d 
 |-  ( ( A e. S /\ B e. S ) -> ( ( A. c e. { A , B } ( ( B ( +g ` M ) A ) ( +g ` M ) c ) = ( B ( +g ` M ) ( A ( +g ` M ) c ) ) /\ A. c e. { A , B } ( ( B ( +g ` M ) B ) ( +g ` M ) c ) = ( B ( +g ` M ) ( B ( +g ` M ) c ) ) ) <-> ( ( ( ( B ( +g ` M ) A ) ( +g ` M ) A ) = ( B ( +g ` M ) ( A ( +g ` M ) A ) ) /\ ( ( B ( +g ` M ) A ) ( +g ` M ) B ) = ( B ( +g ` M ) ( A ( +g ` M ) B ) ) ) /\ ( ( ( B ( +g ` M ) B ) ( +g ` M ) A ) = ( B ( +g ` M ) ( B ( +g ` M ) A ) ) /\ ( ( B ( +g ` M ) B ) ( +g ` M ) B ) = ( B ( +g ` M ) ( B ( +g ` M ) B ) ) ) ) ) )
127 111 126 anbi12d 
 |-  ( ( A e. S /\ B e. S ) -> ( ( ( A. c e. { A , B } ( ( A ( +g ` M ) A ) ( +g ` M ) c ) = ( A ( +g ` M ) ( A ( +g ` M ) c ) ) /\ A. c e. { A , B } ( ( A ( +g ` M ) B ) ( +g ` M ) c ) = ( A ( +g ` M ) ( B ( +g ` M ) c ) ) ) /\ ( A. c e. { A , B } ( ( B ( +g ` M ) A ) ( +g ` M ) c ) = ( B ( +g ` M ) ( A ( +g ` M ) c ) ) /\ A. c e. { A , B } ( ( B ( +g ` M ) B ) ( +g ` M ) c ) = ( B ( +g ` M ) ( B ( +g ` M ) c ) ) ) ) <-> ( ( ( ( ( A ( +g ` M ) A ) ( +g ` M ) A ) = ( A ( +g ` M ) ( A ( +g ` M ) A ) ) /\ ( ( A ( +g ` M ) A ) ( +g ` M ) B ) = ( A ( +g ` M ) ( A ( +g ` M ) B ) ) ) /\ ( ( ( A ( +g ` M ) B ) ( +g ` M ) A ) = ( A ( +g ` M ) ( B ( +g ` M ) A ) ) /\ ( ( A ( +g ` M ) B ) ( +g ` M ) B ) = ( A ( +g ` M ) ( B ( +g ` M ) B ) ) ) ) /\ ( ( ( ( B ( +g ` M ) A ) ( +g ` M ) A ) = ( B ( +g ` M ) ( A ( +g ` M ) A ) ) /\ ( ( B ( +g ` M ) A ) ( +g ` M ) B ) = ( B ( +g ` M ) ( A ( +g ` M ) B ) ) ) /\ ( ( ( B ( +g ` M ) B ) ( +g ` M ) A ) = ( B ( +g ` M ) ( B ( +g ` M ) A ) ) /\ ( ( B ( +g ` M ) B ) ( +g ` M ) B ) = ( B ( +g ` M ) ( B ( +g ` M ) B ) ) ) ) ) ) )
128 67 92 127 3bitrd 
 |-  ( ( A e. S /\ B e. S ) -> ( A. a e. { A , B } A. b e. { A , B } A. c e. { A , B } ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) <-> ( ( ( ( ( A ( +g ` M ) A ) ( +g ` M ) A ) = ( A ( +g ` M ) ( A ( +g ` M ) A ) ) /\ ( ( A ( +g ` M ) A ) ( +g ` M ) B ) = ( A ( +g ` M ) ( A ( +g ` M ) B ) ) ) /\ ( ( ( A ( +g ` M ) B ) ( +g ` M ) A ) = ( A ( +g ` M ) ( B ( +g ` M ) A ) ) /\ ( ( A ( +g ` M ) B ) ( +g ` M ) B ) = ( A ( +g ` M ) ( B ( +g ` M ) B ) ) ) ) /\ ( ( ( ( B ( +g ` M ) A ) ( +g ` M ) A ) = ( B ( +g ` M ) ( A ( +g ` M ) A ) ) /\ ( ( B ( +g ` M ) A ) ( +g ` M ) B ) = ( B ( +g ` M ) ( A ( +g ` M ) B ) ) ) /\ ( ( ( B ( +g ` M ) B ) ( +g ` M ) A ) = ( B ( +g ` M ) ( B ( +g ` M ) A ) ) /\ ( ( B ( +g ` M ) B ) ( +g ` M ) B ) = ( B ( +g ` M ) ( B ( +g ` M ) B ) ) ) ) ) ) )
129 128 3adant3 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( A. a e. { A , B } A. b e. { A , B } A. c e. { A , B } ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) <-> ( ( ( ( ( A ( +g ` M ) A ) ( +g ` M ) A ) = ( A ( +g ` M ) ( A ( +g ` M ) A ) ) /\ ( ( A ( +g ` M ) A ) ( +g ` M ) B ) = ( A ( +g ` M ) ( A ( +g ` M ) B ) ) ) /\ ( ( ( A ( +g ` M ) B ) ( +g ` M ) A ) = ( A ( +g ` M ) ( B ( +g ` M ) A ) ) /\ ( ( A ( +g ` M ) B ) ( +g ` M ) B ) = ( A ( +g ` M ) ( B ( +g ` M ) B ) ) ) ) /\ ( ( ( ( B ( +g ` M ) A ) ( +g ` M ) A ) = ( B ( +g ` M ) ( A ( +g ` M ) A ) ) /\ ( ( B ( +g ` M ) A ) ( +g ` M ) B ) = ( B ( +g ` M ) ( A ( +g ` M ) B ) ) ) /\ ( ( ( B ( +g ` M ) B ) ( +g ` M ) A ) = ( B ( +g ` M ) ( B ( +g ` M ) A ) ) /\ ( ( B ( +g ` M ) B ) ( +g ` M ) B ) = ( B ( +g ` M ) ( B ( +g ` M ) B ) ) ) ) ) ) )
130 39 56 129 mpbir2and 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> A. a e. { A , B } A. b e. { A , B } A. c e. { A , B } ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) )
131 4 130 syl 
 |-  ( ( # ` S ) = 2 -> A. a e. { A , B } A. b e. { A , B } A. c e. { A , B } ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) )
132 2 1 eqtr2i 
 |-  { A , B } = ( Base ` M )
133 132 8 issgrp 
 |-  ( M e. Smgrp <-> ( M e. Mgm /\ A. a e. { A , B } A. b e. { A , B } A. c e. { A , B } ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) ) )
134 7 131 133 sylanbrc 
 |-  ( ( # ` S ) = 2 -> M e. Smgrp )