Proof of Theorem mgm2nsgrplem2
Step | Hyp | Ref
| Expression |
1 | | prid1g 4570 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵}) |
2 | | mgm2nsgrp.s |
. . 3
⊢ 𝑆 = {𝐴, 𝐵} |
3 | 1, 2 | syl6eleqr 2877 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑆) |
4 | | prid2g 4571 |
. . 3
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ {𝐴, 𝐵}) |
5 | 4, 2 | syl6eleqr 2877 |
. 2
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ 𝑆) |
6 | | mgm2nsgrp.p |
. . . . 5
⊢ ⚬ =
(+g‘𝑀) |
7 | | mgm2nsgrp.o |
. . . . 5
⊢
(+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) |
8 | 6, 7 | eqtri 2802 |
. . . 4
⊢ ⚬ =
(𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) |
9 | 8 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ⚬ = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴))) |
10 | | ifeq1 4354 |
. . . . . . 7
⊢ (𝐵 = 𝐴 → if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴) = if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐴, 𝐴)) |
11 | | ifid 4389 |
. . . . . . 7
⊢ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐴, 𝐴) = 𝐴 |
12 | 10, 11 | syl6eq 2830 |
. . . . . 6
⊢ (𝐵 = 𝐴 → if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴) = 𝐴) |
13 | 12 | a1d 25 |
. . . . 5
⊢ (𝐵 = 𝐴 → (𝑦 = 𝐵 → if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴) = 𝐴)) |
14 | | eqeq1 2782 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐵 → (𝑦 = 𝐴 ↔ 𝐵 = 𝐴)) |
15 | 14 | bicomd 215 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐵 → (𝐵 = 𝐴 ↔ 𝑦 = 𝐴)) |
16 | 15 | notbid 310 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → (¬ 𝐵 = 𝐴 ↔ ¬ 𝑦 = 𝐴)) |
17 | 16 | biimpac 471 |
. . . . . . . 8
⊢ ((¬
𝐵 = 𝐴 ∧ 𝑦 = 𝐵) → ¬ 𝑦 = 𝐴) |
18 | 17 | intnand 481 |
. . . . . . 7
⊢ ((¬
𝐵 = 𝐴 ∧ 𝑦 = 𝐵) → ¬ (𝑥 = 𝐴 ∧ 𝑦 = 𝐴)) |
19 | 18 | iffalsed 4361 |
. . . . . 6
⊢ ((¬
𝐵 = 𝐴 ∧ 𝑦 = 𝐵) → if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴) = 𝐴) |
20 | 19 | ex 405 |
. . . . 5
⊢ (¬
𝐵 = 𝐴 → (𝑦 = 𝐵 → if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴) = 𝐴)) |
21 | 13, 20 | pm2.61i 177 |
. . . 4
⊢ (𝑦 = 𝐵 → if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴) = 𝐴) |
22 | 21 | ad2antll 716 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝑥 = (𝐴 ⚬ 𝐴) ∧ 𝑦 = 𝐵)) → if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴) = 𝐴) |
23 | | iftrue 4356 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴) = 𝐵) |
24 | 23 | adantl 474 |
. . . . 5
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐴)) → if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴) = 𝐵) |
25 | | simpl 475 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝐴 ∈ 𝑆) |
26 | | simpr 477 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝐵 ∈ 𝑆) |
27 | 9, 24, 25, 25, 26 | ovmpod 7118 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ⚬ 𝐴) = 𝐵) |
28 | 27, 26 | eqeltrd 2866 |
. . 3
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ⚬ 𝐴) ∈ 𝑆) |
29 | 9, 22, 28, 26, 25 | ovmpod 7118 |
. 2
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴 ⚬ 𝐴) ⚬ 𝐵) = 𝐴) |
30 | 3, 5, 29 | syl2an 586 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ⚬ 𝐴) ⚬ 𝐵) = 𝐴) |