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 ⊢ 𝑆 = { 𝐴 , 𝐵 }
mgm2nsgrp.b ⊢ ( Base ‘ 𝑀 ) = 𝑆
sgrp2nmnd.o ⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝐴 , 𝐴 , 𝐵 ) )
Assertion sgrp2nmndlem4 ( ( ♯ ‘ 𝑆 ) = 2 → 𝑀 ∈ Smgrp )

Proof

Step Hyp Ref Expression
1 mgm2nsgrp.s ⊢ 𝑆 = { 𝐴 , 𝐵 }
2 mgm2nsgrp.b ⊢ ( Base ‘ 𝑀 ) = 𝑆
3 sgrp2nmnd.o ⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝐴 , 𝐴 , 𝐵 ) )
4 1 hashprdifel ⊢ ( ( ♯ ‘ 𝑆 ) = 2 → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) )
5 3simpa ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )
6 1 2 3 sgrp2nmndlem1 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝑀 ∈ Mgm )
7 4 5 6 3syl ⊢ ( ( ♯ ‘ 𝑆 ) = 2 → 𝑀 ∈ Mgm )
8 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
9 1 2 3 8 sgrp2nmndlem2 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) = 𝐴 )
10 9 oveq1d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) )
11 9 oveq2d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) )
12 10 11 eqtr4d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) )
13 12 anidms ⊢ ( 𝐴 ∈ 𝑆 → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) )
14 13 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) )
15 9 anidms ⊢ ( 𝐴 ∈ 𝑆 → ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) = 𝐴 )
16 15 adantr ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) = 𝐴 )
17 16 oveq1d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) )
18 1 2 3 8 sgrp2nmndlem2 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) = 𝐴 )
19 18 oveq2d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) )
20 16 19 18 3eqtr4rd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) )
21 17 20 eqtrd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) )
22 21 3adant3 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) )
23 14 22 jca ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) ) )
24 18 3adant3 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) = 𝐴 )
25 1 2 3 8 sgrp2nmndlem3 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) = 𝐵 )
26 25 oveq2d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) )
27 24 oveq1d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) )
28 15 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) = 𝐴 )
29 27 28 eqtrd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = 𝐴 )
30 24 26 29 3eqtr4rd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) )
31 simp2 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝑆 )
32 1 2 3 8 sgrp2nmndlem3 ⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) = 𝐵 )
33 31 32 syld3an1 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) = 𝐵 )
34 33 oveq2d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) )
35 18 oveq1d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) )
36 35 18 eqtrd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = 𝐴 )
37 36 3adant3 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = 𝐴 )
38 24 34 37 3eqtr4rd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) )
39 23 30 38 jca32 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ∧ ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ) )
40 25 oveq1d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) )
41 28 oveq2d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) )
42 40 41 eqtr4d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) )
43 24 oveq2d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) )
44 25 oveq1d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) )
45 44 33 eqtrd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = 𝐵 )
46 25 43 45 3eqtr4rd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) )
47 42 46 jca ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) ) )
48 25 oveq2d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) )
49 33 oveq1d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) )
50 49 25 eqtrd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = 𝐵 )
51 33 48 50 3eqtr4rd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) )
52 32 oveq1d ⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) )
53 32 oveq2d ⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) )
54 52 53 eqtr4d ⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) )
55 31 54 syld3an1 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) )
56 47 51 55 jca32 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ∧ ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ) )
57 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝑏 ) )
58 57 oveq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝐴 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) )
59 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) )
60 58 59 eqeq12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
61 60 2ralbidv ⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑏 ∈ { 𝐴 , 𝐵 } ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ∀ 𝑏 ∈ { 𝐴 , 𝐵 } ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
62 oveq1 ⊢ ( 𝑎 = 𝐵 → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝑏 ) )
63 62 oveq1d ⊢ ( 𝑎 = 𝐵 → ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝐵 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) )
64 oveq1 ⊢ ( 𝑎 = 𝐵 → ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) )
65 63 64 eqeq12d ⊢ ( 𝑎 = 𝐵 → ( ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
66 65 2ralbidv ⊢ ( 𝑎 = 𝐵 → ( ∀ 𝑏 ∈ { 𝐴 , 𝐵 } ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ∀ 𝑏 ∈ { 𝐴 , 𝐵 } ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
67 61 66 ralprg ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑎 ∈ { 𝐴 , 𝐵 } ∀ 𝑏 ∈ { 𝐴 , 𝐵 } ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ∀ 𝑏 ∈ { 𝐴 , 𝐵 } ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ∧ ∀ 𝑏 ∈ { 𝐴 , 𝐵 } ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ) ) )
68 oveq2 ⊢ ( 𝑏 = 𝐴 → ( 𝐴 ( +g ‘ 𝑀 ) 𝑏 ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) )
69 68 oveq1d ⊢ ( 𝑏 = 𝐴 → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) )
70 oveq1 ⊢ ( 𝑏 = 𝐴 → ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) )
71 70 oveq2d ⊢ ( 𝑏 = 𝐴 → ( 𝐴 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) )
72 69 71 eqeq12d ⊢ ( 𝑏 = 𝐴 → ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
73 72 ralbidv ⊢ ( 𝑏 = 𝐴 → ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
74 oveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐴 ( +g ‘ 𝑀 ) 𝑏 ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) )
75 74 oveq1d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) )
76 oveq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) )
77 76 oveq2d ⊢ ( 𝑏 = 𝐵 → ( 𝐴 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) )
78 75 77 eqeq12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
79 78 ralbidv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
80 73 79 ralprg ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑏 ∈ { 𝐴 , 𝐵 } ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ) ) )
81 oveq2 ⊢ ( 𝑏 = 𝐴 → ( 𝐵 ( +g ‘ 𝑀 ) 𝑏 ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) )
82 81 oveq1d ⊢ ( 𝑏 = 𝐴 → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) )
83 70 oveq2d ⊢ ( 𝑏 = 𝐴 → ( 𝐵 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) )
84 82 83 eqeq12d ⊢ ( 𝑏 = 𝐴 → ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
85 84 ralbidv ⊢ ( 𝑏 = 𝐴 → ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
86 oveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐵 ( +g ‘ 𝑀 ) 𝑏 ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) )
87 86 oveq1d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) )
88 76 oveq2d ⊢ ( 𝑏 = 𝐵 → ( 𝐵 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) )
89 87 88 eqeq12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
90 89 ralbidv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
91 85 90 ralprg ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑏 ∈ { 𝐴 , 𝐵 } ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ) ) )
92 80 91 anbi12d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( ∀ 𝑏 ∈ { 𝐴 , 𝐵 } ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ∧ ∀ 𝑏 ∈ { 𝐴 , 𝐵 } ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ) ↔ ( ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ) ∧ ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ) ) ) )
93 oveq2 ⊢ ( 𝑐 = 𝐴 → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) )
94 oveq2 ⊢ ( 𝑐 = 𝐴 → ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) )
95 94 oveq2d ⊢ ( 𝑐 = 𝐴 → ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) )
96 93 95 eqeq12d ⊢ ( 𝑐 = 𝐴 → ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) ) )
97 oveq2 ⊢ ( 𝑐 = 𝐵 → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) )
98 oveq2 ⊢ ( 𝑐 = 𝐵 → ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) )
99 98 oveq2d ⊢ ( 𝑐 = 𝐵 → ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) )
100 97 99 eqeq12d ⊢ ( 𝑐 = 𝐵 → ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) ) )
101 96 100 ralprg ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ) )
102 oveq2 ⊢ ( 𝑐 = 𝐴 → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) )
103 oveq2 ⊢ ( 𝑐 = 𝐴 → ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) )
104 103 oveq2d ⊢ ( 𝑐 = 𝐴 → ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) )
105 102 104 eqeq12d ⊢ ( 𝑐 = 𝐴 → ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) ) )
106 oveq2 ⊢ ( 𝑐 = 𝐵 → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) )
107 oveq2 ⊢ ( 𝑐 = 𝐵 → ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) )
108 107 oveq2d ⊢ ( 𝑐 = 𝐵 → ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) )
109 106 108 eqeq12d ⊢ ( 𝑐 = 𝐵 → ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) ) )
110 105 109 ralprg ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ) )
111 101 110 anbi12d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ) ↔ ( ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ∧ ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ) ) )
112 oveq2 ⊢ ( 𝑐 = 𝐴 → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) )
113 94 oveq2d ⊢ ( 𝑐 = 𝐴 → ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) )
114 112 113 eqeq12d ⊢ ( 𝑐 = 𝐴 → ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) ) )
115 oveq2 ⊢ ( 𝑐 = 𝐵 → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) )
116 98 oveq2d ⊢ ( 𝑐 = 𝐵 → ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) )
117 115 116 eqeq12d ⊢ ( 𝑐 = 𝐵 → ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) ) )
118 114 117 ralprg ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ) )
119 oveq2 ⊢ ( 𝑐 = 𝐴 → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) )
120 103 oveq2d ⊢ ( 𝑐 = 𝐴 → ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) )
121 119 120 eqeq12d ⊢ ( 𝑐 = 𝐴 → ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) ) )
122 oveq2 ⊢ ( 𝑐 = 𝐵 → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) )
123 107 oveq2d ⊢ ( 𝑐 = 𝐵 → ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) )
124 122 123 eqeq12d ⊢ ( 𝑐 = 𝐵 → ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) ) )
125 121 124 ralprg ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ) )
126 118 125 anbi12d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ) ↔ ( ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ∧ ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ) ) )
127 111 126 anbi12d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ) ∧ ( ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝑐 ) ) ∧ ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝑐 ) ) ) ) ↔ ( ( ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ∧ ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ) ∧ ( ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ∧ ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ) ) ) )
128 67 92 127 3bitrd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑎 ∈ { 𝐴 , 𝐵 } ∀ 𝑏 ∈ { 𝐴 , 𝐵 } ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ∧ ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ) ∧ ( ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ∧ ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ) ) ) )
129 128 3adant3 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ∀ 𝑎 ∈ { 𝐴 , 𝐵 } ∀ 𝑏 ∈ { 𝐴 , 𝐵 } ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ↔ ( ( ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ∧ ( ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐴 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ) ∧ ( ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ∧ ( ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐴 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ) ∧ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝑀 ) ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ) ) ) ) ) )
130 39 56 129 mpbir2and ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ∀ 𝑎 ∈ { 𝐴 , 𝐵 } ∀ 𝑏 ∈ { 𝐴 , 𝐵 } ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) )
131 4 130 syl ⊢ ( ( ♯ ‘ 𝑆 ) = 2 → ∀ 𝑎 ∈ { 𝐴 , 𝐵 } ∀ 𝑏 ∈ { 𝐴 , 𝐵 } ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) )
132 2 1 eqtr2i ⊢ { 𝐴 , 𝐵 } = ( Base ‘ 𝑀 )
133 132 8 issgrp ⊢ ( 𝑀 ∈ Smgrp ↔ ( 𝑀 ∈ Mgm ∧ ∀ 𝑎 ∈ { 𝐴 , 𝐵 } ∀ 𝑏 ∈ { 𝐴 , 𝐵 } ∀ 𝑐 ∈ { 𝐴 , 𝐵 } ( ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ( +g ‘ 𝑀 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑀 ) ( 𝑏 ( +g ‘ 𝑀 ) 𝑐 ) ) ) )
134 7 131 133 sylanbrc ⊢ ( ( ♯ ‘ 𝑆 ) = 2 → 𝑀 ∈ Smgrp )