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	\|- ( ph -> D e. V )
	psgnunilem1.p	\|- ( ph -> P e. T )
	psgnunilem1.q	\|- ( ph -> Q e. T )
	psgnunilem1.a	\|- ( ph -> A e. dom ( P \ _I ) )
Assertion	psgnunilem1	\|- ( ph -> ( ( P o. Q ) = ( _I \|` D ) \/ E. r e. T E. s e. T ( ( P o. Q ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem psgnunilem1

Proof