Proof of Theorem sgrp2rid2
Step | Hyp | Ref
| Expression |
1 | | prid1g 4676 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵}) |
2 | | mgm2nsgrp.s |
. . . 4
⊢ 𝑆 = {𝐴, 𝐵} |
3 | 1, 2 | eleqtrrdi 2849 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑆) |
4 | | prid2g 4677 |
. . . 4
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ {𝐴, 𝐵}) |
5 | 4, 2 | eleqtrrdi 2849 |
. . 3
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ 𝑆) |
6 | | simpl 486 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝐴 ∈ 𝑆) |
7 | | mgm2nsgrp.b |
. . . . . 6
⊢
(Base‘𝑀) =
𝑆 |
8 | | sgrp2nmnd.o |
. . . . . 6
⊢
(+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) |
9 | | sgrp2nmnd.p |
. . . . . 6
⊢ ⚬ =
(+g‘𝑀) |
10 | 2, 7, 8, 9 | sgrp2nmndlem2 18351 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → (𝐴 ⚬ 𝐴) = 𝐴) |
11 | 6, 10 | syldan 594 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ⚬ 𝐴) = 𝐴) |
12 | | oveq1 7220 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → (𝐴 ⚬ 𝐴) = (𝐵 ⚬ 𝐴)) |
13 | | id 22 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) |
14 | 12, 13 | eqeq12d 2753 |
. . . . . 6
⊢ (𝐴 = 𝐵 → ((𝐴 ⚬ 𝐴) = 𝐴 ↔ (𝐵 ⚬ 𝐴) = 𝐵)) |
15 | 11, 14 | syl5ib 247 |
. . . . 5
⊢ (𝐴 = 𝐵 → ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐵 ⚬ 𝐴) = 𝐵)) |
16 | | simprl 771 |
. . . . . . 7
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → 𝐴 ∈ 𝑆) |
17 | | simprr 773 |
. . . . . . 7
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → 𝐵 ∈ 𝑆) |
18 | | neqne 2948 |
. . . . . . . 8
⊢ (¬
𝐴 = 𝐵 → 𝐴 ≠ 𝐵) |
19 | 18 | adantr 484 |
. . . . . . 7
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → 𝐴 ≠ 𝐵) |
20 | 2, 7, 8, 9 | sgrp2nmndlem3 18352 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐵 ⚬ 𝐴) = 𝐵) |
21 | 16, 17, 19, 20 | syl3anc 1373 |
. . . . . 6
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐵 ⚬ 𝐴) = 𝐵) |
22 | 21 | ex 416 |
. . . . 5
⊢ (¬
𝐴 = 𝐵 → ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐵 ⚬ 𝐴) = 𝐵)) |
23 | 15, 22 | pm2.61i 185 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐵 ⚬ 𝐴) = 𝐵) |
24 | 2, 7, 8, 9 | sgrp2nmndlem2 18351 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ⚬ 𝐵) = 𝐴) |
25 | 13, 13 | oveq12d 7231 |
. . . . . . . 8
⊢ (𝐴 = 𝐵 → (𝐴 ⚬ 𝐴) = (𝐵 ⚬ 𝐵)) |
26 | 25, 13 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → ((𝐴 ⚬ 𝐴) = 𝐴 ↔ (𝐵 ⚬ 𝐵) = 𝐵)) |
27 | 11, 26 | syl5ib 247 |
. . . . . 6
⊢ (𝐴 = 𝐵 → ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐵 ⚬ 𝐵) = 𝐵)) |
28 | 2, 7, 8, 9 | sgrp2nmndlem3 18352 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐵 ⚬ 𝐵) = 𝐵) |
29 | 17, 17, 19, 28 | syl3anc 1373 |
. . . . . . 7
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐵 ⚬ 𝐵) = 𝐵) |
30 | 29 | ex 416 |
. . . . . 6
⊢ (¬
𝐴 = 𝐵 → ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐵 ⚬ 𝐵) = 𝐵)) |
31 | 27, 30 | pm2.61i 185 |
. . . . 5
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐵 ⚬ 𝐵) = 𝐵) |
32 | 24, 31 | jca 515 |
. . . 4
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴 ⚬ 𝐵) = 𝐴 ∧ (𝐵 ⚬ 𝐵) = 𝐵)) |
33 | 11, 23, 32 | jca31 518 |
. . 3
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (((𝐴 ⚬ 𝐴) = 𝐴 ∧ (𝐵 ⚬ 𝐴) = 𝐵) ∧ ((𝐴 ⚬ 𝐵) = 𝐴 ∧ (𝐵 ⚬ 𝐵) = 𝐵))) |
34 | 3, 5, 33 | syl2an 599 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (((𝐴 ⚬ 𝐴) = 𝐴 ∧ (𝐵 ⚬ 𝐴) = 𝐵) ∧ ((𝐴 ⚬ 𝐵) = 𝐴 ∧ (𝐵 ⚬ 𝐵) = 𝐵))) |
35 | 2 | raleqi 3323 |
. . . . 5
⊢
(∀𝑦 ∈
𝑆 (𝑦 ⚬ 𝑥) = 𝑦 ↔ ∀𝑦 ∈ {𝐴, 𝐵} (𝑦 ⚬ 𝑥) = 𝑦) |
36 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑦 ⚬ 𝑥) = (𝐴 ⚬ 𝑥)) |
37 | | id 22 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → 𝑦 = 𝐴) |
38 | 36, 37 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((𝑦 ⚬ 𝑥) = 𝑦 ↔ (𝐴 ⚬ 𝑥) = 𝐴)) |
39 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑦 ⚬ 𝑥) = (𝐵 ⚬ 𝑥)) |
40 | | id 22 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵) |
41 | 39, 40 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝑦 ⚬ 𝑥) = 𝑦 ↔ (𝐵 ⚬ 𝑥) = 𝐵)) |
42 | 38, 41 | ralprg 4610 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑦 ∈ {𝐴, 𝐵} (𝑦 ⚬ 𝑥) = 𝑦 ↔ ((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵))) |
43 | 35, 42 | syl5bb 286 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑦 ∈ 𝑆 (𝑦 ⚬ 𝑥) = 𝑦 ↔ ((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵))) |
44 | 43 | ralbidv 3118 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑦 ⚬ 𝑥) = 𝑦 ↔ ∀𝑥 ∈ 𝑆 ((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵))) |
45 | 2 | raleqi 3323 |
. . . 4
⊢
(∀𝑥 ∈
𝑆 ((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵) ↔ ∀𝑥 ∈ {𝐴, 𝐵} ((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵)) |
46 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐴 ⚬ 𝑥) = (𝐴 ⚬ 𝐴)) |
47 | 46 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝐴 ⚬ 𝑥) = 𝐴 ↔ (𝐴 ⚬ 𝐴) = 𝐴)) |
48 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐵 ⚬ 𝑥) = (𝐵 ⚬ 𝐴)) |
49 | 48 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝐵 ⚬ 𝑥) = 𝐵 ↔ (𝐵 ⚬ 𝐴) = 𝐵)) |
50 | 47, 49 | anbi12d 634 |
. . . . 5
⊢ (𝑥 = 𝐴 → (((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵) ↔ ((𝐴 ⚬ 𝐴) = 𝐴 ∧ (𝐵 ⚬ 𝐴) = 𝐵))) |
51 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝐴 ⚬ 𝑥) = (𝐴 ⚬ 𝐵)) |
52 | 51 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝐴 ⚬ 𝑥) = 𝐴 ↔ (𝐴 ⚬ 𝐵) = 𝐴)) |
53 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝐵 ⚬ 𝑥) = (𝐵 ⚬ 𝐵)) |
54 | 53 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝐵 ⚬ 𝑥) = 𝐵 ↔ (𝐵 ⚬ 𝐵) = 𝐵)) |
55 | 52, 54 | anbi12d 634 |
. . . . 5
⊢ (𝑥 = 𝐵 → (((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵) ↔ ((𝐴 ⚬ 𝐵) = 𝐴 ∧ (𝐵 ⚬ 𝐵) = 𝐵))) |
56 | 50, 55 | ralprg 4610 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵} ((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵) ↔ (((𝐴 ⚬ 𝐴) = 𝐴 ∧ (𝐵 ⚬ 𝐴) = 𝐵) ∧ ((𝐴 ⚬ 𝐵) = 𝐴 ∧ (𝐵 ⚬ 𝐵) = 𝐵)))) |
57 | 45, 56 | syl5bb 286 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ 𝑆 ((𝐴 ⚬ 𝑥) = 𝐴 ∧ (𝐵 ⚬ 𝑥) = 𝐵) ↔ (((𝐴 ⚬ 𝐴) = 𝐴 ∧ (𝐵 ⚬ 𝐴) = 𝐵) ∧ ((𝐴 ⚬ 𝐵) = 𝐴 ∧ (𝐵 ⚬ 𝐵) = 𝐵)))) |
58 | 44, 57 | bitrd 282 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑦 ⚬ 𝑥) = 𝑦 ↔ (((𝐴 ⚬ 𝐴) = 𝐴 ∧ (𝐵 ⚬ 𝐴) = 𝐵) ∧ ((𝐴 ⚬ 𝐵) = 𝐴 ∧ (𝐵 ⚬ 𝐵) = 𝐵)))) |
59 | 34, 58 | mpbird 260 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑦 ⚬ 𝑥) = 𝑦) |