Metamath Proof Explorer

Theorem symgfcoeu

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

Ref Expression
Hypothesis symgfcoeu.g 
|- G = ( Base ` ( SymGrp ` D ) )
Assertion symgfcoeu 
|- ( ( D e. V /\ P e. G /\ Q e. G ) -> E! p e. G Q = ( P o. p ) )

Proof

Step Hyp Ref Expression
1 symgfcoeu.g 
 |-  G = ( Base ` ( SymGrp ` D ) )
2 eqid 
 |-  ( SymGrp ` D ) = ( SymGrp ` D )
3 eqid 
 |-  ( invg ` ( SymGrp ` D ) ) = ( invg ` ( SymGrp ` D ) )
4 2 1 3 symginv 
 |-  ( P e. G -> ( ( invg ` ( SymGrp ` D ) ) ` P ) = `' P )
5 4 3ad2ant2 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> ( ( invg ` ( SymGrp ` D ) ) ` P ) = `' P )
6 2 symggrp 
 |-  ( D e. V -> ( SymGrp ` D ) e. Grp )
7 6 3ad2ant1 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> ( SymGrp ` D ) e. Grp )
8 simp2 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> P e. G )
9 1 3 grpinvcl 
 |-  ( ( ( SymGrp ` D ) e. Grp /\ P e. G ) -> ( ( invg ` ( SymGrp ` D ) ) ` P ) e. G )
10 7 8 9 syl2anc 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> ( ( invg ` ( SymGrp ` D ) ) ` P ) e. G )
11 5 10 eqeltrrd 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> `' P e. G )
12 simp3 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> Q e. G )
13 eqid 
 |-  ( +g ` ( SymGrp ` D ) ) = ( +g ` ( SymGrp ` D ) )
14 2 1 13 symgov 
 |-  ( ( `' P e. G /\ Q e. G ) -> ( `' P ( +g ` ( SymGrp ` D ) ) Q ) = ( `' P o. Q ) )
15 2 1 13 symgcl 
 |-  ( ( `' P e. G /\ Q e. G ) -> ( `' P ( +g ` ( SymGrp ` D ) ) Q ) e. G )
16 14 15 eqeltrrd 
 |-  ( ( `' P e. G /\ Q e. G ) -> ( `' P o. Q ) e. G )
17 11 12 16 syl2anc 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> ( `' P o. Q ) e. G )
18 coass 
 |-  ( ( P o. `' P ) o. Q ) = ( P o. ( `' P o. Q ) )
19 2 1 symgbasf1o 
 |-  ( P e. G -> P : D -1-1-onto-> D )
20 f1ococnv2 
 |-  ( P : D -1-1-onto-> D -> ( P o. `' P ) = ( _I |` D ) )
21 8 19 20 3syl 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> ( P o. `' P ) = ( _I |` D ) )
22 21 coeq1d 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> ( ( P o. `' P ) o. Q ) = ( ( _I |` D ) o. Q ) )
23 18 22 eqtr3id 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> ( P o. ( `' P o. Q ) ) = ( ( _I |` D ) o. Q ) )
24 2 1 symgbasf1o 
 |-  ( Q e. G -> Q : D -1-1-onto-> D )
25 f1of 
 |-  ( Q : D -1-1-onto-> D -> Q : D --> D )
26 12 24 25 3syl 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> Q : D --> D )
27 fcoi2 
 |-  ( Q : D --> D -> ( ( _I |` D ) o. Q ) = Q )
28 26 27 syl 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> ( ( _I |` D ) o. Q ) = Q )
29 23 28 eqtr2d 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> Q = ( P o. ( `' P o. Q ) ) )
30 simpr 
 |-  ( ( ( ( D e. V /\ P e. G /\ Q e. G ) /\ p e. G ) /\ Q = ( P o. p ) ) -> Q = ( P o. p ) )
31 30 coeq2d 
 |-  ( ( ( ( D e. V /\ P e. G /\ Q e. G ) /\ p e. G ) /\ Q = ( P o. p ) ) -> ( `' P o. Q ) = ( `' P o. ( P o. p ) ) )
32 coass 
 |-  ( ( `' P o. P ) o. p ) = ( `' P o. ( P o. p ) )
33 f1ococnv1 
 |-  ( P : D -1-1-onto-> D -> ( `' P o. P ) = ( _I |` D ) )
34 8 19 33 3syl 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> ( `' P o. P ) = ( _I |` D ) )
35 34 coeq1d 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> ( ( `' P o. P ) o. p ) = ( ( _I |` D ) o. p ) )
36 35 ad2antrr 
 |-  ( ( ( ( D e. V /\ P e. G /\ Q e. G ) /\ p e. G ) /\ Q = ( P o. p ) ) -> ( ( `' P o. P ) o. p ) = ( ( _I |` D ) o. p ) )
37 32 36 eqtr3id 
 |-  ( ( ( ( D e. V /\ P e. G /\ Q e. G ) /\ p e. G ) /\ Q = ( P o. p ) ) -> ( `' P o. ( P o. p ) ) = ( ( _I |` D ) o. p ) )
38 simplr 
 |-  ( ( ( ( D e. V /\ P e. G /\ Q e. G ) /\ p e. G ) /\ Q = ( P o. p ) ) -> p e. G )
39 2 1 symgbasf1o 
 |-  ( p e. G -> p : D -1-1-onto-> D )
40 f1of 
 |-  ( p : D -1-1-onto-> D -> p : D --> D )
41 38 39 40 3syl 
 |-  ( ( ( ( D e. V /\ P e. G /\ Q e. G ) /\ p e. G ) /\ Q = ( P o. p ) ) -> p : D --> D )
42 fcoi2 
 |-  ( p : D --> D -> ( ( _I |` D ) o. p ) = p )
43 41 42 syl 
 |-  ( ( ( ( D e. V /\ P e. G /\ Q e. G ) /\ p e. G ) /\ Q = ( P o. p ) ) -> ( ( _I |` D ) o. p ) = p )
44 31 37 43 3eqtrrd 
 |-  ( ( ( ( D e. V /\ P e. G /\ Q e. G ) /\ p e. G ) /\ Q = ( P o. p ) ) -> p = ( `' P o. Q ) )
45 44 ex 
 |-  ( ( ( D e. V /\ P e. G /\ Q e. G ) /\ p e. G ) -> ( Q = ( P o. p ) -> p = ( `' P o. Q ) ) )
46 45 ralrimiva 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> A. p e. G ( Q = ( P o. p ) -> p = ( `' P o. Q ) ) )
47 coeq2 
 |-  ( p = ( `' P o. Q ) -> ( P o. p ) = ( P o. ( `' P o. Q ) ) )
48 47 eqeq2d 
 |-  ( p = ( `' P o. Q ) -> ( Q = ( P o. p ) <-> Q = ( P o. ( `' P o. Q ) ) ) )
49 48 eqreu 
 |-  ( ( ( `' P o. Q ) e. G /\ Q = ( P o. ( `' P o. Q ) ) /\ A. p e. G ( Q = ( P o. p ) -> p = ( `' P o. Q ) ) ) -> E! p e. G Q = ( P o. p ) )
50 17 29 46 49 syl3anc 
 |-  ( ( D e. V /\ P e. G /\ Q e. G ) -> E! p e. G Q = ( P o. p ) )