Metamath Proof Explorer

Theorem cyc3genpmlem

Description: Lemma for cyc3genpm . (Contributed by Thierry Arnoux, 24-Sep-2023)

Ref Expression
Hypotheses cyc3genpm.t 
|- C = ( M " ( `' # " { 3 } ) )
cyc3genpm.a 
|- A = ( pmEven ` D )
cyc3genpm.s 
|- S = ( SymGrp ` D )
cyc3genpm.n 
|- N = ( # ` D )
cyc3genpm.m 
|- M = ( toCyc ` D )
cyc3genpmlem.t 
|- .x. = ( +g ` S )
cyc3genpmlem.i 
|- ( ph -> I e. D )
cyc3genpmlem.j 
|- ( ph -> J e. D )
cyc3genpmlem.k 
|- ( ph -> K e. D )
cyc3genpmlem.l 
|- ( ph -> L e. D )
cyc3genpmlem.e 
|- ( ph -> E = ( M ` <" I J "> ) )
cyc3genpmlem.f 
|- ( ph -> F = ( M ` <" K L "> ) )
cyc3genpmlem.d 
|- ( ph -> D e. V )
cyc3genpmlem.1 
|- ( ph -> I =/= J )
cyc3genpmlem.2 
|- ( ph -> K =/= L )
Assertion cyc3genpmlem 
|- ( ph -> E. c e. Word C ( E .x. F ) = ( S gsum c ) )

Proof

Step Hyp Ref Expression
1 cyc3genpm.t 
 |-  C = ( M " ( `' # " { 3 } ) )
2 cyc3genpm.a 
 |-  A = ( pmEven ` D )
3 cyc3genpm.s 
 |-  S = ( SymGrp ` D )
4 cyc3genpm.n 
 |-  N = ( # ` D )
5 cyc3genpm.m 
 |-  M = ( toCyc ` D )
6 cyc3genpmlem.t 
 |-  .x. = ( +g ` S )
7 cyc3genpmlem.i 
 |-  ( ph -> I e. D )
8 cyc3genpmlem.j 
 |-  ( ph -> J e. D )
9 cyc3genpmlem.k 
 |-  ( ph -> K e. D )
10 cyc3genpmlem.l 
 |-  ( ph -> L e. D )
11 cyc3genpmlem.e 
 |-  ( ph -> E = ( M ` <" I J "> ) )
12 cyc3genpmlem.f 
 |-  ( ph -> F = ( M ` <" K L "> ) )
13 cyc3genpmlem.d 
 |-  ( ph -> D e. V )
14 cyc3genpmlem.1 
 |-  ( ph -> I =/= J )
15 cyc3genpmlem.2 
 |-  ( ph -> K =/= L )
16 wrd0 
 |-  (/) e. Word C
17 16 a1i 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> (/) e. Word C )
18 simpr 
 |-  ( ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) /\ c = (/) ) -> c = (/) )
19 18 oveq2d 
 |-  ( ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) /\ c = (/) ) -> ( S gsum c ) = ( S gsum (/) ) )
20 19 eqeq2d 
 |-  ( ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) /\ c = (/) ) -> ( ( E .x. F ) = ( S gsum c ) <-> ( E .x. F ) = ( S gsum (/) ) ) )
21 5 13 7 8 14 3 cycpm2cl 
 |-  ( ph -> ( M ` <" I J "> ) e. ( Base ` S ) )
22 11 21 eqeltrd 
 |-  ( ph -> E e. ( Base ` S ) )
23 5 13 9 10 15 3 cycpm2cl 
 |-  ( ph -> ( M ` <" K L "> ) e. ( Base ` S ) )
24 12 23 eqeltrd 
 |-  ( ph -> F e. ( Base ` S ) )
25 eqid 
 |-  ( Base ` S ) = ( Base ` S )
26 3 25 6 symgov 
 |-  ( ( E e. ( Base ` S ) /\ F e. ( Base ` S ) ) -> ( E .x. F ) = ( E o. F ) )
27 22 24 26 syl2anc 
 |-  ( ph -> ( E .x. F ) = ( E o. F ) )
28 27 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> ( E .x. F ) = ( E o. F ) )
29 11 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> E = ( M ` <" I J "> ) )
30 eqid 
 |-  ( pmTrsp ` D ) = ( pmTrsp ` D )
31 5 13 7 8 14 30 cycpm2tr 
 |-  ( ph -> ( M ` <" I J "> ) = ( ( pmTrsp ` D ) ` { I , J } ) )
