/
algseq_1.miz
378 lines (370 loc) · 14.7 KB
/
algseq_1.miz
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
:: Construction of Finite Sequences over Ring and Left-, Right-,
:: and Bi-Modules over a Ring
:: by Micha{\l} Muzalewski and Les{\l}aw W. Szczerba
::
:: Received September 13, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, CARD_1, ARYTM_3, XBOOLE_0, XXREAL_0, TARSKI,
STRUCT_0, FUNCT_1, SUPINF_2, FUNCOP_1, SUBSET_1, FINSEQ_1, PRE_POLY,
RELAT_1, AFINSQ_1, ALGSEQ_1;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, NUMBERS, ORDINAL1, NAT_1,
RELAT_1, FUNCT_1, FUNCOP_1, STRUCT_0, FUNCT_2, XXREAL_0;
constructors FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, RLVECT_1, RELSET_1;
registrations ORDINAL1, RELSET_1, XREAL_0, STRUCT_0;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, CARD_1;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, NAT_1, FUNCOP_1, XREAL_1,
XXREAL_0, CARD_1, ORDINAL1;
schemes FUNCT_2, NAT_1;
begin
theorem
L1: (for R2 being Nat holds (for R5 being Nat holds (R2 in ( Segm R5 ) iff R2 < R5))) by NAT_1:44;
theorem
L2: (( Segm ( 0 ) ) = ( {} ) & ( Segm 1 ) = { ( 0 ) } & ( Segm 2 ) = { ( 0 ) , 1 }) by CARD_1:49 , CARD_1:50;
theorem
L3: (for R5 being Nat holds R5 in ( Segm ( R5 + 1 ) )) by NAT_1:45;
theorem
L4: (for R4 being Nat holds (for R5 being Nat holds (R5 <= R4 iff ( Segm R5 ) c= ( Segm R4 )))) by NAT_1:39;
theorem
L5: (for R4 being Nat holds (for R5 being Nat holds (( Segm R5 ) = ( Segm R4 ) implies R5 = R4)));
theorem
L6: (for R2 being Nat holds (for R5 being Nat holds (R2 <= R5 implies (( Segm R2 ) = ( ( Segm R2 ) /\ ( Segm R5 ) ) & ( Segm R2 ) = ( ( Segm R5 ) /\ ( Segm R2 ) ))))) by NAT_1:46;
theorem
L7: (for R2 being Nat holds (for R5 being Nat holds ((( Segm R2 ) = ( ( Segm R2 ) /\ ( Segm R5 ) ) or ( Segm R2 ) = ( ( Segm R5 ) /\ ( Segm R2 ) )) implies R2 <= R5))) by NAT_1:46;
definition
let R7 being non empty ZeroStr;
let C1 being (sequence of R7);
attr C1 is finite-Support
means
:L8: (ex R5 being Nat st (for R1 being Nat holds (R1 >= R5 implies ( C1 . R1 ) = ( 0. R7 ))));
end;
registration
let R7 being non empty ZeroStr;
cluster finite-Support for (sequence of R7);
existence
proof
set D1 = ( ( NAT ) --> ( 0. R7 ) );
reconsider D2 = D1 as (Function of ( NAT ) , (the carrier of R7));
take D2;
take ( 0 );
let R1 being Nat;
assume L10: R1 >= ( 0 );
L11: R1 in ( NAT ) by ORDINAL1:def 12;
thus L12: thesis by L11 , FUNCOP_1:7;
end;
end;
definition
let R7 being non empty ZeroStr;
mode AlgSequence of R7
is finite-Support (sequence of R7);
end;
definition
let R7 being non empty ZeroStr;
let R8 being (AlgSequence of R7);
let C2 being Nat;
pred C2 is_at_least_length_of R8
means
:L15: (for R1 being Nat holds (R1 >= C2 implies ( R8 . R1 ) = ( 0. R7 )))
;end;
L17: (for R7 being non empty ZeroStr holds (for R8 being (AlgSequence of R7) holds (ex R4 being Nat st R4 is_at_least_length_of R8)))
proof
let R7 being non empty ZeroStr;
let R8 being (AlgSequence of R7);
consider R5 being Nat such that L18: (for R1 being Nat holds (R1 >= R5 implies ( R8 . R1 ) = ( 0. R7 ))) by L8;
take R5;
thus L19: thesis by L18 , L15;
end;
L20: (for R2 being Nat holds (for R3 being Nat holds (for R7 being non empty ZeroStr holds (for R8 being (AlgSequence of R7) holds ((R2 is_at_least_length_of R8 & (for R4 being Nat holds (R4 is_at_least_length_of R8 implies R2 <= R4)) & R3 is_at_least_length_of R8 & (for R4 being Nat holds (R4 is_at_least_length_of R8 implies R3 <= R4))) implies R2 = R3)))))
proof
let R2 being Nat;
let R3 being Nat;
let R7 being non empty ZeroStr;
let R8 being (AlgSequence of R7);
assume L21: (R2 is_at_least_length_of R8 & (for R4 being Nat holds (R4 is_at_least_length_of R8 implies R2 <= R4)) & R3 is_at_least_length_of R8 & (for R4 being Nat holds (R4 is_at_least_length_of R8 implies R3 <= R4)));
L22: (R2 <= R3 & R3 <= R2) by L21;
thus L23: thesis by L22 , XXREAL_0:1;
end;
definition
let R7 being non empty ZeroStr;
let R8 being (AlgSequence of R7);
func len R8 -> (Element of ( NAT )) means
:L24: (it is_at_least_length_of R8 & (for R4 being Nat holds (R4 is_at_least_length_of R8 implies it <= R4)));
existence
proof
defpred S1[ Nat ] means $1 is_at_least_length_of R8;
L25: (ex B1 being Nat st S1[ B1 ]) by L17;
L26: (ex R2 being Nat st (S1[ R2 ] & (for R5 being Nat holds (S1[ R5 ] implies R2 <= R5)))) from NAT_1:sch 5(L25);
consider R2 being Nat such that L27: (R2 is_at_least_length_of R8 & (for R5 being Nat holds (R5 is_at_least_length_of R8 implies R2 <= R5))) by L26;
take R2;
thus L28: thesis by L27 , ORDINAL1:def 12;
end;
uniqueness by L20;
end;
theorem
L30: (for R1 being Nat holds (for R7 being non empty ZeroStr holds (for R8 being (AlgSequence of R7) holds (R1 >= ( len R8 ) implies ( R8 . R1 ) = ( 0. R7 )))))
proof
let R1 being Nat;
let R7 being non empty ZeroStr;
let R8 being (AlgSequence of R7);
assume L31: R1 >= ( len R8 );
L32: ( len R8 ) is_at_least_length_of R8 by L24;
thus L33: thesis by L32 , L31 , L15;
end;
theorem
L34: (for R2 being Nat holds (for R7 being non empty ZeroStr holds (for R8 being (AlgSequence of R7) holds ((for R1 being Nat holds (R1 < R2 implies ( R8 . R1 ) <> ( 0. R7 ))) implies ( len R8 ) >= R2))))
proof
let R2 being Nat;
let R7 being non empty ZeroStr;
let R8 being (AlgSequence of R7);
assume L35: (for R1 being Nat holds (R1 < R2 implies ( R8 . R1 ) <> ( 0. R7 )));
L36: (for R1 being Nat holds (R1 < R2 implies ( len R8 ) > R1))
proof
let R1 being Nat;
assume L37: R1 < R2;
L38: ( R8 . R1 ) <> ( 0. R7 ) by L37 , L35;
thus L39: thesis by L38 , L30;
end;
thus L40: thesis by L36;
end;
theorem
L41: (for R2 being Nat holds (for R7 being non empty ZeroStr holds (for R8 being (AlgSequence of R7) holds (( len R8 ) = ( R2 + 1 ) implies ( R8 . R2 ) <> ( 0. R7 )))))
proof
let R2 being Nat;
let R7 being non empty ZeroStr;
let R8 being (AlgSequence of R7);
assume L42: ( len R8 ) = ( R2 + 1 );
L43: R2 < ( len R8 ) by L42 , XREAL_1:29;
L44: (not R2 is_at_least_length_of R8) by L43 , L24;
consider R1 being Nat such that L45: R1 >= R2 and L46: ( R8 . R1 ) <> ( 0. R7 ) by L44 , L15;
L47: R1 < ( R2 + 1 ) by L42 , L46 , L30;
L48: R1 <= R2 by L47 , NAT_1:13;
thus L49: thesis by L48 , L45 , L46 , XXREAL_0:1;
end;
definition
let R7 being non empty ZeroStr;
let R8 being (AlgSequence of R7);
func support R8 -> (Subset of ( NAT )) equals
( Segm ( len R8 ) );
coherence;
end;
theorem
L51: (for R2 being Nat holds (for R7 being non empty ZeroStr holds (for R8 being (AlgSequence of R7) holds (R2 = ( len R8 ) iff ( Segm R2 ) = ( support R8 )))));
scheme AlgSeqLambdaF { F1() -> non empty ZeroStr , F2() -> Nat , F3(Nat) -> (Element of F1()) } : (ex B2 being (AlgSequence of F1()) st (( len B2 ) <= F2() & (for R2 being Nat holds (R2 < F2() implies ( B2 . R2 ) = F3(R2)))))
proof
defpred S2[ Nat , (Element of F1()) ] means (($1 < F2() & $2 = F3($1)) or ($1 >= F2() & $2 = ( 0. F1() )));
L52: (for B3 being (Element of ( NAT )) holds (ex B4 being (Element of F1()) st S2[ B3 , B4 ]))
proof
let C3 being (Element of ( NAT ));
L53: (C3 < F2() implies (C3 < F2() & F3(C3) = F3(C3)));
thus L54: thesis by L53;
end;
L55: (ex B5 being (Function of ( NAT ) , (the carrier of F1())) st (for B6 being (Element of ( NAT )) holds S2[ B6 , ( B5 . B6 ) ])) from FUNCT_2:sch 3(L52);
consider C4 being (Function of ( NAT ) , (the carrier of F1())) such that L56: (for B7 being (Element of ( NAT )) holds ((B7 < F2() & ( C4 . B7 ) = F3(B7)) or (B7 >= F2() & ( C4 . B7 ) = ( 0. F1() )))) by L55;
L57: (ex R5 being Nat st (for R1 being Nat holds (R1 >= R5 implies ( C4 . R1 ) = ( 0. F1() ))))
proof
reconsider D3 = F2() as (Element of ( NAT )) by ORDINAL1:def 12;
take D3;
let R1 being Nat;
L58: R1 in ( NAT ) by ORDINAL1:def 12;
thus L59: thesis by L58 , L56;
end;
reconsider D4 = C4 as (AlgSequence of F1()) by L57 , L8;
take D4;
L60:
now
let R1 being Nat;
assume L61: R1 >= F2();
L62: R1 in ( NAT ) by ORDINAL1:def 12;
thus L63: ( D4 . R1 ) = ( 0. F1() ) by L62 , L56 , L61;
end;
L64: F2() is_at_least_length_of D4 by L60 , L15;
thus L65: ( len D4 ) <= F2() by L64 , L24;
let R2 being Nat;
L66: R2 in ( NAT ) by ORDINAL1:def 12;
thus L67: thesis by L66 , L56;
end;
theorem
L68: (for R7 being non empty ZeroStr holds (for R8 being (AlgSequence of R7) holds (for R9 being (AlgSequence of R7) holds ((( len R8 ) = ( len R9 ) & (for R2 being Nat holds (R2 < ( len R8 ) implies ( R8 . R2 ) = ( R9 . R2 )))) implies R8 = R9))))
proof
let R7 being non empty ZeroStr;
let R8 being (AlgSequence of R7);
let R9 being (AlgSequence of R7);
assume that
L69: ( len R8 ) = ( len R9 )
and
L70: (for R2 being Nat holds (R2 < ( len R8 ) implies ( R8 . R2 ) = ( R9 . R2 )));
L71: (for R6 being set holds (R6 in ( NAT ) implies ( R8 . R6 ) = ( R9 . R6 )))
proof
let R6 being set;
assume L72: R6 in ( NAT );
reconsider D5 = R6 as (Element of ( NAT )) by L72;
L73: (D5 >= ( len R8 ) implies ( R8 . D5 ) = ( R9 . D5 ))
proof
assume L74: D5 >= ( len R8 );
L75: ( R8 . D5 ) = ( 0. R7 ) by L74 , L30;
thus L76: thesis by L75 , L69 , L74 , L30;
end;
thus L77: thesis by L73 , L70;
end;
L78: (( dom R8 ) = ( NAT ) & ( dom R9 ) = ( NAT )) by FUNCT_2:def 1;
thus L79: thesis by L78 , L71 , FUNCT_1:2;
end;
theorem
L80: (for R7 being non empty ZeroStr holds ((the carrier of R7) <> { ( 0. R7 ) } implies (for R2 being Nat holds (ex B8 being (AlgSequence of R7) st ( len B8 ) = R2))))
proof
let R7 being non empty ZeroStr;
set D6 = (the carrier of R7);
assume L81: D6 <> { ( 0. R7 ) };
consider C5 being set such that L82: C5 in D6 and L83: C5 <> ( 0. R7 ) by L81 , ZFMISC_1:35;
reconsider D7 = C5 as (Element of R7) by L82;
let R2 being Nat;
deffunc H1(Nat) = D7;
consider C6 being (AlgSequence of R7) such that L84: (( len C6 ) <= R2 & (for R1 being Nat holds (R1 < R2 implies ( C6 . R1 ) = H1(R1)))) from AlgSeqLambdaF;
L85: (for R1 being Nat holds (R1 < R2 implies ( C6 . R1 ) <> ( 0. R7 ))) by L83 , L84;
L86: ( len C6 ) >= R2 by L85 , L34;
L87: ( len C6 ) = R2 by L86 , L84 , XXREAL_0:1;
thus L88: thesis by L87;
end;
definition
let R7 being non empty ZeroStr;
let R10 being (Element of R7);
func <%R10 %> -> (AlgSequence of R7) means
:L89: (( len it ) <= 1 & ( it . ( 0 ) ) = R10);
existence
proof
deffunc H2(Nat) = R10;
consider R8 being (AlgSequence of R7) such that L90: (( len R8 ) <= 1 & (for R2 being Nat holds (R2 < 1 implies ( R8 . R2 ) = H2(R2)))) from AlgSeqLambdaF;
take R8;
thus L91: thesis by L90;
end;
uniqueness
proof
let R8 being (AlgSequence of R7);
let R9 being (AlgSequence of R7);
assume that
L92: ( len R8 ) <= 1
and
L93: ( R8 . ( 0 ) ) = R10
and
L94: ( len R9 ) <= 1
and
L95: ( R9 . ( 0 ) ) = R10;
L96: 1 = ( ( 0 ) + 1 );
L97:
now
assume L98: R10 = ( 0. R7 );
L99: ( len R8 ) < 1 by L98 , L92 , L93 , L96 , L41 , XXREAL_0:1;
L100: ( len R8 ) = ( 0 ) by L99 , NAT_1:14;
L101: ( len R9 ) < 1 by L94 , L95 , L96 , L98 , L41 , XXREAL_0:1;
thus L102: ( len R8 ) = ( len R9 ) by L101 , L100 , NAT_1:14;
end;
L103: (for R2 being Nat holds (R2 < ( len R8 ) implies ( R8 . R2 ) = ( R9 . R2 )))
proof
let R2 being Nat;
assume L104: R2 < ( len R8 );
L105: R2 < 1 by L104 , L92 , XXREAL_0:2;
L106: R2 = ( 0 ) by L105 , NAT_1:14;
thus L107: thesis by L106 , L93 , L95;
end;
L108:
now
assume L109: R10 <> ( 0. R7 );
L110: ( len R8 ) = 1 by L109 , L92 , L93 , L96 , L30 , NAT_1:8;
thus L111: ( len R8 ) = ( len R9 ) by L110 , L94 , L95 , L96 , L109 , L30 , NAT_1:8;
end;
thus L112: thesis by L108 , L97 , L103 , L68;
end;
end;
L114: (for R7 being non empty ZeroStr holds (for R8 being (AlgSequence of R7) holds (R8 = <% ( 0. R7 ) %> implies ( len R8 ) = ( 0 ))))
proof
let R7 being non empty ZeroStr;
let R8 being (AlgSequence of R7);
assume L115: R8 = <% ( 0. R7 ) %>;
L116: (( R8 . ( 0 ) ) = ( 0. R7 ) & ( len R8 ) <= 1) by L115 , L89;
L117: ( ( 0 ) + 1 ) = 1;
L118: ( len R8 ) < 1 by L117 , L116 , L41 , XXREAL_0:1;
thus L119: thesis by L118 , NAT_1:14;
end;
theorem
L120: (for R7 being non empty ZeroStr holds (for R8 being (AlgSequence of R7) holds (R8 = <% ( 0. R7 ) %> iff ( len R8 ) = ( 0 ))))
proof
let R7 being non empty ZeroStr;
let R8 being (AlgSequence of R7);
thus L121: (R8 = <% ( 0. R7 ) %> implies ( len R8 ) = ( 0 )) by L114;
thus L122: (( len R8 ) = ( 0 ) implies R8 = <% ( 0. R7 ) %>)
proof
assume L123: ( len R8 ) = ( 0 );
L124: (( len R8 ) = ( len <% ( 0. R7 ) %> ) & (for R2 being Nat holds (R2 < ( len R8 ) implies ( R8 . R2 ) = ( <% ( 0. R7 ) %> . R2 )))) by L123 , L114 , NAT_1:2;
thus L125: thesis by L124 , L68;
end;
end;
theorem
L123: (for R7 being non empty ZeroStr holds (for R8 being (AlgSequence of R7) holds (R8 = <% ( 0. R7 ) %> iff ( support R8 ) = ( {} )))) by L120;
theorem
L124: (for R1 being Nat holds (for R7 being non empty ZeroStr holds ( <% ( 0. R7 ) %> . R1 ) = ( 0. R7 )))
proof
let R1 being Nat;
let R7 being non empty ZeroStr;
set D8 = <% ( 0. R7 ) %>;
L125:
now
assume L126: R1 <> ( 0 );
L127: R1 > ( 0 ) by L126 , NAT_1:3;
L128: R1 >= ( len D8 ) by L127 , L120;
thus L129: thesis by L128 , L30;
end;
thus L130: thesis by L125 , L89;
end;
theorem
L131: (for R7 being non empty ZeroStr holds (for R8 being (AlgSequence of R7) holds (R8 = <% ( 0. R7 ) %> iff ( rng R8 ) = { ( 0. R7 ) })))
proof
let R7 being non empty ZeroStr;
let R8 being (AlgSequence of R7);
thus L132: (R8 = <% ( 0. R7 ) %> implies ( rng R8 ) = { ( 0. R7 ) })
proof
assume L133: R8 = <% ( 0. R7 ) %>;
thus L134: ( rng R8 ) c= { ( 0. R7 ) }
proof
let C7 being set;
assume L135: C7 in ( rng R8 );
consider C8 being set such that L136: C8 in ( dom R8 ) and L137: C7 = ( R8 . C8 ) by L135 , FUNCT_1:def 3;
reconsider D9 = C8 as (Element of ( NAT )) by L136 , FUNCT_2:def 1;
L138: ( R8 . D9 ) = ( 0. R7 ) by L133 , L124;
thus L139: thesis by L138 , L137 , TARSKI:def 1;
end;
thus L140: { ( 0. R7 ) } c= ( rng R8 )
proof
let C9 being set;
assume L141: C9 in { ( 0. R7 ) };
L142: C9 = ( 0. R7 ) by L141 , TARSKI:def 1;
L143: ( R8 . ( 0 ) ) = C9 by L142 , L133 , L89;
L144: ( dom R8 ) = ( NAT ) by FUNCT_2:def 1;
thus L145: thesis by L144 , L143 , FUNCT_1:def 3;
end;
end;
thus L141: (( rng R8 ) = { ( 0. R7 ) } implies R8 = <% ( 0. R7 ) %>)
proof
assume L142: ( rng R8 ) = { ( 0. R7 ) };
L143: (for R2 being Nat holds (R2 >= ( 0 ) implies ( R8 . R2 ) = ( 0. R7 )))
proof
let R2 being Nat;
L144: R2 in ( NAT ) by ORDINAL1:def 12;
L145: R2 in ( dom R8 ) by L144 , FUNCT_2:def 1;
L146: ( R8 . R2 ) in ( rng R8 ) by L145 , FUNCT_1:def 3;
thus L147: thesis by L146 , L142 , TARSKI:def 1;
end;
L148: ( 0 ) is_at_least_length_of R8 by L143 , L15;
L149: (for R4 being Nat holds (R4 is_at_least_length_of R8 implies ( 0 ) <= R4)) by NAT_1:2;
L150: ( len R8 ) = ( 0 ) by L149 , L148 , L24;
thus L151: thesis by L150 , L120;
end;
end;