Proof of Theorem sgrp2rid2
Step | Hyp | Ref
| Expression |
1 | | prid1g 4239 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵}) |
2 | | mgm2nsgrp.s |
. . . 4
⊢ 𝑆 = {𝐴, 𝐵} |
3 | 1, 2 | syl6eleqr 2699 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑆) |
4 | | prid2g 4240 |
. . . 4
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ {𝐴, 𝐵}) |
5 | 4, 2 | syl6eleqr 2699 |
. . 3
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ 𝑆) |
6 | | simpl 472 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝐴 ∈ 𝑆) |
7 | | mgm2nsgrp.b |
. . . . . 6
⊢
(Base‘𝑀) =
𝑆 |
8 | | sgrp2nmnd.o |
. . . . . 6
⊢
(+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) |
9 | | sgrp2nmnd.p |
. . . . . 6
⊢ ⚬ =
(+g‘𝑀) |
10 | 2, 7, 8, 9 | sgrp2nmndlem2 17234 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → (𝐴 ⚬ 𝐴) = 𝐴) |
11 | 6, 10 | syldan 486 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ⚬ 𝐴) = 𝐴) |
12 | | oveq1 6556 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → (𝐴 ⚬ 𝐴) = (𝐵 ⚬ 𝐴)) |
13 | | id 22 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) |
14 | 12, 13 | eqeq12d 2625 |
. . . . . 6
⊢ (𝐴 = 𝐵 → ((𝐴 ⚬ 𝐴) = 𝐴 ↔ (𝐵 ⚬ 𝐴) = 𝐵)) |
15 | 11, 14 | syl5ib 233 |
. . . . 5
⊢ (𝐴 = 𝐵 → ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐵 ⚬ 𝐴) = 𝐵)) |
16 | | simprl 790 |
. . . . . . 7
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → 𝐴 ∈ 𝑆) |
17 | | simprr 792 |
. . . . . . 7
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → 𝐵 ∈ 𝑆) |
18 | | df-ne 2782 |
. . . . . . . . 9
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) |
19 | 18 | biimpri 217 |
. . . . . . . 8
⊢ (¬
𝐴 = 𝐵 → 𝐴 ≠ 𝐵) |
20 | 19 | adantr 480 |
. . . . . . 7
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → 𝐴 ≠ 𝐵) |
21 | 2, 7, 8, 9 | sgrp2nmndlem3 17235 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐵 ⚬ 𝐴) = 𝐵) |
22 | 16, 17, 20, 21 | syl3anc 1318 |
. . . . . 6
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐵 ⚬ 𝐴) = 𝐵) |
23 | 22 | ex 449 |
. . . . 5
⊢ (¬
𝐴 = 𝐵 → ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐵 ⚬ 𝐴) = 𝐵)) |
24 | 15, 23 | pm2.61i 175 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐵 ⚬ 𝐴) = 𝐵) |
25 | 2, 7, 8, 9 | sgrp2nmndlem2 17234 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ⚬ 𝐵) = 𝐴) |
26 | 13, 13 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝐴 = 𝐵 → (𝐴 ⚬ 𝐴) = (𝐵 ⚬ 𝐵)) |
27 | 26, 13 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → ((𝐴 ⚬ 𝐴) = 𝐴 ↔ (𝐵 ⚬ 𝐵) = 𝐵)) |
28 | 11, 27 | syl5ib 233 |
. . . . . 6
⊢ (𝐴 = 𝐵 → ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐵 ⚬ 𝐵) = 𝐵)) |
29 | 2, 7, 8, 9 | sgrp2nmndlem3 17235 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐵 ⚬ 𝐵) = 𝐵) |
30 | 17, 17, 20, 29 | syl3anc 1318 |
. . . . . . 7
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐵 ⚬ 𝐵) = 𝐵) |
31 | 30 | ex 449 |
. . . . . 6
⊢ (¬
𝐴 = 𝐵 → ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐵 ⚬ 𝐵) = 𝐵)) |
32 | 28, 31 | pm2.61i 175 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐵 ⚬ 𝐵) = 𝐵) |
33 | 25, 32 | jca 553 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴 ⚬ 𝐵) = 𝐴 ∧ (𝐵 ⚬ 𝐵) = 𝐵)) |
34 | 11, 24, 33 | jca31 555 |
. . 3
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (((𝐴 ⚬ 𝐴) = 𝐴 ∧ (𝐵 ⚬ 𝐴) = 𝐵) ∧ ((𝐴 ⚬ 𝐵) = 𝐴 ∧ (𝐵 ⚬ 𝐵) = 𝐵))) |
35 | 3, 5, 34 | syl2an 493 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (((𝐴 ⚬ 𝐴) = 𝐴 ∧ (𝐵 ⚬ 𝐴) = 𝐵) ∧ ((𝐴 ⚬ 𝐵) = 𝐴 ∧ (𝐵 ⚬ 𝐵) = 𝐵))) |
36 | 2 | raleqi 3119 |
. . . . 5
⊢
(∀𝑦 ∈
𝑆 (𝑦 ⚬ 𝑥) = 𝑦 ↔ ∀𝑦 ∈ {𝐴, 𝐵} (𝑦 ⚬ 𝑥) = 𝑦) |
37 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑦 ⚬ 𝑥) = (𝐴 ⚬ 𝑥)) |
38 | | id 22 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → 𝑦 = 𝐴) |
39 | 37, 38 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((𝑦 ⚬ 𝑥) = 𝑦 ↔ (𝐴 ⚬ 𝑥) = 𝐴)) |
40 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑦 ⚬ 𝑥) = (𝐵 ⚬ 𝑥)) |
41 | | id 22 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵) |
42 | 40, 41 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝑦 ⚬ 𝑥) = 𝑦 ↔ (𝐵 ⚬ 𝑥) = 𝐵)) |
43 | 39, 42 | ralprg 4181 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑦 ∈ {𝐴, 𝐵} (𝑦 ⚬ 𝑥) = 𝑦 ↔ ((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵))) |
44 | 36, 43 | syl5bb 271 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑦 ∈ 𝑆 (𝑦 ⚬ 𝑥) = 𝑦 ↔ ((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵))) |
45 | 44 | ralbidv 2969 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑦 ⚬ 𝑥) = 𝑦 ↔ ∀𝑥 ∈ 𝑆 ((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵))) |
46 | 2 | raleqi 3119 |
. . . 4
⊢
(∀𝑥 ∈
𝑆 ((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵) ↔ ∀𝑥 ∈ {𝐴, 𝐵} ((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵)) |
47 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐴 ⚬ 𝑥) = (𝐴 ⚬ 𝐴)) |
48 | 47 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝐴 ⚬ 𝑥) = 𝐴 ↔ (𝐴 ⚬ 𝐴) = 𝐴)) |
49 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐵 ⚬ 𝑥) = (𝐵 ⚬ 𝐴)) |
50 | 49 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝐵 ⚬ 𝑥) = 𝐵 ↔ (𝐵 ⚬ 𝐴) = 𝐵)) |
51 | 48, 50 | anbi12d 743 |
. . . . 5
⊢ (𝑥 = 𝐴 → (((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵) ↔ ((𝐴 ⚬ 𝐴) = 𝐴 ∧ (𝐵 ⚬ 𝐴) = 𝐵))) |
52 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝐴 ⚬ 𝑥) = (𝐴 ⚬ 𝐵)) |
53 | 52 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝐴 ⚬ 𝑥) = 𝐴 ↔ (𝐴 ⚬ 𝐵) = 𝐴)) |
54 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝐵 ⚬ 𝑥) = (𝐵 ⚬ 𝐵)) |
55 | 54 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝐵 ⚬ 𝑥) = 𝐵 ↔ (𝐵 ⚬ 𝐵) = 𝐵)) |
56 | 53, 55 | anbi12d 743 |
. . . . 5
⊢ (𝑥 = 𝐵 → (((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵) ↔ ((𝐴 ⚬ 𝐵) = 𝐴 ∧ (𝐵 ⚬ 𝐵) = 𝐵))) |
57 | 51, 56 | ralprg 4181 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵} ((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵) ↔ (((𝐴 ⚬ 𝐴) = 𝐴 ∧ (𝐵 ⚬ 𝐴) = 𝐵) ∧ ((𝐴 ⚬ 𝐵) = 𝐴 ∧ (𝐵 ⚬ 𝐵) = 𝐵)))) |
58 | 46, 57 | syl5bb 271 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ 𝑆 ((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵) ↔ (((𝐴 ⚬ 𝐴) = 𝐴 ∧ (𝐵 ⚬ 𝐴) = 𝐵) ∧ ((𝐴 ⚬ 𝐵) = 𝐴 ∧ (𝐵 ⚬ 𝐵) = 𝐵)))) |
59 | 45, 58 | bitrd 267 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑦 ⚬ 𝑥) = 𝑦 ↔ (((𝐴 ⚬ 𝐴) = 𝐴 ∧ (𝐵 ⚬ 𝐴) = 𝐵) ∧ ((𝐴 ⚬ 𝐵) = 𝐴 ∧ (𝐵 ⚬ 𝐵) = 𝐵)))) |
60 | 35, 59 | mpbird 246 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑦 ⚬ 𝑥) = 𝑦) |