32 31 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> ( M ` <" I J "> ) = ( ( pmTrsp ` D ) ` { I , J } ) )
33 29 32 eqtrd 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> E = ( ( pmTrsp ` D ) ` { I , J } ) )
34 5 13 9 10 15 30 cycpm2tr 
 |-  ( ph -> ( M ` <" K L "> ) = ( ( pmTrsp ` D ) ` { K , L } ) )
35 34 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> ( M ` <" K L "> ) = ( ( pmTrsp ` D ) ` { K , L } ) )
36 12 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> F = ( M ` <" K L "> ) )
37 7 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> I e. D )
38 8 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> J e. D )
39 14 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> I =/= J )
40 simplr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> I e. { K , L } )
41 simpr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> J e. { K , L } )
42 40 41 prssd 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> { I , J } C_ { K , L } )
43 ssprsseq 
 |-  ( ( I e. D /\ J e. D /\ I =/= J ) -> ( { I , J } C_ { K , L } <-> { I , J } = { K , L } ) )
44 43 biimpa 
 |-  ( ( ( I e. D /\ J e. D /\ I =/= J ) /\ { I , J } C_ { K , L } ) -> { I , J } = { K , L } )
45 37 38 39 42 44 syl31anc 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> { I , J } = { K , L } )
46 45 fveq2d 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> ( ( pmTrsp ` D ) ` { I , J } ) = ( ( pmTrsp ` D ) ` { K , L } ) )
47 35 36 46 3eqtr4d 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> F = ( ( pmTrsp ` D ) ` { I , J } ) )
48 33 47 coeq12d 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> ( E o. F ) = ( ( ( pmTrsp ` D ) ` { I , J } ) o. ( ( pmTrsp ` D ) ` { I , J } ) ) )
49 13 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> D e. V )
50 37 38 prssd 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> { I , J } C_ D )
51 pr2nelem 
 |-  ( ( I e. D /\ J e. D /\ I =/= J ) -> { I , J } ~~ 2o )
52 37 38 39 51 syl3anc 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> { I , J } ~~ 2o )
53 eqid 
 |-  ran ( pmTrsp ` D ) = ran ( pmTrsp ` D )
54 30 53 pmtrrn 
 |-  ( ( D e. V /\ { I , J } C_ D /\ { I , J } ~~ 2o ) -> ( ( pmTrsp ` D ) ` { I , J } ) e. ran ( pmTrsp ` D ) )
55 49 50 52 54 syl3anc 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> ( ( pmTrsp ` D ) ` { I , J } ) e. ran ( pmTrsp ` D ) )
56 30 53 pmtrfinv 
 |-  ( ( ( pmTrsp ` D ) ` { I , J } ) e. ran ( pmTrsp ` D ) -> ( ( ( pmTrsp ` D ) ` { I , J } ) o. ( ( pmTrsp ` D ) ` { I , J } ) ) = ( _I |` D ) )
57 55 56 syl 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> ( ( ( pmTrsp ` D ) ` { I , J } ) o. ( ( pmTrsp ` D ) ` { I , J } ) ) = ( _I |` D ) )
58 28 48 57 3eqtrd 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> ( E .x. F ) = ( _I |` D ) )
59 3 symgid 
 |-  ( D e. V -> ( _I |` D ) = ( 0g ` S ) )
60 49 59 syl 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> ( _I |` D ) = ( 0g ` S ) )
61 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
62 61 gsum0 
 |-  ( S gsum (/) ) = ( 0g ` S )
63 60 62 eqtr4di 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> ( _I |` D ) = ( S gsum (/) ) )
64 58 63 eqtrd 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> ( E .x. F ) = ( S gsum (/) ) )
65 17 20 64 rspcedvd 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ J e. { K , L } ) -> E. c e. Word C ( E .x. F ) = ( S gsum c ) )
66 13 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> D e. V )
67 7 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> I e. D )
68 9 10 prssd 
 |-  ( ph -> { K , L } C_ D )
69 68 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> { K , L } C_ D )
70 simplr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> I e. { K , L } )
71 pr2nelem 
 |-  ( ( K e. D /\ L e. D /\ K =/= L ) -> { K , L } ~~ 2o )
