Without-reservation form of the MML.

data/7.13.01-4.181.1147/algseq_1.miz

@@ -0,0 +1,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;