pmtrfconj

Description: Any conjugate of a transposition is a transposition. (Contributed by Stefan O'Rear, 22-Aug-2015)

	Ref	Expression
Hypotheses	pmtrrn.t	$⊢ T = pmTrsp (D)$
	pmtrrn.r	$⊢ R = ran T$
Assertion	pmtrfconj	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to (G \circ F) \circ G^{-1} \in R$

Proof

Step	Hyp	Ref	Expression
1		pmtrrn.t	$⊢ T = pmTrsp (D)$
2		pmtrrn.r	$⊢ R = ran T$
3	1 2	pmtrfb	$⊢ F \in R \leftrightarrow (D \in V \land F : D \underset{1-1 onto}{⟶} D \land dom (F ∖ I) \approx 2_{𝑜})$
4	3	simp1bi	$⊢ F \in R \to D \in V$
5	4	adantr	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to D \in V$
6		simpr	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to G : D \underset{1-1 onto}{⟶} D$
7	1 2	pmtrff1o	$⊢ F \in R \to F : D \underset{1-1 onto}{⟶} D$
8	7	adantr	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to F : D \underset{1-1 onto}{⟶} D$
9		f1oco	$⊢ (G : D \underset{1-1 onto}{⟶} D \land F : D \underset{1-1 onto}{⟶} D) \to (G \circ F) : D \underset{1-1 onto}{⟶} D$
10	6 8 9	syl2anc	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to (G \circ F) : D \underset{1-1 onto}{⟶} D$
11		f1ocnv	$⊢ G : D \underset{1-1 onto}{⟶} D \to G^{-1} : D \underset{1-1 onto}{⟶} D$
12	11	adantl	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to G^{-1} : D \underset{1-1 onto}{⟶} D$
13		f1oco	$⊢ ((G \circ F) : D \underset{1-1 onto}{⟶} D \land G^{-1} : D \underset{1-1 onto}{⟶} D) \to ((G \circ F) \circ G^{-1}) : D \underset{1-1 onto}{⟶} D$
14	10 12 13	syl2anc	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to ((G \circ F) \circ G^{-1}) : D \underset{1-1 onto}{⟶} D$
15		f1of	$⊢ F : D \underset{1-1 onto}{⟶} D \to F : D ⟶ D$
16	7 15	syl	$⊢ F \in R \to F : D ⟶ D$
17	16	adantr	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to F : D ⟶ D$
18		f1omvdconj	$⊢ (F : D ⟶ D \land G : D \underset{1-1 onto}{⟶} D) \to dom (((G \circ F) \circ G^{-1}) ∖ I) = G [dom (F ∖ I)]$
19	17 6 18	syl2anc	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to dom (((G \circ F) \circ G^{-1}) ∖ I) = G [dom (F ∖ I)]$
20		f1of1	$⊢ G : D \underset{1-1 onto}{⟶} D \to G : D \underset{1-1}{⟶} D$
21	20	adantl	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to G : D \underset{1-1}{⟶} D$
22		difss	$⊢ F ∖ I \subseteq F$
23		dmss	$⊢ F ∖ I \subseteq F \to dom (F ∖ I) \subseteq dom F$
24	22 23	ax-mp	$⊢ dom (F ∖ I) \subseteq dom F$
25	24 17	fssdm	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to dom (F ∖ I) \subseteq D$
26	5 25	ssexd	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to dom (F ∖ I) \in V$
27		f1imaeng	$⊢ (G : D \underset{1-1}{⟶} D \land dom (F ∖ I) \subseteq D \land dom (F ∖ I) \in V) \to G [dom (F ∖ I)] \approx dom (F ∖ I)$
28	21 25 26 27	syl3anc	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to G [dom (F ∖ I)] \approx dom (F ∖ I)$
29	19 28	eqbrtrd	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to dom (((G \circ F) \circ G^{-1}) ∖ I) \approx dom (F ∖ I)$
30	3	simp3bi	$⊢ F \in R \to dom (F ∖ I) \approx 2_{𝑜}$
31	30	adantr	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to dom (F ∖ I) \approx 2_{𝑜}$
32		entr	$⊢ (dom (((G \circ F) \circ G^{-1}) ∖ I) \approx dom (F ∖ I) \land dom (F ∖ I) \approx 2_{𝑜}) \to dom (((G \circ F) \circ G^{-1}) ∖ I) \approx 2_{𝑜}$
33	29 31 32	syl2anc	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to dom (((G \circ F) \circ G^{-1}) ∖ I) \approx 2_{𝑜}$
34	1 2	pmtrfb	$⊢ (G \circ F) \circ G^{-1} \in R \leftrightarrow (D \in V \land ((G \circ F) \circ G^{-1}) : D \underset{1-1 onto}{⟶} D \land dom (((G \circ F) \circ G^{-1}) ∖ I) \approx 2_{𝑜})$
35	5 14 33 34	syl3anbrc	$⊢ (F \in R \land G : D \underset{1-1 onto}{⟶} D) \to (G \circ F) \circ G^{-1} \in R$

Metamath Proof Explorer

Theorem pmtrfconj

Proof