72 9 10 15 71 syl3anc 
 |-  ( ph -> { K , L } ~~ 2o )
73 72 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> { K , L } ~~ 2o )
74 unidifsnel 
 |-  ( ( I e. { K , L } /\ { K , L } ~~ 2o ) -> U. ( { K , L } \ { I } ) e. { K , L } )
75 70 73 74 syl2anc 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> U. ( { K , L } \ { I } ) e. { K , L } )
76 69 75 sseldd 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> U. ( { K , L } \ { I } ) e. D )
77 8 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> J e. D )
78 unidifsnne 
 |-  ( ( I e. { K , L } /\ { K , L } ~~ 2o ) -> U. ( { K , L } \ { I } ) =/= I )
79 70 73 78 syl2anc 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> U. ( { K , L } \ { I } ) =/= I )
80 79 necomd 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> I =/= U. ( { K , L } \ { I } ) )
81 nelne2 
 |-  ( ( U. ( { K , L } \ { I } ) e. { K , L } /\ -. J e. { K , L } ) -> U. ( { K , L } \ { I } ) =/= J )
82 75 81 sylancom 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> U. ( { K , L } \ { I } ) =/= J )
83 14 necomd 
 |-  ( ph -> J =/= I )
84 83 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> J =/= I )
85 5 3 66 67 76 77 80 82 84 cycpm3cl2 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" I U. ( { K , L } \ { I } ) J "> ) e. ( M " ( `' # " { 3 } ) ) )
86 85 1 eleqtrrdi 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" I U. ( { K , L } \ { I } ) J "> ) e. C )
87 86 s1cld 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> <" ( M ` <" I U. ( { K , L } \ { I } ) J "> ) "> e. Word C )
88 simpr 
 |-  ( ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) /\ c = <" ( M ` <" I U. ( { K , L } \ { I } ) J "> ) "> ) -> c = <" ( M ` <" I U. ( { K , L } \ { I } ) J "> ) "> )
89 88 oveq2d 
 |-  ( ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) /\ c = <" ( M ` <" I U. ( { K , L } \ { I } ) J "> ) "> ) -> ( S gsum c ) = ( S gsum <" ( M ` <" I U. ( { K , L } \ { I } ) J "> ) "> ) )
90 89 eqeq2d 
 |-  ( ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) /\ c = <" ( M ` <" I U. ( { K , L } \ { I } ) J "> ) "> ) -> ( ( E .x. F ) = ( S gsum c ) <-> ( E .x. F ) = ( S gsum <" ( M ` <" I U. ( { K , L } \ { I } ) J "> ) "> ) ) )
91 5 3 66 67 76 77 80 82 84 6 cyc3co2 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" I U. ( { K , L } \ { I } ) J "> ) = ( ( M ` <" I J "> ) .x. ( M ` <" I U. ( { K , L } \ { I } ) "> ) ) )
92 5 3 66 67 76 77 80 82 84 cycpm3cl 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" I U. ( { K , L } \ { I } ) J "> ) e. ( Base ` S ) )
93 25 gsumws1 
 |-  ( ( M ` <" I U. ( { K , L } \ { I } ) J "> ) e. ( Base ` S ) -> ( S gsum <" ( M ` <" I U. ( { K , L } \ { I } ) J "> ) "> ) = ( M ` <" I U. ( { K , L } \ { I } ) J "> ) )
94 92 93 syl 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> ( S gsum <" ( M ` <" I U. ( { K , L } \ { I } ) J "> ) "> ) = ( M ` <" I U. ( { K , L } \ { I } ) J "> ) )
95 11 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> E = ( M ` <" I J "> ) )
96 en2eleq 
 |-  ( ( I e. { K , L } /\ { K , L } ~~ 2o ) -> { K , L } = { I , U. ( { K , L } \ { I } ) } )
