Metamath Proof Explorer

Theorem cyc3co2

Description: Represent a 3-cycle as a composition of two 2-cycles. (Contributed by Thierry Arnoux, 19-Sep-2023)

Ref Expression
Hypotheses cycpm3.c 
|- C = ( toCyc ` D )
cycpm3.s 
|- S = ( SymGrp ` D )
cycpm3.d 
|- ( ph -> D e. V )
cycpm3.i 
|- ( ph -> I e. D )
cycpm3.j 
|- ( ph -> J e. D )
cycpm3.k 
|- ( ph -> K e. D )
cycpm3.1 
|- ( ph -> I =/= J )
cycpm3.2 
|- ( ph -> J =/= K )
cycpm3.3 
|- ( ph -> K =/= I )
cyc3co2.t 
|- .x. = ( +g ` S )
Assertion cyc3co2 
|- ( ph -> ( C ` <" I J K "> ) = ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) )

Proof

Step Hyp Ref Expression
1 cycpm3.c 
 |-  C = ( toCyc ` D )
2 cycpm3.s 
 |-  S = ( SymGrp ` D )
3 cycpm3.d 
 |-  ( ph -> D e. V )
4 cycpm3.i 
 |-  ( ph -> I e. D )
5 cycpm3.j 
 |-  ( ph -> J e. D )
6 cycpm3.k 
 |-  ( ph -> K e. D )
7 cycpm3.1 
 |-  ( ph -> I =/= J )
8 cycpm3.2 
 |-  ( ph -> J =/= K )
9 cycpm3.3 
 |-  ( ph -> K =/= I )
10 cyc3co2.t 
 |-  .x. = ( +g ` S )
11 1 2 3 4 5 6 7 8 9 cycpm3cl 
 |-  ( ph -> ( C ` <" I J K "> ) e. ( Base ` S ) )
12 eqid 
 |-  ( Base ` S ) = ( Base ` S )
13 2 12 symgbasf 
 |-  ( ( C ` <" I J K "> ) e. ( Base ` S ) -> ( C ` <" I J K "> ) : D --> D )
14 11 13 syl 
 |-  ( ph -> ( C ` <" I J K "> ) : D --> D )
15 14 ffnd 
 |-  ( ph -> ( C ` <" I J K "> ) Fn D )
16 2 symggrp 
 |-  ( D e. V -> S e. Grp )
17 3 16 syl 
 |-  ( ph -> S e. Grp )
18 9 necomd 
 |-  ( ph -> I =/= K )
19 1 3 4 6 18 2 cycpm2cl 
 |-  ( ph -> ( C ` <" I K "> ) e. ( Base ` S ) )
20 1 3 4 5 7 2 cycpm2cl 
 |-  ( ph -> ( C ` <" I J "> ) e. ( Base ` S ) )
21 12 10 grpcl 
 |-  ( ( S e. Grp /\ ( C ` <" I K "> ) e. ( Base ` S ) /\ ( C ` <" I J "> ) e. ( Base ` S ) ) -> ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) e. ( Base ` S ) )
22 17 19 20 21 syl3anc 
 |-  ( ph -> ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) e. ( Base ` S ) )
23 2 12 symgbasf 
 |-  ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) e. ( Base ` S ) -> ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) : D --> D )
24 22 23 syl 
 |-  ( ph -> ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) : D --> D )
25 24 ffnd 
 |-  ( ph -> ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) Fn D )
26 1 2 3 4 5 6 7 8 9 cyc3fv1 
 |-  ( ph -> ( ( C ` <" I J K "> ) ` I ) = J )
27 26 adantr 
 |-  ( ( ph /\ x = I ) -> ( ( C ` <" I J K "> ) ` I ) = J )
28 simpr 
 |-  ( ( ph /\ x = I ) -> x = I )
29 28 fveq2d 
 |-  ( ( ph /\ x = I ) -> ( ( C ` <" I J K "> ) ` x ) = ( ( C ` <" I J K "> ) ` I ) )
30 2 12 10 symgov 
 |-  ( ( ( C ` <" I K "> ) e. ( Base ` S ) /\ ( C ` <" I J "> ) e. ( Base ` S ) ) -> ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) = ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) )
31 19 20 30 syl2anc 
 |-  ( ph -> ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) = ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) )
32 31 adantr 
 |-  ( ( ph /\ x = I ) -> ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) = ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) )
33 32 fveq1d 
 |-  ( ( ph /\ x = I ) -> ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) = ( ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) ` x ) )
