:: VECTSP_6 semantic presentation begin definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "GF")); mode :::"Linear_Combination"::: "of" "V" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "GF") ")" ) means :: VECTSP_6:def 1 (Bool "ex" (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "V" "st" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "V" "st" (Bool (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "GF")))); end; :: deftheorem defines :::"Linear_Combination"::: VECTSP_6:def 1 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "b3")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "GF"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V"))) "iff" (Bool "ex" (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "GF")))))) ")" )))); definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "GF")); let "L" be ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Const "V")); func :::"Carrier"::: "L" -> ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "V" equals :: VECTSP_6:def 2 "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Element":::) "of" "V" : (Bool (Set "L" ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "GF")) "}" ; end; :: deftheorem defines :::"Carrier"::: VECTSP_6:def 2 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) : (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "GF")))) "}" )))); theorem :: VECTSP_6:1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "L")))) "iff" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "GF")))) ")" )) ")" ))))) ; theorem :: VECTSP_6:2 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "GF")))) "iff" (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "L"))))) ")" ))))) ; definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "GF")); func :::"ZeroLC"::: "V" -> ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" "V" means :: VECTSP_6:def 3 (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"ZeroLC"::: VECTSP_6:def 3 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "b3")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_vectsp_6 :::"ZeroLC"::: ) (Set (Var "V")))) "iff" (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )))); theorem :: VECTSP_6:3 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k2_vectsp_6 :::"ZeroLC"::: ) (Set (Var "V")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "GF"))))))) ; definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "GF")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); mode :::"Linear_Combination"::: "of" "A" -> ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" "V" means :: VECTSP_6:def 4 (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) it) ($#r1_tarski :::"c="::: ) "A"); end; :: deftheorem defines :::"Linear_Combination"::: VECTSP_6:def 4 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "b4")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "A"))) "iff" (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "b4"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ))))); theorem :: VECTSP_6:4 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "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 (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "l")) "is" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "B"))))))) ; theorem :: VECTSP_6:5 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_vectsp_6 :::"ZeroLC"::: ) (Set (Var "V"))) "is" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "A")))))) ; theorem :: VECTSP_6:6 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "l")) "being" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V")))) "holds" (Bool (Set (Var "l")) ($#r2_funct_2 :::"="::: ) (Set ($#k2_vectsp_6 :::"ZeroLC"::: ) (Set (Var "V"))))))) ; theorem :: VECTSP_6:7 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Var "L")) "is" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "L"))))))) ; definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "GF")); let "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "V"))); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "V")) "," (Set (Const "GF")); func "f" :::"(#)"::: "F" -> ($#m2_finseq_1 :::"FinSequence":::) "of" "V" means :: VECTSP_6:def 5 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "F")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set "(" "F" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set "(" "F" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"(#)"::: VECTSP_6:def 5 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "GF")) (Bool "for" (Set (Var "b5")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_vectsp_6 :::"(#)"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b5"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" )))))); theorem :: VECTSP_6:8 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "GF")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k3_vectsp_6 :::"(#)"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")))))))))) ; theorem :: VECTSP_6:9 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "GF")) "holds" (Bool (Set (Set (Var "f")) ($#k3_vectsp_6 :::"(#)"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V")))))))) ; theorem :: VECTSP_6:10 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "GF")) "holds" (Bool (Set (Set (Var "f")) ($#k3_vectsp_6 :::"(#)"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "v")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )))))) ; theorem :: VECTSP_6:11 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "GF")) "holds" (Bool (Set (Set (Var "f")) ($#k3_vectsp_6 :::"(#)"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v1")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v1")) ")" ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v2")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v2")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )))))) ; theorem :: VECTSP_6:12 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "GF")) "holds" (Bool (Set (Set (Var "f")) ($#k3_vectsp_6 :::"(#)"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v1")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v1")) ")" ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v2")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v2")) ")" ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v3")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v3")) ")" ) ($#k3_finseq_4 :::"*>"::: ) )))))) ; theorem :: VECTSP_6:13 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "GF")) "holds" (Bool (Set (Set (Var "f")) ($#k3_vectsp_6 :::"(#)"::: ) (Set "(" (Set (Var "F")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_vectsp_6 :::"(#)"::: ) (Set (Var "F")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "f")) ($#k3_vectsp_6 :::"(#)"::: ) (Set (Var "G")) ")" ))))))) ; definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "GF")); let "L" be ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Const "V")); assume (Bool "(" (Bool (Set (Const "V")) "is" ($#v2_rlvect_1 :::"Abelian"::: ) ) & (Bool (Set (Const "V")) "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) & (Bool (Set (Const "V")) "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) ) & (Bool (Set (Const "V")) "is" ($#v13_algstr_0 :::"right_complementable"::: ) ) ")" ) ; func :::"Sum"::: "L" -> ($#m1_subset_1 :::"Element":::) "of" "V" means :: VECTSP_6:def 6 (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_6 :::"Carrier"::: ) "L")) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" "L" ($#k3_vectsp_6 :::"(#)"::: ) (Set (Var "F")) ")" ))) ")" )); end; :: deftheorem defines :::"Sum"::: VECTSP_6:def 6 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v2_rlvect_1 :::"Abelian"::: ) ) & (Bool (Set (Var "V")) "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) & (Bool (Set (Var "V")) "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) ) & (Bool (Set (Var "V")) "is" ($#v13_algstr_0 :::"right_complementable"::: ) )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "L")))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "L")))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "L")) ($#k3_vectsp_6 :::"(#)"::: ) (Set (Var "F")) ")" ))) ")" )) ")" ))))); theorem :: VECTSP_6:14 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "GF"))) ($#r1_hidden :::"<>"::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "GF"))))) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) "is" ($#v1_vectsp_4 :::"linearly-closed"::: ) ) ")" ) "iff" (Bool "for" (Set (Var "l")) "being" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "l"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) ")" )))) ; theorem :: VECTSP_6:15 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) "holds" (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set "(" ($#k2_vectsp_6 :::"ZeroLC"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))) ; theorem :: VECTSP_6:16 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "l")) "being" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V")))) "holds" (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))))) ; theorem :: VECTSP_6:17 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "l")) "being" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) "holds" (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")))))))) ; theorem :: VECTSP_6:18 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2")))) "holds" (Bool "for" (Set (Var "l")) "being" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k7_domain_1 :::"}"::: ) ) "holds" (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "v1")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "v2")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v2")) ")" ))))))) ; theorem :: VECTSP_6:19 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))))) ; theorem :: VECTSP_6:20 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))) "holds" (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")))))))) ; theorem :: VECTSP_6:21 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2")))) "holds" (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v1")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v2")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v2")) ")" ))))))) ; definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "GF")); let "L1", "L2" be ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Const "V")); :: original: :::"="::: redefine pred "L1" :::"="::: "L2" means :: VECTSP_6:def 7 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "V" "holds" (Bool (Set "L1" ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set "L2" ($#k3_funct_2 :::"."::: ) (Set (Var "v"))))); end; :: deftheorem defines :::"="::: VECTSP_6:def 7 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "L1")) ($#r1_vectsp_6 :::"="::: ) (Set (Var "L2"))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "L1")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "L2")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))))) ")" )))); definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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"::: ) ; let "V" be ($#~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" (Set (Const "GF")); let "L1", "L2" be ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Const "V")); func "L1" :::"+"::: "L2" -> ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" "V" equals :: VECTSP_6:def 8 (Set "L1" ($#k1_vfunct_1 :::"+"::: ) "L2"); end; :: deftheorem defines :::"+"::: VECTSP_6:def 8 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "L1")) ($#k5_vectsp_6 :::"+"::: ) (Set (Var "L2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "L1")) ($#k1_vfunct_1 :::"+"::: ) (Set (Var "L2"))))))); theorem :: VECTSP_6:22 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "L1")) ($#k5_vectsp_6 :::"+"::: ) (Set (Var "L2")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L1")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "L2")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ))))))) ; theorem :: VECTSP_6:23 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set "(" (Set (Var "L1")) ($#k5_vectsp_6 :::"+"::: ) (Set (Var "L2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "L1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "L2")) ")" )))))) ; theorem :: VECTSP_6:24 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "L1")) "is" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "A"))) & (Bool (Set (Var "L2")) "is" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set (Set (Var "L1")) ($#k5_vectsp_6 :::"+"::: ) (Set (Var "L2"))) "is" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "A"))))))) ; theorem :: VECTSP_6:25 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "L1")) ($#k5_vectsp_6 :::"+"::: ) (Set (Var "L2"))) ($#r1_vectsp_6 :::"="::: ) (Set (Set (Var "L2")) ($#k5_vectsp_6 :::"+"::: ) (Set (Var "L1"))))))) ; theorem :: VECTSP_6:26 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "," (Set (Var "L3")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "L1")) ($#k5_vectsp_6 :::"+"::: ) (Set "(" (Set (Var "L2")) ($#k5_vectsp_6 :::"+"::: ) (Set (Var "L3")) ")" )) ($#r1_vectsp_6 :::"="::: ) (Set (Set "(" (Set (Var "L1")) ($#k5_vectsp_6 :::"+"::: ) (Set (Var "L2")) ")" ) ($#k5_vectsp_6 :::"+"::: ) (Set (Var "L3"))))))) ; theorem :: VECTSP_6:27 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "L")) ($#k5_vectsp_6 :::"+"::: ) (Set "(" ($#k2_vectsp_6 :::"ZeroLC"::: ) (Set (Var "V")) ")" )) ($#r1_vectsp_6 :::"="::: ) (Set (Var "L"))) & (Bool (Set (Set "(" ($#k2_vectsp_6 :::"ZeroLC"::: ) (Set (Var "V")) ")" ) ($#k5_vectsp_6 :::"+"::: ) (Set (Var "L"))) ($#r1_vectsp_6 :::"="::: ) (Set (Var "L"))) ")" )))) ; definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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"::: ) ; let "V" be ($#~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" (Set (Const "GF")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "GF")); let "L" be ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Const "V")); func "a" :::"*"::: "L" -> ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" "V" means :: VECTSP_6:def 9 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "V" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set "a" ($#k6_algstr_0 :::"*"::: ) (Set "(" "L" ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))); end; :: deftheorem defines :::"*"::: VECTSP_6:def 9 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "," (Set (Var "b5")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "L")))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "b5")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))) ")" ))))); theorem :: VECTSP_6:28 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set "(" (Set (Var "a")) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "L")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "L")))))))) ; theorem :: VECTSP_6:29 (Bool "for" (Set (Var "GF")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "GF"))))) "holds" (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set "(" (Set (Var "a")) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "L")))))))) ; theorem :: VECTSP_6:30 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "GF")) ")" ) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "L"))) ($#r1_vectsp_6 :::"="::: ) (Set ($#k2_vectsp_6 :::"ZeroLC"::: ) (Set (Var "V"))))))) ; theorem :: VECTSP_6:31 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "GF")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "L")) "is" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set (Set (Var "a")) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "L"))) "is" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "A")))))))) ; theorem :: VECTSP_6:32 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "L"))) ($#r1_vectsp_6 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "L")) ")" ) ($#k5_vectsp_6 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "L")) ")" ))))))) ; theorem :: VECTSP_6:33 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "GF")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k6_vectsp_6 :::"*"::: ) (Set "(" (Set (Var "L1")) ($#k5_vectsp_6 :::"+"::: ) (Set (Var "L2")) ")" )) ($#r1_vectsp_6 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "L1")) ")" ) ($#k5_vectsp_6 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "L2")) ")" ))))))) ; theorem :: VECTSP_6:34 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k6_vectsp_6 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "L")) ")" )) ($#r1_vectsp_6 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "L")))))))) ; theorem :: VECTSP_6:35 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "GF")) ")" ) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "L"))) ($#r1_vectsp_6 :::"="::: ) (Set (Var "L")))))) ; definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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"::: ) ; let "V" be ($#~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" (Set (Const "GF")); let "L" be ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Const "V")); func :::"-"::: "L" -> ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" "V" equals :: VECTSP_6:def 10 (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) "GF" ")" ) ")" ) ($#k6_vectsp_6 :::"*"::: ) "L"); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Const "V")) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Const "GF")) ")" ) ")" ) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Const "GF")) ")" ) ")" ) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "b1"))))) ; end; :: deftheorem defines :::"-"::: VECTSP_6:def 10 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k7_vectsp_6 :::"-"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "GF")) ")" ) ")" ) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "L"))))))); theorem :: VECTSP_6:36 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k7_vectsp_6 :::"-"::: ) (Set (Var "L")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ))))))) ; theorem :: VECTSP_6:37 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "L1")) ($#k5_vectsp_6 :::"+"::: ) (Set (Var "L2"))) ($#r1_vectsp_6 :::"="::: ) (Set ($#k2_vectsp_6 :::"ZeroLC"::: ) (Set (Var "V"))))) "holds" (Bool (Set (Var "L2")) ($#r1_vectsp_6 :::"="::: ) (Set ($#k7_vectsp_6 :::"-"::: ) (Set (Var "L1"))))))) ; theorem :: VECTSP_6:38 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set "(" ($#k7_vectsp_6 :::"-"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "L"))))))) ; theorem :: VECTSP_6:39 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "L")) "is" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set ($#k7_vectsp_6 :::"-"::: ) (Set (Var "L"))) "is" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "A"))))))) ; definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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"::: ) ; let "V" be ($#~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" (Set (Const "GF")); let "L1", "L2" be ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Const "V")); func "L1" :::"-"::: "L2" -> ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" "V" equals :: VECTSP_6:def 11 (Set "L1" ($#k5_vectsp_6 :::"+"::: ) (Set "(" ($#k7_vectsp_6 :::"-"::: ) "L2" ")" )); end; :: deftheorem defines :::"-"::: VECTSP_6:def 11 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "L1")) ($#k8_vectsp_6 :::"-"::: ) (Set (Var "L2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "L1")) ($#k5_vectsp_6 :::"+"::: ) (Set "(" ($#k7_vectsp_6 :::"-"::: ) (Set (Var "L2")) ")" )))))); theorem :: VECTSP_6:40 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "L1")) ($#k8_vectsp_6 :::"-"::: ) (Set (Var "L2")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L1")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "L2")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ))))))) ; theorem :: VECTSP_6:41 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set "(" (Set (Var "L1")) ($#k8_vectsp_6 :::"-"::: ) (Set (Var "L2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "L1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "L2")) ")" )))))) ; theorem :: VECTSP_6:42 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "L1")) "is" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "A"))) & (Bool (Set (Var "L2")) "is" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set (Set (Var "L1")) ($#k8_vectsp_6 :::"-"::: ) (Set (Var "L2"))) "is" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "A"))))))) ; theorem :: VECTSP_6:43 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "L")) ($#k8_vectsp_6 :::"-"::: ) (Set (Var "L"))) ($#r1_vectsp_6 :::"="::: ) (Set ($#k2_vectsp_6 :::"ZeroLC"::: ) (Set (Var "V"))))))) ; theorem :: VECTSP_6:44 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set "(" (Set (Var "L1")) ($#k5_vectsp_6 :::"+"::: ) (Set (Var "L2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "L1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "L2")) ")" )))))) ; theorem :: VECTSP_6:45 (Bool "for" (Set (Var "GF")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "GF")) "holds" (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set "(" (Set (Var "a")) ($#k6_vectsp_6 :::"*"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "L")) ")" ))))))) ; theorem :: VECTSP_6:46 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set "(" ($#k7_vectsp_6 :::"-"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "L")) ")" )))))) ; theorem :: VECTSP_6:47 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set "(" (Set (Var "L1")) ($#k8_vectsp_6 :::"-"::: ) (Set (Var "L2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "L1")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "L2")) ")" )))))) ; theorem :: VECTSP_6:48 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "GF")) "holds" (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "GF")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")))))) ; theorem :: VECTSP_6:49 (Bool "for" (Set (Var "GF")) "being" ($#l6_algstr_0 :::"Field":::) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "GF")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "GF"))))) ;