Proof of Theorem symgfcoeu
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . 6
⊢
(SymGrp‘𝐷) =
(SymGrp‘𝐷) |
| 2 | | symgfcoeu.g |
. . . . . 6
⊢ 𝐺 =
(Base‘(SymGrp‘𝐷)) |
| 3 | | eqid 2737 |
. . . . . 6
⊢
(invg‘(SymGrp‘𝐷)) =
(invg‘(SymGrp‘𝐷)) |
| 4 | 1, 2, 3 | symginv 19420 |
. . . . 5
⊢ (𝑃 ∈ 𝐺 →
((invg‘(SymGrp‘𝐷))‘𝑃) = ◡𝑃) |
| 5 | 4 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) →
((invg‘(SymGrp‘𝐷))‘𝑃) = ◡𝑃) |
| 6 | 1 | symggrp 19418 |
. . . . . 6
⊢ (𝐷 ∈ 𝑉 → (SymGrp‘𝐷) ∈ Grp) |
| 7 | 6 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (SymGrp‘𝐷) ∈ Grp) |
| 8 | | simp2 1138 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → 𝑃 ∈ 𝐺) |
| 9 | 2, 3 | grpinvcl 19005 |
. . . . 5
⊢
(((SymGrp‘𝐷)
∈ Grp ∧ 𝑃 ∈
𝐺) →
((invg‘(SymGrp‘𝐷))‘𝑃) ∈ 𝐺) |
| 10 | 7, 8, 9 | syl2anc 584 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) →
((invg‘(SymGrp‘𝐷))‘𝑃) ∈ 𝐺) |
| 11 | 5, 10 | eqeltrrd 2842 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ◡𝑃 ∈ 𝐺) |
| 12 | | simp3 1139 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → 𝑄 ∈ 𝐺) |
| 13 | | eqid 2737 |
. . . . 5
⊢
(+g‘(SymGrp‘𝐷)) =
(+g‘(SymGrp‘𝐷)) |
| 14 | 1, 2, 13 | symgov 19401 |
. . . 4
⊢ ((◡𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (◡𝑃(+g‘(SymGrp‘𝐷))𝑄) = (◡𝑃 ∘ 𝑄)) |
| 15 | 1, 2, 13 | symgcl 19402 |
. . . 4
⊢ ((◡𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (◡𝑃(+g‘(SymGrp‘𝐷))𝑄) ∈ 𝐺) |
| 16 | 14, 15 | eqeltrrd 2842 |
. . 3
⊢ ((◡𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (◡𝑃 ∘ 𝑄) ∈ 𝐺) |
| 17 | 11, 12, 16 | syl2anc 584 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (◡𝑃 ∘ 𝑄) ∈ 𝐺) |
| 18 | | coass 6285 |
. . . 4
⊢ ((𝑃 ∘ ◡𝑃) ∘ 𝑄) = (𝑃 ∘ (◡𝑃 ∘ 𝑄)) |
| 19 | 1, 2 | symgbasf1o 19392 |
. . . . . 6
⊢ (𝑃 ∈ 𝐺 → 𝑃:𝐷–1-1-onto→𝐷) |
| 20 | | f1ococnv2 6875 |
. . . . . 6
⊢ (𝑃:𝐷–1-1-onto→𝐷 → (𝑃 ∘ ◡𝑃) = ( I ↾ 𝐷)) |
| 21 | 8, 19, 20 | 3syl 18 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (𝑃 ∘ ◡𝑃) = ( I ↾ 𝐷)) |
| 22 | 21 | coeq1d 5872 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ((𝑃 ∘ ◡𝑃) ∘ 𝑄) = (( I ↾ 𝐷) ∘ 𝑄)) |
| 23 | 18, 22 | eqtr3id 2791 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (𝑃 ∘ (◡𝑃 ∘ 𝑄)) = (( I ↾ 𝐷) ∘ 𝑄)) |
| 24 | 1, 2 | symgbasf1o 19392 |
. . . 4
⊢ (𝑄 ∈ 𝐺 → 𝑄:𝐷–1-1-onto→𝐷) |
| 25 | | f1of 6848 |
. . . 4
⊢ (𝑄:𝐷–1-1-onto→𝐷 → 𝑄:𝐷⟶𝐷) |
| 26 | | fcoi2 6783 |
. . . 4
⊢ (𝑄:𝐷⟶𝐷 → (( I ↾ 𝐷) ∘ 𝑄) = 𝑄) |
| 27 | 12, 24, 25, 26 | 4syl 19 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (( I ↾ 𝐷) ∘ 𝑄) = 𝑄) |
| 28 | 23, 27 | eqtr2d 2778 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → 𝑄 = (𝑃 ∘ (◡𝑃 ∘ 𝑄))) |
| 29 | | simpr 484 |
. . . . . 6
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) ∧ 𝑄 = (𝑃 ∘ 𝑝)) → 𝑄 = (𝑃 ∘ 𝑝)) |
| 30 | 29 | coeq2d 5873 |
. . . . 5
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) ∧ 𝑄 = (𝑃 ∘ 𝑝)) → (◡𝑃 ∘ 𝑄) = (◡𝑃 ∘ (𝑃 ∘ 𝑝))) |
| 31 | | coass 6285 |
. . . . . 6
⊢ ((◡𝑃 ∘ 𝑃) ∘ 𝑝) = (◡𝑃 ∘ (𝑃 ∘ 𝑝)) |
| 32 | | f1ococnv1 6877 |
. . . . . . . . 9
⊢ (𝑃:𝐷–1-1-onto→𝐷 → (◡𝑃 ∘ 𝑃) = ( I ↾ 𝐷)) |
| 33 | 8, 19, 32 | 3syl 18 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → (◡𝑃 ∘ 𝑃) = ( I ↾ 𝐷)) |
| 34 | 33 | coeq1d 5872 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ((◡𝑃 ∘ 𝑃) ∘ 𝑝) = (( I ↾ 𝐷) ∘ 𝑝)) |
| 35 | 34 | ad2antrr 726 |
. . . . . 6
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) ∧ 𝑄 = (𝑃 ∘ 𝑝)) → ((◡𝑃 ∘ 𝑃) ∘ 𝑝) = (( I ↾ 𝐷) ∘ 𝑝)) |
| 36 | 31, 35 | eqtr3id 2791 |
. . . . 5
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) ∧ 𝑄 = (𝑃 ∘ 𝑝)) → (◡𝑃 ∘ (𝑃 ∘ 𝑝)) = (( I ↾ 𝐷) ∘ 𝑝)) |
| 37 | | simplr 769 |
. . . . . 6
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) ∧ 𝑄 = (𝑃 ∘ 𝑝)) → 𝑝 ∈ 𝐺) |
| 38 | 1, 2 | symgbasf1o 19392 |
. . . . . 6
⊢ (𝑝 ∈ 𝐺 → 𝑝:𝐷–1-1-onto→𝐷) |
| 39 | | f1of 6848 |
. . . . . 6
⊢ (𝑝:𝐷–1-1-onto→𝐷 → 𝑝:𝐷⟶𝐷) |
| 40 | | fcoi2 6783 |
. . . . . 6
⊢ (𝑝:𝐷⟶𝐷 → (( I ↾ 𝐷) ∘ 𝑝) = 𝑝) |
| 41 | 37, 38, 39, 40 | 4syl 19 |
. . . . 5
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) ∧ 𝑄 = (𝑃 ∘ 𝑝)) → (( I ↾ 𝐷) ∘ 𝑝) = 𝑝) |
| 42 | 30, 36, 41 | 3eqtrrd 2782 |
. . . 4
⊢ ((((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) ∧ 𝑄 = (𝑃 ∘ 𝑝)) → 𝑝 = (◡𝑃 ∘ 𝑄)) |
| 43 | 42 | ex 412 |
. . 3
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) ∧ 𝑝 ∈ 𝐺) → (𝑄 = (𝑃 ∘ 𝑝) → 𝑝 = (◡𝑃 ∘ 𝑄))) |
| 44 | 43 | ralrimiva 3146 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ∀𝑝 ∈ 𝐺 (𝑄 = (𝑃 ∘ 𝑝) → 𝑝 = (◡𝑃 ∘ 𝑄))) |
| 45 | | coeq2 5869 |
. . . 4
⊢ (𝑝 = (◡𝑃 ∘ 𝑄) → (𝑃 ∘ 𝑝) = (𝑃 ∘ (◡𝑃 ∘ 𝑄))) |
| 46 | 45 | eqeq2d 2748 |
. . 3
⊢ (𝑝 = (◡𝑃 ∘ 𝑄) → (𝑄 = (𝑃 ∘ 𝑝) ↔ 𝑄 = (𝑃 ∘ (◡𝑃 ∘ 𝑄)))) |
| 47 | 46 | eqreu 3735 |
. 2
⊢ (((◡𝑃 ∘ 𝑄) ∈ 𝐺 ∧ 𝑄 = (𝑃 ∘ (◡𝑃 ∘ 𝑄)) ∧ ∀𝑝 ∈ 𝐺 (𝑄 = (𝑃 ∘ 𝑝) → 𝑝 = (◡𝑃 ∘ 𝑄))) → ∃!𝑝 ∈ 𝐺 𝑄 = (𝑃 ∘ 𝑝)) |
| 48 | 17, 28, 44, 47 | syl3anc 1373 |
1
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑄 = (𝑃 ∘ 𝑝)) |