Metamath Proof Explorer


Theorem 1arithidom

Description: Uniqueness of prime factorizations in an integral domain R . Given two equal products F and G of prime elements, F and G are equal up to a renumbering w and a multiplication by units u . See also 1arith . Chapter VII, Paragraph 3, Section 3, Proposition 2 of BourbakiCAlg2, p. 228. (Contributed by Thierry Arnoux, 27-May-2025)

Ref Expression
Hypotheses 1arithidom.u U = Unit R
1arithidom.i P = RPrime R
1arithidom.m M = mulGrp R
1arithidom.t · ˙ = R
1arithidom.j J = 0 ..^ F
1arithidom.r φ R IDomn
1arithidom.f φ F Word P
1arithidom.g φ G Word P
1arithidom.1 φ M F = M G
Assertion 1arithidom φ w u U J w : J 1-1 onto J G = u · ˙ f F w

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 · ˙ = R
5 1arithidom.j J = 0 ..^ F
6 1arithidom.r φ R IDomn
7 1arithidom.f φ F Word P
8 1arithidom.g φ G Word P
9 1arithidom.1 φ M F = M G
10 6 idomringd φ R Ring
11 eqid 1 R = 1 R
12 1 11 1unit R Ring 1 R U
13 10 12 syl φ 1 R U
14 oveq1 k = 1 R k · ˙ M G = 1 R · ˙ M G
15 14 adantl φ k = 1 R k · ˙ M G = 1 R · ˙ M G
16 eqid Base R = Base R
17 10 adantr φ k = 1 R R Ring
18 3 16 mgpbas Base R = Base M
19 3 11 ringidval 1 R = 0 M
20 id R IDomn R IDomn
21 20 idomcringd R IDomn R CRing
22 3 crngmgp R CRing M CMnd
23 21 22 syl R IDomn M CMnd
24 6 23 syl φ M CMnd
25 ovexd φ 0 ..^ G V
26 eqidd φ G = G
27 26 8 wrdfd φ G : 0 ..^ G P
28 6 adantr φ p P R IDomn
29 simpr φ p P p P
30 16 2 28 29 rprmcl φ p P p Base R
31 30 ex φ p P p Base R
32 31 ssrdv φ P Base R
33 27 32 fssd φ G : 0 ..^ G Base R
34 13 8 wrdfsupp φ finSupp 1 R G
35 18 19 24 25 33 34 gsumcl φ M G Base R
36 35 adantr φ k = 1 R M G Base R
37 16 4 11 17 36 ringlidmd φ k = 1 R 1 R · ˙ M G = M G
38 15 37 eqtrd φ k = 1 R k · ˙ M G = M G
39 38 eqeq2d φ k = 1 R M F = k · ˙ M G M F = M G
40 13 39 9 rspcedvd φ k U M F = k · ˙ M G
41 oveq2 g = G M g = M G
42 41 oveq2d g = G k · ˙ M g = k · ˙ M G
43 42 eqeq2d g = G M F = k · ˙ M g M F = k · ˙ M G
44 43 rexbidv g = G k U M F = k · ˙ M g k U M F = k · ˙ M G
45 eqeq1 g = G g = u · ˙ f F w G = u · ˙ f F w
46 45 anbi2d g = G w : 0 ..^ F 1-1 onto 0 ..^ F g = u · ˙ f F w w : 0 ..^ F 1-1 onto 0 ..^ F G = u · ˙ f F w
47 46 rexbidv g = G u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F g = u · ˙ f F w u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F G = u · ˙ f F w
48 47 exbidv g = G w u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F g = u · ˙ f F w w u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F G = u · ˙ f F w
49 44 48 imbi12d g = G k U M F = k · ˙ M g w u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F g = u · ˙ f F w k U M F = k · ˙ M G w u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F G = u · ˙ f F w
50 oveq2 h = M h = M
51 50 eqeq1d h = M h = k · ˙ M g M = k · ˙ M g
52 51 rexbidv h = k U M h = k · ˙ M g k U M = k · ˙ M g
53 fveq2 h = h =
54 53 oveq2d h = 0 ..^ h = 0 ..^
55 54 oveq2d h = U 0 ..^ h = U 0 ..^
56 eqidd h = w = w
57 56 54 54 f1oeq123d h = w : 0 ..^ h 1-1 onto 0 ..^ h w : 0 ..^ 1-1 onto 0 ..^
58 coeq1 h = h w = w
59 58 oveq2d h = u · ˙ f h w = u · ˙ f w
60 59 eqeq2d h = g = u · ˙ f h w g = u · ˙ f w
61 57 60 anbi12d h = w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w w : 0 ..^ 1-1 onto 0 ..^ g = u · ˙ f w
62 55 61 rexeqbidv h = u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w u U 0 ..^ w : 0 ..^ 1-1 onto 0 ..^ g = u · ˙ f w
63 62 exbidv h = w u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w w u U 0 ..^ w : 0 ..^ 1-1 onto 0 ..^ g = u · ˙ f w
64 52 63 imbi12d h = k U M h = k · ˙ M g w u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w k U M = k · ˙ M g w u U 0 ..^ w : 0 ..^ 1-1 onto 0 ..^ g = u · ˙ f w
65 64 ralbidv h = g Word P k U M h = k · ˙ M g w u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w g Word P k U M = k · ˙ M g w u U 0 ..^ w : 0 ..^ 1-1 onto 0 ..^ g = u · ˙ f w
66 65 imbi2d h = R IDomn g Word P k U M h = k · ˙ M g w u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w R IDomn g Word P k U M = k · ˙ M g w u U 0 ..^ w : 0 ..^ 1-1 onto 0 ..^ g = u · ˙ f w
67 oveq2 h = f M h = M f
68 67 eqeq1d h = f M h = k · ˙ M g M f = k · ˙ M g
69 68 rexbidv h = f k U M h = k · ˙ M g k U M f = k · ˙ M g
70 fveq2 h = f h = f
71 70 oveq2d h = f 0 ..^ h = 0 ..^ f
72 71 oveq2d h = f U 0 ..^ h = U 0 ..^ f
73 eqidd h = f w = w
74 73 71 71 f1oeq123d h = f w : 0 ..^ h 1-1 onto 0 ..^ h w : 0 ..^ f 1-1 onto 0 ..^ f
75 coeq1 h = f h w = f w
76 75 oveq2d h = f u · ˙ f h w = u · ˙ f f w
77 76 eqeq2d h = f g = u · ˙ f h w g = u · ˙ f f w
78 74 77 anbi12d h = f w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w
79 72 78 rexeqbidv h = f u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w
80 79 exbidv h = f w u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w
81 69 80 imbi12d h = f k U M h = k · ˙ M g w u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w
82 81 ralbidv h = f g Word P k U M h = k · ˙ M g w u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w
83 82 imbi2d h = f R IDomn g Word P k U M h = k · ˙ M g w u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w
84 oveq2 h = f ++ ⟨“ p ”⟩ M h = M f ++ ⟨“ p ”⟩
85 84 eqeq1d h = f ++ ⟨“ p ”⟩ M h = k · ˙ M g M f ++ ⟨“ p ”⟩ = k · ˙ M g
86 85 rexbidv h = f ++ ⟨“ p ”⟩ k U M h = k · ˙ M g k U M f ++ ⟨“ p ”⟩ = k · ˙ M g
87 fveq2 h = f ++ ⟨“ p ”⟩ h = f ++ ⟨“ p ”⟩
88 87 oveq2d h = f ++ ⟨“ p ”⟩ 0 ..^ h = 0 ..^ f ++ ⟨“ p ”⟩
89 88 oveq2d h = f ++ ⟨“ p ”⟩ U 0 ..^ h = U 0 ..^ f ++ ⟨“ p ”⟩
90 eqidd h = f ++ ⟨“ p ”⟩ w = w
91 90 88 88 f1oeq123d h = f ++ ⟨“ p ”⟩ w : 0 ..^ h 1-1 onto 0 ..^ h w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩
92 coeq1 h = f ++ ⟨“ p ”⟩ h w = f ++ ⟨“ p ”⟩ w
93 92 oveq2d h = f ++ ⟨“ p ”⟩ u · ˙ f h w = u · ˙ f f ++ ⟨“ p ”⟩ w
94 93 eqeq2d h = f ++ ⟨“ p ”⟩ g = u · ˙ f h w g = u · ˙ f f ++ ⟨“ p ”⟩ w
95 91 94 anbi12d h = f ++ ⟨“ p ”⟩ w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ w
96 89 95 rexeqbidv h = f ++ ⟨“ p ”⟩ u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w u U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ w
97 96 exbidv h = f ++ ⟨“ p ”⟩ w u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w w u U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ w
98 86 97 imbi12d h = f ++ ⟨“ p ”⟩ k U M h = k · ˙ M g w u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w k U M f ++ ⟨“ p ”⟩ = k · ˙ M g w u U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ w
99 98 ralbidv h = f ++ ⟨“ p ”⟩ g Word P k U M h = k · ˙ M g w u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w g Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M g w u U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ w
100 99 imbi2d h = f ++ ⟨“ p ”⟩ R IDomn g Word P k U M h = k · ˙ M g w u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w R IDomn g Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M g w u U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ w
101 oveq2 h = F M h = M F
102 101 eqeq1d h = F M h = k · ˙ M g M F = k · ˙ M g
103 102 rexbidv h = F k U M h = k · ˙ M g k U M F = k · ˙ M g
104 fveq2 h = F h = F
105 104 oveq2d h = F 0 ..^ h = 0 ..^ F
106 105 oveq2d h = F U 0 ..^ h = U 0 ..^ F
107 eqidd h = F w = w
108 107 105 105 f1oeq123d h = F w : 0 ..^ h 1-1 onto 0 ..^ h w : 0 ..^ F 1-1 onto 0 ..^ F
109 coeq1 h = F h w = F w
110 109 oveq2d h = F u · ˙ f h w = u · ˙ f F w
111 110 eqeq2d h = F g = u · ˙ f h w g = u · ˙ f F w
112 108 111 anbi12d h = F w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w w : 0 ..^ F 1-1 onto 0 ..^ F g = u · ˙ f F w
113 106 112 rexeqbidv h = F u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F g = u · ˙ f F w
114 113 exbidv h = F w u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w w u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F g = u · ˙ f F w
115 103 114 imbi12d h = F k U M h = k · ˙ M g w u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w k U M F = k · ˙ M g w u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F g = u · ˙ f F w
116 115 ralbidv h = F g Word P k U M h = k · ˙ M g w u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w g Word P k U M F = k · ˙ M g w u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F g = u · ˙ f F w
117 116 imbi2d h = F R IDomn g Word P k U M h = k · ˙ M g w u U 0 ..^ h w : 0 ..^ h 1-1 onto 0 ..^ h g = u · ˙ f h w R IDomn g Word P k U M F = k · ˙ M g w u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F g = u · ˙ f F w
118 0ex V
119 118 a1i R IDomn g Word P k U M = k · ˙ M g V
120 118 snid
121 1 fvexi U V
122 mapdm0 U V U =
123 121 122 ax-mp U =
124 120 123 eleqtrri U
125 124 a1i R IDomn g Word P k U M = k · ˙ M g U
126 f1o0 : 1-1 onto
127 126 biantrur g = u · ˙ f : 1-1 onto g = u · ˙ f
128 co02 =
129 128 oveq2i u · ˙ f = u · ˙ f
130 of0r u · ˙ f =
131 129 130 eqtri u · ˙ f =
132 131 eqeq2i g = u · ˙ f g =
133 127 132 bitr3i : 1-1 onto g = u · ˙ f g =
134 133 a1i R IDomn g Word P k U M = k · ˙ M g u = : 1-1 onto g = u · ˙ f g =
135 simpl R IDomn g Word P R IDomn
136 135 idomcringd R IDomn g Word P R CRing
137 136 ad2antrr R IDomn g Word P k U M = k · ˙ M g R CRing
138 simplr R IDomn g Word P k U M = k · ˙ M g k U
139 16 1 unitcl k U k Base R
140 138 139 syl R IDomn g Word P k U M = k · ˙ M g k Base R
141 137 22 syl R IDomn g Word P k U M = k · ˙ M g M CMnd
142 ovexd R IDomn g Word P k U M = k · ˙ M g 0 ..^ g V
143 eqidd R IDomn g Word P k U M = k · ˙ M g g = g
144 simpl R IDomn p P R IDomn
145 simpr R IDomn p P p P
146 16 2 144 145 rprmcl R IDomn p P p Base R
147 146 ex R IDomn p P p Base R
148 147 ssrdv R IDomn P Base R
149 sswrd P Base R Word P Word Base R
150 148 149 syl R IDomn Word P Word Base R
151 150 sselda R IDomn g Word P g Word Base R
152 151 ad2antrr R IDomn g Word P k U M = k · ˙ M g g Word Base R
153 143 152 wrdfd R IDomn g Word P k U M = k · ˙ M g g : 0 ..^ g Base R
154 135 idomringd R IDomn g Word P R Ring
155 154 12 syl R IDomn g Word P 1 R U
156 155 ad2antrr R IDomn g Word P k U M = k · ˙ M g 1 R U
157 156 152 wrdfsupp R IDomn g Word P k U M = k · ˙ M g finSupp 1 R g
158 18 19 141 142 153 157 gsumcl R IDomn g Word P k U M = k · ˙ M g M g Base R
159 simpr R IDomn g Word P k U M = k · ˙ M g M = k · ˙ M g
160 19 gsum0 M = 1 R
161 160 156 eqeltrid R IDomn g Word P k U M = k · ˙ M g M U
162 159 161 eqeltrrd R IDomn g Word P k U M = k · ˙ M g k · ˙ M g U
163 1 4 16 unitmulclb R CRing k Base R M g Base R k · ˙ M g U k U M g U
164 163 biimpa R CRing k Base R M g Base R k · ˙ M g U k U M g U
165 137 140 158 162 164 syl31anc R IDomn g Word P k U M = k · ˙ M g k U M g U
166 165 simprd R IDomn g Word P k U M = k · ˙ M g M g U
167 166 r19.29an R IDomn g Word P k U M = k · ˙ M g M g U
168 16 1 3 136 151 unitprodclb R IDomn g Word P M g U ran g U
169 168 adantr R IDomn g Word P k U M = k · ˙ M g M g U ran g U
170 167 169 mpbid R IDomn g Word P k U M = k · ˙ M g ran g U
171 170 adantr R IDomn g Word P k U M = k · ˙ M g g ran g U
172 eqidd R IDomn g Word P g = g
173 simpr R IDomn g Word P g Word P
174 172 173 wrdfd R IDomn g Word P g : 0 ..^ g P
175 174 freld R IDomn g Word P Rel g
176 175 ad2antrr R IDomn g Word P k U M = k · ˙ M g g Rel g
177 simpr R IDomn g Word P k U M = k · ˙ M g g g
178 relrn0 Rel g g = ran g =
179 178 necon3bid Rel g g ran g
180 179 biimpa Rel g g ran g
181 176 177 180 syl2anc R IDomn g Word P k U M = k · ˙ M g g ran g
182 n0 ran g i i ran g
183 181 182 sylib R IDomn g Word P k U M = k · ˙ M g g i i ran g
184 simpr R IDomn g Word P k U M = k · ˙ M g g i ran g i ran g
185 135 ad3antrrr R IDomn g Word P k U M = k · ˙ M g g i ran g R IDomn
186 174 frnd R IDomn g Word P ran g P
187 186 ad2antrr R IDomn g Word P k U M = k · ˙ M g g ran g P
188 187 sselda R IDomn g Word P k U M = k · ˙ M g g i ran g i P
189 2 1 185 188 rprmnunit R IDomn g Word P k U M = k · ˙ M g g i ran g ¬ i U
190 nelss i ran g ¬ i U ¬ ran g U
191 184 189 190 syl2anc R IDomn g Word P k U M = k · ˙ M g g i ran g ¬ ran g U
192 183 191 exlimddv R IDomn g Word P k U M = k · ˙ M g g ¬ ran g U
193 171 192 pm2.65da R IDomn g Word P k U M = k · ˙ M g ¬ g
194 nne ¬ g g =
195 193 194 sylib R IDomn g Word P k U M = k · ˙ M g g =
196 125 134 195 rspcedvd R IDomn g Word P k U M = k · ˙ M g u U : 1-1 onto g = u · ˙ f
197 hash0 = 0
198 197 oveq2i 0 ..^ = 0 ..^ 0
199 fzo0 0 ..^ 0 =
200 198 199 eqtri 0 ..^ =
201 200 oveq2i U 0 ..^ = U
202 201 a1i w = U 0 ..^ = U
203 id w = w =
204 200 a1i w = 0 ..^ =
205 203 204 204 f1oeq123d w = w : 0 ..^ 1-1 onto 0 ..^ : 1-1 onto
206 coeq2 w = w =
207 206 oveq2d w = u · ˙ f w = u · ˙ f
208 207 eqeq2d w = g = u · ˙ f w g = u · ˙ f
209 205 208 anbi12d w = w : 0 ..^ 1-1 onto 0 ..^ g = u · ˙ f w : 1-1 onto g = u · ˙ f
210 202 209 rexeqbidv w = u U 0 ..^ w : 0 ..^ 1-1 onto 0 ..^ g = u · ˙ f w u U : 1-1 onto g = u · ˙ f
211 119 196 210 spcedv R IDomn g Word P k U M = k · ˙ M g w u U 0 ..^ w : 0 ..^ 1-1 onto 0 ..^ g = u · ˙ f w
212 211 ex R IDomn g Word P k U M = k · ˙ M g w u U 0 ..^ w : 0 ..^ 1-1 onto 0 ..^ g = u · ˙ f w
213 212 ralrimiva R IDomn g Word P k U M = k · ˙ M g w u U 0 ..^ w : 0 ..^ 1-1 onto 0 ..^ g = u · ˙ f w
214 eqid 0 ..^ h = 0 ..^ h
215 simp-4r f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j j 0 ..^ h
216 simp-4r f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j h Word P
217 216 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j h Word P
218 eqid h r prefix h 1 = h r prefix h 1
219 214 215 217 218 wrdpmtrlast f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩
220 eqid 0 ..^ f = 0 ..^ f
221 simp-5r f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j R IDomn
222 221 ad6antr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h R IDomn
223 simp-5l f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h f Word P
224 223 ad8antr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h f Word P
225 eqidd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h M f = M f
226 simp-7r f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j p P
227 226 ad6antr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h p P
228 simplr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w
229 228 ad10antr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w
230 222 229 mpd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w
231 217 ad4antr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h Word P
232 simp-9r f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h k U M f ++ ⟨“ p ”⟩ = k · ˙ M h
233 215 ad4antr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h j 0 ..^ h
234 simpr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j p r R h j
235 234 ad6antr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h p r R h j
236 simp-6r f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h t U
237 simp-5r f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h t · ˙ p = h j
238 simp-4r f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h r : 0 ..^ h 1-1 onto 0 ..^ h
239 simpllr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h r = h r prefix h 1 ++ ⟨“ h j ”⟩
240 simplr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h m U
241 simpr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h M f ++ ⟨“ p ”⟩ = m · ˙ M h
242 1 2 3 4 220 222 224 224 225 227 230 231 232 233 235 236 237 238 239 240 241 1arithidomlem1 f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h c d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c
243 ovexd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c c ++ ⟨“ f ”⟩ V
244 vex r V
245 244 cnvex r -1 V
246 245 a1i f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c r -1 V
247 243 246 coexd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c c ++ ⟨“ f ”⟩ r -1 V
248 oveq1 s = d ++ ⟨“ t ”⟩ r -1 s · ˙ f f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ r -1 = d ++ ⟨“ t ”⟩ r -1 · ˙ f f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ r -1
249 248 eqeq2d s = d ++ ⟨“ t ”⟩ r -1 h = s · ˙ f f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ r -1 h = d ++ ⟨“ t ”⟩ r -1 · ˙ f f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ r -1
250 249 anbi2d s = d ++ ⟨“ t ”⟩ r -1 c ++ ⟨“ f ”⟩ r -1 : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ r -1 c ++ ⟨“ f ”⟩ r -1 : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = d ++ ⟨“ t ”⟩ r -1 · ˙ f f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ r -1
251 121 a1i f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c U V
252 ovexd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c 0 ..^ f ++ ⟨“ p ”⟩ V
253 simplr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c d U 0 ..^ f
254 elmapi d U 0 ..^ f d : 0 ..^ f U
255 253 254 syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c d : 0 ..^ f U
256 iswrdi d : 0 ..^ f U d Word U
257 255 256 syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c d Word U
258 ccatws1len d Word U d ++ ⟨“ t ”⟩ = d + 1
259 257 258 syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c d ++ ⟨“ t ”⟩ = d + 1
260 elmapfn d U 0 ..^ f d Fn 0 ..^ f
261 hashfn d Fn 0 ..^ f d = 0 ..^ f
262 253 260 261 3syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c d = 0 ..^ f
263 223 ad10antr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c f Word P
264 lencl f Word P f 0
265 263 264 syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c f 0
266 hashfzo0 f 0 0 ..^ f = f
267 265 266 syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c 0 ..^ f = f
268 262 267 eqtrd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c d = f
269 268 oveq1d f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c d + 1 = f + 1
270 simprr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c h r prefix h 1 = d · ˙ f f c
271 270 dmeqd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c dom h r prefix h 1 = dom d · ˙ f f c
272 f1of r : 0 ..^ h 1-1 onto 0 ..^ h r : 0 ..^ h 0 ..^ h
273 iswrdi r : 0 ..^ h 0 ..^ h r Word 0 ..^ h
274 238 272 273 3syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h r Word 0 ..^ h
275 eqidd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j h = h
276 275 216 wrdfd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j h : 0 ..^ h P
277 276 ad6antr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h : 0 ..^ h P
278 wrdco r Word 0 ..^ h h : 0 ..^ h P h r Word P
279 274 277 278 syl2anc f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h r Word P
280 279 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c h r Word P
281 elfzo0 j 0 ..^ h j 0 h j < h
282 281 simp2bi j 0 ..^ h h
283 nnm1nn0 h h 1 0
284 233 282 283 3syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h 1 0
285 lenco r Word 0 ..^ h h : 0 ..^ h P h r = r
286 274 277 285 syl2anc f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h r = r
287 lencl r Word 0 ..^ h r 0
288 274 287 syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h r 0
289 286 288 eqeltrd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h r 0
290 lencl h Word P h 0
291 231 290 syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h 0
292 291 nn0red f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h
293 292 lem1d f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h 1 h
294 238 272 syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h r : 0 ..^ h 0 ..^ h
295 ffn r : 0 ..^ h 0 ..^ h r Fn 0 ..^ h
296 hashfn r Fn 0 ..^ h r = 0 ..^ h
297 294 295 296 3syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h r = 0 ..^ h
298 hashfzo0 h 0 0 ..^ h = h
299 231 290 298 3syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h 0 ..^ h = h
300 286 297 299 3eqtrrd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h = h r
301 293 300 breqtrd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h 1 h r
302 elfz2nn0 h 1 0 h r h 1 0 h r 0 h 1 h r
303 284 289 301 302 syl3anbrc f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h 1 0 h r
304 303 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c h 1 0 h r
305 pfxfn h r Word P h 1 0 h r h r prefix h 1 Fn 0 ..^ h 1
306 280 304 305 syl2anc f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c h r prefix h 1 Fn 0 ..^ h 1
307 306 fndmd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c dom h r prefix h 1 = 0 ..^ h 1
308 222 idomringd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h R Ring
309 308 ad3antrrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c x U y P R Ring
310 simprl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c x U y P x U
311 16 1 unitcl x U x Base R
312 310 311 syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c x U y P x Base R
313 222 ad3antrrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c x U y P R IDomn
314 simprr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c x U y P y P
315 16 2 313 314 rprmcl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c x U y P y Base R
316 16 4 309 312 315 ringcld f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c x U y P x · ˙ y Base R
317 eqidd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c f = f
318 317 263 wrdfd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c f : 0 ..^ f P
319 simprl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c c : 0 ..^ f 1-1 onto 0 ..^ f
320 f1of c : 0 ..^ f 1-1 onto 0 ..^ f c : 0 ..^ f 0 ..^ f
321 319 320 syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c c : 0 ..^ f 0 ..^ f
322 318 321 fcod f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c f c : 0 ..^ f P
323 ovexd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c 0 ..^ f V
324 inidm 0 ..^ f 0 ..^ f = 0 ..^ f
325 316 255 322 323 323 324 off f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c d · ˙ f f c : 0 ..^ f Base R
326 325 fdmd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c dom d · ˙ f f c = 0 ..^ f
327 271 307 326 3eqtr3d f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c 0 ..^ h 1 = 0 ..^ f
328 284 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c h 1 0
329 328 265 fzo0opth f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c 0 ..^ h 1 = 0 ..^ f h 1 = f
330 327 329 mpbid f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c h 1 = f
331 330 oveq1d f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c h - 1 + 1 = f + 1
332 282 ad10antlr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c h
333 332 nncnd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c h
334 npcan1 h h - 1 + 1 = h
335 333 334 syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c h - 1 + 1 = h
336 331 335 eqtr3d f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c f + 1 = h
337 259 269 336 3eqtrd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c d ++ ⟨“ t ”⟩ = h
338 337 oveq2d f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c 0 ..^ d ++ ⟨“ t ”⟩ = 0 ..^ h
339 eqidd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c d ++ ⟨“ t ”⟩ = d ++ ⟨“ t ”⟩
340 236 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c t U
341 ccatws1cl d Word U t U d ++ ⟨“ t ”⟩ Word U
342 257 340 341 syl2anc f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c d ++ ⟨“ t ”⟩ Word U
343 339 342 wrdfd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c d ++ ⟨“ t ”⟩ : 0 ..^ d ++ ⟨“ t ”⟩ U
344 338 343 feq2dd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c d ++ ⟨“ t ”⟩ : 0 ..^ h U
345 ccatws1len f Word P f ++ ⟨“ p ”⟩ = f + 1
346 263 345 syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c f ++ ⟨“ p ”⟩ = f + 1
347 346 336 eqtrd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c f ++ ⟨“ p ”⟩ = h
348 347 oveq2d f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c 0 ..^ f ++ ⟨“ p ”⟩ = 0 ..^ h
349 348 eqcomd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c 0 ..^ h = 0 ..^ f ++ ⟨“ p ”⟩
350 238 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c r : 0 ..^ h 1-1 onto 0 ..^ h
351 f1ocnv r : 0 ..^ h 1-1 onto 0 ..^ h r -1 : 0 ..^ h 1-1 onto 0 ..^ h
352 f1of r -1 : 0 ..^ h 1-1 onto 0 ..^ h r -1 : 0 ..^ h 0 ..^ h
353 350 351 352 3syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c r -1 : 0 ..^ h 0 ..^ h
354 349 353 feq2dd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c r -1 : 0 ..^ f ++ ⟨“ p ”⟩ 0 ..^ h
355 344 354 fcod f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c d ++ ⟨“ t ”⟩ r -1 : 0 ..^ f ++ ⟨“ p ”⟩ U
356 251 252 355 elmapdd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c d ++ ⟨“ t ”⟩ r -1 U 0 ..^ f ++ ⟨“ p ”⟩
357 222 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c R IDomn
358 eqidd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c M f = M f
359 227 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c p P
360 230 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w
361 231 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c h Word P
362 232 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c k U M f ++ ⟨“ p ”⟩ = k · ˙ M h
363 233 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c j 0 ..^ h
364 235 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c p r R h j
365 237 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c t · ˙ p = h j
366 simp-5r f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c h r = h r prefix h 1 ++ ⟨“ h j ”⟩
367 simp-4r f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c m U
368 simpllr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c M f ++ ⟨“ p ”⟩ = m · ˙ M h
369 1 2 3 4 220 357 263 263 358 359 360 361 362 363 364 340 365 350 366 367 368 253 319 270 1arithidomlem2 f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c c ++ ⟨“ f ”⟩ r -1 : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = d ++ ⟨“ t ”⟩ r -1 · ˙ f f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ r -1
370 250 356 369 rspcedvdw f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c s U 0 ..^ f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ r -1 : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ r -1
371 f1oeq1 v = c ++ ⟨“ f ”⟩ r -1 v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ r -1 : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩
372 coeq2 v = c ++ ⟨“ f ”⟩ r -1 f ++ ⟨“ p ”⟩ v = f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ r -1
373 372 oveq2d v = c ++ ⟨“ f ”⟩ r -1 s · ˙ f f ++ ⟨“ p ”⟩ v = s · ˙ f f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ r -1
374 373 eqeq2d v = c ++ ⟨“ f ”⟩ r -1 h = s · ˙ f f ++ ⟨“ p ”⟩ v h = s · ˙ f f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ r -1
375 371 374 anbi12d v = c ++ ⟨“ f ”⟩ r -1 v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v c ++ ⟨“ f ”⟩ r -1 : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ r -1
376 375 rexbidv v = c ++ ⟨“ f ”⟩ r -1 s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v s U 0 ..^ f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ r -1 : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ c ++ ⟨“ f ”⟩ r -1
377 247 370 376 spcedv f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v
378 377 r19.29an f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h d U 0 ..^ f c : 0 ..^ f 1-1 onto 0 ..^ f h r prefix h 1 = d · ˙ f f c v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v
379 242 378 exlimddv f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v
380 simp-7r f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ k U M f ++ ⟨“ p ”⟩ = k · ˙ M h
381 oveq1 k = m k · ˙ M h = m · ˙ M h
382 381 eqeq2d k = m M f ++ ⟨“ p ”⟩ = k · ˙ M h M f ++ ⟨“ p ”⟩ = m · ˙ M h
383 382 cbvrexvw k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h
384 380 383 sylib f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ m U M f ++ ⟨“ p ”⟩ = m · ˙ M h
385 379 384 r19.29a f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v
386 385 anasss f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j r : 0 ..^ h 1-1 onto 0 ..^ h h r = h r prefix h 1 ++ ⟨“ h j ”⟩ v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v
387 219 386 exlimddv f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v
388 eqid r R = r R
389 simplr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j j 0 ..^ h
390 276 389 ffvelcdmd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j h j P
391 16 2 388 221 226 234 390 4 1 rprmasso3 f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j t U t · ˙ p = h j
392 387 391 r19.29a f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v
393 suppssdm h supp 1 R dom h
394 eqidd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h = h
395 simpllr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h R IDomn
396 395 150 syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h Word P Word Base R
397 396 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h Word P Word Base R
398 simp-4r f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h Word P
399 397 398 sseldd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h Word Base R
400 394 399 wrdfd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h : 0 ..^ h Base R
401 393 400 fssdm f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h h supp 1 R 0 ..^ h
402 21 ad5antlr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h R CRing
403 simp-5r f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h p P
404 403 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h p P
405 ovexd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h 0 ..^ h V
406 fvexd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h 1 R V
407 406 398 wrdfsupp f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h finSupp 1 R h
408 simp-5r f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h R IDomn
409 simplr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h m U
410 16 1 unitcl m U m Base R
411 409 410 syl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h m Base R
412 23 ad5antlr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h M CMnd
413 18 19 412 405 400 407 gsumcl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h M h Base R
414 16 2 395 403 rprmcl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h p Base R
415 414 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h p Base R
416 ovexd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h 0 ..^ f V
417 eqidd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h f = f
418 396 223 sseldd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h f Word Base R
419 418 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h f Word Base R
420 417 419 wrdfd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h f : 0 ..^ f Base R
421 406 419 wrdfsupp f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h finSupp 1 R f
422 18 19 412 416 420 421 gsumcl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h M f Base R
423 16 388 4 dvdsrmul p Base R M f Base R p r R M f · ˙ p
424 415 422 423 syl2anc f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h p r R M f · ˙ p
425 20 idomringd R IDomn R Ring
426 3 ringmgp R Ring M Mnd
427 425 426 syl R IDomn M Mnd
428 427 ad3antlr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h M Mnd
429 3 4 mgpplusg · ˙ = + M
430 18 429 gsumccatsn M Mnd f Word Base R p Base R M f ++ ⟨“ p ”⟩ = M f · ˙ p
431 428 418 414 430 syl3anc f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h M f ++ ⟨“ p ”⟩ = M f · ˙ p
432 431 ad2antrr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h M f ++ ⟨“ p ”⟩ = M f · ˙ p
433 simpr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h M f ++ ⟨“ p ”⟩ = m · ˙ M h
434 432 433 eqtr3d f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h M f · ˙ p = m · ˙ M h
435 424 434 breqtrd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h p r R m · ˙ M h
436 16 2 388 4 408 404 411 413 435 rprmdvds f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h p r R m p r R M h
437 1 2 388 402 404 409 rprmndvdsru f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h ¬ p r R m
438 436 437 orcnd f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h p r R M h
439 16 2 388 11 3 402 404 405 407 400 438 rprmdvdsprod f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h j supp 1 R h p r R h j
440 ssrexv h supp 1 R 0 ..^ h j supp 1 R h p r R h j j 0 ..^ h p r R h j
441 401 439 440 sylc f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h j 0 ..^ h p r R h j
442 383 biimpi k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h
443 442 adantl f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h m U M f ++ ⟨“ p ”⟩ = m · ˙ M h
444 441 443 r19.29a f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h j 0 ..^ h p r R h j
445 392 444 r19.29a f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v
446 445 ex f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v
447 446 ralrimiva f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v
448 f1oeq1 w = v w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩
449 coeq2 w = v f ++ ⟨“ p ”⟩ w = f ++ ⟨“ p ”⟩ v
450 449 oveq2d w = v u · ˙ f f ++ ⟨“ p ”⟩ w = u · ˙ f f ++ ⟨“ p ”⟩ v
451 450 eqeq2d w = v g = u · ˙ f f ++ ⟨“ p ”⟩ w g = u · ˙ f f ++ ⟨“ p ”⟩ v
452 448 451 anbi12d w = v w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ w v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ v
453 452 rexbidv w = v u U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ w u U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ v
454 453 cbvexvw w u U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ w v u U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ v
455 oveq1 u = s u · ˙ f f ++ ⟨“ p ”⟩ v = s · ˙ f f ++ ⟨“ p ”⟩ v
456 455 eqeq2d u = s g = u · ˙ f f ++ ⟨“ p ”⟩ v g = s · ˙ f f ++ ⟨“ p ”⟩ v
457 456 anbi2d u = s v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ v v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = s · ˙ f f ++ ⟨“ p ”⟩ v
458 457 cbvrexvw u U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = s · ˙ f f ++ ⟨“ p ”⟩ v
459 458 exbii v u U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ v v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = s · ˙ f f ++ ⟨“ p ”⟩ v
460 454 459 bitri w u U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ w v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = s · ˙ f f ++ ⟨“ p ”⟩ v
461 460 imbi2i k U M f ++ ⟨“ p ”⟩ = k · ˙ M g w u U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ w k U M f ++ ⟨“ p ”⟩ = k · ˙ M g v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = s · ˙ f f ++ ⟨“ p ”⟩ v
462 461 ralbii g Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M g w u U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ w g Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M g v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = s · ˙ f f ++ ⟨“ p ”⟩ v
463 oveq2 g = h M g = M h
464 463 oveq2d g = h k · ˙ M g = k · ˙ M h
465 464 eqeq2d g = h M f ++ ⟨“ p ”⟩ = k · ˙ M g M f ++ ⟨“ p ”⟩ = k · ˙ M h
466 465 rexbidv g = h k U M f ++ ⟨“ p ”⟩ = k · ˙ M g k U M f ++ ⟨“ p ”⟩ = k · ˙ M h
467 eqeq1 g = h g = s · ˙ f f ++ ⟨“ p ”⟩ v h = s · ˙ f f ++ ⟨“ p ”⟩ v
468 467 anbi2d g = h v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = s · ˙ f f ++ ⟨“ p ”⟩ v v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v
469 468 rexbidv g = h s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = s · ˙ f f ++ ⟨“ p ”⟩ v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v
470 469 exbidv g = h v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = s · ˙ f f ++ ⟨“ p ”⟩ v v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v
471 466 470 imbi12d g = h k U M f ++ ⟨“ p ”⟩ = k · ˙ M g v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = s · ˙ f f ++ ⟨“ p ”⟩ v k U M f ++ ⟨“ p ”⟩ = k · ˙ M h v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v
472 471 cbvralvw g Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M g v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = s · ˙ f f ++ ⟨“ p ”⟩ v h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v
473 462 472 bitri g Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M g w u U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ w h Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M h v s U 0 ..^ f ++ ⟨“ p ”⟩ v : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ h = s · ˙ f f ++ ⟨“ p ”⟩ v
474 447 473 sylibr f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn g Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M g w u U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ w
475 474 exp31 f Word P p P R IDomn g Word P k U M f = k · ˙ M g w u U 0 ..^ f w : 0 ..^ f 1-1 onto 0 ..^ f g = u · ˙ f f w R IDomn g Word P k U M f ++ ⟨“ p ”⟩ = k · ˙ M g w u U 0 ..^ f ++ ⟨“ p ”⟩ w : 0 ..^ f ++ ⟨“ p ”⟩ 1-1 onto 0 ..^ f ++ ⟨“ p ”⟩ g = u · ˙ f f ++ ⟨“ p ”⟩ w
476 66 83 100 117 213 475 wrdind F Word P R IDomn g Word P k U M F = k · ˙ M g w u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F g = u · ˙ f F w
477 7 6 476 sylc φ g Word P k U M F = k · ˙ M g w u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F g = u · ˙ f F w
478 49 477 8 rspcdva φ k U M F = k · ˙ M G w u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F G = u · ˙ f F w
479 40 478 mpd φ w u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F G = u · ˙ f F w
480 5 oveq2i U J = U 0 ..^ F
481 f1oeq23 J = 0 ..^ F J = 0 ..^ F w : J 1-1 onto J w : 0 ..^ F 1-1 onto 0 ..^ F
482 5 5 481 mp2an w : J 1-1 onto J w : 0 ..^ F 1-1 onto 0 ..^ F
483 482 anbi1i w : J 1-1 onto J G = u · ˙ f F w w : 0 ..^ F 1-1 onto 0 ..^ F G = u · ˙ f F w
484 480 483 rexeqbii u U J w : J 1-1 onto J G = u · ˙ f F w u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F G = u · ˙ f F w
485 484 exbii w u U J w : J 1-1 onto J G = u · ˙ f F w w u U 0 ..^ F w : 0 ..^ F 1-1 onto 0 ..^ F G = u · ˙ f F w
486 479 485 sylibr φ w u U J w : J 1-1 onto J G = u · ˙ f F w