97 70 73 96 syl2anc 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> { K , L } = { I , U. ( { K , L } \ { I } ) } )
98 97 fveq2d 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( pmTrsp ` D ) ` { K , L } ) = ( ( pmTrsp ` D ) ` { I , U. ( { K , L } \ { I } ) } ) )
99 12 34 eqtrd 
 |-  ( ph -> F = ( ( pmTrsp ` D ) ` { K , L } ) )
100 99 ad2antrr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> F = ( ( pmTrsp ` D ) ` { K , L } ) )
101 5 66 67 76 80 30 cycpm2tr 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" I U. ( { K , L } \ { I } ) "> ) = ( ( pmTrsp ` D ) ` { I , U. ( { K , L } \ { I } ) } ) )
102 98 100 101 3eqtr4d 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> F = ( M ` <" I U. ( { K , L } \ { I } ) "> ) )
103 95 102 oveq12d 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> ( E .x. F ) = ( ( M ` <" I J "> ) .x. ( M ` <" I U. ( { K , L } \ { I } ) "> ) ) )
104 91 94 103 3eqtr4rd 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> ( E .x. F ) = ( S gsum <" ( M ` <" I U. ( { K , L } \ { I } ) J "> ) "> ) )
105 87 90 104 rspcedvd 
 |-  ( ( ( ph /\ I e. { K , L } ) /\ -. J e. { K , L } ) -> E. c e. Word C ( E .x. F ) = ( S gsum c ) )
106 65 105 pm2.61dan 
 |-  ( ( ph /\ I e. { K , L } ) -> E. c e. Word C ( E .x. F ) = ( S gsum c ) )
107 13 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> D e. V )
108 8 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> J e. D )
109 68 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> { K , L } C_ D )
110 simpr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> J e. { K , L } )
111 72 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> { K , L } ~~ 2o )
112 unidifsnel 
 |-  ( ( J e. { K , L } /\ { K , L } ~~ 2o ) -> U. ( { K , L } \ { J } ) e. { K , L } )
113 110 111 112 syl2anc 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> U. ( { K , L } \ { J } ) e. { K , L } )
114 109 113 sseldd 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> U. ( { K , L } \ { J } ) e. D )
115 7 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> I e. D )
116 unidifsnne 
 |-  ( ( J e. { K , L } /\ { K , L } ~~ 2o ) -> U. ( { K , L } \ { J } ) =/= J )
117 110 111 116 syl2anc 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> U. ( { K , L } \ { J } ) =/= J )
118 117 necomd 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> J =/= U. ( { K , L } \ { J } ) )
119 simplr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> -. I e. { K , L } )
120 nelne2 
 |-  ( ( U. ( { K , L } \ { J } ) e. { K , L } /\ -. I e. { K , L } ) -> U. ( { K , L } \ { J } ) =/= I )
121 113 119 120 syl2anc 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> U. ( { K , L } \ { J } ) =/= I )
122 14 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> I =/= J )
123 5 3 107 108 114 115 118 121 122 cycpm3cl2 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> ( M ` <" J U. ( { K , L } \ { J } ) I "> ) e. ( M " ( `' # " { 3 } ) ) )
124 123 1 eleqtrrdi 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> ( M ` <" J U. ( { K , L } \ { J } ) I "> ) e. C )
125 124 s1cld 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> <" ( M ` <" J U. ( { K , L } \ { J } ) I "> ) "> e. Word C )
126 simpr 
 |-  ( ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) /\ c = <" ( M ` <" J U. ( { K , L } \ { J } ) I "> ) "> ) -> c = <" ( M ` <" J U. ( { K , L } \ { J } ) I "> ) "> )
127 126 oveq2d 
 |-  ( ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) /\ c = <" ( M ` <" J U. ( { K , L } \ { J } ) I "> ) "> ) -> ( S gsum c ) = ( S gsum <" ( M ` <" J U. ( { K , L } \ { J } ) I "> ) "> ) )
128 127 eqeq2d 
 |-  ( ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) /\ c = <" ( M ` <" J U. ( { K , L } \ { J } ) I "> ) "> ) -> ( ( E .x. F ) = ( S gsum c ) <-> ( E .x. F ) = ( S gsum <" ( M ` <" J U. ( { K , L } \ { J } ) I "> ) "> ) ) )
129 5 3 107 108 114 115 118 121 122 6 cyc3co2 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> ( M ` <" J U. ( { K , L } \ { J } ) I "> ) = ( ( M ` <" J I "> ) .x. ( M ` <" J U. ( { K , L } \ { J } ) "> ) ) )
130 5 3 107 108 114 115 118 121 122 cycpm3cl 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> ( M ` <" J U. ( { K , L } \ { J } ) I "> ) e. ( Base ` S ) )
131 25 gsumws1 
 |-  ( ( M ` <" J U. ( { K , L } \ { J } ) I "> ) e. ( Base ` S ) -> ( S gsum <" ( M ` <" J U. ( { K , L } \ { J } ) I "> ) "> ) = ( M ` <" J U. ( { K , L } \ { J } ) I "> ) )
