psgnunilem1

Description: Lemma for psgnuni . Given two consequtive transpositions in a representation of a permutation, either they are equal and therefore equivalent to the identity, or they are not and it is possible to commute them such that a chosen point in the left transposition is preserved in the right. By repeating this process, a point can be removed from a representation of the identity. (Contributed by Stefan O'Rear, 22-Aug-2015)

	Ref	Expression
Hypotheses	psgnunilem1.t	$⊢ T = ran pmTrsp (D)$
	psgnunilem1.d	$⊢ φ \to D \in V$
	psgnunilem1.p	$⊢ φ \to P \in T$
	psgnunilem1.q	$⊢ φ \to Q \in T$
	psgnunilem1.a	$⊢ φ \to A \in dom (P ∖ I)$
Assertion	psgnunilem1	$⊢ φ \to (P \circ Q = {I ↾}_{D} \lor \exists r \in T \exists s \in T (P \circ Q = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))$

Proof

Step	Hyp	Ref	Expression
1		psgnunilem1.t	$⊢ T = ran pmTrsp (D)$
2		psgnunilem1.d	$⊢ φ \to D \in V$
3		psgnunilem1.p	$⊢ φ \to P \in T$
4		psgnunilem1.q	$⊢ φ \to Q \in T$
5		psgnunilem1.a	$⊢ φ \to A \in dom (P ∖ I)$
6		eqid	$⊢ pmTrsp (D) = pmTrsp (D)$
7	6 1	pmtrfinv	$⊢ Q \in T \to Q \circ Q = {I ↾}_{D}$
8	4 7	syl	$⊢ φ \to Q \circ Q = {I ↾}_{D}$
9		coeq1	$⊢ P = Q \to P \circ Q = Q \circ Q$
10	9	eqeq1d	$⊢ P = Q \to (P \circ Q = {I ↾}_{D} \leftrightarrow Q \circ Q = {I ↾}_{D})$
11	8 10	syl5ibrcom	$⊢ φ \to (P = Q \to P \circ Q = {I ↾}_{D})$
12	11	adantr	$⊢ (φ \land A \in dom (Q ∖ I)) \to (P = Q \to P \circ Q = {I ↾}_{D})$
13	12	imp	$⊢ ((φ \land A \in dom (Q ∖ I)) \land P = Q) \to P \circ Q = {I ↾}_{D}$
14	13	orcd	$⊢ ((φ \land A \in dom (Q ∖ I)) \land P = Q) \to (P \circ Q = {I ↾}_{D} \lor \exists r \in T \exists s \in T (P \circ Q = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))$
15	6 1	pmtrfcnv	$⊢ P \in T \to P^{-1} = P$
16	3 15	syl	$⊢ φ \to P^{-1} = P$
17	16	eqcomd	$⊢ φ \to P = P^{-1}$
18	17	coeq2d	$⊢ φ \to (P \circ Q) \circ P = (P \circ Q) \circ P^{-1}$
19	6 1	pmtrff1o	$⊢ P \in T \to P : D \underset{1-1 onto}{⟶} D$
20	3 19	syl	$⊢ φ \to P : D \underset{1-1 onto}{⟶} D$
21	6 1	pmtrfconj	$⊢ (Q \in T \land P : D \underset{1-1 onto}{⟶} D) \to (P \circ Q) \circ P^{-1} \in T$
22	4 20 21	syl2anc	$⊢ φ \to (P \circ Q) \circ P^{-1} \in T$
23	18 22	eqeltrd	$⊢ φ \to (P \circ Q) \circ P \in T$
24	23	ad2antrr	$⊢ ((φ \land A \in dom (Q ∖ I)) \land P \neq Q) \to (P \circ Q) \circ P \in T$
25	3	ad2antrr	$⊢ ((φ \land A \in dom (Q ∖ I)) \land P \neq Q) \to P \in T$
26		coass	$⊢ ((P \circ Q) \circ P) \circ P = (P \circ Q) \circ (P \circ P)$
27	6 1	pmtrfinv	$⊢ P \in T \to P \circ P = {I ↾}_{D}$
28	3 27	syl	$⊢ φ \to P \circ P = {I ↾}_{D}$
29	28	coeq2d	$⊢ φ \to (P \circ Q) \circ (P \circ P) = (P \circ Q) \circ ({I ↾}_{D})$
30		f1of	$⊢ P : D \underset{1-1 onto}{⟶} D \to P : D ⟶ D$
31	20 30	syl	$⊢ φ \to P : D ⟶ D$
32	6 1	pmtrff1o	$⊢ Q \in T \to Q : D \underset{1-1 onto}{⟶} D$
33	4 32	syl	$⊢ φ \to Q : D \underset{1-1 onto}{⟶} D$
34		f1of	$⊢ Q : D \underset{1-1 onto}{⟶} D \to Q : D ⟶ D$
35	33 34	syl	$⊢ φ \to Q : D ⟶ D$
36		fco	$⊢ (P : D ⟶ D \land Q : D ⟶ D) \to (P \circ Q) : D ⟶ D$
37	31 35 36	syl2anc	$⊢ φ \to (P \circ Q) : D ⟶ D$
38		fcoi1	$⊢ (P \circ Q) : D ⟶ D \to (P \circ Q) \circ ({I ↾}_{D}) = P \circ Q$
39	37 38	syl	$⊢ φ \to (P \circ Q) \circ ({I ↾}_{D}) = P \circ Q$
40	29 39	eqtrd	$⊢ φ \to (P \circ Q) \circ (P \circ P) = P \circ Q$
41	26 40	syl5req	$⊢ φ \to P \circ Q = ((P \circ Q) \circ P) \circ P$
42	41	ad2antrr	$⊢ ((φ \land A \in dom (Q ∖ I)) \land P \neq Q) \to P \circ Q = ((P \circ Q) \circ P) \circ P$
43	5	ad2antrr	$⊢ ((φ \land A \in dom (Q ∖ I)) \land P \neq Q) \to A \in dom (P ∖ I)$
44	20	adantr	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to P : D \underset{1-1 onto}{⟶} D$
45	33	adantr	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to Q : D \underset{1-1 onto}{⟶} D$
46	6 1	pmtrfb	$⊢ P \in T \leftrightarrow (D \in V \land P : D \underset{1-1 onto}{⟶} D \land dom (P ∖ I) \approx 2_{𝑜})$
47	46	simp3bi	$⊢ P \in T \to dom (P ∖ I) \approx 2_{𝑜}$
48	3 47	syl	$⊢ φ \to dom (P ∖ I) \approx 2_{𝑜}$
49	48	adantr	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to dom (P ∖ I) \approx 2_{𝑜}$
50		2onn	$⊢ 2_{𝑜} \in ω$
51		nnfi	$⊢ 2_{𝑜} \in ω \to 2_{𝑜} \in Fin$
52	50 51	ax-mp	$⊢ 2_{𝑜} \in Fin$
53	6 1	pmtrfb	$⊢ Q \in T \leftrightarrow (D \in V \land Q : D \underset{1-1 onto}{⟶} D \land dom (Q ∖ I) \approx 2_{𝑜})$
54	53	simp3bi	$⊢ Q \in T \to dom (Q ∖ I) \approx 2_{𝑜}$
55	4 54	syl	$⊢ φ \to dom (Q ∖ I) \approx 2_{𝑜}$
56		enfi	$⊢ dom (Q ∖ I) \approx 2_{𝑜} \to (dom (Q ∖ I) \in Fin \leftrightarrow 2_{𝑜} \in Fin)$
57	55 56	syl	$⊢ φ \to (dom (Q ∖ I) \in Fin \leftrightarrow 2_{𝑜} \in Fin)$
58	52 57	mpbiri	$⊢ φ \to dom (Q ∖ I) \in Fin$
59	58	adantr	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to dom (Q ∖ I) \in Fin$
60	5	adantr	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to A \in dom (P ∖ I)$
61		en2eleq	$⊢ (A \in dom (P ∖ I) \land dom (P ∖ I) \approx 2_{𝑜}) \to dom (P ∖ I) = \{A, ⋃ (dom (P ∖ I) ∖ \{A\})\}$
62	60 49 61	syl2anc	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to dom (P ∖ I) = \{A, ⋃ (dom (P ∖ I) ∖ \{A\})\}$
63		simprl	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to A \in dom (Q ∖ I)$
64		f1ofn	$⊢ P : D \underset{1-1 onto}{⟶} D \to P Fn D$
65	20 64	syl	$⊢ φ \to P Fn D$
66	65	adantr	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to P Fn D$
67		fimass	$⊢ P : D ⟶ D \to P [dom (Q ∖ I)] \subseteq D$
68	31 67	syl	$⊢ φ \to P [dom (Q ∖ I)] \subseteq D$
69	68	adantr	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to P [dom (Q ∖ I)] \subseteq D$
70		simprr	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to A \in P [dom (Q ∖ I)]$
71		fnfvima	$⊢ (P Fn D \land P [dom (Q ∖ I)] \subseteq D \land A \in P [dom (Q ∖ I)]) \to P (A) \in P [P [dom (Q ∖ I)]]$
72	66 69 70 71	syl3anc	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to P (A) \in P [P [dom (Q ∖ I)]]$
73		difss	$⊢ P ∖ I \subseteq P$
74		dmss	$⊢ P ∖ I \subseteq P \to dom (P ∖ I) \subseteq dom P$
75	73 74	ax-mp	$⊢ dom (P ∖ I) \subseteq dom P$
76		f1odm	$⊢ P : D \underset{1-1 onto}{⟶} D \to dom P = D$
77	20 76	syl	$⊢ φ \to dom P = D$
78	75 77	sseqtrid	$⊢ φ \to dom (P ∖ I) \subseteq D$
79	78 5	sseldd	$⊢ φ \to A \in D$
80		eqid	$⊢ dom (P ∖ I) = dom (P ∖ I)$
81	6 1 80	pmtrffv	$⊢ (P \in T \land A \in D) \to P (A) = if (A \in dom (P ∖ I), ⋃ (dom (P ∖ I) ∖ \{A\}), A)$
82	3 79 81	syl2anc	$⊢ φ \to P (A) = if (A \in dom (P ∖ I), ⋃ (dom (P ∖ I) ∖ \{A\}), A)$
83	5	iftrued	$⊢ φ \to if (A \in dom (P ∖ I), ⋃ (dom (P ∖ I) ∖ \{A\}), A) = ⋃ (dom (P ∖ I) ∖ \{A\})$
84	82 83	eqtrd	$⊢ φ \to P (A) = ⋃ (dom (P ∖ I) ∖ \{A\})$
85	84	adantr	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to P (A) = ⋃ (dom (P ∖ I) ∖ \{A\})$
86		imaco	$⊢ (P \circ P) [dom (Q ∖ I)] = P [P [dom (Q ∖ I)]]$
87	28	imaeq1d	$⊢ φ \to (P \circ P) [dom (Q ∖ I)] = ({I ↾}_{D}) [dom (Q ∖ I)]$
88		difss	$⊢ Q ∖ I \subseteq Q$
89		dmss	$⊢ Q ∖ I \subseteq Q \to dom (Q ∖ I) \subseteq dom Q$
90	88 89	ax-mp	$⊢ dom (Q ∖ I) \subseteq dom Q$
91		f1odm	$⊢ Q : D \underset{1-1 onto}{⟶} D \to dom Q = D$
92	90 91	sseqtrid	$⊢ Q : D \underset{1-1 onto}{⟶} D \to dom (Q ∖ I) \subseteq D$
93	33 92	syl	$⊢ φ \to dom (Q ∖ I) \subseteq D$
94		resiima	$⊢ dom (Q ∖ I) \subseteq D \to ({I ↾}_{D}) [dom (Q ∖ I)] = dom (Q ∖ I)$
95	93 94	syl	$⊢ φ \to ({I ↾}_{D}) [dom (Q ∖ I)] = dom (Q ∖ I)$
96	87 95	eqtrd	$⊢ φ \to (P \circ P) [dom (Q ∖ I)] = dom (Q ∖ I)$
97	86 96	eqtr3id	$⊢ φ \to P [P [dom (Q ∖ I)]] = dom (Q ∖ I)$
98	97	adantr	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to P [P [dom (Q ∖ I)]] = dom (Q ∖ I)$
99	72 85 98	3eltr3d	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to ⋃ (dom (P ∖ I) ∖ \{A\}) \in dom (Q ∖ I)$
100	63 99	prssd	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to \{A, ⋃ (dom (P ∖ I) ∖ \{A\})\} \subseteq dom (Q ∖ I)$
101	62 100	eqsstrd	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to dom (P ∖ I) \subseteq dom (Q ∖ I)$
102	55	ensymd	$⊢ φ \to 2_{𝑜} \approx dom (Q ∖ I)$
103		entr	$⊢ (dom (P ∖ I) \approx 2_{𝑜} \land 2_{𝑜} \approx dom (Q ∖ I)) \to dom (P ∖ I) \approx dom (Q ∖ I)$
104	48 102 103	syl2anc	$⊢ φ \to dom (P ∖ I) \approx dom (Q ∖ I)$
105	104	adantr	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to dom (P ∖ I) \approx dom (Q ∖ I)$
106		fisseneq	$⊢ (dom (Q ∖ I) \in Fin \land dom (P ∖ I) \subseteq dom (Q ∖ I) \land dom (P ∖ I) \approx dom (Q ∖ I)) \to dom (P ∖ I) = dom (Q ∖ I)$
107	59 101 105 106	syl3anc	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to dom (P ∖ I) = dom (Q ∖ I)$
108	107	eqcomd	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to dom (Q ∖ I) = dom (P ∖ I)$
109		f1otrspeq	$⊢ ((P : D \underset{1-1 onto}{⟶} D \land Q : D \underset{1-1 onto}{⟶} D) \land (dom (P ∖ I) \approx 2_{𝑜} \land dom (Q ∖ I) = dom (P ∖ I))) \to P = Q$
110	44 45 49 108 109	syl22anc	$⊢ (φ \land (A \in dom (Q ∖ I) \land A \in P [dom (Q ∖ I)])) \to P = Q$
111	110	expr	$⊢ (φ \land A \in dom (Q ∖ I)) \to (A \in P [dom (Q ∖ I)] \to P = Q)$
112	111	necon3ad	$⊢ (φ \land A \in dom (Q ∖ I)) \to (P \neq Q \to \neg A \in P [dom (Q ∖ I)])$
113	112	imp	$⊢ ((φ \land A \in dom (Q ∖ I)) \land P \neq Q) \to \neg A \in P [dom (Q ∖ I)]$
114	18	difeq1d	$⊢ φ \to ((P \circ Q) \circ P) ∖ I = ((P \circ Q) \circ P^{-1}) ∖ I$
115	114	dmeqd	$⊢ φ \to dom (((P \circ Q) \circ P) ∖ I) = dom (((P \circ Q) \circ P^{-1}) ∖ I)$
116		f1omvdconj	$⊢ (Q : D ⟶ D \land P : D \underset{1-1 onto}{⟶} D) \to dom (((P \circ Q) \circ P^{-1}) ∖ I) = P [dom (Q ∖ I)]$
117	35 20 116	syl2anc	$⊢ φ \to dom (((P \circ Q) \circ P^{-1}) ∖ I) = P [dom (Q ∖ I)]$
118	115 117	eqtrd	$⊢ φ \to dom (((P \circ Q) \circ P) ∖ I) = P [dom (Q ∖ I)]$
119	118	eleq2d	$⊢ φ \to (A \in dom (((P \circ Q) \circ P) ∖ I) \leftrightarrow A \in P [dom (Q ∖ I)])$
120	119	ad2antrr	$⊢ ((φ \land A \in dom (Q ∖ I)) \land P \neq Q) \to (A \in dom (((P \circ Q) \circ P) ∖ I) \leftrightarrow A \in P [dom (Q ∖ I)])$
121	113 120	mtbird	$⊢ ((φ \land A \in dom (Q ∖ I)) \land P \neq Q) \to \neg A \in dom (((P \circ Q) \circ P) ∖ I)$
122		coeq1	$⊢ r = (P \circ Q) \circ P \to r \circ s = ((P \circ Q) \circ P) \circ s$
123	122	eqeq2d	$⊢ r = (P \circ Q) \circ P \to (P \circ Q = r \circ s \leftrightarrow P \circ Q = ((P \circ Q) \circ P) \circ s)$
124		difeq1	$⊢ r = (P \circ Q) \circ P \to r ∖ I = ((P \circ Q) \circ P) ∖ I$
125	124	dmeqd	$⊢ r = (P \circ Q) \circ P \to dom (r ∖ I) = dom (((P \circ Q) \circ P) ∖ I)$
126	125	eleq2d	$⊢ r = (P \circ Q) \circ P \to (A \in dom (r ∖ I) \leftrightarrow A \in dom (((P \circ Q) \circ P) ∖ I))$
127	126	notbid	$⊢ r = (P \circ Q) \circ P \to (\neg A \in dom (r ∖ I) \leftrightarrow \neg A \in dom (((P \circ Q) \circ P) ∖ I))$
128	123 127	3anbi13d	$⊢ r = (P \circ Q) \circ P \to ((P \circ Q = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)) \leftrightarrow (P \circ Q = ((P \circ Q) \circ P) \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (((P \circ Q) \circ P) ∖ I)))$
129		coeq2	$⊢ s = P \to ((P \circ Q) \circ P) \circ s = ((P \circ Q) \circ P) \circ P$
130	129	eqeq2d	$⊢ s = P \to (P \circ Q = ((P \circ Q) \circ P) \circ s \leftrightarrow P \circ Q = ((P \circ Q) \circ P) \circ P)$
131		difeq1	$⊢ s = P \to s ∖ I = P ∖ I$
132	131	dmeqd	$⊢ s = P \to dom (s ∖ I) = dom (P ∖ I)$
133	132	eleq2d	$⊢ s = P \to (A \in dom (s ∖ I) \leftrightarrow A \in dom (P ∖ I))$
134	130 133	3anbi12d	$⊢ s = P \to ((P \circ Q = ((P \circ Q) \circ P) \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (((P \circ Q) \circ P) ∖ I)) \leftrightarrow (P \circ Q = ((P \circ Q) \circ P) \circ P \land A \in dom (P ∖ I) \land \neg A \in dom (((P \circ Q) \circ P) ∖ I)))$
135	128 134	rspc2ev	$⊢ ((P \circ Q) \circ P \in T \land P \in T \land (P \circ Q = ((P \circ Q) \circ P) \circ P \land A \in dom (P ∖ I) \land \neg A \in dom (((P \circ Q) \circ P) ∖ I))) \to \exists r \in T \exists s \in T (P \circ Q = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I))$
136	24 25 42 43 121 135	syl113anc	$⊢ ((φ \land A \in dom (Q ∖ I)) \land P \neq Q) \to \exists r \in T \exists s \in T (P \circ Q = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I))$
137	136	olcd	$⊢ ((φ \land A \in dom (Q ∖ I)) \land P \neq Q) \to (P \circ Q = {I ↾}_{D} \lor \exists r \in T \exists s \in T (P \circ Q = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))$
138	14 137	pm2.61dane	$⊢ (φ \land A \in dom (Q ∖ I)) \to (P \circ Q = {I ↾}_{D} \lor \exists r \in T \exists s \in T (P \circ Q = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))$
139	4	adantr	$⊢ (φ \land \neg A \in dom (Q ∖ I)) \to Q \in T$
140		coass	$⊢ (Q \circ P) \circ Q = Q \circ (P \circ Q)$
141	6 1	pmtrfcnv	$⊢ Q \in T \to Q^{-1} = Q$
142	4 141	syl	$⊢ φ \to Q^{-1} = Q$
143	142	eqcomd	$⊢ φ \to Q = Q^{-1}$
144	143	coeq2d	$⊢ φ \to (Q \circ P) \circ Q = (Q \circ P) \circ Q^{-1}$
145	140 144	eqtr3id	$⊢ φ \to Q \circ (P \circ Q) = (Q \circ P) \circ Q^{-1}$
146	6 1	pmtrfconj	$⊢ (P \in T \land Q : D \underset{1-1 onto}{⟶} D) \to (Q \circ P) \circ Q^{-1} \in T$
147	3 33 146	syl2anc	$⊢ φ \to (Q \circ P) \circ Q^{-1} \in T$
148	145 147	eqeltrd	$⊢ φ \to Q \circ (P \circ Q) \in T$
149	148	adantr	$⊢ (φ \land \neg A \in dom (Q ∖ I)) \to Q \circ (P \circ Q) \in T$
150	8	coeq1d	$⊢ φ \to (Q \circ Q) \circ (P \circ Q) = ({I ↾}_{D}) \circ (P \circ Q)$
151		fcoi2	$⊢ (P \circ Q) : D ⟶ D \to ({I ↾}_{D}) \circ (P \circ Q) = P \circ Q$
152	37 151	syl	$⊢ φ \to ({I ↾}_{D}) \circ (P \circ Q) = P \circ Q$
153	150 152	eqtr2d	$⊢ φ \to P \circ Q = (Q \circ Q) \circ (P \circ Q)$
154		coass	$⊢ (Q \circ Q) \circ (P \circ Q) = Q \circ (Q \circ (P \circ Q))$
155	153 154	eqtrdi	$⊢ φ \to P \circ Q = Q \circ (Q \circ (P \circ Q))$
156	155	adantr	$⊢ (φ \land \neg A \in dom (Q ∖ I)) \to P \circ Q = Q \circ (Q \circ (P \circ Q))$
157		f1ofn	$⊢ Q : D \underset{1-1 onto}{⟶} D \to Q Fn D$
158	33 157	syl	$⊢ φ \to Q Fn D$
159		fnelnfp	$⊢ (Q Fn D \land A \in D) \to (A \in dom (Q ∖ I) \leftrightarrow Q (A) \neq A)$
160	158 79 159	syl2anc	$⊢ φ \to (A \in dom (Q ∖ I) \leftrightarrow Q (A) \neq A)$
161	160	necon2bbid	$⊢ φ \to (Q (A) = A \leftrightarrow \neg A \in dom (Q ∖ I))$
162	161	biimpar	$⊢ (φ \land \neg A \in dom (Q ∖ I)) \to Q (A) = A$
163		fnfvima	$⊢ (Q Fn D \land dom (P ∖ I) \subseteq D \land A \in dom (P ∖ I)) \to Q (A) \in Q [dom (P ∖ I)]$
164	158 78 5 163	syl3anc	$⊢ φ \to Q (A) \in Q [dom (P ∖ I)]$
165	164	adantr	$⊢ (φ \land \neg A \in dom (Q ∖ I)) \to Q (A) \in Q [dom (P ∖ I)]$
166	162 165	eqeltrrd	$⊢ (φ \land \neg A \in dom (Q ∖ I)) \to A \in Q [dom (P ∖ I)]$
167	145	difeq1d	$⊢ φ \to (Q \circ (P \circ Q)) ∖ I = ((Q \circ P) \circ Q^{-1}) ∖ I$
168	167	dmeqd	$⊢ φ \to dom ((Q \circ (P \circ Q)) ∖ I) = dom (((Q \circ P) \circ Q^{-1}) ∖ I)$
169		f1omvdconj	$⊢ (P : D ⟶ D \land Q : D \underset{1-1 onto}{⟶} D) \to dom (((Q \circ P) \circ Q^{-1}) ∖ I) = Q [dom (P ∖ I)]$
170	31 33 169	syl2anc	$⊢ φ \to dom (((Q \circ P) \circ Q^{-1}) ∖ I) = Q [dom (P ∖ I)]$
171	168 170	eqtrd	$⊢ φ \to dom ((Q \circ (P \circ Q)) ∖ I) = Q [dom (P ∖ I)]$
172	171	adantr	$⊢ (φ \land \neg A \in dom (Q ∖ I)) \to dom ((Q \circ (P \circ Q)) ∖ I) = Q [dom (P ∖ I)]$
173	166 172	eleqtrrd	$⊢ (φ \land \neg A \in dom (Q ∖ I)) \to A \in dom ((Q \circ (P \circ Q)) ∖ I)$
174		simpr	$⊢ (φ \land \neg A \in dom (Q ∖ I)) \to \neg A \in dom (Q ∖ I)$
175		coeq1	$⊢ r = Q \to r \circ s = Q \circ s$
176	175	eqeq2d	$⊢ r = Q \to (P \circ Q = r \circ s \leftrightarrow P \circ Q = Q \circ s)$
177		difeq1	$⊢ r = Q \to r ∖ I = Q ∖ I$
178	177	dmeqd	$⊢ r = Q \to dom (r ∖ I) = dom (Q ∖ I)$
179	178	eleq2d	$⊢ r = Q \to (A \in dom (r ∖ I) \leftrightarrow A \in dom (Q ∖ I))$
180	179	notbid	$⊢ r = Q \to (\neg A \in dom (r ∖ I) \leftrightarrow \neg A \in dom (Q ∖ I))$
181	176 180	3anbi13d	$⊢ r = Q \to ((P \circ Q = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)) \leftrightarrow (P \circ Q = Q \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (Q ∖ I)))$
182		coeq2	$⊢ s = Q \circ (P \circ Q) \to Q \circ s = Q \circ (Q \circ (P \circ Q))$
183	182	eqeq2d	$⊢ s = Q \circ (P \circ Q) \to (P \circ Q = Q \circ s \leftrightarrow P \circ Q = Q \circ (Q \circ (P \circ Q)))$
184		difeq1	$⊢ s = Q \circ (P \circ Q) \to s ∖ I = (Q \circ (P \circ Q)) ∖ I$
185	184	dmeqd	$⊢ s = Q \circ (P \circ Q) \to dom (s ∖ I) = dom ((Q \circ (P \circ Q)) ∖ I)$
186	185	eleq2d	$⊢ s = Q \circ (P \circ Q) \to (A \in dom (s ∖ I) \leftrightarrow A \in dom ((Q \circ (P \circ Q)) ∖ I))$
187	183 186	3anbi12d	$⊢ s = Q \circ (P \circ Q) \to ((P \circ Q = Q \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (Q ∖ I)) \leftrightarrow (P \circ Q = Q \circ (Q \circ (P \circ Q)) \land A \in dom ((Q \circ (P \circ Q)) ∖ I) \land \neg A \in dom (Q ∖ I)))$
188	181 187	rspc2ev	$⊢ (Q \in T \land Q \circ (P \circ Q) \in T \land (P \circ Q = Q \circ (Q \circ (P \circ Q)) \land A \in dom ((Q \circ (P \circ Q)) ∖ I) \land \neg A \in dom (Q ∖ I))) \to \exists r \in T \exists s \in T (P \circ Q = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I))$
189	139 149 156 173 174 188	syl113anc	$⊢ (φ \land \neg A \in dom (Q ∖ I)) \to \exists r \in T \exists s \in T (P \circ Q = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I))$
190	189	olcd	$⊢ (φ \land \neg A \in dom (Q ∖ I)) \to (P \circ Q = {I ↾}_{D} \lor \exists r \in T \exists s \in T (P \circ Q = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))$
191	138 190	pm2.61dan	$⊢ φ \to (P \circ Q = {I ↾}_{D} \lor \exists r \in T \exists s \in T (P \circ Q = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))$

Metamath Proof Explorer

Theorem psgnunilem1

Proof