Proof of Theorem symgfcoeu
Step | Hyp | Ref
| Expression |
1 | | eqid 2778 |
. . . . . 6
⊢
(SymGrp‘𝐷) =
(SymGrp‘𝐷) |
2 | | symgfcoeu.g |
. . . . . 6
⊢ 𝐺 =
(Base‘(SymGrp‘𝐷)) |
3 | | eqid 2778 |
. . . . . 6
⊢
(invg‘(SymGrp‘𝐷)) =
(invg‘(SymGrp‘𝐷)) |
4 | 1, 2, 3 | symginv 18209 |
. . . . 5
⊢ (𝑃 ∈ 𝐺 →
((invg‘(SymGrp‘𝐷))‘𝑃) = ◡𝑃) |
5 | 4 | 3ad2ant2 1125 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) →
((invg‘(SymGrp‘𝐷))‘𝑃) = ◡𝑃) |
6 | 1 | symggrp 18207 |
. . . . . 6
⊢ (𝐷 ∈ 𝑉 → (SymGrp‘𝐷) ∈ Grp) |
7 | 6 | 3ad2ant1 1124 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (SymGrp‘𝐷) ∈ Grp) |
8 | | simp2 1128 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → 𝑃 ∈ 𝐺) |
9 | 2, 3 | grpinvcl 17858 |
. . . . 5
⊢
(((SymGrp‘𝐷)
∈ Grp ∧ 𝑃 ∈
𝐺) →
((invg‘(SymGrp‘𝐷))‘𝑃) ∈ 𝐺) |
10 | 7, 8, 9 | syl2anc 579 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) →
((invg‘(SymGrp‘𝐷))‘𝑃) ∈ 𝐺) |
11 | 5, 10 | eqeltrrd 2860 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ◡𝑃 ∈ 𝐺) |
12 | | simp3 1129 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → 𝑄 ∈ 𝐺) |
13 | | eqid 2778 |
. . . . 5
⊢
(+g‘(SymGrp‘𝐷)) =
(+g‘(SymGrp‘𝐷)) |
14 | 1, 2, 13 | symgov 18197 |
. . . 4
⊢ ((◡𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (◡𝑃(+g‘(SymGrp‘𝐷))𝑄) = (◡𝑃 ∘ 𝑄)) |
15 | 1, 2, 13 | symgcl 18198 |
. . . 4
⊢ ((◡𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (◡𝑃(+g‘(SymGrp‘𝐷))𝑄) ∈ 𝐺) |
16 | 14, 15 | eqeltrrd 2860 |
. . 3
⊢ ((◡𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (◡𝑃 ∘ 𝑄) ∈ 𝐺) |
17 | 11, 12, 16 | syl2anc 579 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (◡𝑃 ∘ 𝑄) ∈ 𝐺) |
18 | | coass 5910 |
. . . 4
⊢ ((𝑃 ∘ ◡𝑃) ∘ 𝑄) = (𝑃 ∘ (◡𝑃 ∘ 𝑄)) |
19 | 1, 2 | symgbasf1o 18190 |
. . . . . 6
⊢ (𝑃 ∈ 𝐺 → 𝑃:𝐷–1-1-onto→𝐷) |
20 | | f1ococnv2 6419 |
. . . . . 6
⊢ (𝑃:𝐷–1-1-onto→𝐷 → (𝑃 ∘ ◡𝑃) = ( I ↾ 𝐷)) |
21 | 8, 19, 20 | 3syl 18 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (𝑃 ∘ ◡𝑃) = ( I ↾ 𝐷)) |
22 | 21 | coeq1d 5531 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ((𝑃 ∘ ◡𝑃) ∘ 𝑄) = (( I ↾ 𝐷) ∘ 𝑄)) |
23 | 18, 22 | syl5eqr 2828 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (𝑃 ∘ (◡𝑃 ∘ 𝑄)) = (( I ↾ 𝐷) ∘ 𝑄)) |
24 | 1, 2 | symgbasf1o 18190 |
. . . . 5
⊢ (𝑄 ∈ 𝐺 → 𝑄:𝐷–1-1-onto→𝐷) |
25 | | f1of 6393 |
. . . . 5
⊢ (𝑄:𝐷–1-1-onto→𝐷 → 𝑄:𝐷⟶𝐷) |
26 | 12, 24, 25 | 3syl 18 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → 𝑄:𝐷⟶𝐷) |
27 | | fcoi2 6331 |
. . . 4
⊢ (𝑄:𝐷⟶𝐷 → (( I ↾ 𝐷) ∘ 𝑄) = 𝑄) |
28 | 26, 27 | syl 17 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (( I ↾ 𝐷) ∘ 𝑄) = 𝑄) |
29 | 23, 28 | eqtr2d 2815 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → 𝑄 = (𝑃 ∘ (◡𝑃 ∘ 𝑄))) |
30 | | simpr 479 |
. . . . . 6
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) ∧ 𝑄 = (𝑃 ∘ 𝑝)) → 𝑄 = (𝑃 ∘ 𝑝)) |
31 | 30 | coeq2d 5532 |
. . . . 5
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) ∧ 𝑄 = (𝑃 ∘ 𝑝)) → (◡𝑃 ∘ 𝑄) = (◡𝑃 ∘ (𝑃 ∘ 𝑝))) |
32 | | coass 5910 |
. . . . . . 7
⊢ ((◡𝑃 ∘ 𝑃) ∘ 𝑝) = (◡𝑃 ∘ (𝑃 ∘ 𝑝)) |
33 | 32 | a1i 11 |
. . . . . 6
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) ∧ 𝑄 = (𝑃 ∘ 𝑝)) → ((◡𝑃 ∘ 𝑃) ∘ 𝑝) = (◡𝑃 ∘ (𝑃 ∘ 𝑝))) |
34 | | f1ococnv1 6421 |
. . . . . . . . 9
⊢ (𝑃:𝐷–1-1-onto→𝐷 → (◡𝑃 ∘ 𝑃) = ( I ↾ 𝐷)) |
35 | 8, 19, 34 | 3syl 18 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (◡𝑃 ∘ 𝑃) = ( I ↾ 𝐷)) |
36 | 35 | coeq1d 5531 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ((◡𝑃 ∘ 𝑃) ∘ 𝑝) = (( I ↾ 𝐷) ∘ 𝑝)) |
37 | 36 | ad2antrr 716 |
. . . . . 6
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) ∧ 𝑄 = (𝑃 ∘ 𝑝)) → ((◡𝑃 ∘ 𝑃) ∘ 𝑝) = (( I ↾ 𝐷) ∘ 𝑝)) |
38 | 33, 37 | eqtr3d 2816 |
. . . . 5
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) ∧ 𝑄 = (𝑃 ∘ 𝑝)) → (◡𝑃 ∘ (𝑃 ∘ 𝑝)) = (( I ↾ 𝐷) ∘ 𝑝)) |
39 | | simplr 759 |
. . . . . . 7
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) ∧ 𝑄 = (𝑃 ∘ 𝑝)) → 𝑝 ∈ 𝐺) |
40 | 1, 2 | symgbasf1o 18190 |
. . . . . . 7
⊢ (𝑝 ∈ 𝐺 → 𝑝:𝐷–1-1-onto→𝐷) |
41 | | f1of 6393 |
. . . . . . 7
⊢ (𝑝:𝐷–1-1-onto→𝐷 → 𝑝:𝐷⟶𝐷) |
42 | 39, 40, 41 | 3syl 18 |
. . . . . 6
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) ∧ 𝑄 = (𝑃 ∘ 𝑝)) → 𝑝:𝐷⟶𝐷) |
43 | | fcoi2 6331 |
. . . . . 6
⊢ (𝑝:𝐷⟶𝐷 → (( I ↾ 𝐷) ∘ 𝑝) = 𝑝) |
44 | 42, 43 | syl 17 |
. . . . 5
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) ∧ 𝑄 = (𝑃 ∘ 𝑝)) → (( I ↾ 𝐷) ∘ 𝑝) = 𝑝) |
45 | 31, 38, 44 | 3eqtrrd 2819 |
. . . 4
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) ∧ 𝑄 = (𝑃 ∘ 𝑝)) → 𝑝 = (◡𝑃 ∘ 𝑄)) |
46 | 45 | ex 403 |
. . 3
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) → (𝑄 = (𝑃 ∘ 𝑝) → 𝑝 = (◡𝑃 ∘ 𝑄))) |
47 | 46 | ralrimiva 3148 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ∀𝑝 ∈ 𝐺 (𝑄 = (𝑃 ∘ 𝑝) → 𝑝 = (◡𝑃 ∘ 𝑄))) |
48 | | eqidd 2779 |
. . . 4
⊢ (𝑝 = (◡𝑃 ∘ 𝑄) → 𝑄 = 𝑄) |
49 | | coeq2 5528 |
. . . 4
⊢ (𝑝 = (◡𝑃 ∘ 𝑄) → (𝑃 ∘ 𝑝) = (𝑃 ∘ (◡𝑃 ∘ 𝑄))) |
50 | 48, 49 | eqeq12d 2793 |
. . 3
⊢ (𝑝 = (◡𝑃 ∘ 𝑄) → (𝑄 = (𝑃 ∘ 𝑝) ↔ 𝑄 = (𝑃 ∘ (◡𝑃 ∘ 𝑄)))) |
51 | 50 | eqreu 3610 |
. 2
⊢ (((◡𝑃 ∘ 𝑄) ∈ 𝐺 ∧ 𝑄 = (𝑃 ∘ (◡𝑃 ∘ 𝑄)) ∧ ∀𝑝 ∈ 𝐺 (𝑄 = (𝑃 ∘ 𝑝) → 𝑝 = (◡𝑃 ∘ 𝑄))) → ∃!𝑝 ∈ 𝐺 𝑄 = (𝑃 ∘ 𝑝)) |
52 | 17, 29, 47, 51 | syl3anc 1439 |
1
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑄 = (𝑃 ∘ 𝑝)) |