132 130 131 syl 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> ( S gsum <" ( M ` <" J U. ( { K , L } \ { J } ) I "> ) "> ) = ( M ` <" J U. ( { K , L } \ { J } ) I "> ) )
133 prcom 
 |-  { I , J } = { J , I }
134 133 fveq2i 
 |-  ( ( pmTrsp ` D ) ` { I , J } ) = ( ( pmTrsp ` D ) ` { J , I } )
135 5 13 8 7 83 30 cycpm2tr 
 |-  ( ph -> ( M ` <" J I "> ) = ( ( pmTrsp ` D ) ` { J , I } ) )
136 134 31 135 3eqtr4a 
 |-  ( ph -> ( M ` <" I J "> ) = ( M ` <" J I "> ) )
137 11 136 eqtrd 
 |-  ( ph -> E = ( M ` <" J I "> ) )
138 137 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> E = ( M ` <" J I "> ) )
139 en2eleq 
 |-  ( ( J e. { K , L } /\ { K , L } ~~ 2o ) -> { K , L } = { J , U. ( { K , L } \ { J } ) } )
140 110 111 139 syl2anc 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> { K , L } = { J , U. ( { K , L } \ { J } ) } )
141 140 fveq2d 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> ( ( pmTrsp ` D ) ` { K , L } ) = ( ( pmTrsp ` D ) ` { J , U. ( { K , L } \ { J } ) } ) )
142 99 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> F = ( ( pmTrsp ` D ) ` { K , L } ) )
143 5 107 108 114 118 30 cycpm2tr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> ( M ` <" J U. ( { K , L } \ { J } ) "> ) = ( ( pmTrsp ` D ) ` { J , U. ( { K , L } \ { J } ) } ) )
144 141 142 143 3eqtr4d 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> F = ( M ` <" J U. ( { K , L } \ { J } ) "> ) )
145 138 144 oveq12d 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> ( E .x. F ) = ( ( M ` <" J I "> ) .x. ( M ` <" J U. ( { K , L } \ { J } ) "> ) ) )
146 129 132 145 3eqtr4rd 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> ( E .x. F ) = ( S gsum <" ( M ` <" J U. ( { K , L } \ { J } ) I "> ) "> ) )
147 125 128 146 rspcedvd 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ J e. { K , L } ) -> E. c e. Word C ( E .x. F ) = ( S gsum c ) )
148 13 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> D e. V )
149 8 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> J e. D )
150 9 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> K e. D )
151 7 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> I e. D )
152 simpr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> -. J e. { K , L } )
153 149 152 nelpr1 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> J =/= K )
154 prid1g 
 |-  ( K e. D -> K e. { K , L } )
155 9 154 syl 
 |-  ( ph -> K e. { K , L } )
156 155 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> K e. { K , L } )
157 simplr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> -. I e. { K , L } )
158 nelne2 
 |-  ( ( K e. { K , L } /\ -. I e. { K , L } ) -> K =/= I )
159 156 157 158 syl2anc 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> K =/= I )
160 14 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> I =/= J )
161 5 3 148 149 150 151 153 159 160 cycpm3cl2 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" J K I "> ) e. ( M " ( `' # " { 3 } ) ) )
162 161 1 eleqtrrdi 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" J K I "> ) e. C )
163 10 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> L e. D )
164 15 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> K =/= L )
165 prid2g 
 |-  ( L e. D -> L e. { K , L } )
166 163 165 syl 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> L e. { K , L } )
167 nelne2 
 |-  ( ( L e. { K , L } /\ -. J e. { K , L } ) -> L =/= J )
168 166 167 sylancom 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> L =/= J )
169 5 3 148 150 163 149 164 168 153 cycpm3cl2 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" K L J "> ) e. ( M " ( `' # " { 3 } ) ) )
170 169 1 eleqtrrdi 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" K L J "> ) e. C )
171 162 170 s2cld 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> <" ( M ` <" J K I "> ) ( M ` <" K L J "> ) "> e. Word C )
172 simpr 
 |-  ( ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) /\ c = <" ( M ` <" J K I "> ) ( M ` <" K L J "> ) "> ) -> c = <" ( M ` <" J K I "> ) ( M ` <" K L J "> ) "> )
