Step | Hyp | Ref
| Expression |
1 | | grpfo.1 |
. . . 4
⊢ 𝑋 = ran 𝐺 |
2 | 1 | grpoidinv 28589 |
. . 3
⊢ (𝐺 ∈ GrpOp →
∃𝑢 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢))) |
3 | | simpll 767 |
. . . . . . . . 9
⊢ ((((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢)) → (𝑢𝐺𝑧) = 𝑧) |
4 | 3 | ralimi 3083 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢)) → ∀𝑧 ∈ 𝑋 (𝑢𝐺𝑧) = 𝑧) |
5 | | oveq2 7221 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑢𝐺𝑧) = (𝑢𝐺𝑥)) |
6 | | id 22 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → 𝑧 = 𝑥) |
7 | 5, 6 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → ((𝑢𝐺𝑧) = 𝑧 ↔ (𝑢𝐺𝑥) = 𝑥)) |
8 | 7 | cbvralvw 3358 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑋 (𝑢𝐺𝑧) = 𝑧 ↔ ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥) |
9 | 4, 8 | sylib 221 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢)) → ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥) |
10 | 9 | adantl 485 |
. . . . . 6
⊢ (((𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋) ∧ ∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢))) → ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥) |
11 | 9 | ad2antlr 727 |
. . . . . . . 8
⊢ ((((𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋) ∧ ∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢))) ∧ 𝑤 ∈ 𝑋) → ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥) |
12 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢)) → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢)) |
13 | 12 | ralimi 3083 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢)) → ∀𝑧 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢)) |
14 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑤 → (𝑦𝐺𝑧) = (𝑦𝐺𝑤)) |
15 | 14 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑤 → ((𝑦𝐺𝑧) = 𝑢 ↔ (𝑦𝐺𝑤) = 𝑢)) |
16 | | oveq1 7220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑤 → (𝑧𝐺𝑦) = (𝑤𝐺𝑦)) |
17 | 16 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑤 → ((𝑧𝐺𝑦) = 𝑢 ↔ (𝑤𝐺𝑦) = 𝑢)) |
18 | 15, 17 | anbi12d 634 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑤 → (((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢) ↔ ((𝑦𝐺𝑤) = 𝑢 ∧ (𝑤𝐺𝑦) = 𝑢))) |
19 | 18 | rexbidv 3216 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑤 → (∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢) ↔ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑤) = 𝑢 ∧ (𝑤𝐺𝑦) = 𝑢))) |
20 | 19 | rspcva 3535 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ 𝑋 ∧ ∀𝑧 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢)) → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑤) = 𝑢 ∧ (𝑤𝐺𝑦) = 𝑢)) |
21 | 20 | adantll 714 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋) ∧ ∀𝑧 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢)) → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑤) = 𝑢 ∧ (𝑤𝐺𝑦) = 𝑢)) |
22 | 13, 21 | sylan2 596 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋) ∧ ∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢))) → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑤) = 𝑢 ∧ (𝑤𝐺𝑦) = 𝑢)) |
23 | 1 | grpoidinvlem4 28588 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑤) = 𝑢 ∧ (𝑤𝐺𝑦) = 𝑢)) → (𝑤𝐺𝑢) = (𝑢𝐺𝑤)) |
24 | 22, 23 | syldan 594 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ GrpOp ∧ 𝑤 ∈ 𝑋) ∧ ∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢))) → (𝑤𝐺𝑢) = (𝑢𝐺𝑤)) |
25 | 24 | an32s 652 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ GrpOp ∧
∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢))) ∧ 𝑤 ∈ 𝑋) → (𝑤𝐺𝑢) = (𝑢𝐺𝑤)) |
26 | 25 | adantllr 719 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋) ∧ ∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢))) ∧ 𝑤 ∈ 𝑋) → (𝑤𝐺𝑢) = (𝑢𝐺𝑤)) |
27 | 26 | adantr 484 |
. . . . . . . . . 10
⊢
(((((𝐺 ∈ GrpOp
∧ 𝑢 ∈ 𝑋) ∧ ∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢))) ∧ 𝑤 ∈ 𝑋) ∧ (∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥 ∧ ∀𝑥 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑥)) → (𝑤𝐺𝑢) = (𝑢𝐺𝑤)) |
28 | | oveq2 7221 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑢 → (𝑤𝐺𝑥) = (𝑤𝐺𝑢)) |
29 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑢 → 𝑥 = 𝑢) |
30 | 28, 29 | eqeq12d 2753 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑢 → ((𝑤𝐺𝑥) = 𝑥 ↔ (𝑤𝐺𝑢) = 𝑢)) |
31 | 30 | rspcva 3535 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑥) → (𝑤𝐺𝑢) = 𝑢) |
32 | 31 | adantll 714 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑥) → (𝑤𝐺𝑢) = 𝑢) |
33 | 32 | ad2ant2rl 749 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) ∧ (∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥 ∧ ∀𝑥 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑥)) → (𝑤𝐺𝑢) = 𝑢) |
34 | 33 | adantllr 719 |
. . . . . . . . . 10
⊢
(((((𝐺 ∈ GrpOp
∧ 𝑢 ∈ 𝑋) ∧ ∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢))) ∧ 𝑤 ∈ 𝑋) ∧ (∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥 ∧ ∀𝑥 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑥)) → (𝑤𝐺𝑢) = 𝑢) |
35 | | oveq2 7221 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝑢𝐺𝑥) = (𝑢𝐺𝑤)) |
36 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → 𝑥 = 𝑤) |
37 | 35, 36 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → ((𝑢𝐺𝑥) = 𝑥 ↔ (𝑢𝐺𝑤) = 𝑤)) |
38 | 37 | rspcva 3535 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥) → (𝑢𝐺𝑤) = 𝑤) |
39 | 38 | ad2ant2lr 748 |
. . . . . . . . . 10
⊢
(((((𝐺 ∈ GrpOp
∧ 𝑢 ∈ 𝑋) ∧ ∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢))) ∧ 𝑤 ∈ 𝑋) ∧ (∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥 ∧ ∀𝑥 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑥)) → (𝑢𝐺𝑤) = 𝑤) |
40 | 27, 34, 39 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢
(((((𝐺 ∈ GrpOp
∧ 𝑢 ∈ 𝑋) ∧ ∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢))) ∧ 𝑤 ∈ 𝑋) ∧ (∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥 ∧ ∀𝑥 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑥)) → 𝑢 = 𝑤) |
41 | 40 | ex 416 |
. . . . . . . 8
⊢ ((((𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋) ∧ ∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢))) ∧ 𝑤 ∈ 𝑋) → ((∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥 ∧ ∀𝑥 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑥) → 𝑢 = 𝑤)) |
42 | 11, 41 | mpand 695 |
. . . . . . 7
⊢ ((((𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋) ∧ ∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢))) ∧ 𝑤 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑥 → 𝑢 = 𝑤)) |
43 | 42 | ralrimiva 3105 |
. . . . . 6
⊢ (((𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋) ∧ ∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢))) → ∀𝑤 ∈ 𝑋 (∀𝑥 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑥 → 𝑢 = 𝑤)) |
44 | 10, 43 | jca 515 |
. . . . 5
⊢ (((𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋) ∧ ∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢))) → (∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥 ∧ ∀𝑤 ∈ 𝑋 (∀𝑥 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑥 → 𝑢 = 𝑤))) |
45 | 44 | ex 416 |
. . . 4
⊢ ((𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋) → (∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢)) → (∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥 ∧ ∀𝑤 ∈ 𝑋 (∀𝑥 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑥 → 𝑢 = 𝑤)))) |
46 | 45 | reximdva 3193 |
. . 3
⊢ (𝐺 ∈ GrpOp →
(∃𝑢 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (((𝑢𝐺𝑧) = 𝑧 ∧ (𝑧𝐺𝑢) = 𝑧) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑧) = 𝑢 ∧ (𝑧𝐺𝑦) = 𝑢)) → ∃𝑢 ∈ 𝑋 (∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥 ∧ ∀𝑤 ∈ 𝑋 (∀𝑥 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑥 → 𝑢 = 𝑤)))) |
47 | 2, 46 | mpd 15 |
. 2
⊢ (𝐺 ∈ GrpOp →
∃𝑢 ∈ 𝑋 (∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥 ∧ ∀𝑤 ∈ 𝑋 (∀𝑥 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑥 → 𝑢 = 𝑤))) |
48 | | oveq1 7220 |
. . . . 5
⊢ (𝑢 = 𝑤 → (𝑢𝐺𝑥) = (𝑤𝐺𝑥)) |
49 | 48 | eqeq1d 2739 |
. . . 4
⊢ (𝑢 = 𝑤 → ((𝑢𝐺𝑥) = 𝑥 ↔ (𝑤𝐺𝑥) = 𝑥)) |
50 | 49 | ralbidv 3118 |
. . 3
⊢ (𝑢 = 𝑤 → (∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥 ↔ ∀𝑥 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑥)) |
51 | 50 | reu8 3646 |
. 2
⊢
(∃!𝑢 ∈
𝑋 ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥 ↔ ∃𝑢 ∈ 𝑋 (∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥 ∧ ∀𝑤 ∈ 𝑋 (∀𝑥 ∈ 𝑋 (𝑤𝐺𝑥) = 𝑥 → 𝑢 = 𝑤))) |
52 | 47, 51 | sylibr 237 |
1
⊢ (𝐺 ∈ GrpOp →
∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥) |