:: VECTSP10 semantic presentation begin definitionlet "K" be ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; func :::"StructVectSp"::: "K" -> ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" "K" equals :: VECTSP10:def 1 (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "K") "," (Set "(" ($#k4_struct_0 :::"0."::: ) "K" ")" ) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "K") "#)" ); end; :: deftheorem defines :::"StructVectSp"::: VECTSP10:def 1 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool (Set ($#k1_vectsp10 :::"StructVectSp"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) "#)" ))); registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k1_vectsp10 :::"StructVectSp"::: ) "K") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_vectsp_1 :::"strict"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k1_vectsp10 :::"StructVectSp"::: ) "K") -> ($#v2_rlvect_1 :::"Abelian"::: ) ($#v7_vectsp_1 :::"strict"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k1_vectsp10 :::"StructVectSp"::: ) "K") -> ($#v3_rlvect_1 :::"add-associative"::: ) ($#v7_vectsp_1 :::"strict"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k1_vectsp10 :::"StructVectSp"::: ) "K") -> ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v7_vectsp_1 :::"strict"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k1_vectsp10 :::"StructVectSp"::: ) "K") -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v7_vectsp_1 :::"strict"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k1_vectsp10 :::"StructVectSp"::: ) "K") -> ($#v7_vectsp_1 :::"strict"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k1_vectsp10 :::"StructVectSp"::: ) "K") -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v7_vectsp_1 :::"strict"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) for ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" "K"; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v7_vectsp_1 :::"strict"::: ) for ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" "K"; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v7_vectsp_1 :::"strict"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) for ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" "K"; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v7_vectsp_1 :::"strict"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) for ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" "K"; end; theorem :: VECTSP10:1 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (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"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" ))))) ; theorem :: VECTSP10:2 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "S")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V")))) & (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))))) ; theorem :: VECTSP10:3 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v"))))) ")" ))))) ; theorem :: VECTSP10:4 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Scalar":::) "of" "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))))) ; theorem :: VECTSP10:5 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "v2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2"))))) "holds" (Bool (Set (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k1_domain_1 :::"]"::: ) )))))) ; theorem :: VECTSP10:6 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2")))))))) ; theorem :: VECTSP10:7 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "v2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) ")" ))))) ; theorem :: VECTSP10:8 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W2")) "," (Set (Var "W1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "v2")) "," (Set (Var "v1")) ($#k1_domain_1 :::"]"::: ) )))))) ; theorem :: VECTSP10:9 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1")))) "holds" (Bool (Set (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "v")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k1_domain_1 :::"]"::: ) )))))) ; theorem :: VECTSP10:10 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "v")) ($#k1_domain_1 :::"]"::: ) )))))) ; theorem :: VECTSP10:11 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "V1")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W1")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1")))) "holds" (Bool (Set (Var "v")) "is" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V1")))))))) ; theorem :: VECTSP10:12 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "," (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "V1"))) & (Bool (Set (Var "W2")) ($#r1_hidden :::"="::: ) (Set (Var "V2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "V1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "V2")))))))) ; theorem :: VECTSP10:13 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "w")))) "holds" (Bool (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )))))))) ; theorem :: VECTSP10:14 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "X")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W")) "," (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ))))))))) ; theorem :: VECTSP10:15 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "X")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Set (Var "y")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "W")) ")" ) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) )))))))) ; theorem :: VECTSP10:16 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "X")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) "st" (Bool (Bool (Set (Var "w")) ($#r1_struct_0 :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "w")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "w")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k1_domain_1 :::"]"::: ) ))))))))) ; theorem :: VECTSP10:17 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Set (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k1_domain_1 :::"]"::: ) ))))))) ; theorem :: VECTSP10:18 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "X")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "X"))(Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Set (Set (Var "w")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "r")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_domain_1 :::"]"::: ) ))))))))))) ; theorem :: VECTSP10:19 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "X")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Set (Var "w1")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set "(" (Set (Var "r1")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Set (Var "w2")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x2")) "," (Set "(" (Set (Var "r2")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "w1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w2")) ")" ) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "x1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set "(" (Set (Var "r1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "r2")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_domain_1 :::"]"::: ) ))))))))))) ; theorem :: VECTSP10:20 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "X")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "t")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Set (Var "w")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "r")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "t")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "w")) ")" ) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "t")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set "(" (Set (Var "t")) ($#k8_group_1 :::"*"::: ) (Set (Var "r")) ")" ) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_domain_1 :::"]"::: ) ))))))))))) ; begin definitionlet "K" 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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); func :::"CosetSet"::: "(" "V" "," "W" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" "V" equals :: VECTSP10:def 2 "{" (Set (Var "A")) where A "is" ($#m2_vectsp_4 :::"Coset"::: ) "of" "W" : (Bool verum) "}" ; end; :: deftheorem defines :::"CosetSet"::: VECTSP10:def 2 : (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_vectsp10 :::"CosetSet"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "A")) where A "is" ($#m2_vectsp_4 :::"Coset"::: ) "of" (Set (Var "W")) : (Bool verum) "}" )))); definitionlet "K" 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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); func :::"addCoset"::: "(" "V" "," "W" ")" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k2_vectsp10 :::"CosetSet"::: ) "(" "V" "," "W" ")" ")" ) means :: VECTSP10:def 3 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_vectsp10 :::"CosetSet"::: ) "(" "V" "," "W" ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_vectsp_4 :::"+"::: ) "W")) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_vectsp_4 :::"+"::: ) "W"))) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_vectsp_4 :::"+"::: ) "W")))); end; :: deftheorem defines :::"addCoset"::: VECTSP10:def 3 : (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k2_vectsp10 :::"CosetSet"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_vectsp10 :::"addCoset"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" )) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_vectsp10 :::"CosetSet"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W")))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W")))))) ")" ))))); definitionlet "K" 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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); func :::"zeroCoset"::: "(" "V" "," "W" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_vectsp10 :::"CosetSet"::: ) "(" "V" "," "W" ")" ) equals :: VECTSP10:def 4 (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W"); end; :: deftheorem defines :::"zeroCoset"::: VECTSP10:def 4 : (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_vectsp10 :::"zeroCoset"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))))))); definitionlet "K" 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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); func :::"lmultCoset"::: "(" "V" "," "W" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") "," (Set "(" ($#k2_vectsp10 :::"CosetSet"::: ) "(" "V" "," "W" ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k2_vectsp10 :::"CosetSet"::: ) "(" "V" "," "W" ")" ")" ) means :: VECTSP10:def 5 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" "K" (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_vectsp10 :::"CosetSet"::: ) "(" "V" "," "W" ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_vectsp_4 :::"+"::: ) "W"))) "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "z")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_vectsp_4 :::"+"::: ) "W"))))); end; :: deftheorem defines :::"lmultCoset"::: VECTSP10:def 5 : (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "," (Set "(" ($#k2_vectsp10 :::"CosetSet"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k2_vectsp10 :::"CosetSet"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_vectsp10 :::"lmultCoset"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" )) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_vectsp10 :::"CosetSet"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "z")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W"))))))) ")" ))))); definitionlet "K" 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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); func :::"VectQuot"::: "(" "V" "," "W" ")" -> ($#~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"::: ) ($#v7_vectsp_1 :::"strict"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" "K" means :: VECTSP10:def 6 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k2_vectsp10 :::"CosetSet"::: ) "(" "V" "," "W" ")" )) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k3_vectsp10 :::"addCoset"::: ) "(" "V" "," "W" ")" )) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_vectsp10 :::"zeroCoset"::: ) "(" "V" "," "W" ")" )) & (Bool (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k5_vectsp10 :::"lmultCoset"::: ) "(" "V" "," "W" ")" )) ")" ); end; :: deftheorem defines :::"VectQuot"::: VECTSP10:def 6 : (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b4")) "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"::: ) ($#v7_vectsp_1 :::"strict"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k2_vectsp10 :::"CosetSet"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" )) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b4"))) ($#r1_funct_2 :::"="::: ) (Set ($#k3_vectsp10 :::"addCoset"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" )) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k4_vectsp10 :::"zeroCoset"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" )) & (Bool (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "b4"))) ($#r1_funct_2 :::"="::: ) (Set ($#k5_vectsp10 :::"lmultCoset"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" )) ")" ) ")" ))))); theorem :: VECTSP10:21 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k4_vectsp10 :::"zeroCoset"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_vectsp10 :::"zeroCoset"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" )) ")" )))) ; theorem :: VECTSP10:22 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "w")) "is" ($#m2_vectsp_4 :::"Coset"::: ) "of" (Set (Var "W"))) & (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W"))))) ")" ))))) ; theorem :: VECTSP10:23 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "v")) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W"))) "is" ($#m2_vectsp_4 :::"Coset"::: ) "of" (Set (Var "W"))) & (Bool (Set (Set (Var "v")) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W"))) "is" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ")" )) ")" ))))) ; theorem :: VECTSP10:24 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#m2_vectsp_4 :::"Coset"::: ) "of" (Set (Var "W")) "holds" (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ")" )))))) ; theorem :: VECTSP10:25 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Scalar":::) "of" "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W")))))))))) ; theorem :: VECTSP10:26 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ")" ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W")))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "A1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2")) ")" ) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W"))))))))) ; begin theorem :: VECTSP10:27 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "X")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "fi")) "being" ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "ex" (Set (Var "psi")) "being" ($#m1_subset_1 :::"linear-Functional":::) "of" (Set "(" (Set (Var "X")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "psi")) ($#k5_relset_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ($#r1_hidden :::"="::: ) (Set (Var "fi"))) & (Bool (Set (Set (Var "psi")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" ))))))))) ; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V")) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V")) ($#v1_funct_2 :::"quasi_total"::: ) ($#v13_vectsp_1 :::"additive"::: ) ($#v2_hahnban1 :::"0-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v13_vectsp_1 :::"additive"::: ) -> ($#v2_hahnban1 :::"0-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_hahnban1 :::"homogeneous"::: ) -> ($#v2_hahnban1 :::"0-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "K" 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 "K")); cluster (Set ($#k7_hahnban1 :::"0Functional"::: ) "V") -> ($#v3_funct_1 :::"constant"::: ) ; end; registrationlet "K" 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 "K")); cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V")) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_1 :::"constant"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V")) ($#v1_funct_2 :::"quasi_total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v2_hahnban1 :::"0-preserving"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); :: original: :::"constant"::: redefine attr "f" is :::"constant"::: means :: VECTSP10:def 7 (Bool "f" ($#r2_funct_2 :::"="::: ) (Set ($#k7_hahnban1 :::"0Functional"::: ) "V")); end; :: deftheorem defines :::"constant"::: VECTSP10:def 7 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#v2_hahnban1 :::"0-preserving"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_funct_1 :::"constant"::: ) ) "iff" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set ($#k7_hahnban1 :::"0Functional"::: ) (Set (Var "V")))) ")" )))); registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V")) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_1 :::"constant"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V")) ($#v1_funct_2 :::"quasi_total"::: ) ($#v13_vectsp_1 :::"additive"::: ) ($#v2_hahnban1 :::"0-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V")) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")) ($#v1_funct_1 :::"Function-like"::: ) ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) bbbadV1_PARTFUN1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V")) ($#v1_funct_2 :::"quasi_total"::: ) ($#v13_vectsp_1 :::"additive"::: ) ($#v1_hahnban1 :::"homogeneous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_zfmisc_1 :::"trivial"::: ) ($#v1_funct_2 :::"quasi_total"::: ) -> ($#v3_funct_1 :::"constant"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "v" be ($#m1_subset_1 :::"Vector":::) "of" (Set (Const "V")); let "W" be ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Const "v")) ($#k6_domain_1 :::"}"::: ) )); assume (Bool (Set (Const "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Const "V")))) ; func :::"coeffFunctional"::: "(" "v" "," "W" ")" -> bbbadV3_FUNCT_1() ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_subset_1 :::"linear-Functional":::) "of" "V" means :: VECTSP10:def 8 (Bool "(" (Bool (Set it ($#k3_funct_2 :::"."::: ) "v") ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) "K")) & (Bool (Set it ($#k5_relset_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W")) ($#r1_hidden :::"="::: ) (Set ($#k7_hahnban1 :::"0Functional"::: ) "W")) ")" ); end; :: deftheorem defines :::"coeffFunctional"::: VECTSP10:def 8 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "for" (Set (Var "b5")) "being" bbbadV3_FUNCT_1() ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k7_vectsp10 :::"coeffFunctional"::: ) "(" (Set (Var "v")) "," (Set (Var "W")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "b5")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K")))) & (Bool (Set (Set (Var "b5")) ($#k5_relset_1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W")))) ($#r1_hidden :::"="::: ) (Set ($#k7_hahnban1 :::"0Functional"::: ) (Set (Var "W")))) ")" ) ")" )))))); theorem :: VECTSP10:28 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" bbbadV3_FUNCT_1() ($#v2_hahnban1 :::"0-preserving"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ))))) ; theorem :: VECTSP10:29 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool (Set (Set "(" ($#k7_vectsp10 :::"coeffFunctional"::: ) "(" (Set (Var "v")) "," (Set (Var "W")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a")))))))) ; theorem :: VECTSP10:30 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set (Var "w")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W")))) "holds" (Bool (Set (Set "(" ($#k7_vectsp10 :::"coeffFunctional"::: ) "(" (Set (Var "v")) "," (Set (Var "W")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))))) ; theorem :: VECTSP10:31 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set (Var "w")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W")))) "holds" (Bool (Set (Set "(" ($#k7_vectsp10 :::"coeffFunctional"::: ) "(" (Set (Var "v")) "," (Set (Var "W")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a")))))))) ; theorem :: VECTSP10:32 (Bool "for" (Set (Var "K")) "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 "K")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k5_hahnban1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ))))))) ; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); cluster (Set "V" ($#k8_hahnban1 :::"*'"::: ) ) -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ; end; begin definitionlet "K" 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 "K")); let "f" be ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); func :::"ker"::: "f" -> ($#m1_subset_1 :::"Subset":::) "of" "V" equals :: VECTSP10:def 9 "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Vector":::) "of" "V" : (Bool (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "K")) "}" ; end; :: deftheorem defines :::"ker"::: VECTSP10:def 9 : (Bool "for" (Set (Var "K")) "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 "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k8_vectsp10 :::"ker"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) : (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) "}" )))); registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v2_hahnban1 :::"0-preserving"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); cluster (Set ($#k8_vectsp10 :::"ker"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: VECTSP10:33 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#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"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k8_vectsp10 :::"ker"::: ) (Set (Var "f"))) "is" ($#v1_vectsp_4 :::"linearly-closed"::: ) )))) ; definitionlet "K" 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 "K")); let "f" be ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); attr "f" is :::"degenerated"::: means :: VECTSP10:def 10 (Bool (Set ($#k8_vectsp10 :::"ker"::: ) "f") ($#r1_hidden :::"<>"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "V" ")" ) ($#k6_domain_1 :::"}"::: ) )); end; :: deftheorem defines :::"degenerated"::: VECTSP10:def 10 : (Bool "for" (Set (Var "K")) "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 "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_vectsp10 :::"degenerated"::: ) ) "iff" (Bool (Set ($#k8_vectsp10 :::"ker"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ")" )))); registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v2_hahnban1 :::"0-preserving"::: ) ($#~v2_vectsp10 "non" ($#v2_vectsp10 :::"degenerated"::: ) ) -> ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "K" 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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Const "V")); func :::"Ker"::: "f" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" "V" means :: VECTSP10:def 11 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k8_vectsp10 :::"ker"::: ) "f")); end; :: deftheorem defines :::"Ker"::: VECTSP10:def 11 : (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "b4")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k9_vectsp10 :::"Ker"::: ) (Set (Var "f")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k8_vectsp10 :::"ker"::: ) (Set (Var "f")))) ")" ))))); definitionlet "K" 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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); let "f" be ($#v13_vectsp_1 :::"additive"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); assume (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "W"))) ($#r1_tarski :::"c="::: ) (Set ($#k8_vectsp10 :::"ker"::: ) (Set (Const "f")))) ; func :::"QFunctional"::: "(" "f" "," "W" ")" -> ($#v13_vectsp_1 :::"additive"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" "V" "," "W" ")" ")" ) means :: VECTSP10:def 12 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" "V" "," "W" ")" ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_vectsp_4 :::"+"::: ) "W"))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "a")))))); end; :: deftheorem defines :::"QFunctional"::: VECTSP10:def 12 : (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#v13_vectsp_1 :::"additive"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#r1_tarski :::"c="::: ) (Set ($#k8_vectsp10 :::"ker"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#v13_vectsp_1 :::"additive"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k10_vectsp10 :::"QFunctional"::: ) "(" (Set (Var "f")) "," (Set (Var "W")) ")" )) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_vectsp_4 :::"+"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k3_funct_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")))))) ")" )))))); theorem :: VECTSP10:34 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#r1_tarski :::"c="::: ) (Set ($#k8_vectsp10 :::"ker"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k10_vectsp10 :::"QFunctional"::: ) "(" (Set (Var "f")) "," (Set (Var "W")) ")" ) "is" ($#v1_hahnban1 :::"homogeneous"::: ) ))))) ; definitionlet "K" 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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Const "V")); func :::"CQFunctional"::: "f" -> ($#m1_subset_1 :::"linear-Functional":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" "V" "," (Set "(" ($#k9_vectsp10 :::"Ker"::: ) "f" ")" ) ")" ")" ) equals :: VECTSP10:def 13 (Set ($#k10_vectsp10 :::"QFunctional"::: ) "(" "f" "," (Set "(" ($#k9_vectsp10 :::"Ker"::: ) "f" ")" ) ")" ); end; :: deftheorem defines :::"CQFunctional"::: VECTSP10:def 13 : (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k11_vectsp10 :::"CQFunctional"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k10_vectsp10 :::"QFunctional"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k9_vectsp10 :::"Ker"::: ) (Set (Var "f")) ")" ) ")" ))))); theorem :: VECTSP10:35 (Bool "for" (Set (Var "K")) "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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "V")) "," (Set "(" ($#k9_vectsp10 :::"Ker"::: ) (Set (Var "f")) ")" ) ")" ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_vectsp_4 :::"+"::: ) (Set "(" ($#k9_vectsp10 :::"Ker"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" ($#k11_vectsp10 :::"CQFunctional"::: ) (Set (Var "f")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))))))))) ; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be bbbadV3_FUNCT_1() ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Const "V")); cluster (Set ($#k11_vectsp10 :::"CQFunctional"::: ) "f") -> bbbadV3_FUNCT_1() ; end; registrationlet "K" 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"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Const "V")); cluster (Set ($#k11_vectsp10 :::"CQFunctional"::: ) "f") -> ($#~v2_vectsp10 "non" ($#v2_vectsp10 :::"degenerated"::: ) ) ; end;