34 2 12 symgbasf 
 |-  ( ( C ` <" I J "> ) e. ( Base ` S ) -> ( C ` <" I J "> ) : D --> D )
35 20 34 syl 
 |-  ( ph -> ( C ` <" I J "> ) : D --> D )
36 35 ffund 
 |-  ( ph -> Fun ( C ` <" I J "> ) )
37 4 adantr 
 |-  ( ( ph /\ x = I ) -> I e. D )
38 34 fdmd 
 |-  ( ( C ` <" I J "> ) e. ( Base ` S ) -> dom ( C ` <" I J "> ) = D )
39 20 38 syl 
 |-  ( ph -> dom ( C ` <" I J "> ) = D )
40 39 adantr 
 |-  ( ( ph /\ x = I ) -> dom ( C ` <" I J "> ) = D )
41 37 28 40 3eltr4d 
 |-  ( ( ph /\ x = I ) -> x e. dom ( C ` <" I J "> ) )
42 fvco 
 |-  ( ( Fun ( C ` <" I J "> ) /\ x e. dom ( C ` <" I J "> ) ) -> ( ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) ` x ) = ( ( C ` <" I K "> ) ` ( ( C ` <" I J "> ) ` x ) ) )
43 36 41 42 syl2an2r 
 |-  ( ( ph /\ x = I ) -> ( ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) ` x ) = ( ( C ` <" I K "> ) ` ( ( C ` <" I J "> ) ` x ) ) )
44 28 fveq2d 
 |-  ( ( ph /\ x = I ) -> ( ( C ` <" I J "> ) ` x ) = ( ( C ` <" I J "> ) ` I ) )
45 1 3 4 5 7 2 cyc2fv1 
 |-  ( ph -> ( ( C ` <" I J "> ) ` I ) = J )
46 45 adantr 
 |-  ( ( ph /\ x = I ) -> ( ( C ` <" I J "> ) ` I ) = J )
47 44 46 eqtrd 
 |-  ( ( ph /\ x = I ) -> ( ( C ` <" I J "> ) ` x ) = J )
48 47 fveq2d 
 |-  ( ( ph /\ x = I ) -> ( ( C ` <" I K "> ) ` ( ( C ` <" I J "> ) ` x ) ) = ( ( C ` <" I K "> ) ` J ) )
49 8 necomd 
 |-  ( ph -> K =/= J )
50 7 necomd 
 |-  ( ph -> J =/= I )
51 1 2 3 4 6 5 18 49 50 cyc2fvx 
 |-  ( ph -> ( ( C ` <" I K "> ) ` J ) = J )
52 51 adantr 
 |-  ( ( ph /\ x = I ) -> ( ( C ` <" I K "> ) ` J ) = J )
53 43 48 52 3eqtrd 
 |-  ( ( ph /\ x = I ) -> ( ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) ` x ) = J )
54 33 53 eqtrd 
 |-  ( ( ph /\ x = I ) -> ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) = J )
55 27 29 54 3eqtr4d 
 |-  ( ( ph /\ x = I ) -> ( ( C ` <" I J K "> ) ` x ) = ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) )
56 55 adantlr 
 |-  ( ( ( ph /\ x e. { I , J , K } ) /\ x = I ) -> ( ( C ` <" I J K "> ) ` x ) = ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) )
57 1 2 3 4 5 6 7 8 9 cyc3fv2 
 |-  ( ph -> ( ( C ` <" I J K "> ) ` J ) = K )
58 57 adantr 
 |-  ( ( ph /\ x = J ) -> ( ( C ` <" I J K "> ) ` J ) = K )
59 simpr 
 |-  ( ( ph /\ x = J ) -> x = J )
60 59 fveq2d 
 |-  ( ( ph /\ x = J ) -> ( ( C ` <" I J K "> ) ` x ) = ( ( C ` <" I J K "> ) ` J ) )
61 31 adantr 
 |-  ( ( ph /\ x = J ) -> ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) = ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) )
62 61 fveq1d 
 |-  ( ( ph /\ x = J ) -> ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) = ( ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) ` x ) )
63 5 adantr 
 |-  ( ( ph /\ x = J ) -> J e. D )
64 39 adantr 
 |-  ( ( ph /\ x = J ) -> dom ( C ` <" I J "> ) = D )
