:: LMOD_7 semantic presentation begin scheme :: LMOD_7:sch 1 ElementEq{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X1"))) "iff" (Bool P1[(Set (Var "x"))]) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X2"))) "iff" (Bool P1[(Set (Var "x"))]) ")" ) ")" )) "holds" (Bool (Set (Var "X1")) ($#r1_hidden :::"="::: ) (Set (Var "X2")))) proof end; scheme :: LMOD_7:sch 2 UnOpEq{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" )) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "a")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "a")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2")))) proof end; scheme :: LMOD_7:sch 3 TriOpEq{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" )) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"TriOp":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f1")) ($#k2_multop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f2")) ($#k2_multop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2")))) proof end; scheme :: LMOD_7:sch 4 QuaOpEq{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" )) -> ($#m1_hidden :::"set"::: ) } : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"QuaOp":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f1")) ($#k4_multop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f2")) ($#k4_multop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2")))) proof end; scheme :: LMOD_7:sch 5 Fraenkel1Ex{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set F2 "(" ")" ) "st" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) "{" (Set F3 "(" (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "x"))]) "}" )) proof end; scheme :: LMOD_7:sch 6 Fr0{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool P1[(Set F2 "(" ")" )]) provided (Bool (Set F2 "(" ")" ) ($#r2_hidden :::"in"::: ) "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "a"))]) "}" ) proof end; scheme :: LMOD_7:sch 7 Fr1{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "(" (Bool (Set F3 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) "iff" (Bool P1[(Set F3 "(" ")" )]) ")" ) provided (Bool (Set F1 "(" ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P1[(Set (Var "a"))]) "}" ) proof end; scheme :: LMOD_7:sch 8 Fr2{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool P1[(Set F3 "(" ")" )]) provided (Bool (Set F3 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) and (Bool (Set F1 "(" ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) : (Bool P1[(Set (Var "a"))]) "}" ) proof end; scheme :: LMOD_7:sch 9 Fr3{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "(" (Bool (Set F1 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) "st" (Bool "(" (Bool (Set F1 "(" ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool P1[(Set (Var "a"))]) ")" )) ")" ) provided (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) : (Bool P1[(Set (Var "a"))]) "}" ) proof end; scheme :: LMOD_7:sch 10 Fr4{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "(" (Bool (Set F4 "(" ")" ) ($#r2_hidden :::"in"::: ) (Set F5 "(" (Set F3 "(" ")" ) ")" )) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) "holds" (Bool P1[(Set F4 "(" ")" ) "," (Set (Var "b"))])) ")" ) provided (Bool (Set F5 "(" (Set F3 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "a")) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P2[(Set (Var "a")) "," (Set F3 "(" ")" )]) "}" ) and (Bool "(" (Bool P2[(Set F4 "(" ")" ) "," (Set F3 "(" ")" )]) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set F3 "(" ")" ))) "holds" (Bool P1[(Set F4 "(" ")" ) "," (Set (Var "b"))])) ")" ) proof end; begin theorem :: LMOD_7:1 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "K")) "is" ($#v7_struct_0 :::"trivial"::: ) )) & (Bool (Set (Var "A")) "is" ($#v1_lmod_5 :::"linearly-independent"::: ) )) "holds" (Bool "not" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))))) ; theorem :: LMOD_7:2 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "l")) "being" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))))))) ; theorem :: LMOD_7:3 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "K")) "is" ($#v7_struct_0 :::"trivial"::: ) )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "l")) "being" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) & (Bool (Set ($#k1_mod_3 :::"Lin"::: ) (Set (Var "A"))) "is" ($#v7_struct_0 :::"trivial"::: ) ) ")" )))) ; theorem :: LMOD_7:4 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "st" (Bool (Bool (Bool "not" (Set (Var "V")) "is" ($#v7_struct_0 :::"trivial"::: ) ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_mod_3 :::"base"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: LMOD_7:5 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2"))) "is" ($#v1_lmod_5 :::"linearly-independent"::: ) ) & (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2")))) "holds" (Bool (Set (Set "(" ($#k1_mod_3 :::"Lin"::: ) (Set (Var "A1")) ")" ) ($#k2_vectsp_5 :::"/\"::: ) (Set "(" ($#k1_mod_3 :::"Lin"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V"))))))) ; theorem :: LMOD_7:6 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "," (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_mod_3 :::"base"::: ) ) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")))) & (Bool (Set (Var "A1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A2")))) "holds" (Bool (Set (Var "V")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set ($#k1_mod_3 :::"Lin"::: ) (Set (Var "A1"))) "," (Set ($#k1_mod_3 :::"Lin"::: ) (Set (Var "A2"))))))) ; begin definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); mode :::"SUBMODULE_DOMAIN"::: "of" "V" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: LMOD_7:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Var "x")) "is" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" "V")); end; :: deftheorem defines :::"SUBMODULE_DOMAIN"::: LMOD_7:def 1 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_lmod_7 :::"SUBMODULE_DOMAIN"::: ) "of" (Set (Var "V"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3")))) "holds" (Bool (Set (Var "x")) "is" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")))) ")" )))); definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); :: original: :::"Subspaces"::: redefine func :::"Submodules"::: "V" -> ($#m1_lmod_7 :::"SUBMODULE_DOMAIN"::: ) "of" "V"; end; definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "D" be ($#m1_lmod_7 :::"SUBMODULE_DOMAIN"::: ) "of" (Set (Const "V")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "D" -> ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" "V"; end; registrationlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "D" be ($#m1_lmod_7 :::"SUBMODULE_DOMAIN"::: ) "of" (Set (Const "V")); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v7_vectsp_1 :::"strict"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "D"; end; definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); assume (Bool (Bool "not" (Set (Const "V")) "is" ($#v7_struct_0 :::"trivial"::: ) )) ; mode :::"LINE"::: "of" "V" -> ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" "V" means :: LMOD_7:def 2 (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "V")) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_lmod_6 :::"<:"::: ) (Set (Var "a")) ($#k3_lmod_6 :::":>"::: ) )) ")" )); end; :: deftheorem defines :::"LINE"::: LMOD_7:def 2 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "st" (Bool (Bool (Bool "not" (Set (Var "V")) "is" ($#v7_struct_0 :::"trivial"::: ) ))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m3_lmod_7 :::"LINE"::: ) "of" (Set (Var "V"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_lmod_6 :::"<:"::: ) (Set (Var "a")) ($#k3_lmod_6 :::":>"::: ) )) ")" )) ")" )))); definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); mode :::"LINE_DOMAIN"::: "of" "V" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: LMOD_7:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Var "x")) "is" ($#m3_lmod_7 :::"LINE"::: ) "of" "V")); end; :: deftheorem defines :::"LINE_DOMAIN"::: LMOD_7:def 3 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m4_lmod_7 :::"LINE_DOMAIN"::: ) "of" (Set (Var "V"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3")))) "holds" (Bool (Set (Var "x")) "is" ($#m3_lmod_7 :::"LINE"::: ) "of" (Set (Var "V")))) ")" )))); definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); func :::"lines"::: "V" -> ($#m4_lmod_7 :::"LINE_DOMAIN"::: ) "of" "V" means :: LMOD_7:def 4 (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" ($#m3_lmod_7 :::"LINE"::: ) "of" "V") ")" )); end; :: deftheorem defines :::"lines"::: LMOD_7:def 4 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b3")) "being" ($#m4_lmod_7 :::"LINE_DOMAIN"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_lmod_7 :::"lines"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) "is" ($#m3_lmod_7 :::"LINE"::: ) "of" (Set (Var "V"))) ")" )) ")" )))); definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "D" be ($#m4_lmod_7 :::"LINE_DOMAIN"::: ) "of" (Set (Const "V")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "D" -> ($#m3_lmod_7 :::"LINE"::: ) "of" "V"; end; definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); assume that (Bool (Bool "not" (Set (Const "V")) "is" ($#v7_struct_0 :::"trivial"::: ) )) and (Bool (Set (Const "V")) "is" ($#v2_mod_3 :::"free"::: ) ) ; mode :::"HIPERPLANE"::: "of" "V" -> ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" "V" means :: LMOD_7:def 5 (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "V")) & (Bool "V" ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set ($#k3_lmod_6 :::"<:"::: ) (Set (Var "a")) ($#k3_lmod_6 :::":>"::: ) ) "," it) ")" )); end; :: deftheorem defines :::"HIPERPLANE"::: LMOD_7:def 5 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "st" (Bool (Bool (Bool "not" (Set (Var "V")) "is" ($#v7_struct_0 :::"trivial"::: ) )) & (Bool (Set (Var "V")) "is" ($#v2_mod_3 :::"free"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m6_lmod_7 :::"HIPERPLANE"::: ) "of" (Set (Var "V"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set (Var "V")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set ($#k3_lmod_6 :::"<:"::: ) (Set (Var "a")) ($#k3_lmod_6 :::":>"::: ) ) "," (Set (Var "b3"))) ")" )) ")" )))); definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); mode :::"HIPERPLANE_DOMAIN"::: "of" "V" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: LMOD_7:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Var "x")) "is" ($#m6_lmod_7 :::"HIPERPLANE"::: ) "of" "V")); end; :: deftheorem defines :::"HIPERPLANE_DOMAIN"::: LMOD_7:def 6 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m7_lmod_7 :::"HIPERPLANE_DOMAIN"::: ) "of" (Set (Var "V"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3")))) "holds" (Bool (Set (Var "x")) "is" ($#m6_lmod_7 :::"HIPERPLANE"::: ) "of" (Set (Var "V")))) ")" )))); definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); func :::"hiperplanes"::: "V" -> ($#m7_lmod_7 :::"HIPERPLANE_DOMAIN"::: ) "of" "V" means :: LMOD_7:def 7 (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" ($#m6_lmod_7 :::"HIPERPLANE"::: ) "of" "V") ")" )); end; :: deftheorem defines :::"hiperplanes"::: LMOD_7:def 7 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b3")) "being" ($#m7_lmod_7 :::"HIPERPLANE_DOMAIN"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_lmod_7 :::"hiperplanes"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) "is" ($#m6_lmod_7 :::"HIPERPLANE"::: ) "of" (Set (Var "V"))) ")" )) ")" )))); definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "D" be ($#m7_lmod_7 :::"HIPERPLANE_DOMAIN"::: ) "of" (Set (Const "V")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "D" -> ($#m6_lmod_7 :::"HIPERPLANE"::: ) "of" "V"; end; begin definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "Li" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_vectsp_5 :::"Submodules"::: ) (Set (Const "V"))); func :::"Sum"::: "Li" -> ($#m2_lmod_7 :::"Element"::: ) "of" (Set ($#k1_lmod_7 :::"Submodules"::: ) "V") equals :: LMOD_7:def 8 (Set (Set "(" ($#k5_vectsp_5 :::"SubJoin"::: ) "V" ")" ) ($#k1_finsop_1 :::"$$"::: ) "Li"); func :::"/\"::: "Li" -> ($#m2_lmod_7 :::"Element"::: ) "of" (Set ($#k1_lmod_7 :::"Submodules"::: ) "V") equals :: LMOD_7:def 9 (Set (Set "(" ($#k6_vectsp_5 :::"SubMeet"::: ) "V" ")" ) ($#k1_finsop_1 :::"$$"::: ) "Li"); end; :: deftheorem defines :::"Sum"::: LMOD_7:def 8 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "Li")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_vectsp_5 :::"Submodules"::: ) (Set (Var "V"))) "holds" (Bool (Set ($#k4_lmod_7 :::"Sum"::: ) (Set (Var "Li"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_vectsp_5 :::"SubJoin"::: ) (Set (Var "V")) ")" ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "Li"))))))); :: deftheorem defines :::"/\"::: LMOD_7:def 9 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "Li")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_vectsp_5 :::"Submodules"::: ) (Set (Var "V"))) "holds" (Bool (Set ($#k5_lmod_7 :::"/\"::: ) (Set (Var "Li"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_vectsp_5 :::"SubMeet"::: ) (Set (Var "V")) ")" ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "Li"))))))); theorem :: LMOD_7:7 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set ($#k5_vectsp_5 :::"SubJoin"::: ) (Set (Var "V"))) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set ($#k5_vectsp_5 :::"SubJoin"::: ) (Set (Var "V"))) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set ($#k5_vectsp_5 :::"SubJoin"::: ) (Set (Var "V"))) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "(" ($#k5_vectsp_5 :::"SubJoin"::: ) (Set (Var "V")) ")" ))) ")" ))) ; theorem :: LMOD_7:8 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set ($#k6_vectsp_5 :::"SubMeet"::: ) (Set (Var "V"))) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set ($#k6_vectsp_5 :::"SubMeet"::: ) (Set (Var "V"))) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set ($#k6_vectsp_5 :::"SubMeet"::: ) (Set (Var "V"))) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "(" ($#k6_vectsp_5 :::"SubMeet"::: ) (Set (Var "V")) ")" ))) ")" ))) ; begin definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "A1", "A2" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); func "A1" :::"+"::: "A2" -> ($#m1_subset_1 :::"Subset":::) "of" "V" means :: LMOD_7:def 10 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "st" (Bool "(" (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) "A1") & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) "A2") & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a2")))) ")" )) ")" )); end; :: deftheorem defines :::"+"::: LMOD_7:def 10 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "b5")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k6_lmod_7 :::"+"::: ) (Set (Var "A2")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool "ex" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "a1")) ($#r2_hidden :::"in"::: ) (Set (Var "A1"))) & (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Var "A2"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a2")))) ")" )) ")" )) ")" )))); begin definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); assume (Bool (Set (Const "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; mode :::"Vector"::: "of" "A" -> ($#m1_subset_1 :::"Vector":::) "of" "V" means :: LMOD_7:def 11 (Bool it "is" ($#m1_subset_1 :::"Element"::: ) "of" "A"); end; :: deftheorem defines :::"Vector"::: LMOD_7:def 11 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m9_lmod_7 :::"Vector"::: ) "of" (Set (Var "A"))) "iff" (Bool (Set (Var "b4")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A"))) ")" ))))); theorem :: LMOD_7:9 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A1")) ($#r1_tarski :::"c="::: ) (Set (Var "A2")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) "is" ($#m9_lmod_7 :::"Vector"::: ) "of" (Set (Var "A1")))) "holds" (Bool (Set (Var "x")) "is" ($#m9_lmod_7 :::"Vector"::: ) "of" (Set (Var "A2"))))))) ; theorem :: LMOD_7:10 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a2")) "," (Set (Var "a1")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "a2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a1")) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W")))) "iff" (Bool (Set (Set (Var "a1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a2"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) ")" ))))) ; theorem :: LMOD_7:11 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "a1")) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W")))) "iff" (Bool (Set (Set (Var "a1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a2"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) ")" ))))) ; definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); func "V" :::".."::: "W" -> ($#m1_hidden :::"set"::: ) means :: LMOD_7:def 12 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_vectsp_4 :::"+"::: ) "W"))) ")" )); end; :: deftheorem defines :::".."::: LMOD_7:def 12 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "V")) ($#k7_lmod_7 :::".."::: ) (Set (Var "W")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W"))))) ")" )) ")" ))))); registrationlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); cluster (Set "V" ($#k7_lmod_7 :::".."::: ) "W") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); let "a" be ($#m1_subset_1 :::"Vector":::) "of" (Set (Const "V")); func "a" :::".."::: "W" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "V" ($#k7_lmod_7 :::".."::: ) "W") equals :: LMOD_7:def 13 (Set "a" ($#k3_vectsp_4 :::"+"::: ) "W"); end; :: deftheorem defines :::".."::: LMOD_7:def 13 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k8_lmod_7 :::".."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W")))))))); theorem :: LMOD_7:12 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k7_lmod_7 :::".."::: ) (Set (Var "W"))) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_lmod_7 :::".."::: ) (Set (Var "W"))))))))) ; theorem :: LMOD_7:13 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "a1")) ($#k8_lmod_7 :::".."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k8_lmod_7 :::".."::: ) (Set (Var "W")))) "iff" (Bool (Set (Set (Var "a1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a2"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) ")" ))))) ; definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); let "S1" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Const "V")) ($#k7_lmod_7 :::".."::: ) (Set (Const "W"))); func :::"-"::: "S1" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "V" ($#k7_lmod_7 :::".."::: ) "W") means :: LMOD_7:def 14 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "st" (Bool (Bool "S1" ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_lmod_7 :::".."::: ) "W"))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k8_lmod_7 :::".."::: ) "W"))); let "S2" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Const "V")) ($#k7_lmod_7 :::".."::: ) (Set (Const "W"))); func "S1" :::"+"::: "S2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "V" ($#k7_lmod_7 :::".."::: ) "W") means :: LMOD_7:def 15 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "st" (Bool (Bool "S1" ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k8_lmod_7 :::".."::: ) "W")) & (Bool "S2" ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k8_lmod_7 :::".."::: ) "W"))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k8_lmod_7 :::".."::: ) "W"))); end; :: deftheorem defines :::"-"::: LMOD_7:def 14 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "S1")) "," (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k7_lmod_7 :::".."::: ) (Set (Var "W"))) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k9_lmod_7 :::"-"::: ) (Set (Var "S1")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_lmod_7 :::".."::: ) (Set (Var "W"))))) "holds" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k8_lmod_7 :::".."::: ) (Set (Var "W"))))) ")" ))))); :: deftheorem defines :::"+"::: LMOD_7:def 15 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "b6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k7_lmod_7 :::".."::: ) (Set (Var "W"))) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k10_lmod_7 :::"+"::: ) (Set (Var "S2")))) "iff" (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "S1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k8_lmod_7 :::".."::: ) (Set (Var "W")))) & (Bool (Set (Var "S2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k8_lmod_7 :::".."::: ) (Set (Var "W"))))) "holds" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k8_lmod_7 :::".."::: ) (Set (Var "W"))))) ")" ))))); definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); func :::"COMPL"::: "W" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" "V" ($#k7_lmod_7 :::".."::: ) "W" ")" ) means :: LMOD_7:def 16 (Bool "for" (Set (Var "S1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "V" ($#k7_lmod_7 :::".."::: ) "W") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "S1"))) ($#r1_hidden :::"="::: ) (Set ($#k9_lmod_7 :::"-"::: ) (Set (Var "S1"))))); func :::"ADD"::: "W" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" "V" ($#k7_lmod_7 :::".."::: ) "W" ")" ) means :: LMOD_7:def 17 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "V" ($#k7_lmod_7 :::".."::: ) "W") "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k10_lmod_7 :::"+"::: ) (Set (Var "S2"))))); end; :: deftheorem defines :::"COMPL"::: LMOD_7:def 16 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" (Set (Var "V")) ($#k7_lmod_7 :::".."::: ) (Set (Var "W")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k11_lmod_7 :::"COMPL"::: ) (Set (Var "W")))) "iff" (Bool "for" (Set (Var "S1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k7_lmod_7 :::".."::: ) (Set (Var "W"))) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "S1"))) ($#r1_hidden :::"="::: ) (Set ($#k9_lmod_7 :::"-"::: ) (Set (Var "S1"))))) ")" ))))); :: deftheorem defines :::"ADD"::: LMOD_7:def 17 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" (Set (Var "V")) ($#k7_lmod_7 :::".."::: ) (Set (Var "W")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k12_lmod_7 :::"ADD"::: ) (Set (Var "W")))) "iff" (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k7_lmod_7 :::".."::: ) (Set (Var "W"))) "holds" (Bool (Set (Set (Var "b4")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "S1")) "," (Set (Var "S2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "S1")) ($#k10_lmod_7 :::"+"::: ) (Set (Var "S2"))))) ")" ))))); definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); func "V" :::"."::: "W" -> ($#v8_algstr_0 :::"strict"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) equals :: LMOD_7:def 18 (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "(" "V" ($#k7_lmod_7 :::".."::: ) "W" ")" ) "," (Set "(" ($#k12_lmod_7 :::"ADD"::: ) "W" ")" ) "," (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) "V" ")" ) ($#k8_lmod_7 :::".."::: ) "W" ")" ) "#)" ); end; :: deftheorem defines :::"."::: LMOD_7:def 18 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "V")) ($#k13_lmod_7 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "(" (Set (Var "V")) ($#k7_lmod_7 :::".."::: ) (Set (Var "W")) ")" ) "," (Set "(" ($#k12_lmod_7 :::"ADD"::: ) (Set (Var "W")) ")" ) "," (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k8_lmod_7 :::".."::: ) (Set (Var "W")) ")" ) "#)" ))))); registrationlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); cluster (Set "V" ($#k13_lmod_7 :::"."::: ) "W") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_algstr_0 :::"strict"::: ) ; end; theorem :: LMOD_7:14 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k8_lmod_7 :::".."::: ) (Set (Var "W"))) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "V")) ($#k13_lmod_7 :::"."::: ) (Set (Var "W")) ")" )))))) ; definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); let "a" be ($#m1_subset_1 :::"Vector":::) "of" (Set (Const "V")); func "a" :::"."::: "W" -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" "V" ($#k13_lmod_7 :::"."::: ) "W" ")" ) equals :: LMOD_7:def 19 (Set "a" ($#k8_lmod_7 :::".."::: ) "W"); end; :: deftheorem defines :::"."::: LMOD_7:def 19 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k14_lmod_7 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_lmod_7 :::".."::: ) (Set (Var "W")))))))); theorem :: LMOD_7:15 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "V")) ($#k13_lmod_7 :::"."::: ) (Set (Var "W")) ")" ) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k14_lmod_7 :::"."::: ) (Set (Var "W"))))))))) ; theorem :: LMOD_7:16 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "a1")) ($#k14_lmod_7 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k14_lmod_7 :::"."::: ) (Set (Var "W")))) "iff" (Bool (Set (Set (Var "a1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a2"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) ")" ))))) ; theorem :: LMOD_7:17 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k14_lmod_7 :::"."::: ) (Set (Var "W")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k14_lmod_7 :::"."::: ) (Set (Var "W")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k14_lmod_7 :::"."::: ) (Set (Var "W")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" (Set (Var "V")) ($#k13_lmod_7 :::"."::: ) (Set (Var "W")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k14_lmod_7 :::"."::: ) (Set (Var "W")))) ")" ))))) ; registrationlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); cluster (Set "V" ($#k13_lmod_7 :::"."::: ) "W") -> ($#v8_algstr_0 :::"strict"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ; end; definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); let "r" be ($#m1_subset_1 :::"Scalar":::) "of" (Set (Const "K")); let "S" be ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Const "V")) ($#k13_lmod_7 :::"."::: ) (Set (Const "W")) ")" ); func "r" :::"*"::: "S" -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" "V" ($#k13_lmod_7 :::"."::: ) "W" ")" ) means :: LMOD_7:def 20 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "st" (Bool (Bool "S" ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k14_lmod_7 :::"."::: ) "W"))) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" "r" ($#k4_vectsp_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k14_lmod_7 :::"."::: ) "W"))); end; :: deftheorem defines :::"*"::: LMOD_7:def 20 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "S")) "," (Set (Var "b6")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "V")) ($#k13_lmod_7 :::"."::: ) (Set (Var "W")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k15_lmod_7 :::"*"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k14_lmod_7 :::"."::: ) (Set (Var "W"))))) "holds" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k14_lmod_7 :::"."::: ) (Set (Var "W"))))) ")" )))))); definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); func :::"LMULT"::: "W" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" "V" ($#k13_lmod_7 :::"."::: ) "W" ")" )) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" "V" ($#k13_lmod_7 :::"."::: ) "W" ")" )) means :: LMOD_7:def 21 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Scalar":::) "of" "K" (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" "V" ($#k13_lmod_7 :::"."::: ) "W" ")" ) "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k15_lmod_7 :::"*"::: ) (Set (Var "S")))))); end; :: deftheorem defines :::"LMULT"::: LMOD_7:def 21 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "V")) ($#k13_lmod_7 :::"."::: ) (Set (Var "W")) ")" )) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "V")) ($#k13_lmod_7 :::"."::: ) (Set (Var "W")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k16_lmod_7 :::"LMULT"::: ) (Set (Var "W")))) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "V")) ($#k13_lmod_7 :::"."::: ) (Set (Var "W")) ")" ) "holds" (Bool (Set (Set (Var "b4")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "S")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k15_lmod_7 :::"*"::: ) (Set (Var "S")))))) ")" ))))); begin definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); func "V" :::"/"::: "W" -> ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" "K" equals :: LMOD_7:def 22 (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" "V" ($#k13_lmod_7 :::"."::: ) "W" ")" )) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" "V" ($#k13_lmod_7 :::"."::: ) "W" ")" )) "," (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) "V" ")" ) ($#k14_lmod_7 :::"."::: ) "W" ")" ) "," (Set "(" ($#k16_lmod_7 :::"LMULT"::: ) "W" ")" ) "#)" ); end; :: deftheorem defines :::"/"::: LMOD_7:def 22 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "V")) ($#k17_lmod_7 :::"/"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "V")) ($#k13_lmod_7 :::"."::: ) (Set (Var "W")) ")" )) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set "(" (Set (Var "V")) ($#k13_lmod_7 :::"."::: ) (Set (Var "W")) ")" )) "," (Set "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k14_lmod_7 :::"."::: ) (Set (Var "W")) ")" ) "," (Set "(" ($#k16_lmod_7 :::"LMULT"::: ) (Set (Var "W")) ")" ) "#)" ))))); registrationlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); cluster (Set "V" ($#k17_lmod_7 :::"/"::: ) "W") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_vectsp_1 :::"strict"::: ) ; end; theorem :: LMOD_7:18 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k14_lmod_7 :::"."::: ) (Set (Var "W"))) "is" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" (Set (Var "V")) ($#k17_lmod_7 :::"/"::: ) (Set (Var "W")) ")" )))))) ; theorem :: LMOD_7:19 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" (Set (Var "V")) ($#k17_lmod_7 :::"/"::: ) (Set (Var "W")) ")" ) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "V")) ($#k13_lmod_7 :::"."::: ) (Set (Var "W")) ")" )))))) ; definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); let "a" be ($#m1_subset_1 :::"Vector":::) "of" (Set (Const "V")); func "a" :::"/"::: "W" -> ($#m1_subset_1 :::"Vector":::) "of" (Set "(" "V" ($#k17_lmod_7 :::"/"::: ) "W" ")" ) equals :: LMOD_7:def 23 (Set "a" ($#k14_lmod_7 :::"."::: ) "W"); end; :: deftheorem defines :::"/"::: LMOD_7:def 23 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k18_lmod_7 :::"/"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k14_lmod_7 :::"."::: ) (Set (Var "W")))))))); theorem :: LMOD_7:20 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" (Set (Var "V")) ($#k17_lmod_7 :::"/"::: ) (Set (Var "W")) ")" ) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k18_lmod_7 :::"/"::: ) (Set (Var "W"))))))))) ; theorem :: LMOD_7:21 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "a1")) ($#k18_lmod_7 :::"/"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a2")) ($#k18_lmod_7 :::"/"::: ) (Set (Var "W")))) "iff" (Bool (Set (Set (Var "a1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a2"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) ")" ))))) ; theorem :: LMOD_7:22 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k18_lmod_7 :::"/"::: ) (Set (Var "W")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k18_lmod_7 :::"/"::: ) (Set (Var "W")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k18_lmod_7 :::"/"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "r")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k18_lmod_7 :::"/"::: ) (Set (Var "W")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k18_lmod_7 :::"/"::: ) (Set (Var "W")))) ")" )))))) ; theorem :: LMOD_7:23 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "V")) ($#k17_lmod_7 :::"/"::: ) (Set (Var "W"))) "is" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")))))) ; registrationlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); cluster (Set "V" ($#k17_lmod_7 :::"/"::: ) "W") -> ($#v7_vectsp_1 :::"strict"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ; end;