Metamath Proof Explorer

Theorem 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 syl5req 
 |-  ( 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 ) ) ) )