Metamath Proof Explorer

Theorem isnsgrp

Description: A condition for a structure not to be a semigroup. (Contributed by AV, 30-Jan-2020)

Ref Expression
Hypotheses issgrpn0.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
issgrpn0.o ⊢ ⚬ = ( +g ‘ 𝑀 )
Assertion isnsgrp ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) → 𝑀 ∉ Smgrp ) )

Proof

Step Hyp Ref Expression
1 issgrpn0.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 issgrpn0.o ⊢ ⚬ = ( +g ‘ 𝑀 )
3 simpl1 ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) → 𝑋 ∈ 𝐵 )
4 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ⚬ 𝑦 ) = ( 𝑋 ⚬ 𝑦 ) )
5 4 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( ( 𝑋 ⚬ 𝑦 ) ⚬ 𝑧 ) )
6 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) = ( 𝑋 ⚬ ( 𝑦 ⚬ 𝑧 ) ) )
7 5 6 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ( ( 𝑋 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
8 7 notbid ⊢ ( 𝑥 = 𝑋 → ( ¬ ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ¬ ( ( 𝑋 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
9 8 rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑧 ∈ 𝐵 ¬ ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝐵 ¬ ( ( 𝑋 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
10 9 rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ¬ ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ¬ ( ( 𝑋 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
11 10 adantl ⊢ ( ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) ∧ 𝑥 = 𝑋 ) → ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ¬ ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ¬ ( ( 𝑋 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
12 simpl2 ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) → 𝑌 ∈ 𝐵 )
13 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 ⚬ 𝑦 ) = ( 𝑋 ⚬ 𝑌 ) )
14 13 oveq1d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑧 ) )
15 oveq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ⚬ 𝑧 ) = ( 𝑌 ⚬ 𝑧 ) )
16 15 oveq2d ⊢ ( 𝑦 = 𝑌 → ( 𝑋 ⚬ ( 𝑦 ⚬ 𝑧 ) ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑧 ) ) )
17 14 16 eqeq12d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑧 ) ) ) )
18 17 notbid ⊢ ( 𝑦 = 𝑌 → ( ¬ ( ( 𝑋 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ¬ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑧 ) ) ) )
19 18 adantl ⊢ ( ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) ∧ 𝑦 = 𝑌 ) → ( ¬ ( ( 𝑋 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ¬ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑧 ) ) ) )
20 19 rexbidv ⊢ ( ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) ∧ 𝑦 = 𝑌 ) → ( ∃ 𝑧 ∈ 𝐵 ¬ ( ( 𝑋 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝐵 ¬ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑧 ) ) ) )
21 simpl3 ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) → 𝑍 ∈ 𝐵 )
22 oveq2 ⊢ ( 𝑧 = 𝑍 → ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑧 ) = ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) )
23 oveq2 ⊢ ( 𝑧 = 𝑍 → ( 𝑌 ⚬ 𝑧 ) = ( 𝑌 ⚬ 𝑍 ) )
24 23 oveq2d ⊢ ( 𝑧 = 𝑍 → ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑧 ) ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) )
25 22 24 eqeq12d ⊢ ( 𝑧 = 𝑍 → ( ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑧 ) ) ↔ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) )
26 25 notbid ⊢ ( 𝑧 = 𝑍 → ( ¬ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑧 ) ) ↔ ¬ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) )
27 26 adantl ⊢ ( ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) ∧ 𝑧 = 𝑍 ) → ( ¬ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑧 ) ) ↔ ¬ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) )
28 neneq ⊢ ( ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) → ¬ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) )
29 28 adantl ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) → ¬ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) )
30 21 27 29 rspcedvd ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) → ∃ 𝑧 ∈ 𝐵 ¬ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑧 ) ) )
31 12 20 30 rspcedvd ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) → ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ¬ ( ( 𝑋 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑋 ⚬ ( 𝑦 ⚬ 𝑧 ) ) )
32 3 11 31 rspcedvd ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ¬ ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) )
33 rexnal ⊢ ( ∃ 𝑧 ∈ 𝐵 ¬ ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ¬ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) )
34 33 2rexbii ⊢ ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ¬ ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) )
35 rexnal2 ⊢ ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ¬ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ¬ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) )
36 34 35 bitr2i ⊢ ( ¬ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ¬ ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) )
37 32 36 sylibr ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) → ¬ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) )
38 37 intnand ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) → ¬ ( 𝑀 ∈ Mgm ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
39 1 2 issgrp ⊢ ( 𝑀 ∈ Smgrp ↔ ( 𝑀 ∈ Mgm ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
40 38 39 sylnibr ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) → ¬ 𝑀 ∈ Smgrp )
41 df-nel ⊢ ( 𝑀 ∉ Smgrp ↔ ¬ 𝑀 ∈ Smgrp )
42 40 41 sylibr ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) ) → 𝑀 ∉ Smgrp )
43 42 ex ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( ( 𝑋 ⚬ 𝑌 ) ⚬ 𝑍 ) ≠ ( 𝑋 ⚬ ( 𝑌 ⚬ 𝑍 ) ) → 𝑀 ∉ Smgrp ) )