Metamath Proof Explorer

Theorem symgfcoeu

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

Ref Expression
Hypothesis symgfcoeu.g ⊢ 𝐺 = ( Base ‘ ( SymGrp ‘ 𝐷 ) )
Assertion symgfcoeu ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ∃! 𝑝 ∈ 𝐺 𝑄 = ( 𝑃 ∘ 𝑝 ) )

Proof

Step Hyp Ref Expression
1 symgfcoeu.g ⊢ 𝐺 = ( Base ‘ ( SymGrp ‘ 𝐷 ) )
2 eqid ⊢ ( SymGrp ‘ 𝐷 ) = ( SymGrp ‘ 𝐷 )
3 eqid ⊢ ( invg ‘ ( SymGrp ‘ 𝐷 ) ) = ( invg ‘ ( SymGrp ‘ 𝐷 ) )
4 2 1 3 symginv ⊢ ( 𝑃 ∈ 𝐺 → ( ( invg ‘ ( SymGrp ‘ 𝐷 ) ) ‘ 𝑃 ) = ◡ 𝑃 )
5 4 3ad2ant2 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ( ( invg ‘ ( SymGrp ‘ 𝐷 ) ) ‘ 𝑃 ) = ◡ 𝑃 )
6 2 symggrp ⊢ ( 𝐷 ∈ 𝑉 → ( SymGrp ‘ 𝐷 ) ∈ Grp )
7 6 3ad2ant1 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ( SymGrp ‘ 𝐷 ) ∈ Grp )
8 simp2 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → 𝑃 ∈ 𝐺 )
9 1 3 grpinvcl ⊢ ( ( ( SymGrp ‘ 𝐷 ) ∈ Grp ∧ 𝑃 ∈ 𝐺 ) → ( ( invg ‘ ( SymGrp ‘ 𝐷 ) ) ‘ 𝑃 ) ∈ 𝐺 )
10 7 8 9 syl2anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ( ( invg ‘ ( SymGrp ‘ 𝐷 ) ) ‘ 𝑃 ) ∈ 𝐺 )
11 5 10 eqeltrrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ◡ 𝑃 ∈ 𝐺 )
12 simp3 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → 𝑄 ∈ 𝐺 )
13 eqid ⊢ ( +g ‘ ( SymGrp ‘ 𝐷 ) ) = ( +g ‘ ( SymGrp ‘ 𝐷 ) )
14 2 1 13 symgov ⊢ ( ( ◡ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ( ◡ 𝑃 ( +g ‘ ( SymGrp ‘ 𝐷 ) ) 𝑄 ) = ( ◡ 𝑃 ∘ 𝑄 ) )
15 2 1 13 symgcl ⊢ ( ( ◡ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ( ◡ 𝑃 ( +g ‘ ( SymGrp ‘ 𝐷 ) ) 𝑄 ) ∈ 𝐺 )
16 14 15 eqeltrrd ⊢ ( ( ◡ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ( ◡ 𝑃 ∘ 𝑄 ) ∈ 𝐺 )
17 11 12 16 syl2anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ( ◡ 𝑃 ∘ 𝑄 ) ∈ 𝐺 )
18 coass ⊢ ( ( 𝑃 ∘ ◡ 𝑃 ) ∘ 𝑄 ) = ( 𝑃 ∘ ( ◡ 𝑃 ∘ 𝑄 ) )
19 2 1 symgbasf1o ⊢ ( 𝑃 ∈ 𝐺 → 𝑃 : 𝐷 –1-1-onto→ 𝐷 )
20 f1ococnv2 ⊢ ( 𝑃 : 𝐷 –1-1-onto→ 𝐷 → ( 𝑃 ∘ ◡ 𝑃 ) = ( I ↾ 𝐷 ) )
21 8 19 20 3syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ( 𝑃 ∘ ◡ 𝑃 ) = ( I ↾ 𝐷 ) )
22 21 coeq1d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ( ( 𝑃 ∘ ◡ 𝑃 ) ∘ 𝑄 ) = ( ( I ↾ 𝐷 ) ∘ 𝑄 ) )
23 18 22 eqtr3id ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ( 𝑃 ∘ ( ◡ 𝑃 ∘ 𝑄 ) ) = ( ( I ↾ 𝐷 ) ∘ 𝑄 ) )
24 2 1 symgbasf1o ⊢ ( 𝑄 ∈ 𝐺 → 𝑄 : 𝐷 –1-1-onto→ 𝐷 )
25 f1of ⊢ ( 𝑄 : 𝐷 –1-1-onto→ 𝐷 → 𝑄 : 𝐷 ⟶ 𝐷 )
26 12 24 25 3syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → 𝑄 : 𝐷 ⟶ 𝐷 )
27 fcoi2 ⊢ ( 𝑄 : 𝐷 ⟶ 𝐷 → ( ( I ↾ 𝐷 ) ∘ 𝑄 ) = 𝑄 )
28 26 27 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ( ( I ↾ 𝐷 ) ∘ 𝑄 ) = 𝑄 )
29 23 28 eqtr2d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → 𝑄 = ( 𝑃 ∘ ( ◡ 𝑃 ∘ 𝑄 ) ) )
30 simpr ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑄 = ( 𝑃 ∘ 𝑝 ) ) → 𝑄 = ( 𝑃 ∘ 𝑝 ) )
31 30 coeq2d ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑄 = ( 𝑃 ∘ 𝑝 ) ) → ( ◡ 𝑃 ∘ 𝑄 ) = ( ◡ 𝑃 ∘ ( 𝑃 ∘ 𝑝 ) ) )
32 coass ⊢ ( ( ◡ 𝑃 ∘ 𝑃 ) ∘ 𝑝 ) = ( ◡ 𝑃 ∘ ( 𝑃 ∘ 𝑝 ) )
33 f1ococnv1 ⊢ ( 𝑃 : 𝐷 –1-1-onto→ 𝐷 → ( ◡ 𝑃 ∘ 𝑃 ) = ( I ↾ 𝐷 ) )
34 8 19 33 3syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ( ◡ 𝑃 ∘ 𝑃 ) = ( I ↾ 𝐷 ) )
35 34 coeq1d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ( ( ◡ 𝑃 ∘ 𝑃 ) ∘ 𝑝 ) = ( ( I ↾ 𝐷 ) ∘ 𝑝 ) )
36 35 ad2antrr ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑄 = ( 𝑃 ∘ 𝑝 ) ) → ( ( ◡ 𝑃 ∘ 𝑃 ) ∘ 𝑝 ) = ( ( I ↾ 𝐷 ) ∘ 𝑝 ) )
37 32 36 eqtr3id ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑄 = ( 𝑃 ∘ 𝑝 ) ) → ( ◡ 𝑃 ∘ ( 𝑃 ∘ 𝑝 ) ) = ( ( I ↾ 𝐷 ) ∘ 𝑝 ) )
38 simplr ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑄 = ( 𝑃 ∘ 𝑝 ) ) → 𝑝 ∈ 𝐺 )
39 2 1 symgbasf1o ⊢ ( 𝑝 ∈ 𝐺 → 𝑝 : 𝐷 –1-1-onto→ 𝐷 )
40 f1of ⊢ ( 𝑝 : 𝐷 –1-1-onto→ 𝐷 → 𝑝 : 𝐷 ⟶ 𝐷 )
41 38 39 40 3syl ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑄 = ( 𝑃 ∘ 𝑝 ) ) → 𝑝 : 𝐷 ⟶ 𝐷 )
42 fcoi2 ⊢ ( 𝑝 : 𝐷 ⟶ 𝐷 → ( ( I ↾ 𝐷 ) ∘ 𝑝 ) = 𝑝 )
43 41 42 syl ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑄 = ( 𝑃 ∘ 𝑝 ) ) → ( ( I ↾ 𝐷 ) ∘ 𝑝 ) = 𝑝 )
44 31 37 43 3eqtrrd ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) ∧ 𝑝 ∈ 𝐺 ) ∧ 𝑄 = ( 𝑃 ∘ 𝑝 ) ) → 𝑝 = ( ◡ 𝑃 ∘ 𝑄 ) )
45 44 ex ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) ∧ 𝑝 ∈ 𝐺 ) → ( 𝑄 = ( 𝑃 ∘ 𝑝 ) → 𝑝 = ( ◡ 𝑃 ∘ 𝑄 ) ) )
46 45 ralrimiva ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ∀ 𝑝 ∈ 𝐺 ( 𝑄 = ( 𝑃 ∘ 𝑝 ) → 𝑝 = ( ◡ 𝑃 ∘ 𝑄 ) ) )
47 coeq2 ⊢ ( 𝑝 = ( ◡ 𝑃 ∘ 𝑄 ) → ( 𝑃 ∘ 𝑝 ) = ( 𝑃 ∘ ( ◡ 𝑃 ∘ 𝑄 ) ) )
48 47 eqeq2d ⊢ ( 𝑝 = ( ◡ 𝑃 ∘ 𝑄 ) → ( 𝑄 = ( 𝑃 ∘ 𝑝 ) ↔ 𝑄 = ( 𝑃 ∘ ( ◡ 𝑃 ∘ 𝑄 ) ) ) )
49 48 eqreu ⊢ ( ( ( ◡ 𝑃 ∘ 𝑄 ) ∈ 𝐺 ∧ 𝑄 = ( 𝑃 ∘ ( ◡ 𝑃 ∘ 𝑄 ) ) ∧ ∀ 𝑝 ∈ 𝐺 ( 𝑄 = ( 𝑃 ∘ 𝑝 ) → 𝑝 = ( ◡ 𝑃 ∘ 𝑄 ) ) ) → ∃! 𝑝 ∈ 𝐺 𝑄 = ( 𝑃 ∘ 𝑝 ) )
50 17 29 46 49 syl3anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺 ) → ∃! 𝑝 ∈ 𝐺 𝑄 = ( 𝑃 ∘ 𝑝 ) )