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

Proof

Step Hyp Ref Expression
1 mgm2nsgrp.s ⊢ 𝑆 = { 𝐴 , 𝐵 }
2 mgm2nsgrp.b ⊢ ( Base ‘ 𝑀 ) = 𝑆
3 sgrp2nmnd.o ⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝐴 , 𝐴 , 𝐵 ) )
4 1 hashprdifel ⊢ ( ( ♯ ‘ 𝑆 ) = 2 → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) )
5 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
6 1 2 3 5 sgrp2nmndlem2 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) = 𝐴 )
7 6 3adant3 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) = 𝐴 )
8 simp3 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
9 7 8 eqnetrd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ≠ 𝐵 )
10 9 olcd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ≠ 𝐴 ∨ ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ≠ 𝐵 ) )
11 oveq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) )
12 id ⊢ ( 𝑦 = 𝐴 → 𝑦 = 𝐴 )
13 11 12 neeq12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ↔ ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ≠ 𝐴 ) )
14 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) )
15 id ⊢ ( 𝑦 = 𝐵 → 𝑦 = 𝐵 )
16 14 15 neeq12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ↔ ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ≠ 𝐵 ) )
17 13 16 rexprg ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ↔ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ≠ 𝐴 ∨ ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ≠ 𝐵 ) ) )
18 17 3adant3 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ↔ ( ( 𝐴 ( +g ‘ 𝑀 ) 𝐴 ) ≠ 𝐴 ∨ ( 𝐴 ( +g ‘ 𝑀 ) 𝐵 ) ≠ 𝐵 ) ) )
19 10 18 mpbird ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 )
20 1 2 3 5 sgrp2nmndlem3 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) = 𝐵 )
21 necom ⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
22 df-ne ⊢ ( 𝐵 ≠ 𝐴 ↔ ¬ 𝐵 = 𝐴 )
23 21 22 sylbb ⊢ ( 𝐴 ≠ 𝐵 → ¬ 𝐵 = 𝐴 )
24 23 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ¬ 𝐵 = 𝐴 )
25 24 adantr ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) = 𝐵 ) → ¬ 𝐵 = 𝐴 )
26 eqeq1 ⊢ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) = 𝐵 → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) = 𝐴 ↔ 𝐵 = 𝐴 ) )
27 26 adantl ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) = 𝐵 ) → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) = 𝐴 ↔ 𝐵 = 𝐴 ) )
28 25 27 mtbird ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) = 𝐵 ) → ¬ ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) = 𝐴 )
29 20 28 mpdan ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ¬ ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) = 𝐴 )
30 29 neqned ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ≠ 𝐴 )
31 30 orcd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ≠ 𝐴 ∨ ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ≠ 𝐵 ) )
32 oveq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐵 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) )
33 32 12 neeq12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ↔ ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ≠ 𝐴 ) )
34 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐵 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) )
35 34 15 neeq12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐵 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ↔ ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ≠ 𝐵 ) )
36 33 35 rexprg ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝐵 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ↔ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ≠ 𝐴 ∨ ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ≠ 𝐵 ) ) )
37 36 3adant3 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝐵 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ↔ ( ( 𝐵 ( +g ‘ 𝑀 ) 𝐴 ) ≠ 𝐴 ∨ ( 𝐵 ( +g ‘ 𝑀 ) 𝐵 ) ≠ 𝐵 ) ) )
38 31 37 mpbird ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝐵 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 )
39 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) )
40 39 neeq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ↔ ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ) )
41 40 rexbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ↔ ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ) )
42 oveq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝐵 ( +g ‘ 𝑀 ) 𝑦 ) )
43 42 neeq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ↔ ( 𝐵 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ) )
44 43 rexbidv ⊢ ( 𝑥 = 𝐵 → ( ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ↔ ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝐵 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ) )
45 41 44 ralprg ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ↔ ( ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ∧ ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝐵 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ) ) )
46 45 3adant3 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ↔ ( ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝐴 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ∧ ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝐵 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 ) ) )
47 19 38 46 mpbir2and ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 )
48 2 1 eqtr2i ⊢ { 𝐴 , 𝐵 } = ( Base ‘ 𝑀 )
49 48 5 isnmnd ⊢ ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ∃ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ≠ 𝑦 → 𝑀 ∉ Mnd )
50 4 47 49 3syl ⊢ ( ( ♯ ‘ 𝑆 ) = 2 → 𝑀 ∉ Mnd )