65 63 59 64 3eltr4d 
 |-  ( ( ph /\ x = J ) -> x e. dom ( C ` <" I J "> ) )
66 36 65 42 syl2an2r 
 |-  ( ( ph /\ x = J ) -> ( ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) ` x ) = ( ( C ` <" I K "> ) ` ( ( C ` <" I J "> ) ` x ) ) )
67 59 fveq2d 
 |-  ( ( ph /\ x = J ) -> ( ( C ` <" I J "> ) ` x ) = ( ( C ` <" I J "> ) ` J ) )
68 1 3 4 5 7 2 cyc2fv2 
 |-  ( ph -> ( ( C ` <" I J "> ) ` J ) = I )
69 68 adantr 
 |-  ( ( ph /\ x = J ) -> ( ( C ` <" I J "> ) ` J ) = I )
70 67 69 eqtrd 
 |-  ( ( ph /\ x = J ) -> ( ( C ` <" I J "> ) ` x ) = I )
71 70 fveq2d 
 |-  ( ( ph /\ x = J ) -> ( ( C ` <" I K "> ) ` ( ( C ` <" I J "> ) ` x ) ) = ( ( C ` <" I K "> ) ` I ) )
72 1 3 4 6 18 2 cyc2fv1 
 |-  ( ph -> ( ( C ` <" I K "> ) ` I ) = K )
73 72 adantr 
 |-  ( ( ph /\ x = J ) -> ( ( C ` <" I K "> ) ` I ) = K )
74 66 71 73 3eqtrd 
 |-  ( ( ph /\ x = J ) -> ( ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) ` x ) = K )
75 62 74 eqtrd 
 |-  ( ( ph /\ x = J ) -> ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) = K )
76 58 60 75 3eqtr4d 
 |-  ( ( ph /\ x = J ) -> ( ( C ` <" I J K "> ) ` x ) = ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) )
77 76 adantlr 
 |-  ( ( ( ph /\ x e. { I , J , K } ) /\ x = J ) -> ( ( C ` <" I J K "> ) ` x ) = ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) )
78 1 2 3 4 5 6 7 8 9 cyc3fv3 
 |-  ( ph -> ( ( C ` <" I J K "> ) ` K ) = I )
79 78 adantr 
 |-  ( ( ph /\ x = K ) -> ( ( C ` <" I J K "> ) ` K ) = I )
80 simpr 
 |-  ( ( ph /\ x = K ) -> x = K )
81 80 fveq2d 
 |-  ( ( ph /\ x = K ) -> ( ( C ` <" I J K "> ) ` x ) = ( ( C ` <" I J K "> ) ` K ) )
82 31 adantr 
 |-  ( ( ph /\ x = K ) -> ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) = ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) )
83 82 fveq1d 
 |-  ( ( ph /\ x = K ) -> ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) = ( ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) ` x ) )
84 6 adantr 
 |-  ( ( ph /\ x = K ) -> K e. D )
85 39 adantr 
 |-  ( ( ph /\ x = K ) -> dom ( C ` <" I J "> ) = D )
86 84 80 85 3eltr4d 
 |-  ( ( ph /\ x = K ) -> x e. dom ( C ` <" I J "> ) )
87 36 86 42 syl2an2r 
 |-  ( ( ph /\ x = K ) -> ( ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) ` x ) = ( ( C ` <" I K "> ) ` ( ( C ` <" I J "> ) ` x ) ) )
88 80 fveq2d 
 |-  ( ( ph /\ x = K ) -> ( ( C ` <" I J "> ) ` x ) = ( ( C ` <" I J "> ) ` K ) )
89 1 2 3 4 5 6 7 8 9 cyc2fvx 
 |-  ( ph -> ( ( C ` <" I J "> ) ` K ) = K )
90 89 adantr 
 |-  ( ( ph /\ x = K ) -> ( ( C ` <" I J "> ) ` K ) = K )
91 88 90 eqtrd 
 |-  ( ( ph /\ x = K ) -> ( ( C ` <" I J "> ) ` x ) = K )
92 91 fveq2d 
 |-  ( ( ph /\ x = K ) -> ( ( C ` <" I K "> ) ` ( ( C ` <" I J "> ) ` x ) ) = ( ( C ` <" I K "> ) ` K ) )
93 1 3 4 6 18 2 cyc2fv2 
 |-  ( ph -> ( ( C ` <" I K "> ) ` K ) = I )
94 93 adantr 
 |-  ( ( ph /\ x = K ) -> ( ( C ` <" I K "> ) ` K ) = I )
95 87 92 94 3eqtrd 
 |-  ( ( ph /\ x = K ) -> ( ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) ` x ) = I )
