f1omvdco2

Description: If exactly one of two permutations is limited to a set of points, then the composition will not be. (Contributed by Stefan O'Rear, 23-Aug-2015)

		Ref	Expression
	Assertion	f1omvdco2	$⊢ (F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A \land (dom (F ∖ I) \subseteq X ⊻ dom (G ∖ I) \subseteq X)) \to \neg dom ((F \circ G) ∖ I) \subseteq X$

Proof

Step	Hyp	Ref	Expression
1		excxor	$⊢ (dom (F ∖ I) \subseteq X ⊻ dom (G ∖ I) \subseteq X) \leftrightarrow ((dom (F ∖ I) \subseteq X \land \neg dom (G ∖ I) \subseteq X) \lor (\neg dom (F ∖ I) \subseteq X \land dom (G ∖ I) \subseteq X))$
2		coass	$⊢ (F^{-1} \circ F) \circ G = F^{-1} \circ (F \circ G)$
3		f1ococnv1	$⊢ F : A \underset{1-1 onto}{⟶} A \to F^{-1} \circ F = {I ↾}_{A}$
4	3	coeq1d	$⊢ F : A \underset{1-1 onto}{⟶} A \to (F^{-1} \circ F) \circ G = ({I ↾}_{A}) \circ G$
5		f1of	$⊢ G : A \underset{1-1 onto}{⟶} A \to G : A ⟶ A$
6		fcoi2	$⊢ G : A ⟶ A \to ({I ↾}_{A}) \circ G = G$
7	5 6	syl	$⊢ G : A \underset{1-1 onto}{⟶} A \to ({I ↾}_{A}) \circ G = G$
8	4 7	sylan9eq	$⊢ (F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \to (F^{-1} \circ F) \circ G = G$
9	2 8	eqtr3id	$⊢ (F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \to F^{-1} \circ (F \circ G) = G$
10	9	difeq1d	$⊢ (F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \to (F^{-1} \circ (F \circ G)) ∖ I = G ∖ I$
11	10	dmeqd	$⊢ (F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \to dom ((F^{-1} \circ (F \circ G)) ∖ I) = dom (G ∖ I)$
12	11	adantr	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \subseteq X \land dom ((F \circ G) ∖ I) \subseteq X)) \to dom ((F^{-1} \circ (F \circ G)) ∖ I) = dom (G ∖ I)$
13		mvdco	$⊢ dom ((F^{-1} \circ (F \circ G)) ∖ I) \subseteq dom (F^{-1} ∖ I) \cup dom ((F \circ G) ∖ I)$
14		f1omvdcnv	$⊢ F : A \underset{1-1 onto}{⟶} A \to dom (F^{-1} ∖ I) = dom (F ∖ I)$
15	14	ad2antrr	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \subseteq X \land dom ((F \circ G) ∖ I) \subseteq X)) \to dom (F^{-1} ∖ I) = dom (F ∖ I)$
16		simprl	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \subseteq X \land dom ((F \circ G) ∖ I) \subseteq X)) \to dom (F ∖ I) \subseteq X$
17	15 16	eqsstrd	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \subseteq X \land dom ((F \circ G) ∖ I) \subseteq X)) \to dom (F^{-1} ∖ I) \subseteq X$
18		simprr	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \subseteq X \land dom ((F \circ G) ∖ I) \subseteq X)) \to dom ((F \circ G) ∖ I) \subseteq X$
19	17 18	unssd	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \subseteq X \land dom ((F \circ G) ∖ I) \subseteq X)) \to dom (F^{-1} ∖ I) \cup dom ((F \circ G) ∖ I) \subseteq X$
20	13 19	sstrid	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \subseteq X \land dom ((F \circ G) ∖ I) \subseteq X)) \to dom ((F^{-1} \circ (F \circ G)) ∖ I) \subseteq X$
21	12 20	eqsstrrd	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (F ∖ I) \subseteq X \land dom ((F \circ G) ∖ I) \subseteq X)) \to dom (G ∖ I) \subseteq X$
22	21	expr	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land dom (F ∖ I) \subseteq X) \to (dom ((F \circ G) ∖ I) \subseteq X \to dom (G ∖ I) \subseteq X)$
23	22	con3d	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land dom (F ∖ I) \subseteq X) \to (\neg dom (G ∖ I) \subseteq X \to \neg dom ((F \circ G) ∖ I) \subseteq X)$
24	23	expimpd	$⊢ (F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \to ((dom (F ∖ I) \subseteq X \land \neg dom (G ∖ I) \subseteq X) \to \neg dom ((F \circ G) ∖ I) \subseteq X)$
25		coass	$⊢ (F \circ G) \circ G^{-1} = F \circ (G \circ G^{-1})$
26		f1ococnv2	$⊢ G : A \underset{1-1 onto}{⟶} A \to G \circ G^{-1} = {I ↾}_{A}$
27	26	coeq2d	$⊢ G : A \underset{1-1 onto}{⟶} A \to F \circ (G \circ G^{-1}) = F \circ ({I ↾}_{A})$
28		f1of	$⊢ F : A \underset{1-1 onto}{⟶} A \to F : A ⟶ A$
29		fcoi1	$⊢ F : A ⟶ A \to F \circ ({I ↾}_{A}) = F$
30	28 29	syl	$⊢ F : A \underset{1-1 onto}{⟶} A \to F \circ ({I ↾}_{A}) = F$
31	27 30	sylan9eqr	$⊢ (F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \to F \circ (G \circ G^{-1}) = F$
32	25 31	eqtrid	$⊢ (F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \to (F \circ G) \circ G^{-1} = F$
33	32	difeq1d	$⊢ (F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \to ((F \circ G) \circ G^{-1}) ∖ I = F ∖ I$
34	33	dmeqd	$⊢ (F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \to dom (((F \circ G) \circ G^{-1}) ∖ I) = dom (F ∖ I)$
35	34	adantr	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (G ∖ I) \subseteq X \land dom ((F \circ G) ∖ I) \subseteq X)) \to dom (((F \circ G) \circ G^{-1}) ∖ I) = dom (F ∖ I)$
36		mvdco	$⊢ dom (((F \circ G) \circ G^{-1}) ∖ I) \subseteq dom ((F \circ G) ∖ I) \cup dom (G^{-1} ∖ I)$
37		simprr	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (G ∖ I) \subseteq X \land dom ((F \circ G) ∖ I) \subseteq X)) \to dom ((F \circ G) ∖ I) \subseteq X$
38		f1omvdcnv	$⊢ G : A \underset{1-1 onto}{⟶} A \to dom (G^{-1} ∖ I) = dom (G ∖ I)$
39	38	ad2antlr	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (G ∖ I) \subseteq X \land dom ((F \circ G) ∖ I) \subseteq X)) \to dom (G^{-1} ∖ I) = dom (G ∖ I)$
40		simprl	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (G ∖ I) \subseteq X \land dom ((F \circ G) ∖ I) \subseteq X)) \to dom (G ∖ I) \subseteq X$
41	39 40	eqsstrd	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (G ∖ I) \subseteq X \land dom ((F \circ G) ∖ I) \subseteq X)) \to dom (G^{-1} ∖ I) \subseteq X$
42	37 41	unssd	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (G ∖ I) \subseteq X \land dom ((F \circ G) ∖ I) \subseteq X)) \to dom ((F \circ G) ∖ I) \cup dom (G^{-1} ∖ I) \subseteq X$
43	36 42	sstrid	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (G ∖ I) \subseteq X \land dom ((F \circ G) ∖ I) \subseteq X)) \to dom (((F \circ G) \circ G^{-1}) ∖ I) \subseteq X$
44	35 43	eqsstrrd	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land (dom (G ∖ I) \subseteq X \land dom ((F \circ G) ∖ I) \subseteq X)) \to dom (F ∖ I) \subseteq X$
45	44	expr	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land dom (G ∖ I) \subseteq X) \to (dom ((F \circ G) ∖ I) \subseteq X \to dom (F ∖ I) \subseteq X)$
46	45	con3d	$⊢ ((F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \land dom (G ∖ I) \subseteq X) \to (\neg dom (F ∖ I) \subseteq X \to \neg dom ((F \circ G) ∖ I) \subseteq X)$
47	46	expimpd	$⊢ (F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \to ((dom (G ∖ I) \subseteq X \land \neg dom (F ∖ I) \subseteq X) \to \neg dom ((F \circ G) ∖ I) \subseteq X)$
48	47	ancomsd	$⊢ (F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \to ((\neg dom (F ∖ I) \subseteq X \land dom (G ∖ I) \subseteq X) \to \neg dom ((F \circ G) ∖ I) \subseteq X)$
49	24 48	jaod	$⊢ (F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \to (((dom (F ∖ I) \subseteq X \land \neg dom (G ∖ I) \subseteq X) \lor (\neg dom (F ∖ I) \subseteq X \land dom (G ∖ I) \subseteq X)) \to \neg dom ((F \circ G) ∖ I) \subseteq X)$
50	1 49	biimtrid	$⊢ (F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A) \to ((dom (F ∖ I) \subseteq X ⊻ dom (G ∖ I) \subseteq X) \to \neg dom ((F \circ G) ∖ I) \subseteq X)$
51	50	3impia	$⊢ (F : A \underset{1-1 onto}{⟶} A \land G : A \underset{1-1 onto}{⟶} A \land (dom (F ∖ I) \subseteq X ⊻ dom (G ∖ I) \subseteq X)) \to \neg dom ((F \circ G) ∖ I) \subseteq X$

Metamath Proof Explorer

Theorem f1omvdco2

Proof