173 172 oveq2d 
 |-  ( ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) /\ c = <" ( M ` <" J K I "> ) ( M ` <" K L J "> ) "> ) -> ( S gsum c ) = ( S gsum <" ( M ` <" J K I "> ) ( M ` <" K L J "> ) "> ) )
174 173 eqeq2d 
 |-  ( ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) /\ c = <" ( M ` <" J K I "> ) ( M ` <" K L J "> ) "> ) -> ( ( E .x. F ) = ( S gsum c ) <-> ( E .x. F ) = ( S gsum <" ( M ` <" J K I "> ) ( M ` <" K L J "> ) "> ) ) )
175 148 59 syl 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( _I |` D ) = ( 0g ` S ) )
176 175 oveq1d 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( _I |` D ) .x. ( M ` <" K L "> ) ) = ( ( 0g ` S ) .x. ( M ` <" K L "> ) ) )
177 3 symggrp 
 |-  ( D e. V -> S e. Grp )
178 13 177 syl 
 |-  ( ph -> S e. Grp )
179 178 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> S e. Grp )
180 23 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" K L "> ) e. ( Base ` S ) )
181 25 6 61 grplid 
 |-  ( ( S e. Grp /\ ( M ` <" K L "> ) e. ( Base ` S ) ) -> ( ( 0g ` S ) .x. ( M ` <" K L "> ) ) = ( M ` <" K L "> ) )
182 179 180 181 syl2anc 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( 0g ` S ) .x. ( M ` <" K L "> ) ) = ( M ` <" K L "> ) )
183 176 182 eqtrd 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( _I |` D ) .x. ( M ` <" K L "> ) ) = ( M ` <" K L "> ) )
184 183 oveq2d 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( M ` <" I J "> ) .x. ( ( _I |` D ) .x. ( M ` <" K L "> ) ) ) = ( ( M ` <" I J "> ) .x. ( M ` <" K L "> ) ) )
185 21 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" I J "> ) e. ( Base ` S ) )
186 5 148 149 150 153 30 cycpm2tr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" J K "> ) = ( ( pmTrsp ` D ) ` { J , K } ) )
187 53 3 25 symgtrf 
 |-  ran ( pmTrsp ` D ) C_ ( Base ` S )
188 8 9 prssd 
 |-  ( ph -> { J , K } C_ D )
189 188 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> { J , K } C_ D )
190 pr2nelem 
 |-  ( ( J e. D /\ K e. D /\ J =/= K ) -> { J , K } ~~ 2o )
191 149 150 153 190 syl3anc 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> { J , K } ~~ 2o )
192 30 53 pmtrrn 
 |-  ( ( D e. V /\ { J , K } C_ D /\ { J , K } ~~ 2o ) -> ( ( pmTrsp ` D ) ` { J , K } ) e. ran ( pmTrsp ` D ) )
193 148 189 191 192 syl3anc 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( pmTrsp ` D ) ` { J , K } ) e. ran ( pmTrsp ` D ) )
194 187 193 sselid 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( pmTrsp ` D ) ` { J , K } ) e. ( Base ` S ) )
195 186 194 eqeltrd 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" J K "> ) e. ( Base ` S ) )
196 153 necomd 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> K =/= J )
197 5 148 150 149 196 30 cycpm2tr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" K J "> ) = ( ( pmTrsp ` D ) ` { K , J } ) )
198 prcom 
 |-  { J , K } = { K , J }
199 198 a1i 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> { J , K } = { K , J } )
200 199 fveq2d 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( pmTrsp ` D ) ` { J , K } ) = ( ( pmTrsp ` D ) ` { K , J } ) )
201 197 200 eqtr4d 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" K J "> ) = ( ( pmTrsp ` D ) ` { J , K } ) )
202 201 194 eqeltrd 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" K J "> ) e. ( Base ` S ) )
203 25 6 grpcl 
 |-  ( ( S e. Grp /\ ( M ` <" K J "> ) e. ( Base ` S ) /\ ( M ` <" K L "> ) e. ( Base ` S ) ) -> ( ( M ` <" K J "> ) .x. ( M ` <" K L "> ) ) e. ( Base ` S ) )
