f1omvdconj

Description: Conjugation of a permutation takes the image of the moved subclass. (Contributed by Stefan O'Rear, 22-Aug-2015)

		Ref	Expression
	Assertion	f1omvdconj	$⊢ (F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \to dom (((G \circ F) \circ G^{-1}) ∖ I) = G [dom (F ∖ I)]$

Proof

Step	Hyp	Ref	Expression
1		difss	$⊢ ((G \circ F) \circ G^{-1}) ∖ I \subseteq (G \circ F) \circ G^{-1}$
2		dmss	$⊢ ((G \circ F) \circ G^{-1}) ∖ I \subseteq (G \circ F) \circ G^{-1} \to dom (((G \circ F) \circ G^{-1}) ∖ I) \subseteq dom ((G \circ F) \circ G^{-1})$
3	1 2	ax-mp	$⊢ dom (((G \circ F) \circ G^{-1}) ∖ I) \subseteq dom ((G \circ F) \circ G^{-1})$
4		dmcoss	$⊢ dom ((G \circ F) \circ G^{-1}) \subseteq dom G^{-1}$
5	3 4	sstri	$⊢ dom (((G \circ F) \circ G^{-1}) ∖ I) \subseteq dom G^{-1}$
6		f1ocnv	$⊢ G : A \underset{1-1 onto}{⟶} A \to G^{-1} : A \underset{1-1 onto}{⟶} A$
7	6	adantl	$⊢ (F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \to G^{-1} : A \underset{1-1 onto}{⟶} A$
8		f1odm	$⊢ G^{-1} : A \underset{1-1 onto}{⟶} A \to dom G^{-1} = A$
9	7 8	syl	$⊢ (F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \to dom G^{-1} = A$
10	5 9	sseqtrid	$⊢ (F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \to dom (((G \circ F) \circ G^{-1}) ∖ I) \subseteq A$
11	10	sselda	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in dom (((G \circ F) \circ G^{-1}) ∖ I)) \to x \in A$
12		imassrn	$⊢ G [dom (F ∖ I)] \subseteq ran G$
13		f1of	$⊢ G : A \underset{1-1 onto}{⟶} A \to G : A ⟶ A$
14	13	adantl	$⊢ (F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \to G : A ⟶ A$
15	14	frnd	$⊢ (F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \to ran G \subseteq A$
16	12 15	sstrid	$⊢ (F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \to G [dom (F ∖ I)] \subseteq A$
17	16	sselda	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in G [dom (F ∖ I)]) \to x \in A$
18		simpl	$⊢ (F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \to F : A ⟶ A$
19		fco	$⊢ (G : A ⟶ A \land F : A ⟶ A) \to (G \circ F) : A ⟶ A$
20	14 18 19	syl2anc	$⊢ (F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \to (G \circ F) : A ⟶ A$
21		f1of	$⊢ G^{-1} : A \underset{1-1 onto}{⟶} A \to G^{-1} : A ⟶ A$
22	7 21	syl	$⊢ (F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \to G^{-1} : A ⟶ A$
23		fco	$⊢ ((G \circ F) : A ⟶ A \land G^{-1} : A ⟶ A) \to ((G \circ F) \circ G^{-1}) : A ⟶ A$
24	20 22 23	syl2anc	$⊢ (F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \to ((G \circ F) \circ G^{-1}) : A ⟶ A$
25	24	ffnd	$⊢ (F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \to ((G \circ F) \circ G^{-1}) Fn A$
26		fnelnfp	$⊢ (((G \circ F) \circ G^{-1}) Fn A \land x \in A) \to (x \in dom (((G \circ F) \circ G^{-1}) ∖ I) \leftrightarrow ((G \circ F) \circ G^{-1}) (x) \neq x)$
27	25 26	sylan	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to (x \in dom (((G \circ F) \circ G^{-1}) ∖ I) \leftrightarrow ((G \circ F) \circ G^{-1}) (x) \neq x)$
28		f1ofn	$⊢ G^{-1} : A \underset{1-1 onto}{⟶} A \to G^{-1} Fn A$
29	7 28	syl	$⊢ (F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \to G^{-1} Fn A$
30		fvco2	$⊢ (G^{-1} Fn A \land x \in A) \to ((G \circ F) \circ G^{-1}) (x) = (G \circ F) (G^{-1} (x))$
31	29 30	sylan	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to ((G \circ F) \circ G^{-1}) (x) = (G \circ F) (G^{-1} (x))$
32		ffn	$⊢ F : A ⟶ A \to F Fn A$
33	32	ad2antrr	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to F Fn A$
34		ffvelrn	$⊢ (G^{-1} : A ⟶ A \land x \in A) \to G^{-1} (x) \in A$
35	22 34	sylan	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to G^{-1} (x) \in A$
36		fvco2	$⊢ (F Fn A \land G^{-1} (x) \in A) \to (G \circ F) (G^{-1} (x)) = G (F (G^{-1} (x)))$
37	33 35 36	syl2anc	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to (G \circ F) (G^{-1} (x)) = G (F (G^{-1} (x)))$
38	31 37	eqtrd	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to ((G \circ F) \circ G^{-1}) (x) = G (F (G^{-1} (x)))$
39	38	eqeq1d	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to (((G \circ F) \circ G^{-1}) (x) = x \leftrightarrow G (F (G^{-1} (x))) = x)$
40		simplr	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to G : A \underset{1-1 onto}{⟶} A$
41		simpll	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to F : A ⟶ A$
42		ffvelrn	$⊢ (F : A ⟶ A \land G^{-1} (x) \in A) \to F (G^{-1} (x)) \in A$
43	41 35 42	syl2anc	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to F (G^{-1} (x)) \in A$
44		simpr	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to x \in A$
45		f1ocnvfvb	$⊢ (G : A \underset{1-1 onto}{⟶} A \land F (G^{-1} (x)) \in A \land x \in A) \to (G (F (G^{-1} (x))) = x \leftrightarrow G^{-1} (x) = F (G^{-1} (x)))$
46	40 43 44 45	syl3anc	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to (G (F (G^{-1} (x))) = x \leftrightarrow G^{-1} (x) = F (G^{-1} (x)))$
47	39 46	bitrd	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to (((G \circ F) \circ G^{-1}) (x) = x \leftrightarrow G^{-1} (x) = F (G^{-1} (x)))$
48	47	necon3bid	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to (((G \circ F) \circ G^{-1}) (x) \neq x \leftrightarrow G^{-1} (x) \neq F (G^{-1} (x)))$
49		necom	$⊢ G^{-1} (x) \neq F (G^{-1} (x)) \leftrightarrow F (G^{-1} (x)) \neq G^{-1} (x)$
50		f1of1	$⊢ G : A \underset{1-1 onto}{⟶} A \to G : A \underset{1-1}{⟶} A$
51	50	ad2antlr	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to G : A \underset{1-1}{⟶} A$
52		difss	$⊢ F ∖ I \subseteq F$
53		dmss	$⊢ F ∖ I \subseteq F \to dom (F ∖ I) \subseteq dom F$
54	52 53	ax-mp	$⊢ dom (F ∖ I) \subseteq dom F$
55		fdm	$⊢ F : A ⟶ A \to dom F = A$
56	54 55	sseqtrid	$⊢ F : A ⟶ A \to dom (F ∖ I) \subseteq A$
57	56	ad2antrr	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to dom (F ∖ I) \subseteq A$
58		f1elima	$⊢ (G : A \underset{1-1}{⟶} A \land G^{-1} (x) \in A \land dom (F ∖ I) \subseteq A) \to (G (G^{-1} (x)) \in G [dom (F ∖ I)] \leftrightarrow G^{-1} (x) \in dom (F ∖ I))$
59	51 35 57 58	syl3anc	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to (G (G^{-1} (x)) \in G [dom (F ∖ I)] \leftrightarrow G^{-1} (x) \in dom (F ∖ I))$
60		f1ocnvfv2	$⊢ (G : A \underset{1-1 onto}{⟶} A \land x \in A) \to G (G^{-1} (x)) = x$
61	60	adantll	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to G (G^{-1} (x)) = x$
62	61	eleq1d	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to (G (G^{-1} (x)) \in G [dom (F ∖ I)] \leftrightarrow x \in G [dom (F ∖ I)])$
63		fnelnfp	$⊢ (F Fn A \land G^{-1} (x) \in A) \to (G^{-1} (x) \in dom (F ∖ I) \leftrightarrow F (G^{-1} (x)) \neq G^{-1} (x))$
64	33 35 63	syl2anc	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to (G^{-1} (x) \in dom (F ∖ I) \leftrightarrow F (G^{-1} (x)) \neq G^{-1} (x))$
65	59 62 64	3bitr3rd	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to (F (G^{-1} (x)) \neq G^{-1} (x) \leftrightarrow x \in G [dom (F ∖ I)])$
66	49 65	syl5bb	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to (G^{-1} (x) \neq F (G^{-1} (x)) \leftrightarrow x \in G [dom (F ∖ I)])$
67	27 48 66	3bitrd	$⊢ ((F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \land x \in A) \to (x \in dom (((G \circ F) \circ G^{-1}) ∖ I) \leftrightarrow x \in G [dom (F ∖ I)])$
68	11 17 67	eqrdav	$⊢ (F : A ⟶ A \land G : A \underset{1-1 onto}{⟶} A) \to dom (((G \circ F) \circ G^{-1}) ∖ I) = G [dom (F ∖ I)]$

Metamath Proof Explorer

Theorem f1omvdconj

Proof