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		fcoi2	$⊢ Q : D ⟶ D \to ({I ↾}_{D}) \circ Q = Q$
27	12 24 25 26	4syl	$⊢ (D \in V \land P \in G \land Q \in G) \to ({I ↾}_{D}) \circ Q = Q$
28	23 27	eqtr2d	$⊢ (D \in V \land P \in G \land Q \in G) \to Q = P \circ (P^{-1} \circ Q)$
29		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$
30	29	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)$
31		coass	$⊢ (P^{-1} \circ P) \circ p = P^{-1} \circ (P \circ p)$
32		f1ococnv1	$⊢ P : D \underset{1-1 onto}{⟶} D \to P^{-1} \circ P = {I ↾}_{D}$
33	8 19 32	3syl	$⊢ (D \in V \land P \in G \land Q \in G) \to P^{-1} \circ P = {I ↾}_{D}$
34	33	coeq1d	$⊢ (D \in V \land P \in G \land Q \in G) \to (P^{-1} \circ P) \circ p = ({I ↾}_{D}) \circ p$
35	34	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$
36	31 35	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$
37		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$
38	2 1	symgbasf1o	$⊢ p \in G \to p : D \underset{1-1 onto}{⟶} D$
39		f1of	$⊢ p : D \underset{1-1 onto}{⟶} D \to p : D ⟶ D$
40		fcoi2	$⊢ p : D ⟶ D \to ({I ↾}_{D}) \circ p = p$
41	37 38 39 40	4syl	$⊢ (((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$
42	30 36 41	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$
43	42	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)$
44	43	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)$
45		coeq2	$⊢ p = P^{-1} \circ Q \to P \circ p = P \circ (P^{-1} \circ Q)$
46	45	eqeq2d	$⊢ p = P^{-1} \circ Q \to (Q = P \circ p \leftrightarrow Q = P \circ (P^{-1} \circ Q))$
47	46	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$
48	17 28 44 47	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