# Metamath Proof Explorer

## Theorem symgfcoeu

Description: Uniqueness property of permutations. (Contributed by Thierry Arnoux, 22-Aug-2020)

Ref Expression
Hypothesis symgfcoeu.g ${⊢}{G}={\mathrm{Base}}_{\mathrm{SymGrp}\left({D}\right)}$
Assertion symgfcoeu ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to \exists !{p}\in {G}\phantom{\rule{.4em}{0ex}}{Q}={P}\circ {p}$

### Proof

Step Hyp Ref Expression
1 symgfcoeu.g ${⊢}{G}={\mathrm{Base}}_{\mathrm{SymGrp}\left({D}\right)}$
2 eqid ${⊢}\mathrm{SymGrp}\left({D}\right)=\mathrm{SymGrp}\left({D}\right)$
3 eqid ${⊢}{inv}_{g}\left(\mathrm{SymGrp}\left({D}\right)\right)={inv}_{g}\left(\mathrm{SymGrp}\left({D}\right)\right)$
4 2 1 3 symginv ${⊢}{P}\in {G}\to {inv}_{g}\left(\mathrm{SymGrp}\left({D}\right)\right)\left({P}\right)={{P}}^{-1}$
5 4 3ad2ant2 ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to {inv}_{g}\left(\mathrm{SymGrp}\left({D}\right)\right)\left({P}\right)={{P}}^{-1}$
6 2 symggrp ${⊢}{D}\in {V}\to \mathrm{SymGrp}\left({D}\right)\in \mathrm{Grp}$
7 6 3ad2ant1 ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to \mathrm{SymGrp}\left({D}\right)\in \mathrm{Grp}$
8 simp2 ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to {P}\in {G}$
9 1 3 grpinvcl ${⊢}\left(\mathrm{SymGrp}\left({D}\right)\in \mathrm{Grp}\wedge {P}\in {G}\right)\to {inv}_{g}\left(\mathrm{SymGrp}\left({D}\right)\right)\left({P}\right)\in {G}$
10 7 8 9 syl2anc ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to {inv}_{g}\left(\mathrm{SymGrp}\left({D}\right)\right)\left({P}\right)\in {G}$
11 5 10 eqeltrrd ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to {{P}}^{-1}\in {G}$
12 simp3 ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to {Q}\in {G}$
13 eqid ${⊢}{+}_{\mathrm{SymGrp}\left({D}\right)}={+}_{\mathrm{SymGrp}\left({D}\right)}$
14 2 1 13 symgov ${⊢}\left({{P}}^{-1}\in {G}\wedge {Q}\in {G}\right)\to {{P}}^{-1}{+}_{\mathrm{SymGrp}\left({D}\right)}{Q}={{P}}^{-1}\circ {Q}$
15 2 1 13 symgcl ${⊢}\left({{P}}^{-1}\in {G}\wedge {Q}\in {G}\right)\to {{P}}^{-1}{+}_{\mathrm{SymGrp}\left({D}\right)}{Q}\in {G}$
16 14 15 eqeltrrd ${⊢}\left({{P}}^{-1}\in {G}\wedge {Q}\in {G}\right)\to {{P}}^{-1}\circ {Q}\in {G}$
17 11 12 16 syl2anc ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to {{P}}^{-1}\circ {Q}\in {G}$
18 coass ${⊢}\left({P}\circ {{P}}^{-1}\right)\circ {Q}={P}\circ \left({{P}}^{-1}\circ {Q}\right)$
19 2 1 symgbasf1o ${⊢}{P}\in {G}\to {P}:{D}\underset{1-1 onto}{⟶}{D}$
20 f1ococnv2 ${⊢}{P}:{D}\underset{1-1 onto}{⟶}{D}\to {P}\circ {{P}}^{-1}={\mathrm{I}↾}_{{D}}$
21 8 19 20 3syl ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to {P}\circ {{P}}^{-1}={\mathrm{I}↾}_{{D}}$
22 21 coeq1d ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to \left({P}\circ {{P}}^{-1}\right)\circ {Q}=\left({\mathrm{I}↾}_{{D}}\right)\circ {Q}$
23 18 22 syl5eqr ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to {P}\circ \left({{P}}^{-1}\circ {Q}\right)=\left({\mathrm{I}↾}_{{D}}\right)\circ {Q}$
24 2 1 symgbasf1o ${⊢}{Q}\in {G}\to {Q}:{D}\underset{1-1 onto}{⟶}{D}$
25 f1of ${⊢}{Q}:{D}\underset{1-1 onto}{⟶}{D}\to {Q}:{D}⟶{D}$
26 12 24 25 3syl ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to {Q}:{D}⟶{D}$
27 fcoi2 ${⊢}{Q}:{D}⟶{D}\to \left({\mathrm{I}↾}_{{D}}\right)\circ {Q}={Q}$
28 26 27 syl ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to \left({\mathrm{I}↾}_{{D}}\right)\circ {Q}={Q}$
29 23 28 eqtr2d ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to {Q}={P}\circ \left({{P}}^{-1}\circ {Q}\right)$
30 simpr ${⊢}\left(\left(\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\wedge {p}\in {G}\right)\wedge {Q}={P}\circ {p}\right)\to {Q}={P}\circ {p}$
31 30 coeq2d ${⊢}\left(\left(\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\wedge {p}\in {G}\right)\wedge {Q}={P}\circ {p}\right)\to {{P}}^{-1}\circ {Q}={{P}}^{-1}\circ \left({P}\circ {p}\right)$
32 coass ${⊢}\left({{P}}^{-1}\circ {P}\right)\circ {p}={{P}}^{-1}\circ \left({P}\circ {p}\right)$
33 f1ococnv1 ${⊢}{P}:{D}\underset{1-1 onto}{⟶}{D}\to {{P}}^{-1}\circ {P}={\mathrm{I}↾}_{{D}}$
34 8 19 33 3syl ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to {{P}}^{-1}\circ {P}={\mathrm{I}↾}_{{D}}$
35 34 coeq1d ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to \left({{P}}^{-1}\circ {P}\right)\circ {p}=\left({\mathrm{I}↾}_{{D}}\right)\circ {p}$
36 35 ad2antrr ${⊢}\left(\left(\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\wedge {p}\in {G}\right)\wedge {Q}={P}\circ {p}\right)\to \left({{P}}^{-1}\circ {P}\right)\circ {p}=\left({\mathrm{I}↾}_{{D}}\right)\circ {p}$
37 32 36 syl5eqr ${⊢}\left(\left(\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\wedge {p}\in {G}\right)\wedge {Q}={P}\circ {p}\right)\to {{P}}^{-1}\circ \left({P}\circ {p}\right)=\left({\mathrm{I}↾}_{{D}}\right)\circ {p}$
38 simplr ${⊢}\left(\left(\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\wedge {p}\in {G}\right)\wedge {Q}={P}\circ {p}\right)\to {p}\in {G}$
39 2 1 symgbasf1o ${⊢}{p}\in {G}\to {p}:{D}\underset{1-1 onto}{⟶}{D}$
40 f1of ${⊢}{p}:{D}\underset{1-1 onto}{⟶}{D}\to {p}:{D}⟶{D}$
41 38 39 40 3syl ${⊢}\left(\left(\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\wedge {p}\in {G}\right)\wedge {Q}={P}\circ {p}\right)\to {p}:{D}⟶{D}$
42 fcoi2 ${⊢}{p}:{D}⟶{D}\to \left({\mathrm{I}↾}_{{D}}\right)\circ {p}={p}$
43 41 42 syl ${⊢}\left(\left(\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\wedge {p}\in {G}\right)\wedge {Q}={P}\circ {p}\right)\to \left({\mathrm{I}↾}_{{D}}\right)\circ {p}={p}$
44 31 37 43 3eqtrrd ${⊢}\left(\left(\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\wedge {p}\in {G}\right)\wedge {Q}={P}\circ {p}\right)\to {p}={{P}}^{-1}\circ {Q}$
45 44 ex ${⊢}\left(\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\wedge {p}\in {G}\right)\to \left({Q}={P}\circ {p}\to {p}={{P}}^{-1}\circ {Q}\right)$
46 45 ralrimiva ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to \forall {p}\in {G}\phantom{\rule{.4em}{0ex}}\left({Q}={P}\circ {p}\to {p}={{P}}^{-1}\circ {Q}\right)$
47 coeq2 ${⊢}{p}={{P}}^{-1}\circ {Q}\to {P}\circ {p}={P}\circ \left({{P}}^{-1}\circ {Q}\right)$
48 47 eqeq2d ${⊢}{p}={{P}}^{-1}\circ {Q}\to \left({Q}={P}\circ {p}↔{Q}={P}\circ \left({{P}}^{-1}\circ {Q}\right)\right)$
49 48 eqreu ${⊢}\left({{P}}^{-1}\circ {Q}\in {G}\wedge {Q}={P}\circ \left({{P}}^{-1}\circ {Q}\right)\wedge \forall {p}\in {G}\phantom{\rule{.4em}{0ex}}\left({Q}={P}\circ {p}\to {p}={{P}}^{-1}\circ {Q}\right)\right)\to \exists !{p}\in {G}\phantom{\rule{.4em}{0ex}}{Q}={P}\circ {p}$
50 17 29 46 49 syl3anc ${⊢}\left({D}\in {V}\wedge {P}\in {G}\wedge {Q}\in {G}\right)\to \exists !{p}\in {G}\phantom{\rule{.4em}{0ex}}{Q}={P}\circ {p}$