Metamath Proof Explorer

Theorem 1arithidomlem1

Description: Lemma for 1arithidom . (Contributed by Thierry Arnoux, 30-May-2025)

Ref Expression
Hypotheses 1arithidom.u 
|- U = ( Unit ` R )
1arithidom.i 
|- P = ( RPrime ` R )
1arithidom.m 
|- M = ( mulGrp ` R )
1arithidom.t 
|- .x. = ( .r ` R )
1arithidom.j 
|- J = ( 0 ..^ ( # ` F ) )
1arithidom.r 
|- ( ph -> R e. IDomn )
1arithidom.f 
|- ( ph -> F e. Word P )
1arithidom.g 
|- ( ph -> G e. Word P )
1arithidom.1 
|- ( ph -> ( M gsum F ) = ( M gsum G ) )
1arithidomlem.1 
|- ( ph -> Q e. P )
1arithidomlem.2 
|- ( ph -> A. g e. Word P ( E. k e. U ( M gsum F ) = ( k .x. ( M gsum g ) ) -> E. w E. u e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ g = ( u oF .x. ( F o. w ) ) ) ) )
1arithidomlem.3 
|- ( ph -> H e. Word P )
1arithidomlem.4 
|- ( ph -> E. k e. U ( M gsum ( F ++ <" Q "> ) ) = ( k .x. ( M gsum H ) ) )
1arithidomlem.5 
|- ( ph -> K e. ( 0 ..^ ( # ` H ) ) )
1arithidomlem.6 
|- ( ph -> Q ( ||r ` R ) ( H ` K ) )
1arithidomlem.7 
|- ( ph -> T e. U )
1arithidomlem.8 
|- ( ph -> ( T .x. Q ) = ( H ` K ) )
1arithidomlem.9 
|- ( ph -> S : ( 0 ..^ ( # ` H ) ) -1-1-onto-> ( 0 ..^ ( # ` H ) ) )
1arithidomlem.10 
|- ( ph -> ( H o. S ) = ( ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ++ <" ( H ` K ) "> ) )
1arithidomlem.11 
|- ( ph -> N e. U )
1arithidomlem.12 
|- ( ph -> ( M gsum ( F ++ <" Q "> ) ) = ( N .x. ( M gsum H ) ) )
Assertion 1arithidomlem1 
|- ( ph -> E. c E. d e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( c : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( d oF .x. ( F o. c ) ) ) )

Proof

Step Hyp Ref Expression
1 1arithidom.u 
 |-  U = ( Unit ` R )
2 1arithidom.i 
 |-  P = ( RPrime ` R )
3 1arithidom.m 
 |-  M = ( mulGrp ` R )
4 1arithidom.t 
 |-  .x. = ( .r ` R )
5 1arithidom.j 
 |-  J = ( 0 ..^ ( # ` F ) )
6 1arithidom.r 
 |-  ( ph -> R e. IDomn )
7 1arithidom.f 
 |-  ( ph -> F e. Word P )
8 1arithidom.g 
 |-  ( ph -> G e. Word P )
9 1arithidom.1 
 |-  ( ph -> ( M gsum F ) = ( M gsum G ) )
10 1arithidomlem.1 
 |-  ( ph -> Q e. P )
11 1arithidomlem.2 
 |-  ( ph -> A. g e. Word P ( E. k e. U ( M gsum F ) = ( k .x. ( M gsum g ) ) -> E. w E. u e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ g = ( u oF .x. ( F o. w ) ) ) ) )
12 1arithidomlem.3 
 |-  ( ph -> H e. Word P )
13 1arithidomlem.4 
 |-  ( ph -> E. k e. U ( M gsum ( F ++ <" Q "> ) ) = ( k .x. ( M gsum H ) ) )
14 1arithidomlem.5 
 |-  ( ph -> K e. ( 0 ..^ ( # ` H ) ) )
15 1arithidomlem.6 
 |-  ( ph -> Q ( ||r ` R ) ( H ` K ) )
16 1arithidomlem.7 
 |-  ( ph -> T e. U )
17 1arithidomlem.8 
 |-  ( ph -> ( T .x. Q ) = ( H ` K ) )
18 1arithidomlem.9 
 |-  ( ph -> S : ( 0 ..^ ( # ` H ) ) -1-1-onto-> ( 0 ..^ ( # ` H ) ) )
19 1arithidomlem.10 
 |-  ( ph -> ( H o. S ) = ( ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ++ <" ( H ` K ) "> ) )
20 1arithidomlem.11 
 |-  ( ph -> N e. U )
21 1arithidomlem.12 
 |-  ( ph -> ( M gsum ( F ++ <" Q "> ) ) = ( N .x. ( M gsum H ) ) )
22 oveq1 
 |-  ( l = ( N .x. T ) -> ( l .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) = ( ( N .x. T ) .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) )
23 22 eqeq2d 
 |-  ( l = ( N .x. T ) -> ( ( M gsum F ) = ( l .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) <-> ( M gsum F ) = ( ( N .x. T ) .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) ) )
24 6 idomringd 
 |-  ( ph -> R e. Ring )
25 1 4 unitmulcl 
 |-  ( ( R e. Ring /\ N e. U /\ T e. U ) -> ( N .x. T ) e. U )
26 24 20 16 25 syl3anc 
 |-  ( ph -> ( N .x. T ) e. U )
27 eqid 
 |-  ( Base ` R ) = ( Base ` R )
28 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
29 3 27 mgpbas 
 |-  ( Base ` R ) = ( Base ` M )
30 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
31 3 30 ringidval 
 |-  ( 1r ` R ) = ( 0g ` M )
32 id 
 |-  ( R e. IDomn -> R e. IDomn )
33 32 idomcringd 
 |-  ( R e. IDomn -> R e. CRing )
34 3 crngmgp 
 |-  ( R e. CRing -> M e. CMnd )
35 33 34 syl 
 |-  ( R e. IDomn -> M e. CMnd )
36 6 35 syl 
 |-  ( ph -> M e. CMnd )
37 ovexd 
 |-  ( ph -> ( 0 ..^ ( # ` F ) ) e. _V )
38 eqidd 
 |-  ( ph -> ( # ` F ) = ( # ` F ) )
39 simpl 
 |-  ( ( R e. IDomn /\ q e. P ) -> R e. IDomn )
40 simpr 
 |-  ( ( R e. IDomn /\ q e. P ) -> q e. P )
41 27 2 39 40 rprmcl 
 |-  ( ( R e. IDomn /\ q e. P ) -> q e. ( Base ` R ) )
42 41 ex 
 |-  ( R e. IDomn -> ( q e. P -> q e. ( Base ` R ) ) )
43 42 ssrdv 
 |-  ( R e. IDomn -> P C_ ( Base ` R ) )
44 sswrd 
 |-  ( P C_ ( Base ` R ) -> Word P C_ Word ( Base ` R ) )
45 6 43 44 3syl 
 |-  ( ph -> Word P C_ Word ( Base ` R ) )
46 45 7 sseldd 
 |-  ( ph -> F e. Word ( Base ` R ) )
47 38 46 wrdfd 
 |-  ( ph -> F : ( 0 ..^ ( # ` F ) ) --> ( Base ` R ) )
48 fvexd 
 |-  ( ph -> ( 1r ` R ) e. _V )
49 48 7 wrdfsupp 
 |-  ( ph -> F finSupp ( 1r ` R ) )
50 29 31 36 37 47 49 gsumcl 
 |-  ( ph -> ( M gsum F ) e. ( Base ` R ) )
51 27 1 unitcl 
 |-  ( N e. U -> N e. ( Base ` R ) )
52 20 51 syl 
 |-  ( ph -> N e. ( Base ` R ) )
53 27 1 unitcl 
 |-  ( T e. U -> T e. ( Base ` R ) )
54 16 53 syl 
 |-  ( ph -> T e. ( Base ` R ) )
55 27 4 24 52 54 ringcld 
 |-  ( ph -> ( N .x. T ) e. ( Base ` R ) )
56 ovexd 
 |-  ( ph -> ( 0 ..^ ( ( # ` H ) - 1 ) ) e. _V )
57 f1of 
 |-  ( S : ( 0 ..^ ( # ` H ) ) -1-1-onto-> ( 0 ..^ ( # ` H ) ) -> S : ( 0 ..^ ( # ` H ) ) --> ( 0 ..^ ( # ` H ) ) )
58 iswrdi 
 |-  ( S : ( 0 ..^ ( # ` H ) ) --> ( 0 ..^ ( # ` H ) ) -> S e. Word ( 0 ..^ ( # ` H ) ) )
59 18 57 58 3syl 
 |-  ( ph -> S e. Word ( 0 ..^ ( # ` H ) ) )
60 eqidd 
 |-  ( ph -> ( # ` H ) = ( # ` H ) )
61 60 12 wrdfd 
 |-  ( ph -> H : ( 0 ..^ ( # ` H ) ) --> P )
62 wrdco 
 |-  ( ( S e. Word ( 0 ..^ ( # ` H ) ) /\ H : ( 0 ..^ ( # ` H ) ) --> P ) -> ( H o. S ) e. Word P )
63 59 61 62 syl2anc 
 |-  ( ph -> ( H o. S ) e. Word P )
64 elfzo0 
 |-  ( K e. ( 0 ..^ ( # ` H ) ) <-> ( K e. NN0 /\ ( # ` H ) e. NN /\ K < ( # ` H ) ) )
65 64 simp2bi 
 |-  ( K e. ( 0 ..^ ( # ` H ) ) -> ( # ` H ) e. NN )
66 nnm1nn0 
 |-  ( ( # ` H ) e. NN -> ( ( # ` H ) - 1 ) e. NN0 )
67 14 65 66 3syl 
 |-  ( ph -> ( ( # ` H ) - 1 ) e. NN0 )
68 lenco 
 |-  ( ( S e. Word ( 0 ..^ ( # ` H ) ) /\ H : ( 0 ..^ ( # ` H ) ) --> P ) -> ( # ` ( H o. S ) ) = ( # ` S ) )
69 59 61 68 syl2anc 
 |-  ( ph -> ( # ` ( H o. S ) ) = ( # ` S ) )
70 lencl 
 |-  ( S e. Word ( 0 ..^ ( # ` H ) ) -> ( # ` S ) e. NN0 )
71 59 70 syl 
 |-  ( ph -> ( # ` S ) e. NN0 )
72 69 71 eqeltrd 
 |-  ( ph -> ( # ` ( H o. S ) ) e. NN0 )
73 lencl 
 |-  ( H e. Word P -> ( # ` H ) e. NN0 )
74 12 73 syl 
 |-  ( ph -> ( # ` H ) e. NN0 )
75 74 nn0red 
 |-  ( ph -> ( # ` H ) e. RR )
76 75 lem1d 
 |-  ( ph -> ( ( # ` H ) - 1 ) <_ ( # ` H ) )
77 18 57 syl 
 |-  ( ph -> S : ( 0 ..^ ( # ` H ) ) --> ( 0 ..^ ( # ` H ) ) )
78 ffn 
 |-  ( S : ( 0 ..^ ( # ` H ) ) --> ( 0 ..^ ( # ` H ) ) -> S Fn ( 0 ..^ ( # ` H ) ) )
79 hashfn 
 |-  ( S Fn ( 0 ..^ ( # ` H ) ) -> ( # ` S ) = ( # ` ( 0 ..^ ( # ` H ) ) ) )
80 77 78 79 3syl 
 |-  ( ph -> ( # ` S ) = ( # ` ( 0 ..^ ( # ` H ) ) ) )
81 hashfzo0 
 |-  ( ( # ` H ) e. NN0 -> ( # ` ( 0 ..^ ( # ` H ) ) ) = ( # ` H ) )
82 12 73 81 3syl 
 |-  ( ph -> ( # ` ( 0 ..^ ( # ` H ) ) ) = ( # ` H ) )
83 69 80 82 3eqtrrd 
 |-  ( ph -> ( # ` H ) = ( # ` ( H o. S ) ) )
84 76 83 breqtrd 
 |-  ( ph -> ( ( # ` H ) - 1 ) <_ ( # ` ( H o. S ) ) )
85 elfz2nn0 
 |-  ( ( ( # ` H ) - 1 ) e. ( 0 ... ( # ` ( H o. S ) ) ) <-> ( ( ( # ` H ) - 1 ) e. NN0 /\ ( # ` ( H o. S ) ) e. NN0 /\ ( ( # ` H ) - 1 ) <_ ( # ` ( H o. S ) ) ) )
86 67 72 84 85 syl3anbrc 
 |-  ( ph -> ( ( # ` H ) - 1 ) e. ( 0 ... ( # ` ( H o. S ) ) ) )
87 pfxlen 
 |-  ( ( ( H o. S ) e. Word P /\ ( ( # ` H ) - 1 ) e. ( 0 ... ( # ` ( H o. S ) ) ) ) -> ( # ` ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) = ( ( # ` H ) - 1 ) )
88 63 86 87 syl2anc 
 |-  ( ph -> ( # ` ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) = ( ( # ` H ) - 1 ) )
89 88 eqcomd 
 |-  ( ph -> ( ( # ` H ) - 1 ) = ( # ` ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) )
90 pfxcl 
 |-  ( ( H o. S ) e. Word P -> ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) e. Word P )
91 63 90 syl 
 |-  ( ph -> ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) e. Word P )
92 45 91 sseldd 
 |-  ( ph -> ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) e. Word ( Base ` R ) )
93 89 92 wrdfd 
 |-  ( ph -> ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) : ( 0 ..^ ( ( # ` H ) - 1 ) ) --> ( Base ` R ) )
94 32 idomringd 
 |-  ( R e. IDomn -> R e. Ring )
95 1 30 1unit 
 |-  ( R e. Ring -> ( 1r ` R ) e. U )
96 6 94 95 3syl 
 |-  ( ph -> ( 1r ` R ) e. U )
97 96 91 wrdfsupp 
 |-  ( ph -> ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) finSupp ( 1r ` R ) )
98 29 31 36 56 93 97 gsumcl 
 |-  ( ph -> ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) e. ( Base ` R ) )
99 27 4 24 55 98 ringcld 
 |-  ( ph -> ( ( N .x. T ) .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) e. ( Base ` R ) )
100 27 2 6 10 rprmcl 
 |-  ( ph -> Q e. ( Base ` R ) )
101 2 28 6 10 rprmnz 
 |-  ( ph -> Q =/= ( 0g ` R ) )
102 100 101 eldifsnd 
 |-  ( ph -> Q e. ( ( Base ` R ) \ { ( 0g ` R ) } ) )
103 3 ringmgp 
 |-  ( R e. Ring -> M e. Mnd )
104 94 103 syl 
 |-  ( R e. IDomn -> M e. Mnd )
105 6 104 syl 
 |-  ( ph -> M e. Mnd )
106 3 4 mgpplusg 
 |-  .x. = ( +g ` M )
107 29 106 gsumccatsn 
 |-  ( ( M e. Mnd /\ F e. Word ( Base ` R ) /\ Q e. ( Base ` R ) ) -> ( M gsum ( F ++ <" Q "> ) ) = ( ( M gsum F ) .x. Q ) )
108 105 46 100 107 syl3anc 
 |-  ( ph -> ( M gsum ( F ++ <" Q "> ) ) = ( ( M gsum F ) .x. Q ) )
109 ovexd 
 |-  ( ph -> ( 0 ..^ ( # ` H ) ) e. _V )
110 45 12 sseldd 
 |-  ( ph -> H e. Word ( Base ` R ) )
111 60 110 wrdfd 
 |-  ( ph -> H : ( 0 ..^ ( # ` H ) ) --> ( Base ` R ) )
112 48 12 wrdfsupp 
 |-  ( ph -> H finSupp ( 1r ` R ) )
113 29 31 36 109 111 112 18 gsumf1o 
 |-  ( ph -> ( M gsum H ) = ( M gsum ( H o. S ) ) )
114 113 oveq2d 
 |-  ( ph -> ( N .x. ( M gsum H ) ) = ( N .x. ( M gsum ( H o. S ) ) ) )
115 21 108 114 3eqtr3d 
 |-  ( ph -> ( ( M gsum F ) .x. Q ) = ( N .x. ( M gsum ( H o. S ) ) ) )
116 29 106 cmn12 
 |-  ( ( M e. CMnd /\ ( T e. ( Base ` R ) /\ ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) e. ( Base ` R ) /\ Q e. ( Base ` R ) ) ) -> ( T .x. ( ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) .x. Q ) ) = ( ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) .x. ( T .x. Q ) ) )
117 36 54 98 100 116 syl13anc 
 |-  ( ph -> ( T .x. ( ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) .x. Q ) ) = ( ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) .x. ( T .x. Q ) ) )
118 27 4 24 54 98 100 ringassd 
 |-  ( ph -> ( ( T .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) .x. Q ) = ( T .x. ( ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) .x. Q ) ) )
119 111 14 ffvelcdmd 
 |-  ( ph -> ( H ` K ) e. ( Base ` R ) )
120 29 106 gsumccatsn 
 |-  ( ( M e. Mnd /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) e. Word ( Base ` R ) /\ ( H ` K ) e. ( Base ` R ) ) -> ( M gsum ( ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ++ <" ( H ` K ) "> ) ) = ( ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) .x. ( H ` K ) ) )
121 105 92 119 120 syl3anc 
 |-  ( ph -> ( M gsum ( ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ++ <" ( H ` K ) "> ) ) = ( ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) .x. ( H ` K ) ) )
122 19 oveq2d 
 |-  ( ph -> ( M gsum ( H o. S ) ) = ( M gsum ( ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ++ <" ( H ` K ) "> ) ) )
123 17 oveq2d 
 |-  ( ph -> ( ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) .x. ( T .x. Q ) ) = ( ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) .x. ( H ` K ) ) )
124 121 122 123 3eqtr4d 
 |-  ( ph -> ( M gsum ( H o. S ) ) = ( ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) .x. ( T .x. Q ) ) )
125 117 118 124 3eqtr4rd 
 |-  ( ph -> ( M gsum ( H o. S ) ) = ( ( T .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) .x. Q ) )
126 125 oveq2d 
 |-  ( ph -> ( N .x. ( M gsum ( H o. S ) ) ) = ( N .x. ( ( T .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) .x. Q ) ) )
127 27 4 24 52 54 98 ringassd 
 |-  ( ph -> ( ( N .x. T ) .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) = ( N .x. ( T .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) ) )
128 127 oveq1d 
 |-  ( ph -> ( ( ( N .x. T ) .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) .x. Q ) = ( ( N .x. ( T .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) ) .x. Q ) )
129 27 4 24 54 98 ringcld 
 |-  ( ph -> ( T .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) e. ( Base ` R ) )
130 27 4 24 52 129 100 ringassd 
 |-  ( ph -> ( ( N .x. ( T .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) ) .x. Q ) = ( N .x. ( ( T .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) .x. Q ) ) )
131 128 130 eqtr2d 
 |-  ( ph -> ( N .x. ( ( T .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) .x. Q ) ) = ( ( ( N .x. T ) .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) .x. Q ) )
132 115 126 131 3eqtrd 
 |-  ( ph -> ( ( M gsum F ) .x. Q ) = ( ( ( N .x. T ) .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) .x. Q ) )
133 27 28 4 50 99 102 6 132 idomrcan 
 |-  ( ph -> ( M gsum F ) = ( ( N .x. T ) .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) )
134 23 26 133 rspcedvdw 
 |-  ( ph -> E. l e. U ( M gsum F ) = ( l .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) )
135 oveq1 
 |-  ( k = l -> ( k .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) = ( l .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) )
136 135 eqeq2d 
 |-  ( k = l -> ( ( M gsum F ) = ( k .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) <-> ( M gsum F ) = ( l .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) ) )
137 136 cbvrexvw 
 |-  ( E. k e. U ( M gsum F ) = ( k .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) <-> E. l e. U ( M gsum F ) = ( l .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) )
138 134 137 sylibr 
 |-  ( ph -> E. k e. U ( M gsum F ) = ( k .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) )
139 oveq2 
 |-  ( g = ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) -> ( M gsum g ) = ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) )
140 139 oveq2d 
 |-  ( g = ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) -> ( k .x. ( M gsum g ) ) = ( k .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) )
141 140 eqeq2d 
 |-  ( g = ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) -> ( ( M gsum F ) = ( k .x. ( M gsum g ) ) <-> ( M gsum F ) = ( k .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) ) )
142 141 rexbidv 
 |-  ( g = ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) -> ( E. k e. U ( M gsum F ) = ( k .x. ( M gsum g ) ) <-> E. k e. U ( M gsum F ) = ( k .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) ) )
143 eqeq1 
 |-  ( g = ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) -> ( g = ( u oF .x. ( F o. w ) ) <-> ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. w ) ) ) )
144 143 anbi2d 
 |-  ( g = ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) -> ( ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ g = ( u oF .x. ( F o. w ) ) ) <-> ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. w ) ) ) ) )
145 144 rexbidv 
 |-  ( g = ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) -> ( E. u e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ g = ( u oF .x. ( F o. w ) ) ) <-> E. u e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. w ) ) ) ) )
146 145 exbidv 
 |-  ( g = ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) -> ( E. w E. u e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ g = ( u oF .x. ( F o. w ) ) ) <-> E. w E. u e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. w ) ) ) ) )
147 142 146 imbi12d 
 |-  ( g = ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) -> ( ( E. k e. U ( M gsum F ) = ( k .x. ( M gsum g ) ) -> E. w E. u e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ g = ( u oF .x. ( F o. w ) ) ) ) <-> ( E. k e. U ( M gsum F ) = ( k .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) -> E. w E. u e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. w ) ) ) ) ) )
148 147 11 91 rspcdva 
 |-  ( ph -> ( E. k e. U ( M gsum F ) = ( k .x. ( M gsum ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ) ) -> E. w E. u e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. w ) ) ) ) )
149 138 148 mpd 
 |-  ( ph -> E. w E. u e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. w ) ) ) )
150 oveq1 
 |-  ( d = u -> ( d oF .x. ( F o. c ) ) = ( u oF .x. ( F o. c ) ) )
151 150 eqeq2d 
 |-  ( d = u -> ( ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( d oF .x. ( F o. c ) ) <-> ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. c ) ) ) )
152 151 anbi2d 
 |-  ( d = u -> ( ( c : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( d oF .x. ( F o. c ) ) ) <-> ( c : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. c ) ) ) ) )
153 152 cbvrexvw 
 |-  ( E. d e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( c : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( d oF .x. ( F o. c ) ) ) <-> E. u e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( c : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. c ) ) ) )
154 f1oeq1 
 |-  ( c = w -> ( c : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) <-> w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) ) )
155 coeq2 
 |-  ( c = w -> ( F o. c ) = ( F o. w ) )
156 155 oveq2d 
 |-  ( c = w -> ( u oF .x. ( F o. c ) ) = ( u oF .x. ( F o. w ) ) )
157 156 eqeq2d 
 |-  ( c = w -> ( ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. c ) ) <-> ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. w ) ) ) )
158 154 157 anbi12d 
 |-  ( c = w -> ( ( c : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. c ) ) ) <-> ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. w ) ) ) ) )
159 158 rexbidv 
 |-  ( c = w -> ( E. u e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( c : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. c ) ) ) <-> E. u e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. w ) ) ) ) )
160 153 159 bitrid 
 |-  ( c = w -> ( E. d e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( c : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( d oF .x. ( F o. c ) ) ) <-> E. u e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. w ) ) ) ) )
161 160 cbvexvw 
 |-  ( E. c E. d e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( c : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( d oF .x. ( F o. c ) ) ) <-> E. w E. u e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( u oF .x. ( F o. w ) ) ) )
162 149 161 sylibr 
 |-  ( ph -> E. c E. d e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( c : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( d oF .x. ( F o. c ) ) ) )