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 \in V \land P \in G \land Q \in G) \to \exists! p \in G Q = P \circ p$

Proof

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

Metamath Proof Explorer

Theorem symgfcoeu

Proof