96 83 95 eqtrd 
 |-  ( ( ph /\ x = K ) -> ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) = I )
97 79 81 96 3eqtr4d 
 |-  ( ( ph /\ x = K ) -> ( ( C ` <" I J K "> ) ` x ) = ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) )
98 97 adantlr 
 |-  ( ( ( ph /\ x e. { I , J , K } ) /\ x = K ) -> ( ( C ` <" I J K "> ) ` x ) = ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) )
99 eltpi 
 |-  ( x e. { I , J , K } -> ( x = I \/ x = J \/ x = K ) )
100 99 adantl 
 |-  ( ( ph /\ x e. { I , J , K } ) -> ( x = I \/ x = J \/ x = K ) )
101 56 77 98 100 mpjao3dan 
 |-  ( ( ph /\ x e. { I , J , K } ) -> ( ( C ` <" I J K "> ) ` x ) = ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) )
102 101 adantlr 
 |-  ( ( ( ph /\ x e. D ) /\ x e. { I , J , K } ) -> ( ( C ` <" I J K "> ) ` x ) = ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) )
103 35 adantr 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> ( C ` <" I J "> ) : D --> D )
104 103 ffund 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> Fun ( C ` <" I J "> ) )
105 simpr 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> x e. ( D \ { I , J , K } ) )
106 105 eldifad 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> x e. D )
107 39 adantr 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> dom ( C ` <" I J "> ) = D )
108 106 107 eleqtrrd 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> x e. dom ( C ` <" I J "> ) )
109 104 108 42 syl2anc 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> ( ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) ` x ) = ( ( C ` <" I K "> ) ` ( ( C ` <" I J "> ) ` x ) ) )
110 3 adantr 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> D e. V )
111 4 5 s2cld 
 |-  ( ph -> <" I J "> e. Word D )
112 111 adantr 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> <" I J "> e. Word D )
113 4 5 7 s2f1 
 |-  ( ph -> <" I J "> : dom <" I J "> -1-1-> D )
114 113 adantr 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> <" I J "> : dom <" I J "> -1-1-> D )
115 tpid1g 
 |-  ( I e. D -> I e. { I , J , K } )
116 4 115 syl 
 |-  ( ph -> I e. { I , J , K } )
117 tpid2g 
 |-  ( J e. D -> J e. { I , J , K } )
118 5 117 syl 
 |-  ( ph -> J e. { I , J , K } )
119 116 118 prssd 
 |-  ( ph -> { I , J } C_ { I , J , K } )
120 4 5 s2rn 
 |-  ( ph -> ran <" I J "> = { I , J } )
121 120 eqcomd 
 |-  ( ph -> { I , J } = ran <" I J "> )
122 4 5 6 s3rn 
 |-  ( ph -> ran <" I J K "> = { I , J , K } )
123 122 eqcomd 
 |-  ( ph -> { I , J , K } = ran <" I J K "> )
124 119 121 123 3sstr3d 
 |-  ( ph -> ran <" I J "> C_ ran <" I J K "> )
125 124 adantr 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> ran <" I J "> C_ ran <" I J K "> )
126 105 eldifbd 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> -. x e. { I , J , K } )
127 122 adantr 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> ran <" I J K "> = { I , J , K } )
128 126 127 neleqtrrd 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> -. x e. ran <" I J K "> )
129 125 128 ssneldd 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> -. x e. ran <" I J "> )
130 1 110 112 114 106 129 cycpmfv3 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> ( ( C ` <" I J "> ) ` x ) = x )
131 130 fveq2d 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> ( ( C ` <" I K "> ) ` ( ( C ` <" I J "> ) ` x ) ) = ( ( C ` <" I K "> ) ` x ) )
132 4 6 s2cld 
 |-  ( ph -> <" I K "> e. Word D )
133 132 adantr 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> <" I K "> e. Word D )
134 4 6 18 s2f1 
 |-  ( ph -> <" I K "> : dom <" I K "> -1-1-> D )
135 134 adantr 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> <" I K "> : dom <" I K "> -1-1-> D )
136 tpid3g 
 |-  ( K e. D -> K e. { I , J , K } )
137 6 136 syl 
 |-  ( ph -> K e. { I , J , K } )
138 116 137 prssd 
 |-  ( ph -> { I , K } C_ { I , J , K } )
139 138 adantr 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> { I , K } C_ { I , J , K } )
140 4 6 s2rn 
 |-  ( ph -> ran <" I K "> = { I , K } )
141 140 eqcomd 
 |-  ( ph -> { I , K } = ran <" I K "> )
142 141 adantr 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> { I , K } = ran <" I K "> )
143 123 adantr 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> { I , J , K } = ran <" I J K "> )
144 139 142 143 3sstr3d 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> ran <" I K "> C_ ran <" I J K "> )
145 144 128 ssneldd 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> -. x e. ran <" I K "> )
146 1 110 133 135 106 145 cycpmfv3 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> ( ( C ` <" I K "> ) ` x ) = x )
147 109 131 146 3eqtrd 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> ( ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) ` x ) = x )
148 31 adantr 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) = ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) )
149 148 fveq1d 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) = ( ( ( C ` <" I K "> ) o. ( C ` <" I J "> ) ) ` x ) )
150 4 5 6 s3cld 
 |-  ( ph -> <" I J K "> e. Word D )
151 150 adantr 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> <" I J K "> e. Word D )
152 4 5 6 7 8 9 s3f1 
 |-  ( ph -> <" I J K "> : dom <" I J K "> -1-1-> D )
153 152 adantr 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> <" I J K "> : dom <" I J K "> -1-1-> D )
154 1 110 151 153 106 128 cycpmfv3 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> ( ( C ` <" I J K "> ) ` x ) = x )
155 147 149 154 3eqtr4rd 
 |-  ( ( ph /\ x e. ( D \ { I , J , K } ) ) -> ( ( C ` <" I J K "> ) ` x ) = ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) )
156 155 adantlr 
 |-  ( ( ( ph /\ x e. D ) /\ x e. ( D \ { I , J , K } ) ) -> ( ( C ` <" I J K "> ) ` x ) = ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) )
157 tpssi 
 |-  ( ( I e. D /\ J e. D /\ K e. D ) -> { I , J , K } C_ D )
158 4 5 6 157 syl3anc 
 |-  ( ph -> { I , J , K } C_ D )
159 undif 
 |-  ( { I , J , K } C_ D <-> ( { I , J , K } u. ( D \ { I , J , K } ) ) = D )
160 158 159 sylib 
 |-  ( ph -> ( { I , J , K } u. ( D \ { I , J , K } ) ) = D )
161 160 eleq2d 
 |-  ( ph -> ( x e. ( { I , J , K } u. ( D \ { I , J , K } ) ) <-> x e. D ) )
162 161 biimpar 
 |-  ( ( ph /\ x e. D ) -> x e. ( { I , J , K } u. ( D \ { I , J , K } ) ) )
163 elun 
 |-  ( x e. ( { I , J , K } u. ( D \ { I , J , K } ) ) <-> ( x e. { I , J , K } \/ x e. ( D \ { I , J , K } ) ) )
164 162 163 sylib 
 |-  ( ( ph /\ x e. D ) -> ( x e. { I , J , K } \/ x e. ( D \ { I , J , K } ) ) )
165 102 156 164 mpjaodan 
 |-  ( ( ph /\ x e. D ) -> ( ( C ` <" I J K "> ) ` x ) = ( ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) ` x ) )
166 15 25 165 eqfnfvd 
 |-  ( ph -> ( C ` <" I J K "> ) = ( ( C ` <" I K "> ) .x. ( C ` <" I J "> ) ) )