204 179 202 180 203 syl3anc 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( M ` <" K J "> ) .x. ( M ` <" K L "> ) ) e. ( Base ` S ) )
205 25 6 grpass 
 |-  ( ( S e. Grp /\ ( ( M ` <" I J "> ) e. ( Base ` S ) /\ ( M ` <" J K "> ) e. ( Base ` S ) /\ ( ( M ` <" K J "> ) .x. ( M ` <" K L "> ) ) e. ( Base ` S ) ) ) -> ( ( ( M ` <" I J "> ) .x. ( M ` <" J K "> ) ) .x. ( ( M ` <" K J "> ) .x. ( M ` <" K L "> ) ) ) = ( ( M ` <" I J "> ) .x. ( ( M ` <" J K "> ) .x. ( ( M ` <" K J "> ) .x. ( M ` <" K L "> ) ) ) ) )
206 179 185 195 204 205 syl13anc 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( ( M ` <" I J "> ) .x. ( M ` <" J K "> ) ) .x. ( ( M ` <" K J "> ) .x. ( M ` <" K L "> ) ) ) = ( ( M ` <" I J "> ) .x. ( ( M ` <" J K "> ) .x. ( ( M ` <" K J "> ) .x. ( M ` <" K L "> ) ) ) ) )
207 25 6 grpass 
 |-  ( ( S e. Grp /\ ( ( M ` <" J K "> ) e. ( Base ` S ) /\ ( M ` <" K J "> ) e. ( Base ` S ) /\ ( M ` <" K L "> ) e. ( Base ` S ) ) ) -> ( ( ( M ` <" J K "> ) .x. ( M ` <" K J "> ) ) .x. ( M ` <" K L "> ) ) = ( ( M ` <" J K "> ) .x. ( ( M ` <" K J "> ) .x. ( M ` <" K L "> ) ) ) )
