:: VECTSP_2 semantic presentation begin registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; attr "IT" is :::"domRing-like"::: means :: VECTSP_2:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool "(" "not" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT")) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT")) "or" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT")) ")" )); end; :: deftheorem defines :::"domRing-like"::: VECTSP_2:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_vectsp_2 :::"domRing-like"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool "(" "not" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")))) "or" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")))) ")" )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; definitionmode comRing is ($#v5_group_1 :::"commutative"::: ) ($#l6_algstr_0 :::"Ring":::); end; definitionmode domRing is ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"comRing":::); end; theorem :: VECTSP_2:1 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set (Var "F")) "is" ($#l6_algstr_0 :::"domRing":::))) ; definitionmode Skew-Field is ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#l6_algstr_0 :::"Ring":::); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) for ($#l4_algstr_0 :::"multLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) for ($#l4_algstr_0 :::"multLoopStr"::: ) ; end; theorem :: VECTSP_2:2 (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 "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "z")))) "implies" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y"))))) "implies" (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" & "(" (Bool (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "z")))) "implies" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")))) ")" & "(" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x"))))) "implies" (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" ")" ))) ; theorem :: VECTSP_2:3 (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 "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) "iff" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "R")))) ")" ))) ; theorem :: VECTSP_2:4 (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 "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")))) ")" )))) ; theorem :: VECTSP_2:5 (Bool "for" (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "F"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) ")" ))) ; theorem :: VECTSP_2:6 (Bool "for" (Set (Var "SF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF"))))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SF")) "st" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "SF"))))))) ; theorem :: VECTSP_2:7 (Bool "for" (Set (Var "SF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "SF"))))) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "SF")))))) ; theorem :: VECTSP_2:8 (Bool "for" (Set (Var "SF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF"))))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z"))))) ; definitionlet "SF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "SF")); assume (Bool (Set (Const "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Const "SF")))) ; redefine func "x" :::"""::: means :: VECTSP_2:def 2 (Bool (Set it ($#k6_algstr_0 :::"*"::: ) "x") ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "SF")); end; :: deftheorem defines :::"""::: VECTSP_2:def 2 : (Bool "for" (Set (Var "SF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF"))))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "SF"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) )) "iff" (Bool (Set (Set (Var "b3")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "SF")))) ")" )))); definitionlet "SF" be ($#l6_algstr_0 :::"Skew-Field":::); let "x", "y" be ($#m1_subset_1 :::"Scalar":::) "of" (Set (Const "SF")); func "x" :::"/"::: "y" -> ($#m1_subset_1 :::"Scalar":::) "of" "SF" equals :: VECTSP_2:def 3 (Set "x" ($#k6_algstr_0 :::"*"::: ) (Set "(" "y" ($#k11_algstr_0 :::"""::: ) ")" )); end; :: deftheorem defines :::"/"::: VECTSP_2:def 3 : (Bool "for" (Set (Var "SF")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "SF")) "holds" (Bool (Set (Set (Var "x")) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k11_algstr_0 :::"""::: ) ")" ))))); theorem :: VECTSP_2:9 (Bool "for" (Set (Var "SF")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF"))))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "SF")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "SF")))) ")" ))) ; theorem :: VECTSP_2:10 (Bool "for" (Set (Var "SF")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "SF"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k11_algstr_0 :::"""::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) )) ")" ))) ; theorem :: VECTSP_2:11 (Bool "for" (Set (Var "SF")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF"))))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k11_algstr_0 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k11_algstr_0 :::"""::: ) )))) ; theorem :: VECTSP_2:12 (Bool "for" (Set (Var "SF")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "SF")) "holds" (Bool "(" "not" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF")))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF")))) "or" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF")))) ")" ))) ; theorem :: VECTSP_2:13 (Bool "for" (Set (Var "SF")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF"))))) "holds" (Bool (Set (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF")))))) ; theorem :: VECTSP_2:14 (Bool "for" (Set (Var "SF")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF"))))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k11_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: VECTSP_2:15 (Bool "for" (Set (Var "SF")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "SF")) ")" ) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) )) & (Bool (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "SF")) ")" ) ($#k1_vectsp_2 :::"/"::: ) (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))) ; theorem :: VECTSP_2:16 (Bool "for" (Set (Var "SF")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF"))))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "SF")) ")" ) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "SF")))) & (Bool (Set (Set "(" (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "SF")) ")" ) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "SF")))) ")" ))) ; theorem :: VECTSP_2:17 (Bool "for" (Set (Var "SF")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF"))))) "holds" (Bool (Set (Set (Var "x")) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "SF")))))) ; theorem :: VECTSP_2:18 (Bool "for" (Set (Var "SF")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF"))))) "holds" (Bool (Set (Set (Var "x")) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ) ($#k1_vectsp_2 :::"/"::: ) (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))))) ; theorem :: VECTSP_2:19 (Bool "for" (Set (Var "SF")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF"))))) "holds" (Bool "(" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "y")))) & (Bool (Set (Set (Var "x")) ($#k1_vectsp_2 :::"/"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "y")) ")" ))) ")" ))) ; theorem :: VECTSP_2:20 (Bool "for" (Set (Var "SF")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "z")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "z")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "z")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "z")))) ")" ))) ; theorem :: VECTSP_2:21 (Bool "for" (Set (Var "SF")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF")))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF"))))) "holds" (Bool (Set (Set (Var "x")) ($#k1_vectsp_2 :::"/"::: ) (Set "(" (Set (Var "y")) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "y")))))) ; theorem :: VECTSP_2:22 (Bool "for" (Set (Var "SF")) "being" ($#l6_algstr_0 :::"Skew-Field":::) (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "SF")) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "SF"))))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_vectsp_2 :::"/"::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; definitionlet "FS" be ($#l1_struct_0 :::"1-sorted"::: ) ; attr "c2" is :::"strict"::: ; struct :::"RightModStr"::: "over" "FS" -> ($#l2_algstr_0 :::"addLoopStr"::: ) ; aggr :::"RightModStr":::(# :::"carrier":::, :::"addF":::, :::"ZeroF":::, :::"rmult"::: #) -> ($#l1_vectsp_2 :::"RightModStr"::: ) "over" "FS"; sel :::"rmult"::: "c2" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "FS") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2"); end; registrationlet "FS" be ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_vectsp_2 :::"RightModStr"::: ) "over" "FS"; end; registrationlet "FS" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); let "Z" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); let "r" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "FS"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "A")); cluster (Set ($#g1_vectsp_2 :::"RightModStr"::: ) "(#" "A" "," "a" "," "Z" "," "r" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; definitionlet "FS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "RMS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Const "FS")); mode Scalar of "RMS" is ($#m1_subset_1 :::"Element":::) "of" "FS"; mode Vector of "RMS" is ($#m1_subset_1 :::"Element":::) "of" "RMS"; end; definitionlet "FS1", "FS2" be ($#l1_struct_0 :::"1-sorted"::: ) ; attr "c3" is :::"strict"::: ; struct :::"BiModStr"::: "over" "FS1" "," "FS2" -> ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" "FS1" "," ($#l1_vectsp_2 :::"RightModStr"::: ) "over" "FS2"; aggr :::"BiModStr":::(# :::"carrier":::, :::"addF":::, :::"ZeroF":::, :::"lmult":::, :::"rmult"::: #) -> ($#l2_vectsp_2 :::"BiModStr"::: ) "over" "FS1" "," "FS2"; end; registrationlet "FS1", "FS2" be ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l2_vectsp_2 :::"BiModStr"::: ) "over" "FS1" "," "FS2"; end; registrationlet "FS1", "FS2" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); let "Z" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); let "l" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "FS1"))) "," (Set (Const "A")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "A")); let "r" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "FS2"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "A")); cluster (Set ($#g2_vectsp_2 :::"BiModStr"::: ) "(#" "A" "," "a" "," "Z" "," "l" "," "r" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; definitionlet "R" be ($#~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"::: ) ; func :::"AbGr"::: "R" -> ($#v8_algstr_0 :::"strict"::: ) ($#l2_algstr_0 :::"AbGroup":::) equals :: VECTSP_2:def 4 (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "R") "," (Set "(" ($#k4_struct_0 :::"0."::: ) "R" ")" ) "#)" ); end; :: deftheorem defines :::"AbGr"::: VECTSP_2:def 4 : (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"::: ) "holds" (Bool (Set ($#k2_vectsp_2 :::"AbGr"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "R"))) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) "#)" ))); registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v7_vectsp_1 :::"strict"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" "R"; end; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); func :::"LeftModule"::: "R" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v7_vectsp_1 :::"strict"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" "R" equals :: VECTSP_2:def 5 (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "R") "," (Set "(" ($#k4_struct_0 :::"0."::: ) "R" ")" ) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "R") "#)" ); end; :: deftheorem defines :::"LeftModule"::: VECTSP_2:def 5 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set ($#k3_vectsp_2 :::"LeftModule"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "R"))) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "R"))) "#)" ))); registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); 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"::: ) ($#v2_vectsp_2 :::"strict"::: ) for ($#l1_vectsp_2 :::"RightModStr"::: ) "over" "R"; end; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); func :::"RightModule"::: "R" -> ($#~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_vectsp_2 :::"strict"::: ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" "R" equals :: VECTSP_2:def 6 (Set ($#g1_vectsp_2 :::"RightModStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "R") "," (Set "(" ($#k4_struct_0 :::"0."::: ) "R" ")" ) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "R") "#)" ); end; :: deftheorem defines :::"RightModule"::: VECTSP_2:def 6 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set ($#k4_vectsp_2 :::"RightModule"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_2 :::"RightModStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "R"))) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" ) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "R"))) "#)" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Const "R")); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); let "v" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")); func "v" :::"*"::: "x" -> ($#m1_subset_1 :::"Element":::) "of" "V" equals :: VECTSP_2:def 7 (Set (Set "the" ($#u1_vectsp_2 :::"rmult"::: ) "of" "V") ($#k2_binop_1 :::"."::: ) "(" "v" "," "x" ")" ); end; :: deftheorem defines :::"*"::: VECTSP_2:def 7 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "R")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_vectsp_2 :::"rmult"::: ) "of" (Set (Var "V"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "x")) ")" )))))); registrationlet "R1", "R2" be ($#l6_algstr_0 :::"Ring":::); 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"::: ) ($#v3_vectsp_2 :::"strict"::: ) for ($#l2_vectsp_2 :::"BiModStr"::: ) "over" "R1" "," "R2"; end; definitionlet "R1", "R2" be ($#l6_algstr_0 :::"Ring":::); func :::"BiModule"::: "(" "R1" "," "R2" ")" -> ($#~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"::: ) ($#v3_vectsp_2 :::"strict"::: ) ($#l2_vectsp_2 :::"BiModStr"::: ) "over" "R1" "," "R2" equals :: VECTSP_2:def 8 (Set ($#g2_vectsp_2 :::"BiModStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "," (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R1") "," (Num 1) ")" ")" ) "," (Set "(" ($#k9_funct_3 :::"pr1"::: ) "(" (Num 1) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R2") ")" ")" ) "#)" ); end; :: deftheorem defines :::"BiModule"::: VECTSP_2:def 8 : (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set ($#k6_vectsp_2 :::"BiModule"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g2_vectsp_2 :::"BiModStr"::: ) "(#" (Num 1) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "," (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R1"))) "," (Num 1) ")" ")" ) "," (Set "(" ($#k9_funct_3 :::"pr1"::: ) "(" (Num 1) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R2"))) ")" ")" ) "#)" ))); theorem :: VECTSP_2:23 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k3_vectsp_2 :::"LeftModule"::: ) (Set (Var "R")) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "w")) ")" ))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ))) & (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "R")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" )))) ; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); 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 ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" "R"; end; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); mode LeftMod of "R" is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" "R"; end; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k3_vectsp_2 :::"LeftModule"::: ) "R") -> ($#~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"::: ) ; end; theorem :: VECTSP_2:24 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k4_vectsp_2 :::"RightModule"::: ) (Set (Var "R")) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" ) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "w")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "y")) ")" ) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" )))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Const "R")); attr "IT" is :::"RightMod-like"::: means :: VECTSP_2:def 9 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" "R" (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" "IT" "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")) ")" ) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "w")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "y")) ")" ) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) "R" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" ))); end; :: deftheorem defines :::"RightMod-like"::: VECTSP_2:def 9 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_vectsp_2 :::"RightMod-like"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")) ")" ) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "w")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "y")) ")" ) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" ))) ")" ))); registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); 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"::: ) ($#v2_vectsp_2 :::"strict"::: ) ($#v4_vectsp_2 :::"RightMod-like"::: ) for ($#l1_vectsp_2 :::"RightModStr"::: ) "over" "R"; end; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); mode RightMod of "R" 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"::: ) ($#v4_vectsp_2 :::"RightMod-like"::: ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" "R"; end; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k4_vectsp_2 :::"RightModule"::: ) "R") -> ($#~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_vectsp_2 :::"strict"::: ) ($#v4_vectsp_2 :::"RightMod-like"::: ) ; end; definitionlet "R1", "R2" be ($#l6_algstr_0 :::"Ring":::); let "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_vectsp_2 :::"BiModStr"::: ) "over" (Set (Const "R1")) "," (Set (Const "R2")); attr "IT" is :::"BiMod-like"::: means :: VECTSP_2:def 10 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" "R1" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Scalar":::) "of" "R2" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" "IT" "holds" (Bool (Set (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "p"))))))); end; :: deftheorem defines :::"BiMod-like"::: VECTSP_2:def 10 : (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_vectsp_2 :::"BiModStr"::: ) "over" (Set (Var "R1")) "," (Set (Var "R2")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_vectsp_2 :::"BiMod-like"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R1")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R2")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "p"))))))) ")" ))); registrationlet "R1", "R2" be ($#l6_algstr_0 :::"Ring":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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"::: ) ($#v3_vectsp_2 :::"strict"::: ) ($#v4_vectsp_2 :::"RightMod-like"::: ) ($#v5_vectsp_2 :::"BiMod-like"::: ) for ($#l2_vectsp_2 :::"BiModStr"::: ) "over" "R1" "," "R2"; end; definitionlet "R1", "R2" be ($#l6_algstr_0 :::"Ring":::); mode BiMod of "R1" "," "R2" is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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"::: ) ($#v4_vectsp_2 :::"RightMod-like"::: ) ($#v5_vectsp_2 :::"BiMod-like"::: ) ($#l2_vectsp_2 :::"BiModStr"::: ) "over" "R1" "," "R2"; end; theorem :: VECTSP_2:25 (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_vectsp_2 :::"BiModStr"::: ) "over" (Set (Var "R1")) "," (Set (Var "R2")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R1")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R2")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "w")) ")" ))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ))) & (Bool (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "R1")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")) ")" ) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "p")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "w")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "p")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "q")) ")" ))) & (Bool (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "q")) ")" ) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "R2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "p")))) ")" ))) ")" ) "iff" (Bool "(" (Bool (Set (Var "V")) "is" ($#v4_vectsp_2 :::"RightMod-like"::: ) ) & (Bool (Set (Var "V")) "is" ($#v8_vectsp_1 :::"vector-distributive"::: ) ) & (Bool (Set (Var "V")) "is" ($#v9_vectsp_1 :::"scalar-distributive"::: ) ) & (Bool (Set (Var "V")) "is" ($#v10_vectsp_1 :::"scalar-associative"::: ) ) & (Bool (Set (Var "V")) "is" ($#v11_vectsp_1 :::"scalar-unital"::: ) ) & (Bool (Set (Var "V")) "is" ($#v5_vectsp_2 :::"BiMod-like"::: ) ) ")" ) ")" ))) ; theorem :: VECTSP_2:26 (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool (Set ($#k6_vectsp_2 :::"BiModule"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" ) "is" ($#l2_vectsp_2 :::"BiMod":::) "of" (Set (Var "R1")) "," (Set (Var "R2")))) ; registrationlet "R1", "R2" be ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k6_vectsp_2 :::"BiModule"::: ) "(" "R1" "," "R2" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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"::: ) ($#v3_vectsp_2 :::"strict"::: ) ($#v4_vectsp_2 :::"RightMod-like"::: ) ($#v5_vectsp_2 :::"BiMod-like"::: ) ; end; theorem :: VECTSP_2:27 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) "st" (Bool (Bool (Set (Var "L")) "is" ($#v4_vectsp_1 :::"well-unital"::: ) )) "holds" (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "L"))))) ; begin theorem :: VECTSP_2:28 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "K")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")))))) ; theorem :: VECTSP_2:29 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "K")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")))))) ; theorem :: VECTSP_2:30 (Bool "for" (Set (Var "F")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) "or" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" ) ")" ))))) ; theorem :: VECTSP_2:31 (Bool "for" (Set (Var "F")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))))))) ; theorem :: VECTSP_2:32 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_2 :::"RightMod-like"::: ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "R")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "R")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")))) & (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" ))))) ; theorem :: VECTSP_2:33 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_2 :::"RightMod-like"::: ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "R")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set (Var "w")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ")" ))) ")" ))))) ; theorem :: VECTSP_2:34 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_2 :::"RightMod-like"::: ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "R")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")) ")" ))))))) ; theorem :: VECTSP_2:35 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_2 :::"RightMod-like"::: ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "R")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "w")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")) ")" ))))))) ; theorem :: VECTSP_2:36 (Bool "for" (Set (Var "F")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_2 :::"RightMod-like"::: ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F")))) "or" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" ) ")" ))))) ; theorem :: VECTSP_2:37 (Bool "for" (Set (Var "F")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_2 :::"RightMod-like"::: ) ($#l1_vectsp_2 :::"RightModStr"::: ) "over" (Set (Var "F")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k5_vectsp_2 :::"*"::: ) (Set (Var "x")) ")" ) ($#k5_vectsp_2 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))))))) ;