:: ZMODUL01 semantic presentation begin definitionattr "c1" is :::"strict"::: ; struct :::"Z_ModuleStruct"::: -> ($#l2_algstr_0 :::"addLoopStr"::: ) ; aggr :::"Z_ModuleStruct":::(# :::"carrier":::, :::"ZeroF":::, :::"addF":::, :::"Mult"::: #) -> ($#l1_zmodul01 :::"Z_ModuleStruct"::: ) ; sel :::"Mult"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k4_numbers :::"INT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_zmodul01 :::"Z_ModuleStruct"::: ) ; end; definitionlet "V" be ($#l1_zmodul01 :::"Z_ModuleStruct"::: ) ; mode VECTOR of "V" is ($#m1_subset_1 :::"Element":::) "of" "V"; end; definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_zmodul01 :::"Z_ModuleStruct"::: ) ; let "v" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); let "a" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; func "a" :::"*"::: "v" -> ($#m1_subset_1 :::"Element":::) "of" "V" equals :: ZMODUL01:def 1 (Set (Set "the" ($#u1_zmodul01 :::"Mult"::: ) "of" "V") ($#k1_binop_1 :::"."::: ) "(" "a" "," "v" ")" ); end; :: deftheorem defines :::"*"::: ZMODUL01:def 1 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_zmodul01 :::"Z_ModuleStruct"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_zmodul01 :::"Mult"::: ) "of" (Set (Var "V"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "v")) ")" ))))); registrationlet "ZS" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "O" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "ZS")); let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "ZS")); let "G" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k4_numbers :::"INT"::: ) ) "," (Set (Const "ZS")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "ZS")); cluster (Set ($#g1_zmodul01 :::"Z_ModuleStruct"::: ) "(#" "ZS" "," "O" "," "F" "," "G" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_zmodul01 :::"Z_ModuleStruct"::: ) ; attr "IT" is :::"vector-distributive"::: means :: ZMODUL01:def 2 (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "IT" "holds" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "w")) ")" ))))); attr "IT" is :::"scalar-distributive"::: means :: ZMODUL01:def 3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "IT" "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")) ")" ))))); attr "IT" is :::"scalar-associative"::: means :: ZMODUL01:def 4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "IT" "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")) ")" ))))); attr "IT" is :::"scalar-unital"::: means :: ZMODUL01:def 5 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "IT" "holds" (Bool (Set (Num 1) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))); end; :: deftheorem defines :::"vector-distributive"::: ZMODUL01:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_zmodul01 :::"Z_ModuleStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_zmodul01 :::"vector-distributive"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "w")) ")" ))))) ")" )); :: deftheorem defines :::"scalar-distributive"::: ZMODUL01:def 3 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_zmodul01 :::"Z_ModuleStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_zmodul01 :::"scalar-distributive"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")) ")" ))))) ")" )); :: deftheorem defines :::"scalar-associative"::: ZMODUL01:def 4 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_zmodul01 :::"Z_ModuleStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_zmodul01 :::"scalar-associative"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")) ")" ))))) ")" )); :: deftheorem defines :::"scalar-unital"::: ZMODUL01:def 5 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_zmodul01 :::"Z_ModuleStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_zmodul01 :::"scalar-unital"::: ) ) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Num 1) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))) ")" )); definitionfunc :::"Trivial-Z_ModuleStruct"::: -> ($#v1_zmodul01 :::"strict"::: ) ($#l1_zmodul01 :::"Z_ModuleStruct"::: ) equals :: ZMODUL01:def 6 (Set ($#g1_zmodul01 :::"Z_ModuleStruct"::: ) "(#" (Num 1) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set ($#k4_numbers :::"INT"::: ) ) "," (Num 1) ")" ")" ) "#)" ); end; :: deftheorem defines :::"Trivial-Z_ModuleStruct"::: ZMODUL01:def 6 : (Bool (Set ($#k2_zmodul01 :::"Trivial-Z_ModuleStruct"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_zmodul01 :::"Z_ModuleStruct"::: ) "(#" (Num 1) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set ($#k4_numbers :::"INT"::: ) ) "," (Num 1) ")" ")" ) "#)" )); registration cluster (Set ($#k2_zmodul01 :::"Trivial-Z_ModuleStruct"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) ($#v1_zmodul01 :::"strict"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_zmodul01 :::"strict"::: ) ($#v2_zmodul01 :::"vector-distributive"::: ) ($#v3_zmodul01 :::"scalar-distributive"::: ) ($#v4_zmodul01 :::"scalar-associative"::: ) ($#v5_zmodul01 :::"scalar-unital"::: ) for ($#l1_zmodul01 :::"Z_ModuleStruct"::: ) ; end; definitionmode Z_Module is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_zmodul01 :::"vector-distributive"::: ) ($#v3_zmodul01 :::"scalar-distributive"::: ) ($#v4_zmodul01 :::"scalar-associative"::: ) ($#v5_zmodul01 :::"scalar-unital"::: ) ($#l1_zmodul01 :::"Z_ModuleStruct"::: ) ; end; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_zmodul01 :::"Z_ModuleStruct"::: ) ; attr "IT" is :::"Mult-cancelable"::: means :: ZMODUL01:def 7 (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "IT" "holds" (Bool "(" "not" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT")) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT")) ")" ))); end; :: deftheorem defines :::"Mult-cancelable"::: ZMODUL01:def 7 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_zmodul01 :::"Z_ModuleStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_zmodul01 :::"Mult-cancelable"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "IT")) "holds" (Bool "(" "not" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")))) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")))) ")" ))) ")" )); theorem :: ZMODUL01:1 (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" )) "holds" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))))) ; theorem :: ZMODUL01:2 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")))))) ; theorem :: ZMODUL01:3 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v6_zmodul01 :::"Mult-cancelable"::: ) ) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "v"))))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))) ; theorem :: ZMODUL01:4 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v6_zmodul01 :::"Mult-cancelable"::: ) ) & (Bool (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))) ; theorem :: ZMODUL01:5 (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))))))) ; theorem :: ZMODUL01:6 (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")) ")" )))))) ; theorem :: ZMODUL01:7 (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k1_zmodul01 :::"*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))))))) ; theorem :: ZMODUL01:8 (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "w")) ")" )))))) ; theorem :: ZMODUL01:9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")) ")" )))))) ; theorem :: ZMODUL01:10 (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v6_zmodul01 :::"Mult-cancelable"::: ) ) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "w"))))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "w")))))) ; theorem :: ZMODUL01:11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v6_zmodul01 :::"Mult-cancelable"::: ) ) & (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))))) ; theorem :: ZMODUL01:12 (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G")) ")" )))))) ; theorem :: ZMODUL01:13 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))) ; theorem :: ZMODUL01:14 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "u")) ($#k2_finseq_4 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "u")) ")" )))))) ; theorem :: ZMODUL01:15 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "w")) ($#k3_finseq_4 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "u")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "w")) ")" )))))) ; theorem :: ZMODUL01:16 (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")) ")" )))))) ; theorem :: ZMODUL01:17 (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F")) ")" )))))) ; begin definitionlet "V" be ($#l1_zmodul01 :::"Z_Module":::); let "V1" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); attr "V1" is :::"linearly-closed"::: means :: ZMODUL01:def 8 (Bool "(" (Bool "(" "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) "V1") & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) "V1")) "holds" (Bool (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u"))) ($#r2_hidden :::"in"::: ) "V1") ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) "V1")) "holds" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) "V1")) ")" ) ")" ); end; :: deftheorem defines :::"linearly-closed"::: ZMODUL01:def 8 : (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "V1")) "is" ($#v7_zmodul01 :::"linearly-closed"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "V1"))) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "V1")))) "holds" (Bool (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u"))) ($#r2_hidden :::"in"::: ) (Set (Var "V1"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "V1")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set (Var "V1")))) ")" ) ")" ) ")" ))); theorem :: ZMODUL01:18 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "V1")) "is" ($#v7_zmodul01 :::"linearly-closed"::: ) )) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set (Var "V1"))))) ; theorem :: ZMODUL01:19 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V1")) "is" ($#v7_zmodul01 :::"linearly-closed"::: ) )) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "V1")))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set (Var "V1")))))) ; theorem :: ZMODUL01:20 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V1")) "is" ($#v7_zmodul01 :::"linearly-closed"::: ) )) "holds" (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "V1"))) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "V1")))) "holds" (Bool (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u"))) ($#r2_hidden :::"in"::: ) (Set (Var "V1")))))) ; theorem :: ZMODUL01:21 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set (Var "V1")))) "holds" (Bool (Set (Var "V1")) "is" ($#v7_zmodul01 :::"linearly-closed"::: ) ))) ; theorem :: ZMODUL01:22 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "," (Set (Var "V3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V1")) "is" ($#v7_zmodul01 :::"linearly-closed"::: ) ) & (Bool (Set (Var "V2")) "is" ($#v7_zmodul01 :::"linearly-closed"::: ) ) & (Bool (Set (Var "V3")) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")) ")" ) where v, u "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) : (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "V1"))) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "V2"))) ")" ) "}" )) "holds" (Bool (Set (Var "V3")) "is" ($#v7_zmodul01 :::"linearly-closed"::: ) ))) ; registrationlet "V" be ($#l1_zmodul01 :::"Z_Module":::); cluster (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "V" ")" ) ($#k1_tarski :::"}"::: ) ) -> ($#v7_zmodul01 :::"linearly-closed"::: ) for ($#m1_subset_1 :::"Subset":::) "of" "V"; end; registrationlet "V" be ($#l1_zmodul01 :::"Z_Module":::); cluster ($#v7_zmodul01 :::"linearly-closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V")); end; registrationlet "V" be ($#l1_zmodul01 :::"Z_Module":::); let "V1", "V2" be ($#v7_zmodul01 :::"linearly-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); cluster (Set "V1" ($#k3_xboole_0 :::"/\"::: ) "V2") -> ($#v7_zmodul01 :::"linearly-closed"::: ) for ($#m1_subset_1 :::"Subset":::) "of" "V"; end; definitionlet "V" be ($#l1_zmodul01 :::"Z_Module":::); mode :::"Submodule"::: "of" "V" -> ($#l1_zmodul01 :::"Z_Module":::) means :: ZMODUL01:def 9 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V")) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "V")) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "V") ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it))) & (Bool (Set "the" ($#u1_zmodul01 :::"Mult"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_zmodul01 :::"Mult"::: ) "of" "V") ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k4_numbers :::"INT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#k2_zfmisc_1 :::":]"::: ) ))) ")" ); end; :: deftheorem defines :::"Submodule"::: ZMODUL01:def 9 : (Bool "for" (Set (Var "V")) "," (Set (Var "b2")) "being" ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))))) & (Bool (Set "the" ($#u1_zmodul01 :::"Mult"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_zmodul01 :::"Mult"::: ) "of" (Set (Var "V"))) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k4_numbers :::"INT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#k2_zfmisc_1 :::":]"::: ) ))) ")" ) ")" )); theorem :: ZMODUL01:23 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "W1")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2")))))) ; theorem :: ZMODUL01:24 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W")))) "holds" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "V")))))) ; theorem :: ZMODUL01:25 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "W")) "holds" (Bool (Set (Var "w")) "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")))))) ; theorem :: ZMODUL01:26 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))) ; theorem :: ZMODUL01:27 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "W1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "W2")))))) ; theorem :: ZMODUL01:28 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Var "w2")) ($#r1_hidden :::"="::: ) (Set (Var "u")))) "holds" (Bool (Set (Set (Var "w1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")))))))) ; theorem :: ZMODUL01:29 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))))))))) ; theorem :: ZMODUL01:30 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "w")))))))) ; theorem :: ZMODUL01:31 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "w1")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Var "w2")) ($#r1_hidden :::"="::: ) (Set (Var "u")))) "holds" (Bool (Set (Set (Var "w1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")))))))) ; theorem :: ZMODUL01:32 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool (Set (Var "V")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")))) ; theorem :: ZMODUL01:33 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))))) ; theorem :: ZMODUL01:34 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "W1"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))))) ; theorem :: ZMODUL01:35 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "W"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "V"))))) ; theorem :: ZMODUL01:36 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W")))) "holds" (Bool (Set (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "W")))))) ; theorem :: ZMODUL01:37 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))))))) ; theorem :: ZMODUL01:38 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W")))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "v"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "W")))))) ; theorem :: ZMODUL01:39 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W")))) "holds" (Bool (Set (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "W")))))) ; theorem :: ZMODUL01:40 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k4_numbers :::"INT"::: ) ) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "V1")) ($#r1_hidden :::"="::: ) (Set (Var "D"))) & (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) ($#k1_realset1 :::"||"::: ) (Set (Var "V1")))) & (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_zmodul01 :::"Mult"::: ) "of" (Set (Var "V"))) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k4_numbers :::"INT"::: ) ) "," (Set (Var "V1")) ($#k2_zfmisc_1 :::":]"::: ) )))) "holds" (Bool (Set ($#g1_zmodul01 :::"Z_ModuleStruct"::: ) "(#" (Set (Var "D")) "," (Set (Var "d1")) "," (Set (Var "A")) "," (Set (Var "M")) "#)" ) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V"))))))))) ; theorem :: ZMODUL01:41 (Bool "for" (Set (Var "V")) "," (Set (Var "X")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#l1_zmodul01 :::"Z_Module":::) "st" (Bool (Bool (Set (Var "V")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "X"))) & (Bool (Set (Var "X")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")))) "holds" (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "X")))) ; theorem :: ZMODUL01:42 (Bool "for" (Set (Var "V")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_zmodul01 :::"Z_Module":::) "st" (Bool (Bool (Set (Var "V")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "X"))) & (Bool (Set (Var "X")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "Y")))) "holds" (Bool (Set (Var "V")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "Y")))) ; theorem :: ZMODUL01:43 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W2"))))) "holds" (Bool (Set (Var "W1")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "W2"))))) ; theorem :: ZMODUL01:44 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1")))) "holds" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) ")" )) "holds" (Bool (Set (Var "W1")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "W2"))))) ; registrationlet "V" be ($#l1_zmodul01 :::"Z_Module":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) bbbadV1_ALGSTR_1() bbbadV2_ALGSTR_1() bbbadV3_ALGSTR_1() bbbadV4_ALGSTR_1() ($#v1_zmodul01 :::"strict"::: ) ($#v2_zmodul01 :::"vector-distributive"::: ) ($#v3_zmodul01 :::"scalar-distributive"::: ) ($#v4_zmodul01 :::"scalar-associative"::: ) ($#v5_zmodul01 :::"scalar-unital"::: ) for ($#m1_zmodul01 :::"Submodule"::: ) "of" "V"; end; theorem :: ZMODUL01:45 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W2"))))) "holds" (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2"))))) ; theorem :: ZMODUL01:46 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) "iff" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) ")" ) ")" )) "holds" (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2"))))) ; theorem :: ZMODUL01:47 (Bool "for" (Set (Var "V")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))))) "holds" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Var "V"))))) ; theorem :: ZMODUL01:48 (Bool "for" (Set (Var "V")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) "iff" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "V"))) ")" ) ")" )) "holds" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Var "V"))))) ; theorem :: ZMODUL01:49 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "V1")))) "holds" (Bool (Set (Var "V1")) "is" ($#v7_zmodul01 :::"linearly-closed"::: ) )))) ; theorem :: ZMODUL01:50 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "V1")) "is" ($#v7_zmodul01 :::"linearly-closed"::: ) )) "holds" (Bool "ex" (Set (Var "W")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Set (Var "V1")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))))))) ; definitionlet "V" be ($#l1_zmodul01 :::"Z_Module":::); func :::"(0)."::: "V" -> ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" "V" means :: ZMODUL01:def 10 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "V" ")" ) ($#k6_domain_1 :::"}"::: ) )); end; :: deftheorem defines :::"(0)."::: ZMODUL01:def 10 : (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "b2")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ")" ))); definitionlet "V" be ($#l1_zmodul01 :::"Z_Module":::); func :::"(Omega)."::: "V" -> ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" "V" equals :: ZMODUL01:def 11 (Set ($#g1_zmodul01 :::"Z_ModuleStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" "V") "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "V") "," (Set "the" ($#u1_zmodul01 :::"Mult"::: ) "of" "V") "#)" ); end; :: deftheorem defines :::"(Omega)."::: ZMODUL01:def 11 : (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool (Set ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#g1_zmodul01 :::"Z_ModuleStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_zmodul01 :::"Mult"::: ) "of" (Set (Var "V"))) "#)" ))); theorem :: ZMODUL01:51 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V")))))) ; theorem :: ZMODUL01:52 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "W1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "W2")))))) ; theorem :: ZMODUL01:53 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "W"))) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V"))))) ; theorem :: ZMODUL01:54 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V"))) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "W"))))) ; theorem :: ZMODUL01:55 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "W1"))) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "W2"))))) ; theorem :: ZMODUL01:56 (Bool "for" (Set (Var "V")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool (Set (Var "V")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V"))))) ; definitionlet "V" be ($#l1_zmodul01 :::"Z_Module":::); let "v" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); let "W" be ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Const "V")); func "v" :::"+"::: "W" -> ($#m1_subset_1 :::"Subset":::) "of" "V" equals :: ZMODUL01:def 12 "{" (Set "(" "v" ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")) ")" ) where u "is" ($#m1_subset_1 :::"VECTOR":::) "of" "V" : (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) "W") "}" ; end; :: deftheorem defines :::"+"::: ZMODUL01:def 12 : (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")) ")" ) where u "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) : (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) "}" )))); definitionlet "V" be ($#l1_zmodul01 :::"Z_Module":::); let "W" be ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Const "V")); mode :::"Coset"::: "of" "W" -> ($#m1_subset_1 :::"Subset":::) "of" "V" means :: ZMODUL01:def 13 (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" "st" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) "W"))); end; :: deftheorem defines :::"Coset"::: ZMODUL01:def 13 : (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Var "W"))) "iff" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))))) ")" )))); theorem :: ZMODUL01:57 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W")))) "iff" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) ")" )))) ; theorem :: ZMODUL01:58 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))))))) ; theorem :: ZMODUL01:59 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W")))))) ; theorem :: ZMODUL01:60 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set "(" ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: ZMODUL01:61 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set "(" ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V")))))) ; theorem :: ZMODUL01:62 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W")))) "iff" (Bool (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W")))) ")" )))) ; theorem :: ZMODUL01:63 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) "iff" (Bool (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W")))) ")" )))) ; theorem :: ZMODUL01:64 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W")))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v")) ")" ) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W")))))))) ; theorem :: ZMODUL01:65 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) "iff" (Bool (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")) ")" ) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W")))) ")" )))) ; theorem :: ZMODUL01:66 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) "iff" (Bool (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" ) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W")))) ")" )))) ; theorem :: ZMODUL01:67 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "u")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W")))) "iff" (Bool (Set (Set (Var "u")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W")))) ")" )))) ; theorem :: ZMODUL01:68 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v1")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W")))) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v2")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "v1")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))))))) ; theorem :: ZMODUL01:69 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_zmodul01 :::"*"::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W")))))))) ; theorem :: ZMODUL01:70 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W")))) "iff" (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) ")" )))) ; theorem :: ZMODUL01:71 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W")))) "iff" (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) ")" )))) ; theorem :: ZMODUL01:72 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W")))) "iff" (Bool "ex" (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v1")))) ")" )) ")" )))) ; theorem :: ZMODUL01:73 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W")))) "iff" (Bool "ex" (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v1")))) ")" )) ")" )))) ; theorem :: ZMODUL01:74 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W")))) & (Bool (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W")))) ")" )) "iff" (Bool (Set (Set (Var "v1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v2"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) ")" )))) ; theorem :: ZMODUL01:75 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))))) "holds" (Bool "ex" (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Var "u"))) ")" ))))) ; theorem :: ZMODUL01:76 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W"))))) "holds" (Bool "ex" (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Var "u"))) ")" ))))) ; theorem :: ZMODUL01:77 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W2"))))) "holds" (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))))) ; theorem :: ZMODUL01:78 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W2"))))) "holds" (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))))) ; theorem :: ZMODUL01:79 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "C")) "being" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v7_zmodul01 :::"linearly-closed"::: ) ) "iff" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W")))) ")" )))) ; theorem :: ZMODUL01:80 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "C1")) "being" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Var "W1")) (Bool "for" (Set (Var "C2")) "being" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Var "W2")) "st" (Bool (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Var "C2")))) "holds" (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2"))))))) ; theorem :: ZMODUL01:81 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) "is" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V")))))) ; theorem :: ZMODUL01:82 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V1")) "is" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V"))))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Set (Var "V1")) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: ZMODUL01:83 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) "is" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Var "W"))))) ; theorem :: ZMODUL01:84 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "is" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V"))))) ; theorem :: ZMODUL01:85 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V1")) "is" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V"))))) "holds" (Bool (Set (Var "V1")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V")))))) ; theorem :: ZMODUL01:86 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "C")) "being" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) "iff" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W")))) ")" )))) ; theorem :: ZMODUL01:87 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "C")) "being" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) "iff" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k5_zmodul01 :::"+"::: ) (Set (Var "W")))) ")" ))))) ; theorem :: ZMODUL01:88 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "C")) "being" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool "ex" (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Set (Var "u")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" )))))) ; theorem :: ZMODUL01:89 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "C")) "being" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool "ex" (Set (Var "v1")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" )))))) ; theorem :: ZMODUL01:90 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool "ex" (Set (Var "C")) "being" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Var "W")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) ")" )) "iff" (Bool (Set (Set (Var "v1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v2"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) ")" )))) ; theorem :: ZMODUL01:91 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "u")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "C"))))))) ; begin definitionlet "V" be ($#l1_zmodul01 :::"Z_Module":::); let "W1", "W2" be ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Const "V")); func "W1" :::"+"::: "W2" -> ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" "V" means :: ZMODUL01:def 14 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")) ")" ) where v, u "is" ($#m1_subset_1 :::"VECTOR":::) "of" "V" : (Bool "(" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) "W1") & (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) "W2") ")" ) "}" ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Const "V")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Const "V")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")) ")" ) where v, u "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")) : (Bool "(" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) ")" ) "}" )) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")) ")" ) where v, u "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")) : (Bool "(" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) & (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) ")" ) "}" ))) ; end; :: deftheorem defines :::"+"::: ZMODUL01:def 14 : (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b4")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")) ")" ) where v, u "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) : (Bool "(" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) ")" ) "}" ) ")" )))); definitionlet "V" be ($#l1_zmodul01 :::"Z_Module":::); let "W1", "W2" be ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Const "V")); func "W1" :::"/\"::: "W2" -> ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" "V" means :: ZMODUL01:def 15 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W1") ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W2"))); commutativity (Bool "for" (Set (Var "b1")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Const "V")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Const "V")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W1"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W2")))))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W2"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W1"))))))) ; end; :: deftheorem defines :::"/\"::: ZMODUL01:def 15 : (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b4")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W2")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W1"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W2"))))) ")" )))); theorem :: ZMODUL01:92 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2")))) "iff" (Bool "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "v2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2")))) ")" )) ")" )))) ; theorem :: ZMODUL01:93 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool "(" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) "or" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) ")" )) "holds" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2"))))))) ; theorem :: ZMODUL01:94 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W2")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) ")" ) ")" )))) ; theorem :: ZMODUL01:95 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W"))))) ; theorem :: ZMODUL01:96 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W3")))))) ; theorem :: ZMODUL01:97 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Var "W1")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2")))))) ; theorem :: ZMODUL01:98 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W2")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "W2"))) "iff" (Bool (Set (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W2"))) ")" )))) ; theorem :: ZMODUL01:99 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V")) ")" ) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W"))))) ; theorem :: ZMODUL01:100 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool (Set (Set "(" ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V")) ")" ) ($#k6_zmodul01 :::"+"::: ) (Set "(" ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_zmodul01 :::"Z_ModuleStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_zmodul01 :::"Mult"::: ) "of" (Set (Var "V"))) "#)" ))) ; theorem :: ZMODUL01:101 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V")) ")" ) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#g1_zmodul01 :::"Z_ModuleStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_zmodul01 :::"Mult"::: ) "of" (Set (Var "V"))) "#)" )))) ; theorem :: ZMODUL01:102 (Bool "for" (Set (Var "V")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool (Set (Set "(" ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V")) ")" ) ($#k6_zmodul01 :::"+"::: ) (Set "(" ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "V")))) ; theorem :: ZMODUL01:103 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W"))))) ; theorem :: ZMODUL01:104 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set "(" (Set (Var "W2")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W3")))))) ; theorem :: ZMODUL01:105 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W2"))) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "W1"))))) ; theorem :: ZMODUL01:106 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W1")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "W2"))) "iff" (Bool (Set (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) ")" )))) ; theorem :: ZMODUL01:107 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V")) ")" ) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V")))))) ; theorem :: ZMODUL01:108 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool (Set (Set "(" ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V")) ")" ) ($#k7_zmodul01 :::"/\"::: ) (Set "(" ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V"))))) ; theorem :: ZMODUL01:109 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V")) ")" ) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W"))))) ; theorem :: ZMODUL01:110 (Bool "for" (Set (Var "V")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool (Set (Set "(" ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V")) ")" ) ($#k7_zmodul01 :::"/\"::: ) (Set "(" ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "V")))) ; theorem :: ZMODUL01:111 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W2"))) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2")))))) ; theorem :: ZMODUL01:112 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W2")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W2")))))) ; theorem :: ZMODUL01:113 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W1")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set "(" (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "W1")))))) ; theorem :: ZMODUL01:114 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k6_zmodul01 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W3")) ")" )) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Set (Var "W2")) ($#k7_zmodul01 :::"/\"::: ) (Set "(" (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W3")) ")" ))))) ; theorem :: ZMODUL01:115 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W2")) ($#k7_zmodul01 :::"/\"::: ) (Set "(" (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k6_zmodul01 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W3")) ")" ))))) ; theorem :: ZMODUL01:116 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W2")) "," (Set (Var "W1")) "," (Set (Var "W3")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W2")) ($#k6_zmodul01 :::"+"::: ) (Set "(" (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W3")) ")" )) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Set "(" (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k7_zmodul01 :::"/\"::: ) (Set "(" (Set (Var "W2")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W3")) ")" ))))) ; theorem :: ZMODUL01:117 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W2")) ($#k6_zmodul01 :::"+"::: ) (Set "(" (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k7_zmodul01 :::"/\"::: ) (Set "(" (Set (Var "W2")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W3")) ")" ))))) ; theorem :: ZMODUL01:118 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W3")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "W3")))) "holds" (Bool (Set (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W3")))))) ; theorem :: ZMODUL01:119 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W2"))) "iff" (Bool (Set (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) ")" ))) ; theorem :: ZMODUL01:120 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W3"))) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Set (Var "W2")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W3"))))))) ; theorem :: ZMODUL01:121 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "W2"))) "or" (Bool (Set (Var "W2")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "W1"))) ")" ) "iff" (Bool "ex" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W2")))))) ")" ))) ; definitionlet "V" be ($#l1_zmodul01 :::"Z_Module":::); func :::"Submodules"::: "V" -> ($#m1_hidden :::"set"::: ) means :: ZMODUL01:def 16 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" "V") ")" )); end; :: deftheorem defines :::"Submodules"::: ZMODUL01:def 16 : (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k8_zmodul01 :::"Submodules"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) "is" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V"))) ")" )) ")" ))); registrationlet "V" be ($#l1_zmodul01 :::"Z_Module":::); cluster (Set ($#k8_zmodul01 :::"Submodules"::: ) "V") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: ZMODUL01:122 (Bool "for" (Set (Var "V")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set ($#k8_zmodul01 :::"Submodules"::: ) (Set (Var "V"))))) ; definitionlet "V" be ($#l1_zmodul01 :::"Z_Module":::); let "W1", "W2" be ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Const "V")); pred "V" :::"is_the_direct_sum_of"::: "W1" "," "W2" means :: ZMODUL01:def 17 (Bool "(" (Bool (Set ($#g1_zmodul01 :::"Z_ModuleStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" "V") "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "V") "," (Set "the" ($#u1_zmodul01 :::"Mult"::: ) "of" "V") "#)" ) ($#r1_hidden :::"="::: ) (Set "W1" ($#k6_zmodul01 :::"+"::: ) "W2")) & (Bool (Set "W1" ($#k7_zmodul01 :::"/\"::: ) "W2") ($#r1_hidden :::"="::: ) (Set ($#k3_zmodul01 :::"(0)."::: ) "V")) ")" ); end; :: deftheorem defines :::"is_the_direct_sum_of"::: ZMODUL01:def 17 : (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2"))) "iff" (Bool "(" (Bool (Set ($#g1_zmodul01 :::"Z_ModuleStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_zmodul01 :::"Mult"::: ) "of" (Set (Var "V"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2")))) & (Bool (Set (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V")))) ")" ) ")" ))); definitionlet "V" be ($#l1_zmodul01 :::"Z_Module":::); let "W" be ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Const "V")); attr "W" is :::"with_Linear_Compl"::: means :: ZMODUL01:def 18 (Bool "ex" (Set (Var "C")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" "V" "st" (Bool "V" ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set (Var "C")) "," "W")); end; :: deftheorem defines :::"with_Linear_Compl"::: ZMODUL01:def 18 : (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v8_zmodul01 :::"with_Linear_Compl"::: ) ) "iff" (Bool "ex" (Set (Var "C")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Set (Var "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set (Var "C")) "," (Set (Var "W")))) ")" ))); registrationlet "V" be ($#l1_zmodul01 :::"Z_Module":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) bbbadV1_ALGSTR_1() bbbadV2_ALGSTR_1() bbbadV3_ALGSTR_1() bbbadV4_ALGSTR_1() ($#v2_zmodul01 :::"vector-distributive"::: ) ($#v3_zmodul01 :::"scalar-distributive"::: ) ($#v4_zmodul01 :::"scalar-associative"::: ) ($#v5_zmodul01 :::"scalar-unital"::: ) ($#v8_zmodul01 :::"with_Linear_Compl"::: ) for ($#m1_zmodul01 :::"Submodule"::: ) "of" "V"; end; definitionlet "V" be ($#l1_zmodul01 :::"Z_Module":::); let "W" be ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Const "V")); assume (Bool (Set (Const "W")) "is" ($#v8_zmodul01 :::"with_Linear_Compl"::: ) ) ; mode :::"Linear_Compl"::: "of" "W" -> ($#m1_zmodul01 :::"Submodule"::: ) "of" "V" means :: ZMODUL01:def 19 (Bool "V" ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) it "," "W"); end; :: deftheorem defines :::"Linear_Compl"::: ZMODUL01:def 19 : (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W")) "is" ($#v8_zmodul01 :::"with_Linear_Compl"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m3_zmodul01 :::"Linear_Compl"::: ) "of" (Set (Var "W"))) "iff" (Bool (Set (Var "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set (Var "b3")) "," (Set (Var "W"))) ")" )))); theorem :: ZMODUL01:123 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool (Set (Var "W2")) "is" ($#m3_zmodul01 :::"Linear_Compl"::: ) "of" (Set (Var "W1"))))) ; theorem :: ZMODUL01:124 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#v8_zmodul01 :::"with_Linear_Compl"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m3_zmodul01 :::"Linear_Compl"::: ) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set (Var "L")) "," (Set (Var "W"))) & (Bool (Set (Var "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set (Var "W")) "," (Set (Var "L"))) ")" )))) ; theorem :: ZMODUL01:125 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#v8_zmodul01 :::"with_Linear_Compl"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m3_zmodul01 :::"Linear_Compl"::: ) "of" (Set (Var "W")) "holds" (Bool (Set (Set (Var "W")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#g1_zmodul01 :::"Z_ModuleStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_zmodul01 :::"Mult"::: ) "of" (Set (Var "V"))) "#)" ))))) ; theorem :: ZMODUL01:126 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#v8_zmodul01 :::"with_Linear_Compl"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m3_zmodul01 :::"Linear_Compl"::: ) "of" (Set (Var "W")) "holds" (Bool (Set (Set (Var "W")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V"))))))) ; theorem :: ZMODUL01:127 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool (Set (Var "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set (Var "W2")) "," (Set (Var "W1"))))) ; theorem :: ZMODUL01:128 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#v8_zmodul01 :::"with_Linear_Compl"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m3_zmodul01 :::"Linear_Compl"::: ) "of" (Set (Var "W")) "holds" (Bool (Set (Var "W")) "is" ($#m3_zmodul01 :::"Linear_Compl"::: ) "of" (Set (Var "L")))))) ; theorem :: ZMODUL01:129 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V"))) "," (Set ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V")))) & (Bool (Set (Var "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V"))) "," (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V")))) ")" )) ; theorem :: ZMODUL01:130 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool "(" (Bool (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V"))) "is" ($#m3_zmodul01 :::"Linear_Compl"::: ) "of" (Set ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V")))) & (Bool (Set ($#k4_zmodul01 :::"(Omega)."::: ) (Set (Var "V"))) "is" ($#m3_zmodul01 :::"Linear_Compl"::: ) "of" (Set ($#k3_zmodul01 :::"(0)."::: ) (Set (Var "V")))) ")" )) ; theorem :: ZMODUL01:131 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "C1")) "being" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Var "W1")) (Bool "for" (Set (Var "C2")) "being" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Var "W2")) "st" (Bool (Bool (Set (Var "C1")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C2")))) "holds" (Bool (Set (Set (Var "C1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C2"))) "is" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W2")))))))) ; theorem :: ZMODUL01:132 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2"))) "iff" (Bool "for" (Set (Var "C1")) "being" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Var "W1")) (Bool "for" (Set (Var "C2")) "being" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Var "W2")) (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Set (Set (Var "C1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))))) ")" ))) ; theorem :: ZMODUL01:133 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set ($#g1_zmodul01 :::"Z_ModuleStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_zmodul01 :::"Mult"::: ) "of" (Set (Var "V"))) "#)" )) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "v2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2")))) ")" ))) ")" ))) ; theorem :: ZMODUL01:134 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "u1")) "," (Set (Var "u2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2"))) & (Bool (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u2")))) & (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "u1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "v2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) & (Bool (Set (Var "u2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2")))) "holds" (Bool "(" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "u1"))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Var "u2"))) ")" )))) ; theorem :: ZMODUL01:135 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2")))) & (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "u1")) "," (Set (Var "u2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u2")))) & (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "u1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "v2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) & (Bool (Set (Var "u2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2")))) "holds" (Bool "(" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "u1"))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Var "u2"))) ")" )))) "holds" (Bool (Set (Var "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2"))))) ; definitionlet "V" be ($#l1_zmodul01 :::"Z_Module":::); let "v" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); let "W1", "W2" be ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Const "V")); assume (Bool (Set (Const "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set (Const "W1")) "," (Set (Const "W2"))) ; func "v" :::"|--"::: "(" "W1" "," "W2" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) means :: ZMODUL01:def 20 (Bool "(" (Bool "v" ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" it ($#k3_domain_1 :::"`2"::: ) ")" ))) & (Bool (Set it ($#k2_domain_1 :::"`1"::: ) ) ($#r1_struct_0 :::"in"::: ) "W1") & (Bool (Set it ($#k3_domain_1 :::"`2"::: ) ) ($#r1_struct_0 :::"in"::: ) "W2") ")" ); end; :: deftheorem defines :::"|--"::: ZMODUL01:def 20 : (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k9_zmodul01 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" )) "iff" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b5")) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b5")) ($#k3_domain_1 :::"`2"::: ) ")" ))) & (Bool (Set (Set (Var "b5")) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Set (Var "b5")) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) ")" ) ")" ))))); theorem :: ZMODUL01:136 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k9_zmodul01 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k9_zmodul01 :::"|--"::: ) "(" (Set (Var "W2")) "," (Set (Var "W1")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ))))) ; theorem :: ZMODUL01:137 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_zmodul01 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k9_zmodul01 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k9_zmodul01 :::"|--"::: ) "(" (Set (Var "W2")) "," (Set (Var "W1")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) ))))) ; theorem :: ZMODUL01:138 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#v8_zmodul01 :::"with_Linear_Compl"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m3_zmodul01 :::"Linear_Compl"::: ) "of" (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Set "(" (Set (Var "t")) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k3_domain_1 :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Set (Var "t")) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Set (Var "t")) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "L")))) "holds" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k9_zmodul01 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ))))))) ; theorem :: ZMODUL01:139 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#v8_zmodul01 :::"with_Linear_Compl"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m3_zmodul01 :::"Linear_Compl"::: ) "of" (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "v")) ($#k9_zmodul01 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "v")) ($#k9_zmodul01 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))))))) ; theorem :: ZMODUL01:140 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#v8_zmodul01 :::"with_Linear_Compl"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m3_zmodul01 :::"Linear_Compl"::: ) "of" (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "v")) ($#k9_zmodul01 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Set "(" (Set (Var "v")) ($#k9_zmodul01 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "L"))) ")" ))))) ; theorem :: ZMODUL01:141 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#v8_zmodul01 :::"with_Linear_Compl"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m3_zmodul01 :::"Linear_Compl"::: ) "of" (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k9_zmodul01 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k9_zmodul01 :::"|--"::: ) "(" (Set (Var "L")) "," (Set (Var "W")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) )))))) ; theorem :: ZMODUL01:142 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#v8_zmodul01 :::"with_Linear_Compl"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m3_zmodul01 :::"Linear_Compl"::: ) "of" (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k9_zmodul01 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k9_zmodul01 :::"|--"::: ) "(" (Set (Var "L")) "," (Set (Var "W")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) )))))) ; definitionlet "V" be ($#l1_zmodul01 :::"Z_Module":::); func :::"SubJoin"::: "V" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k8_zmodul01 :::"Submodules"::: ) "V" ")" ) means :: ZMODUL01:def 21 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k8_zmodul01 :::"Submodules"::: ) "V") (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" "V" "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2")))))); end; :: deftheorem defines :::"SubJoin"::: ZMODUL01:def 21 : (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k8_zmodul01 :::"Submodules"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_zmodul01 :::"SubJoin"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k8_zmodul01 :::"Submodules"::: ) (Set (Var "V"))) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k6_zmodul01 :::"+"::: ) (Set (Var "W2")))))) ")" ))); definitionlet "V" be ($#l1_zmodul01 :::"Z_Module":::); func :::"SubMeet"::: "V" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k8_zmodul01 :::"Submodules"::: ) "V" ")" ) means :: ZMODUL01:def 22 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k8_zmodul01 :::"Submodules"::: ) "V") (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" "V" "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W2")))))); end; :: deftheorem defines :::"SubMeet"::: ZMODUL01:def 22 : (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k8_zmodul01 :::"Submodules"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_zmodul01 :::"SubMeet"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k8_zmodul01 :::"Submodules"::: ) (Set (Var "V"))) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W2")))))) ")" ))); theorem :: ZMODUL01:143 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k8_zmodul01 :::"Submodules"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k10_zmodul01 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k11_zmodul01 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#l3_lattices :::"Lattice":::))) ; registrationlet "V" be ($#l1_zmodul01 :::"Z_Module":::); cluster (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k8_zmodul01 :::"Submodules"::: ) "V" ")" ) "," (Set "(" ($#k10_zmodul01 :::"SubJoin"::: ) "V" ")" ) "," (Set "(" ($#k11_zmodul01 :::"SubMeet"::: ) "V" ")" ) "#)" ) -> ($#v10_lattices :::"Lattice-like"::: ) ; end; theorem :: ZMODUL01:144 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k8_zmodul01 :::"Submodules"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k10_zmodul01 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k11_zmodul01 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#v13_lattices :::"lower-bounded"::: ) )) ; theorem :: ZMODUL01:145 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k8_zmodul01 :::"Submodules"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k10_zmodul01 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k11_zmodul01 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#v14_lattices :::"upper-bounded"::: ) )) ; theorem :: ZMODUL01:146 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k8_zmodul01 :::"Submodules"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k10_zmodul01 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k11_zmodul01 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#l3_lattices :::"01_Lattice":::))) ; theorem :: ZMODUL01:147 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k8_zmodul01 :::"Submodules"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k10_zmodul01 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k11_zmodul01 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#v12_lattices :::"modular"::: ) )) ; theorem :: ZMODUL01:148 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W3"))) "is" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Set (Var "W2")) ($#k7_zmodul01 :::"/\"::: ) (Set (Var "W3")))))) ; theorem :: ZMODUL01:149 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#v1_zmodul01 :::"strict"::: ) ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) ")" )) "holds" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set ($#g1_zmodul01 :::"Z_ModuleStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_zmodul01 :::"Mult"::: ) "of" (Set (Var "V"))) "#)" )))) ; theorem :: ZMODUL01:150 (Bool "for" (Set (Var "V")) "being" ($#l1_zmodul01 :::"Z_Module":::) (Bool "for" (Set (Var "W")) "being" ($#m1_zmodul01 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "C")) "being" ($#m2_zmodul01 :::"Coset"::: ) "of" (Set (Var "W")) "st" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))))))) ; begin definitionlet "AG" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; func :::"Int-mult-left"::: "AG" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k4_numbers :::"INT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "AG") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "AG") means :: ZMODUL01:def 23 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "AG" "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) "AG" ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" )) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) "AG" ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "i")) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")) ")" ) ")" )) ")" ")" ))); end; :: deftheorem defines :::"Int-mult-left"::: ZMODUL01:def 23 : (Bool "for" (Set (Var "AG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k4_numbers :::"INT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AG"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AG"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "AG")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "AG")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) (Set (Var "AG")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" )) ")" & "(" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) (Set (Var "AG")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "i")) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")) ")" ) ")" )) ")" ")" ))) ")" ))); theorem :: ZMODUL01:151 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "i1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "i1")))) "holds" (Bool (Set (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i1")) ($#k5_binom :::"*"::: ) (Set (Var "a")))))))) ; theorem :: ZMODUL01:152 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R"))))))) ; theorem :: ZMODUL01:153 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))))) ; theorem :: ZMODUL01:154 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool (Set (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))))) ; theorem :: ZMODUL01:155 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))))) ; theorem :: ZMODUL01:156 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "k")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "a")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" ")" )))))) ; theorem :: ZMODUL01:157 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")) ")" ) ")" ))))) ; theorem :: ZMODUL01:158 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Bool "not" (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )))) "holds" (Bool (Set (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "R")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "a")) ")" ")" )))))) ; theorem :: ZMODUL01:159 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool (Set (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "R")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "a")) ")" ")" )))))) ; theorem :: ZMODUL01:160 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "b")) ")" ")" )))))) ; theorem :: ZMODUL01:161 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool (Set (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "b")) ")" ")" )))))) ; theorem :: ZMODUL01:162 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "i")) ($#k4_nat_1 :::"*"::: ) (Set (Var "j")) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set "(" (Set "(" ($#k3_binom :::"Nat-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "a")) ")" ")" ) ")" ))))) ; theorem :: ZMODUL01:163 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool (Set (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "R")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "i")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "j")) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set "(" (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "R")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "j")) "," (Set (Var "a")) ")" ")" ) ")" ))))) ; theorem :: ZMODUL01:164 (Bool "for" (Set (Var "AG")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set ($#g1_zmodul01 :::"Z_ModuleStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "AG"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "AG"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "AG"))) "," (Set "(" ($#k12_zmodul01 :::"Int-mult-left"::: ) (Set (Var "AG")) ")" ) "#)" ) "is" ($#l1_zmodul01 :::"Z_Module":::))) ;