208 179 195 202 180 207 syl13anc 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( ( M ` <" J K "> ) .x. ( M ` <" K J "> ) ) .x. ( M ` <" K L "> ) ) = ( ( M ` <" J K "> ) .x. ( ( M ` <" K J "> ) .x. ( M ` <" K L "> ) ) ) )
209 208 oveq2d 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( M ` <" I J "> ) .x. ( ( ( M ` <" J K "> ) .x. ( M ` <" K J "> ) ) .x. ( M ` <" K L "> ) ) ) = ( ( M ` <" I J "> ) .x. ( ( M ` <" J K "> ) .x. ( ( M ` <" K J "> ) .x. ( M ` <" K L "> ) ) ) ) )
210 186 201 oveq12d 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( M ` <" J K "> ) .x. ( M ` <" K J "> ) ) = ( ( ( pmTrsp ` D ) ` { J , K } ) .x. ( ( pmTrsp ` D ) ` { J , K } ) ) )
211 3 25 6 symgov 
 |-  ( ( ( ( pmTrsp ` D ) ` { J , K } ) e. ( Base ` S ) /\ ( ( pmTrsp ` D ) ` { J , K } ) e. ( Base ` S ) ) -> ( ( ( pmTrsp ` D ) ` { J , K } ) .x. ( ( pmTrsp ` D ) ` { J , K } ) ) = ( ( ( pmTrsp ` D ) ` { J , K } ) o. ( ( pmTrsp ` D ) ` { J , K } ) ) )
212 194 194 211 syl2anc 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( ( pmTrsp ` D ) ` { J , K } ) .x. ( ( pmTrsp ` D ) ` { J , K } ) ) = ( ( ( pmTrsp ` D ) ` { J , K } ) o. ( ( pmTrsp ` D ) ` { J , K } ) ) )
213 30 53 pmtrfinv 
 |-  ( ( ( pmTrsp ` D ) ` { J , K } ) e. ran ( pmTrsp ` D ) -> ( ( ( pmTrsp ` D ) ` { J , K } ) o. ( ( pmTrsp ` D ) ` { J , K } ) ) = ( _I |` D ) )
214 193 213 syl 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( ( pmTrsp ` D ) ` { J , K } ) o. ( ( pmTrsp ` D ) ` { J , K } ) ) = ( _I |` D ) )
215 210 212 214 3eqtrd 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( M ` <" J K "> ) .x. ( M ` <" K J "> ) ) = ( _I |` D ) )
216 215 oveq1d 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( ( M ` <" J K "> ) .x. ( M ` <" K J "> ) ) .x. ( M ` <" K L "> ) ) = ( ( _I |` D ) .x. ( M ` <" K L "> ) ) )
217 216 oveq2d 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( M ` <" I J "> ) .x. ( ( ( M ` <" J K "> ) .x. ( M ` <" K J "> ) ) .x. ( M ` <" K L "> ) ) ) = ( ( M ` <" I J "> ) .x. ( ( _I |` D ) .x. ( M ` <" K L "> ) ) ) )
218 206 209 217 3eqtr2rd 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( M ` <" I J "> ) .x. ( ( _I |` D ) .x. ( M ` <" K L "> ) ) ) = ( ( ( M ` <" I J "> ) .x. ( M ` <" J K "> ) ) .x. ( ( M ` <" K J "> ) .x. ( M ` <" K L "> ) ) ) )
219 184 218 eqtr3d 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( M ` <" I J "> ) .x. ( M ` <" K L "> ) ) = ( ( ( M ` <" I J "> ) .x. ( M ` <" J K "> ) ) .x. ( ( M ` <" K J "> ) .x. ( M ` <" K L "> ) ) ) )
220 11 12 oveq12d 
 |-  ( ph -> ( E .x. F ) = ( ( M ` <" I J "> ) .x. ( M ` <" K L "> ) ) )
221 220 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( E .x. F ) = ( ( M ` <" I J "> ) .x. ( M ` <" K L "> ) ) )
222 5 3 148 149 150 151 153 159 160 6 cyc3co2 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" J K I "> ) = ( ( M ` <" J I "> ) .x. ( M ` <" J K "> ) ) )
223 136 oveq1d 
 |-  ( ph -> ( ( M ` <" I J "> ) .x. ( M ` <" J K "> ) ) = ( ( M ` <" J I "> ) .x. ( M ` <" J K "> ) ) )
224 223 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( M ` <" I J "> ) .x. ( M ` <" J K "> ) ) = ( ( M ` <" J I "> ) .x. ( M ` <" J K "> ) ) )
225 222 224 eqtr4d 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" J K I "> ) = ( ( M ` <" I J "> ) .x. ( M ` <" J K "> ) ) )
226 5 3 148 150 163 149 164 168 153 6 cyc3co2 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" K L J "> ) = ( ( M ` <" K J "> ) .x. ( M ` <" K L "> ) ) )
227 225 226 oveq12d 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( ( M ` <" J K I "> ) .x. ( M ` <" K L J "> ) ) = ( ( ( M ` <" I J "> ) .x. ( M ` <" J K "> ) ) .x. ( ( M ` <" K J "> ) .x. ( M ` <" K L "> ) ) ) )
228 219 221 227 3eqtr4d 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( E .x. F ) = ( ( M ` <" J K I "> ) .x. ( M ` <" K L J "> ) ) )
229 178 grpmndd 
 |-  ( ph -> S e. Mnd )
230 229 ad2antrr 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> S e. Mnd )
231 5 3 148 149 150 151 153 159 160 cycpm3cl 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" J K I "> ) e. ( Base ` S ) )
232 226 204 eqeltrd 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( M ` <" K L J "> ) e. ( Base ` S ) )
233 25 6 gsumws2 
 |-  ( ( S e. Mnd /\ ( M ` <" J K I "> ) e. ( Base ` S ) /\ ( M ` <" K L J "> ) e. ( Base ` S ) ) -> ( S gsum <" ( M ` <" J K I "> ) ( M ` <" K L J "> ) "> ) = ( ( M ` <" J K I "> ) .x. ( M ` <" K L J "> ) ) )
234 230 231 232 233 syl3anc 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( S gsum <" ( M ` <" J K I "> ) ( M ` <" K L J "> ) "> ) = ( ( M ` <" J K I "> ) .x. ( M ` <" K L J "> ) ) )
235 228 234 eqtr4d 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> ( E .x. F ) = ( S gsum <" ( M ` <" J K I "> ) ( M ` <" K L J "> ) "> ) )
236 171 174 235 rspcedvd 
 |-  ( ( ( ph /\ -. I e. { K , L } ) /\ -. J e. { K , L } ) -> E. c e. Word C ( E .x. F ) = ( S gsum c ) )
237 147 236 pm2.61dan 
 |-  ( ( ph /\ -. I e. { K , L } ) -> E. c e. Word C ( E .x. F ) = ( S gsum c ) )
238 106 237 pm2.61dan 
 |-  ( ph -> E. c e. Word C ( E .x. F ) = ( S gsum c ) )