Proof of Theorem sgrp2nmndlem5
| Step | Hyp | Ref
| Expression |
| 1 | | mgm2nsgrp.s |
. . 3
⊢ 𝑆 = {𝐴, 𝐵} |
| 2 | 1 | hashprdifel 14437 |
. 2
⊢
((♯‘𝑆) =
2 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵)) |
| 3 | | mgm2nsgrp.b |
. . . . . . . 8
⊢
(Base‘𝑀) =
𝑆 |
| 4 | | sgrp2nmnd.o |
. . . . . . . 8
⊢
(+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) |
| 5 | | eqid 2737 |
. . . . . . . 8
⊢
(+g‘𝑀) = (+g‘𝑀) |
| 6 | 1, 3, 4, 5 | sgrp2nmndlem2 18937 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴(+g‘𝑀)𝐵) = 𝐴) |
| 7 | 6 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐴(+g‘𝑀)𝐵) = 𝐴) |
| 8 | | simp3 1139 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → 𝐴 ≠ 𝐵) |
| 9 | 7, 8 | eqnetrd 3008 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐴(+g‘𝑀)𝐵) ≠ 𝐵) |
| 10 | 9 | olcd 875 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → ((𝐴(+g‘𝑀)𝐴) ≠ 𝐴 ∨ (𝐴(+g‘𝑀)𝐵) ≠ 𝐵)) |
| 11 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝐴(+g‘𝑀)𝑦) = (𝐴(+g‘𝑀)𝐴)) |
| 12 | | id 22 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → 𝑦 = 𝐴) |
| 13 | 11, 12 | neeq12d 3002 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((𝐴(+g‘𝑀)𝑦) ≠ 𝑦 ↔ (𝐴(+g‘𝑀)𝐴) ≠ 𝐴)) |
| 14 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝐴(+g‘𝑀)𝑦) = (𝐴(+g‘𝑀)𝐵)) |
| 15 | | id 22 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵) |
| 16 | 14, 15 | neeq12d 3002 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝐴(+g‘𝑀)𝑦) ≠ 𝑦 ↔ (𝐴(+g‘𝑀)𝐵) ≠ 𝐵)) |
| 17 | 13, 16 | rexprg 4697 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (∃𝑦 ∈ {𝐴, 𝐵} (𝐴(+g‘𝑀)𝑦) ≠ 𝑦 ↔ ((𝐴(+g‘𝑀)𝐴) ≠ 𝐴 ∨ (𝐴(+g‘𝑀)𝐵) ≠ 𝐵))) |
| 18 | 17 | 3adant3 1133 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (∃𝑦 ∈ {𝐴, 𝐵} (𝐴(+g‘𝑀)𝑦) ≠ 𝑦 ↔ ((𝐴(+g‘𝑀)𝐴) ≠ 𝐴 ∨ (𝐴(+g‘𝑀)𝐵) ≠ 𝐵))) |
| 19 | 10, 18 | mpbird 257 |
. . 3
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → ∃𝑦 ∈ {𝐴, 𝐵} (𝐴(+g‘𝑀)𝑦) ≠ 𝑦) |
| 20 | 1, 3, 4, 5 | sgrp2nmndlem3 18938 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐵(+g‘𝑀)𝐴) = 𝐵) |
| 21 | | necom 2994 |
. . . . . . . . . . 11
⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) |
| 22 | | df-ne 2941 |
. . . . . . . . . . 11
⊢ (𝐵 ≠ 𝐴 ↔ ¬ 𝐵 = 𝐴) |
| 23 | 21, 22 | sylbb 219 |
. . . . . . . . . 10
⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 = 𝐴) |
| 24 | 23 | 3ad2ant3 1136 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → ¬ 𝐵 = 𝐴) |
| 25 | 24 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) ∧ (𝐵(+g‘𝑀)𝐴) = 𝐵) → ¬ 𝐵 = 𝐴) |
| 26 | | eqeq1 2741 |
. . . . . . . . 9
⊢ ((𝐵(+g‘𝑀)𝐴) = 𝐵 → ((𝐵(+g‘𝑀)𝐴) = 𝐴 ↔ 𝐵 = 𝐴)) |
| 27 | 26 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) ∧ (𝐵(+g‘𝑀)𝐴) = 𝐵) → ((𝐵(+g‘𝑀)𝐴) = 𝐴 ↔ 𝐵 = 𝐴)) |
| 28 | 25, 27 | mtbird 325 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) ∧ (𝐵(+g‘𝑀)𝐴) = 𝐵) → ¬ (𝐵(+g‘𝑀)𝐴) = 𝐴) |
| 29 | 20, 28 | mpdan 687 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → ¬ (𝐵(+g‘𝑀)𝐴) = 𝐴) |
| 30 | 29 | neqned 2947 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐵(+g‘𝑀)𝐴) ≠ 𝐴) |
| 31 | 30 | orcd 874 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → ((𝐵(+g‘𝑀)𝐴) ≠ 𝐴 ∨ (𝐵(+g‘𝑀)𝐵) ≠ 𝐵)) |
| 32 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝐵(+g‘𝑀)𝑦) = (𝐵(+g‘𝑀)𝐴)) |
| 33 | 32, 12 | neeq12d 3002 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((𝐵(+g‘𝑀)𝑦) ≠ 𝑦 ↔ (𝐵(+g‘𝑀)𝐴) ≠ 𝐴)) |
| 34 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝐵(+g‘𝑀)𝑦) = (𝐵(+g‘𝑀)𝐵)) |
| 35 | 34, 15 | neeq12d 3002 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝐵(+g‘𝑀)𝑦) ≠ 𝑦 ↔ (𝐵(+g‘𝑀)𝐵) ≠ 𝐵)) |
| 36 | 33, 35 | rexprg 4697 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (∃𝑦 ∈ {𝐴, 𝐵} (𝐵(+g‘𝑀)𝑦) ≠ 𝑦 ↔ ((𝐵(+g‘𝑀)𝐴) ≠ 𝐴 ∨ (𝐵(+g‘𝑀)𝐵) ≠ 𝐵))) |
| 37 | 36 | 3adant3 1133 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (∃𝑦 ∈ {𝐴, 𝐵} (𝐵(+g‘𝑀)𝑦) ≠ 𝑦 ↔ ((𝐵(+g‘𝑀)𝐴) ≠ 𝐴 ∨ (𝐵(+g‘𝑀)𝐵) ≠ 𝐵))) |
| 38 | 31, 37 | mpbird 257 |
. . 3
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → ∃𝑦 ∈ {𝐴, 𝐵} (𝐵(+g‘𝑀)𝑦) ≠ 𝑦) |
| 39 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥(+g‘𝑀)𝑦) = (𝐴(+g‘𝑀)𝑦)) |
| 40 | 39 | neeq1d 3000 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑥(+g‘𝑀)𝑦) ≠ 𝑦 ↔ (𝐴(+g‘𝑀)𝑦) ≠ 𝑦)) |
| 41 | 40 | rexbidv 3179 |
. . . . 5
⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ {𝐴, 𝐵} (𝑥(+g‘𝑀)𝑦) ≠ 𝑦 ↔ ∃𝑦 ∈ {𝐴, 𝐵} (𝐴(+g‘𝑀)𝑦) ≠ 𝑦)) |
| 42 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝑥(+g‘𝑀)𝑦) = (𝐵(+g‘𝑀)𝑦)) |
| 43 | 42 | neeq1d 3000 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝑥(+g‘𝑀)𝑦) ≠ 𝑦 ↔ (𝐵(+g‘𝑀)𝑦) ≠ 𝑦)) |
| 44 | 43 | rexbidv 3179 |
. . . . 5
⊢ (𝑥 = 𝐵 → (∃𝑦 ∈ {𝐴, 𝐵} (𝑥(+g‘𝑀)𝑦) ≠ 𝑦 ↔ ∃𝑦 ∈ {𝐴, 𝐵} (𝐵(+g‘𝑀)𝑦) ≠ 𝑦)) |
| 45 | 41, 44 | ralprg 4696 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (∀𝑥 ∈ {𝐴, 𝐵}∃𝑦 ∈ {𝐴, 𝐵} (𝑥(+g‘𝑀)𝑦) ≠ 𝑦 ↔ (∃𝑦 ∈ {𝐴, 𝐵} (𝐴(+g‘𝑀)𝑦) ≠ 𝑦 ∧ ∃𝑦 ∈ {𝐴, 𝐵} (𝐵(+g‘𝑀)𝑦) ≠ 𝑦))) |
| 46 | 45 | 3adant3 1133 |
. . 3
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (∀𝑥 ∈ {𝐴, 𝐵}∃𝑦 ∈ {𝐴, 𝐵} (𝑥(+g‘𝑀)𝑦) ≠ 𝑦 ↔ (∃𝑦 ∈ {𝐴, 𝐵} (𝐴(+g‘𝑀)𝑦) ≠ 𝑦 ∧ ∃𝑦 ∈ {𝐴, 𝐵} (𝐵(+g‘𝑀)𝑦) ≠ 𝑦))) |
| 47 | 19, 38, 46 | mpbir2and 713 |
. 2
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → ∀𝑥 ∈ {𝐴, 𝐵}∃𝑦 ∈ {𝐴, 𝐵} (𝑥(+g‘𝑀)𝑦) ≠ 𝑦) |
| 48 | 3, 1 | eqtr2i 2766 |
. . 3
⊢ {𝐴, 𝐵} = (Base‘𝑀) |
| 49 | 48, 5 | isnmnd 18751 |
. 2
⊢
(∀𝑥 ∈
{𝐴, 𝐵}∃𝑦 ∈ {𝐴, 𝐵} (𝑥(+g‘𝑀)𝑦) ≠ 𝑦 → 𝑀 ∉ Mnd) |
| 50 | 2, 47, 49 | 3syl 18 |
1
⊢
((♯‘𝑆) =
2 → 𝑀 ∉
Mnd) |