:: BILINEAR semantic presentation begin definitionlet "K" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "V", "W" be ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); mode Form of "V" "," "W" is ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K"); end; definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "V", "W" be ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); func :::"NulForm"::: "(" "V" "," "W" ")" -> ($#m1_subset_1 :::"Form":::) "of" "V" "," "W" equals :: BILINEAR:def 1 (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k2_zfmisc_1 :::":]"::: ) ) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "K" ")" )); end; :: deftheorem defines :::"NulForm"::: BILINEAR:def 1 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) "holds" (Bool (Set ($#k1_bilinear :::"NulForm"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ))))); definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f", "g" be ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); func "f" :::"+"::: "g" -> ($#m1_subset_1 :::"Form":::) "of" "V" "," "W" means :: BILINEAR:def 2 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" "W" "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" "g" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ))))); end; :: deftheorem defines :::"+"::: BILINEAR:def 2 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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")) "," (Set (Var "b6")) "being" ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_bilinear :::"+"::: ) (Set (Var "g")))) "iff" (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")) "holds" (Bool (Set (Set (Var "b6")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ))))) ")" )))); definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); func "a" :::"*"::: "f" -> ($#m1_subset_1 :::"Form":::) "of" "V" "," "W" means :: BILINEAR:def 3 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" "W" "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set "a" ($#k6_algstr_0 :::"*"::: ) (Set "(" "f" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ))))); end; :: deftheorem defines :::"*"::: BILINEAR:def 3 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_bilinear :::"*"::: ) (Set (Var "f")))) "iff" (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")) "holds" (Bool (Set (Set (Var "b6")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ))))) ")" )))))); definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); func :::"-"::: "f" -> ($#m1_subset_1 :::"Form":::) "of" "V" "," "W" means :: BILINEAR:def 4 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" "W" "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" "f" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ))))); end; :: deftheorem defines :::"-"::: BILINEAR:def 4 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "f")) "," (Set (Var "b5")) "being" ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k4_bilinear :::"-"::: ) (Set (Var "f")))) "iff" (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")) "holds" (Bool (Set (Set (Var "b5")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ))))) ")" )))); 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"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); redefine func :::"-"::: "f" equals :: BILINEAR:def 5 (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) "K" ")" ) ")" ) ($#k3_bilinear :::"*"::: ) "f"); end; :: deftheorem defines :::"-"::: BILINEAR:def 5 : (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"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set ($#k4_bilinear :::"-"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "K")) ")" ) ")" ) ($#k3_bilinear :::"*"::: ) (Set (Var "f"))))))); definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f", "g" be ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); func "f" :::"-"::: "g" -> ($#m1_subset_1 :::"Form":::) "of" "V" "," "W" equals :: BILINEAR:def 6 (Set "f" ($#k2_bilinear :::"+"::: ) (Set "(" ($#k4_bilinear :::"-"::: ) "g" ")" )); end; :: deftheorem defines :::"-"::: BILINEAR:def 6 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set (Set (Var "f")) ($#k5_bilinear :::"-"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_bilinear :::"+"::: ) (Set "(" ($#k4_bilinear :::"-"::: ) (Set (Var "g")) ")" )))))); definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f", "g" be ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); redefine func "f" :::"-"::: "g" means :: BILINEAR:def 7 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" "W" "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" "g" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ))))); end; :: deftheorem defines :::"-"::: BILINEAR:def 7 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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")) "," (Set (Var "b6")) "being" ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k5_bilinear :::"-"::: ) (Set (Var "g")))) "iff" (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")) "holds" (Bool (Set (Set (Var "b6")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ))))) ")" )))); definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f", "g" be ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); :: original: :::"+"::: redefine func "f" :::"+"::: "g" -> ($#m1_subset_1 :::"Form":::) "of" "V" "," "W"; commutativity (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")) "holds" (Bool (Set (Set (Var "f")) ($#k2_bilinear :::"+"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k2_bilinear :::"+"::: ) (Set (Var "f"))))) ; end; theorem :: BILINEAR:1 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set (Set (Var "f")) ($#k2_bilinear :::"+"::: ) (Set "(" ($#k1_bilinear :::"NulForm"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "f")))))) ; theorem :: BILINEAR:2 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_bilinear :::"+"::: ) (Set (Var "g")) ")" ) ($#k2_bilinear :::"+"::: ) (Set (Var "h"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k2_bilinear :::"+"::: ) (Set "(" (Set (Var "g")) ($#k2_bilinear :::"+"::: ) (Set (Var "h")) ")" )))))) ; theorem :: BILINEAR:3 (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"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set (Set (Var "f")) ($#k5_bilinear :::"-"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set ($#k1_bilinear :::"NulForm"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ))))) ; theorem :: BILINEAR:4 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set (Set (Var "a")) ($#k3_bilinear :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_bilinear :::"+"::: ) (Set (Var "g")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_bilinear :::"*"::: ) (Set (Var "f")) ")" ) ($#k2_bilinear :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_bilinear :::"*"::: ) (Set (Var "g")) ")" ))))))) ; theorem :: BILINEAR:5 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_bilinear :::"*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_bilinear :::"*"::: ) (Set (Var "f")) ")" ) ($#k2_bilinear :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_bilinear :::"*"::: ) (Set (Var "f")) ")" ))))))) ; theorem :: BILINEAR:6 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_bilinear :::"*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k3_bilinear :::"*"::: ) (Set "(" (Set (Var "b")) ($#k3_bilinear :::"*"::: ) (Set (Var "f")) ")" ))))))) ; theorem :: BILINEAR:7 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "K")) ")" ) ($#k3_bilinear :::"*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f")))))) ; begin definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); let "v" be ($#m1_subset_1 :::"Vector":::) "of" (Set (Const "V")); func :::"FunctionalFAF"::: "(" "f" "," "v" ")" -> ($#m1_subset_1 :::"Functional":::) "of" "W" equals :: BILINEAR:def 8 (Set (Set "(" ($#k11_funct_5 :::"curry"::: ) "f" ")" ) ($#k10_funct_5 :::"."::: ) "v"); end; :: deftheorem defines :::"FunctionalFAF"::: BILINEAR:def 8 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set (Var "f")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_funct_5 :::"curry"::: ) (Set (Var "f")) ")" ) ($#k10_funct_5 :::"."::: ) (Set (Var "v")))))))); definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); let "w" be ($#m1_subset_1 :::"Vector":::) "of" (Set (Const "W")); func :::"FunctionalSAF"::: "(" "f" "," "w" ")" -> ($#m1_subset_1 :::"Functional":::) "of" "V" equals :: BILINEAR:def 9 (Set (Set "(" ($#k12_funct_5 :::"curry'"::: ) "f" ")" ) ($#k10_funct_5 :::"."::: ) "w"); end; :: deftheorem defines :::"FunctionalSAF"::: BILINEAR:def 9 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool (Set ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set (Var "f")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" ) ($#k10_funct_5 :::"."::: ) (Set (Var "w")))))))); theorem :: BILINEAR:8 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set (Var "f")) "," (Set (Var "v")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set (Var "f")) "," (Set (Var "v")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) & (Bool "(" "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool (Set (Set "(" ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set (Var "f")) "," (Set (Var "v")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" )) ")" ) ")" ))))) ; theorem :: BILINEAR:9 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set (Var "f")) "," (Set (Var "w")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set (Var "f")) "," (Set (Var "w")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set (Var "f")) "," (Set (Var "w")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" )) ")" ) ")" ))))) ; theorem :: BILINEAR:10 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set "(" ($#k1_bilinear :::"NulForm"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ")" ) "," (Set (Var "v")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k7_hahnban1 :::"0Functional"::: ) (Set (Var "W"))))))) ; theorem :: BILINEAR:11 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool (Set ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set "(" ($#k1_bilinear :::"NulForm"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ")" ) "," (Set (Var "w")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k7_hahnban1 :::"0Functional"::: ) (Set (Var "V"))))))) ; theorem :: BILINEAR:12 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool (Set ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set "(" (Set (Var "f")) ($#k2_bilinear :::"+"::: ) (Set (Var "g")) ")" ) "," (Set (Var "w")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set (Var "f")) "," (Set (Var "w")) ")" ")" ) ($#k3_hahnban1 :::"+"::: ) (Set "(" ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set (Var "g")) "," (Set (Var "w")) ")" ")" ))))))) ; theorem :: BILINEAR:13 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set "(" (Set (Var "f")) ($#k2_bilinear :::"+"::: ) (Set (Var "g")) ")" ) "," (Set (Var "v")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set (Var "f")) "," (Set (Var "v")) ")" ")" ) ($#k3_hahnban1 :::"+"::: ) (Set "(" ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set (Var "g")) "," (Set (Var "v")) ")" ")" ))))))) ; theorem :: BILINEAR:14 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool (Set ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set "(" (Set (Var "a")) ($#k3_bilinear :::"*"::: ) (Set (Var "f")) ")" ) "," (Set (Var "w")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k6_hahnban1 :::"*"::: ) (Set "(" ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set (Var "f")) "," (Set (Var "w")) ")" ")" )))))))) ; theorem :: BILINEAR:15 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set "(" (Set (Var "a")) ($#k3_bilinear :::"*"::: ) (Set (Var "f")) ")" ) "," (Set (Var "v")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k6_hahnban1 :::"*"::: ) (Set "(" ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set (Var "f")) "," (Set (Var "v")) ")" ")" )))))))) ; theorem :: BILINEAR:16 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool (Set ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set "(" ($#k4_bilinear :::"-"::: ) (Set (Var "f")) ")" ) "," (Set (Var "w")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_hahnban1 :::"-"::: ) (Set "(" ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set (Var "f")) "," (Set (Var "w")) ")" ")" ))))))) ; theorem :: BILINEAR:17 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set "(" ($#k4_bilinear :::"-"::: ) (Set (Var "f")) ")" ) "," (Set (Var "v")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_hahnban1 :::"-"::: ) (Set "(" ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set (Var "f")) "," (Set (Var "v")) ")" ")" ))))))) ; theorem :: BILINEAR:18 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool (Set ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set "(" (Set (Var "f")) ($#k5_bilinear :::"-"::: ) (Set (Var "g")) ")" ) "," (Set (Var "w")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set (Var "f")) "," (Set (Var "w")) ")" ")" ) ($#k5_hahnban1 :::"-"::: ) (Set "(" ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set (Var "g")) "," (Set (Var "w")) ")" ")" ))))))) ; theorem :: BILINEAR:19 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set "(" (Set (Var "f")) ($#k5_bilinear :::"-"::: ) (Set (Var "g")) ")" ) "," (Set (Var "v")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set (Var "f")) "," (Set (Var "v")) ")" ")" ) ($#k5_hahnban1 :::"-"::: ) (Set "(" ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set (Var "g")) "," (Set (Var "v")) ")" ")" ))))))) ; begin definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "V", "W" 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")); let "g" be ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "W")); func :::"FormFunctional"::: "(" "f" "," "g" ")" -> ($#m1_subset_1 :::"Form":::) "of" "V" "," "W" means :: BILINEAR:def 10 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" "W" "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" "g" ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ))))); end; :: deftheorem defines :::"FormFunctional"::: BILINEAR:def 10 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )) "iff" (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")) "holds" (Bool (Set (Set (Var "b6")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ))))) ")" )))))); theorem :: BILINEAR:20 (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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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")) (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")) "holds" (Bool (Set (Set "(" ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k7_hahnban1 :::"0Functional"::: ) (Set (Var "W")) ")" ) ")" ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))))))) ; theorem :: BILINEAR:21 (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"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "W")) (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")) "holds" (Bool (Set (Set "(" ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set "(" ($#k7_hahnban1 :::"0Functional"::: ) (Set (Var "V")) ")" ) "," (Set (Var "g")) ")" ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))))))) ; theorem :: BILINEAR:22 (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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k7_hahnban1 :::"0Functional"::: ) (Set (Var "W")) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k1_bilinear :::"NulForm"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ))))) ; theorem :: BILINEAR:23 (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"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "W")) "holds" (Bool (Set ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set "(" ($#k7_hahnban1 :::"0Functional"::: ) (Set (Var "V")) ")" ) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k1_bilinear :::"NulForm"::: ) "(" (Set (Var "V")) "," (Set (Var "W")) ")" ))))) ; theorem :: BILINEAR:24 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set "(" ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set (Var "v")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k6_hahnban1 :::"*"::: ) (Set (Var "g"))))))))) ; theorem :: BILINEAR:25 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool (Set ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set "(" ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set (Var "w")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ) ($#k6_hahnban1 :::"*"::: ) (Set (Var "f"))))))))) ; begin definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); attr "f" is :::"additiveFAF"::: means :: BILINEAR:def 11 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "holds" (Bool (Set ($#k7_bilinear :::"FunctionalFAF"::: ) "(" "f" "," (Set (Var "v")) ")" ) "is" ($#v13_vectsp_1 :::"additive"::: ) )); attr "f" is :::"additiveSAF"::: means :: BILINEAR:def 12 (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" "W" "holds" (Bool (Set ($#k8_bilinear :::"FunctionalSAF"::: ) "(" "f" "," (Set (Var "w")) ")" ) "is" ($#v13_vectsp_1 :::"additive"::: ) )); end; :: deftheorem defines :::"additiveFAF"::: BILINEAR:def 11 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_bilinear :::"additiveFAF"::: ) ) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set (Var "f")) "," (Set (Var "v")) ")" ) "is" ($#v13_vectsp_1 :::"additive"::: ) )) ")" )))); :: deftheorem defines :::"additiveSAF"::: BILINEAR:def 12 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_bilinear :::"additiveSAF"::: ) ) "iff" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool (Set ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set (Var "f")) "," (Set (Var "w")) ")" ) "is" ($#v13_vectsp_1 :::"additive"::: ) )) ")" )))); definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); attr "f" is :::"homogeneousFAF"::: means :: BILINEAR:def 13 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "holds" (Bool (Set ($#k7_bilinear :::"FunctionalFAF"::: ) "(" "f" "," (Set (Var "v")) ")" ) "is" ($#v1_hahnban1 :::"homogeneous"::: ) )); attr "f" is :::"homogeneousSAF"::: means :: BILINEAR:def 14 (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" "W" "holds" (Bool (Set ($#k8_bilinear :::"FunctionalSAF"::: ) "(" "f" "," (Set (Var "w")) ")" ) "is" ($#v1_hahnban1 :::"homogeneous"::: ) )); end; :: deftheorem defines :::"homogeneousFAF"::: BILINEAR:def 13 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_bilinear :::"homogeneousFAF"::: ) ) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k7_bilinear :::"FunctionalFAF"::: ) "(" (Set (Var "f")) "," (Set (Var "v")) ")" ) "is" ($#v1_hahnban1 :::"homogeneous"::: ) )) ")" )))); :: deftheorem defines :::"homogeneousSAF"::: BILINEAR:def 14 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_bilinear :::"homogeneousSAF"::: ) ) "iff" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool (Set ($#k8_bilinear :::"FunctionalSAF"::: ) "(" (Set (Var "f")) "," (Set (Var "w")) ")" ) "is" ($#v1_hahnban1 :::"homogeneous"::: ) )) ")" )))); registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); cluster (Set ($#k1_bilinear :::"NulForm"::: ) "(" "V" "," "W" ")" ) -> ($#v1_bilinear :::"additiveFAF"::: ) ; cluster (Set ($#k1_bilinear :::"NulForm"::: ) "(" "V" "," "W" ")" ) -> ($#v2_bilinear :::"additiveSAF"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k2_zfmisc_1 :::":]"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k2_zfmisc_1 :::":]"::: ) )) bbbadV1_FUNCT_2((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")) ($#v1_bilinear :::"additiveFAF"::: ) ($#v2_bilinear :::"additiveSAF"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k2_zfmisc_1 :::":]"::: ) ) "," (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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); cluster (Set ($#k1_bilinear :::"NulForm"::: ) "(" "V" "," "W" ")" ) -> ($#v3_bilinear :::"homogeneousFAF"::: ) ; cluster (Set ($#k1_bilinear :::"NulForm"::: ) "(" "V" "," "W" ")" ) -> ($#v4_bilinear :::"homogeneousSAF"::: ) ; 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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k2_zfmisc_1 :::":]"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k2_zfmisc_1 :::":]"::: ) )) bbbadV1_FUNCT_2((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")) ($#v1_bilinear :::"additiveFAF"::: ) ($#v2_bilinear :::"additiveSAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k2_zfmisc_1 :::":]"::: ) ) "," (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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); mode bilinear-Form of "V" "," "W" is ($#v1_bilinear :::"additiveFAF"::: ) ($#v2_bilinear :::"additiveSAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" "V" "," "W"; 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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v1_bilinear :::"additiveFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); let "v" be ($#m1_subset_1 :::"Vector":::) "of" (Set (Const "V")); cluster (Set ($#k7_bilinear :::"FunctionalFAF"::: ) "(" "f" "," "v" ")" ) -> ($#v13_vectsp_1 :::"additive"::: ) ; 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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v2_bilinear :::"additiveSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); let "w" be ($#m1_subset_1 :::"Vector":::) "of" (Set (Const "W")); cluster (Set ($#k8_bilinear :::"FunctionalSAF"::: ) "(" "f" "," "w" ")" ) -> ($#v13_vectsp_1 :::"additive"::: ) ; 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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); let "v" be ($#m1_subset_1 :::"Vector":::) "of" (Set (Const "V")); cluster (Set ($#k7_bilinear :::"FunctionalFAF"::: ) "(" "f" "," "v" ")" ) -> ($#v1_hahnban1 :::"homogeneous"::: ) ; 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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); let "w" be ($#m1_subset_1 :::"Vector":::) "of" (Set (Const "W")); cluster (Set ($#k8_bilinear :::"FunctionalSAF"::: ) "(" "f" "," "w" ")" ) -> ($#v1_hahnban1 :::"homogeneous"::: ) ; 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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" 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")); let "g" be ($#v13_vectsp_1 :::"additive"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "W")); cluster (Set ($#k9_bilinear :::"FormFunctional"::: ) "(" "f" "," "g" ")" ) -> ($#v1_bilinear :::"additiveFAF"::: ) ; 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"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v13_vectsp_1 :::"additive"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); let "g" be ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "W")); cluster (Set ($#k9_bilinear :::"FormFunctional"::: ) "(" "f" "," "g" ")" ) -> ($#v2_bilinear :::"additiveSAF"::: ) ; 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_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" 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")); let "g" be ($#v1_hahnban1 :::"homogeneous"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "W")); cluster (Set ($#k9_bilinear :::"FormFunctional"::: ) "(" "f" "," "g" ")" ) -> ($#v3_bilinear :::"homogeneousFAF"::: ) ; 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_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v1_hahnban1 :::"homogeneous"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); let "g" be ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "W")); cluster (Set ($#k9_bilinear :::"FormFunctional"::: ) "(" "f" "," "g" ")" ) -> ($#v4_bilinear :::"homogeneousSAF"::: ) ; end; 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")); let "W" 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")); let "g" be ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "W")); cluster (Set ($#k9_bilinear :::"FormFunctional"::: ) "(" "f" "," "g" ")" ) -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ; end; 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 ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "W" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); let "g" be ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "W")); cluster (Set ($#k9_bilinear :::"FormFunctional"::: ) "(" "f" "," "g" ")" ) -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ; end; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "V", "W" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be bbbadV3_FUNCT_1() ($#v2_hahnban1 :::"0-preserving"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); let "g" be bbbadV3_FUNCT_1() ($#v2_hahnban1 :::"0-preserving"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "W")); cluster (Set ($#k9_bilinear :::"FormFunctional"::: ) "(" "f" "," "g" ")" ) -> ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ; end; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "V", "W" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k2_zfmisc_1 :::":]"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) bbbadV1_PARTFUN1((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k2_zfmisc_1 :::":]"::: ) )) bbbadV1_FUNCT_2((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")) ($#v1_bilinear :::"additiveFAF"::: ) ($#v2_bilinear :::"additiveSAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f", "g" be ($#v2_bilinear :::"additiveSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set "f" ($#k2_bilinear :::"+"::: ) "g") -> ($#v2_bilinear :::"additiveSAF"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f", "g" be ($#v1_bilinear :::"additiveFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set "f" ($#k2_bilinear :::"+"::: ) "g") -> ($#v1_bilinear :::"additiveFAF"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v2_bilinear :::"additiveSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); cluster (Set "a" ($#k3_bilinear :::"*"::: ) "f") -> ($#v2_bilinear :::"additiveSAF"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v1_bilinear :::"additiveFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); cluster (Set "a" ($#k3_bilinear :::"*"::: ) "f") -> ($#v1_bilinear :::"additiveFAF"::: ) ; 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"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v2_bilinear :::"additiveSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set ($#k4_bilinear :::"-"::: ) "f") -> ($#v2_bilinear :::"additiveSAF"::: ) ; 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"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v1_bilinear :::"additiveFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set ($#k4_bilinear :::"-"::: ) "f") -> ($#v1_bilinear :::"additiveFAF"::: ) ; 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"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f", "g" be ($#v2_bilinear :::"additiveSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set "f" ($#k5_bilinear :::"-"::: ) "g") -> ($#v2_bilinear :::"additiveSAF"::: ) ; 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"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f", "g" be ($#v1_bilinear :::"additiveFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set "f" ($#k5_bilinear :::"-"::: ) "g") -> ($#v1_bilinear :::"additiveFAF"::: ) ; 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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f", "g" be ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set "f" ($#k2_bilinear :::"+"::: ) "g") -> ($#v4_bilinear :::"homogeneousSAF"::: ) ; 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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f", "g" be ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set "f" ($#k2_bilinear :::"+"::: ) "g") -> ($#v3_bilinear :::"homogeneousFAF"::: ) ; 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_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); cluster (Set "a" ($#k3_bilinear :::"*"::: ) "f") -> ($#v4_bilinear :::"homogeneousSAF"::: ) ; 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_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); cluster (Set "a" ($#k3_bilinear :::"*"::: ) "f") -> ($#v3_bilinear :::"homogeneousFAF"::: ) ; 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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set ($#k4_bilinear :::"-"::: ) "f") -> ($#v4_bilinear :::"homogeneousSAF"::: ) ; 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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set ($#k4_bilinear :::"-"::: ) "f") -> ($#v3_bilinear :::"homogeneousFAF"::: ) ; 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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f", "g" be ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set "f" ($#k5_bilinear :::"-"::: ) "g") -> ($#v4_bilinear :::"homogeneousSAF"::: ) ; 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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f", "g" be ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set "f" ($#k5_bilinear :::"-"::: ) "g") -> ($#v3_bilinear :::"homogeneousFAF"::: ) ; end; theorem :: BILINEAR:26 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_bilinear :::"additiveSAF"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "u")) ")" ) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "w")) ")" ")" )))))))) ; theorem :: BILINEAR:27 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_bilinear :::"additiveFAF"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set "(" (Set (Var "u")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "u")) ")" ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" )))))))) ; theorem :: BILINEAR:28 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "f")) "being" ($#v1_bilinear :::"additiveFAF"::: ) ($#v2_bilinear :::"additiveSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "u")) ")" ) "," (Set "(" (Set (Var "w")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "t")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "t")) ")" ")" ) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "w")) ")" ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "t")) ")" ")" ) ")" )))))))) ; theorem :: BILINEAR:29 (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")) "," (Set (Var "W")) "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" ($#v1_bilinear :::"additiveFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "W")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))))) ; theorem :: BILINEAR:30 (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")) "," (Set (Var "W")) "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_bilinear :::"additiveSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))))) ; theorem :: BILINEAR:31 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (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")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v4_bilinear :::"homogeneousSAF"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v")) ")" ) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ))))))))) ; theorem :: BILINEAR:32 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (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")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_bilinear :::"homogeneousFAF"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "w")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ))))))))) ; theorem :: BILINEAR: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"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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" ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))))) ; theorem :: BILINEAR:34 (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 "V")) "," (Set (Var "W")) "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" ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "W")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))))) ; theorem :: BILINEAR: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")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "f")) "being" ($#v2_bilinear :::"additiveSAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" ) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "w")) ")" ")" )))))))) ; theorem :: BILINEAR:36 (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")) "," (Set (Var "W")) "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 "w")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "f")) "being" ($#v1_bilinear :::"additiveFAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set "(" (Set (Var "w")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "t")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "t")) ")" ")" )))))))) ; theorem :: BILINEAR:37 (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")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" ) "," (Set "(" (Set (Var "w")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "t")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "t")) ")" ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "w")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "t")) ")" ")" ) ")" )))))))) ; theorem :: BILINEAR:38 (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")) "," (Set (Var "W")) "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")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "u")) ")" ) ")" ) "," (Set "(" (Set (Var "w")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "t")) ")" ")" ) ")" ) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "t")) ")" ")" ) ")" ) ")" ) ")" ))))))))) ; theorem :: BILINEAR:39 (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")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "u")) ")" ) ")" ) "," (Set "(" (Set (Var "w")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "t")) ")" ")" ) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "w")) ")" ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "u")) "," (Set (Var "t")) ")" ")" ) ")" ) ")" ) ")" ))))))))) ; theorem :: BILINEAR:40 (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")) "," (Set (Var "W")) "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" ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "st" (Bool (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_bilinear :::"additiveFAF"::: ) ) "or" (Bool (Set (Var "f")) "is" ($#v2_bilinear :::"additiveSAF"::: ) ) ")" )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_funct_1 :::"constant"::: ) ) "iff" (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")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))) ")" )))) ; begin definitionlet "K" be ($#l2_struct_0 :::"ZeroStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); func :::"leftker"::: "f" -> ($#m1_subset_1 :::"Subset":::) "of" "V" equals :: BILINEAR:def 15 "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Vector":::) "of" "V" : (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" "W" "holds" (Bool (Set "f" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "K"))) "}" ; end; :: deftheorem defines :::"leftker"::: BILINEAR:def 15 : (Bool "for" (Set (Var "K")) "being" ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set ($#k10_bilinear :::"leftker"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) : (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) "}" )))); definitionlet "K" be ($#l2_struct_0 :::"ZeroStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); func :::"rightker"::: "f" -> ($#m1_subset_1 :::"Subset":::) "of" "W" equals :: BILINEAR:def 16 "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Vector":::) "of" "W" : (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "holds" (Bool (Set "f" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "K"))) "}" ; end; :: deftheorem defines :::"rightker"::: BILINEAR:def 16 : (Bool "for" (Set (Var "K")) "being" ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set ($#k11_bilinear :::"rightker"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) : (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) "}" )))); definitionlet "K" be ($#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 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); func :::"diagker"::: "f" -> ($#m1_subset_1 :::"Subset":::) "of" "V" equals :: BILINEAR:def 17 "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Vector":::) "of" "V" : (Bool (Set "f" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "K")) "}" ; end; :: deftheorem defines :::"diagker"::: BILINEAR:def 17 : (Bool "for" (Set (Var "K")) "being" ($#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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds" (Bool (Set ($#k12_bilinear :::"diagker"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "v")) where v "is" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) : (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) "}" )))); 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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#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 "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v2_bilinear :::"additiveSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set ($#k10_bilinear :::"leftker"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; 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")); let "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set ($#k10_bilinear :::"leftker"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; 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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "W" 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 ($#v1_bilinear :::"additiveFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set ($#k11_bilinear :::"rightker"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; 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"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "W" 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")); let "f" be ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set ($#k11_bilinear :::"rightker"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; 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")); let "f" be ($#v1_bilinear :::"additiveFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); cluster (Set ($#k12_bilinear :::"diagker"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; 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")); let "f" be ($#v2_bilinear :::"additiveSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); cluster (Set ($#k12_bilinear :::"diagker"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; 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")); let "f" be ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); cluster (Set ($#k12_bilinear :::"diagker"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; 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")); let "f" be ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); cluster (Set ($#k12_bilinear :::"diagker"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: BILINEAR:41 (Bool "for" (Set (Var "K")) "being" ($#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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k10_bilinear :::"leftker"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k12_bilinear :::"diagker"::: ) (Set (Var "f")))) & (Bool (Set ($#k11_bilinear :::"rightker"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k12_bilinear :::"diagker"::: ) (Set (Var "f")))) ")" )))) ; theorem :: BILINEAR:42 (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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#v2_bilinear :::"additiveSAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set ($#k10_bilinear :::"leftker"::: ) (Set (Var "f"))) "is" ($#v1_vectsp_4 :::"linearly-closed"::: ) )))) ; theorem :: BILINEAR:43 (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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#v1_bilinear :::"additiveFAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set ($#k11_bilinear :::"rightker"::: ) (Set (Var "f"))) "is" ($#v1_vectsp_4 :::"linearly-closed"::: ) )))) ; 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 ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v2_bilinear :::"additiveSAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); func :::"LKer"::: "f" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" "V" means :: BILINEAR:def 18 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k10_bilinear :::"leftker"::: ) "f")); end; :: deftheorem defines :::"LKer"::: BILINEAR:def 18 : (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" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#v2_bilinear :::"additiveSAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "b5")) "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 "b5")) ($#r1_hidden :::"="::: ) (Set ($#k13_bilinear :::"LKer"::: ) (Set (Var "f")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set ($#k10_bilinear :::"leftker"::: ) (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 ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "W" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be ($#v1_bilinear :::"additiveFAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); func :::"RKer"::: "f" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" "W" means :: BILINEAR:def 19 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k11_bilinear :::"rightker"::: ) "f")); end; :: deftheorem defines :::"RKer"::: BILINEAR:def 19 : (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" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#v1_bilinear :::"additiveFAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "b5")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k14_bilinear :::"RKer"::: ) (Set (Var "f")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set ($#k11_bilinear :::"rightker"::: ) (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 ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v2_bilinear :::"additiveSAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); func :::"LQForm"::: "f" -> ($#v2_bilinear :::"additiveSAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" "V" "," (Set "(" ($#k13_bilinear :::"LKer"::: ) "f" ")" ) ")" ")" ) "," "W" means :: BILINEAR:def 20 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" "V" "," (Set "(" ($#k13_bilinear :::"LKer"::: ) "f" ")" ) ")" ")" ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" "W" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_vectsp_4 :::"+"::: ) (Set "(" ($#k13_bilinear :::"LKer"::: ) "f" ")" )))) "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set "f" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ))))); end; :: deftheorem defines :::"LQForm"::: BILINEAR:def 20 : (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" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#v2_bilinear :::"additiveSAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "b5")) "being" ($#v2_bilinear :::"additiveSAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "V")) "," (Set "(" ($#k13_bilinear :::"LKer"::: ) (Set (Var "f")) ")" ) ")" ")" ) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k15_bilinear :::"LQForm"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "V")) "," (Set "(" ($#k13_bilinear :::"LKer"::: ) (Set (Var "f")) ")" ) ")" ")" ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (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 "(" ($#k13_bilinear :::"LKer"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "b5")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (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 ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "W" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be ($#v1_bilinear :::"additiveFAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); func :::"RQForm"::: "f" -> ($#v1_bilinear :::"additiveFAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" "V" "," (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" "W" "," (Set "(" ($#k14_bilinear :::"RKer"::: ) "f" ")" ) ")" ")" ) means :: BILINEAR:def 21 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" "W" "," (Set "(" ($#k14_bilinear :::"RKer"::: ) "f" ")" ) ")" ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" "W" "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k3_vectsp_4 :::"+"::: ) (Set "(" ($#k14_bilinear :::"RKer"::: ) "f" ")" )))) "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set "f" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ))))); end; :: deftheorem defines :::"RQForm"::: BILINEAR:def 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" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#v1_bilinear :::"additiveFAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "b5")) "being" ($#v1_bilinear :::"additiveFAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k14_bilinear :::"RKer"::: ) (Set (Var "f")) ")" ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k16_bilinear :::"RQForm"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k14_bilinear :::"RKer"::: ) (Set (Var "f")) ")" ) ")" ")" ) (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 "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k3_vectsp_4 :::"+"::: ) (Set "(" ($#k14_bilinear :::"RKer"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "b5")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ))))) ")" )))))); 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", "W" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set ($#k15_bilinear :::"LQForm"::: ) "f") -> ($#v1_bilinear :::"additiveFAF"::: ) ($#v2_bilinear :::"additiveSAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ; cluster (Set ($#k16_bilinear :::"RQForm"::: ) "f") -> ($#v1_bilinear :::"additiveFAF"::: ) ($#v2_bilinear :::"additiveSAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ; 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", "W" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); func :::"QForm"::: "f" -> ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" "V" "," (Set "(" ($#k13_bilinear :::"LKer"::: ) "f" ")" ) ")" ")" ) "," (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" "W" "," (Set "(" ($#k14_bilinear :::"RKer"::: ) "f" ")" ) ")" ")" ) means :: BILINEAR:def 22 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" "V" "," (Set "(" ($#k13_bilinear :::"LKer"::: ) "f" ")" ) ")" ")" ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" "W" "," (Set "(" ($#k14_bilinear :::"RKer"::: ) "f" ")" ) ")" ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" "W" "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_vectsp_4 :::"+"::: ) (Set "(" ($#k13_bilinear :::"LKer"::: ) "f" ")" ))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k3_vectsp_4 :::"+"::: ) (Set "(" ($#k14_bilinear :::"RKer"::: ) "f" ")" )))) "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set "f" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" )))))); end; :: deftheorem defines :::"QForm"::: BILINEAR:def 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")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "V")) "," (Set "(" ($#k13_bilinear :::"LKer"::: ) (Set (Var "f")) ")" ) ")" ")" ) "," (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k14_bilinear :::"RKer"::: ) (Set (Var "f")) ")" ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k17_bilinear :::"QForm"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "V")) "," (Set "(" ($#k13_bilinear :::"LKer"::: ) (Set (Var "f")) ")" ) ")" ")" ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set "(" ($#k6_vectsp10 :::"VectQuot"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k14_bilinear :::"RKer"::: ) (Set (Var "f")) ")" ) ")" ")" ) (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 "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k3_vectsp_4 :::"+"::: ) (Set "(" ($#k13_bilinear :::"LKer"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k3_vectsp_4 :::"+"::: ) (Set "(" ($#k14_bilinear :::"RKer"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "b5")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" )))))) ")" ))))); theorem :: BILINEAR:44 (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" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#v2_bilinear :::"additiveSAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set ($#k11_bilinear :::"rightker"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k11_bilinear :::"rightker"::: ) (Set "(" ($#k15_bilinear :::"LQForm"::: ) (Set (Var "f")) ")" ))))))) ; theorem :: BILINEAR:45 (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" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#v1_bilinear :::"additiveFAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set ($#k10_bilinear :::"leftker"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k10_bilinear :::"leftker"::: ) (Set "(" ($#k16_bilinear :::"RQForm"::: ) (Set (Var "f")) ")" ))))))) ; theorem :: BILINEAR:46 (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")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set ($#k14_bilinear :::"RKer"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k14_bilinear :::"RKer"::: ) (Set "(" ($#k15_bilinear :::"LQForm"::: ) (Set (Var "f")) ")" )))))) ; theorem :: BILINEAR:47 (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")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set ($#k13_bilinear :::"LKer"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k13_bilinear :::"LKer"::: ) (Set "(" ($#k16_bilinear :::"RQForm"::: ) (Set (Var "f")) ")" )))))) ; theorem :: BILINEAR:48 (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")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set ($#k17_bilinear :::"QForm"::: ) (Set (Var "f"))) ($#r1_funct_2 :::"="::: ) (Set ($#k16_bilinear :::"RQForm"::: ) (Set "(" ($#k15_bilinear :::"LQForm"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k17_bilinear :::"QForm"::: ) (Set (Var "f"))) ($#r1_funct_2 :::"="::: ) (Set ($#k15_bilinear :::"LQForm"::: ) (Set "(" ($#k16_bilinear :::"RQForm"::: ) (Set (Var "f")) ")" ))) ")" )))) ; theorem :: BILINEAR:49 (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")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set ($#k10_bilinear :::"leftker"::: ) (Set "(" ($#k17_bilinear :::"QForm"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_bilinear :::"leftker"::: ) (Set "(" ($#k16_bilinear :::"RQForm"::: ) (Set "(" ($#k15_bilinear :::"LQForm"::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool (Set ($#k11_bilinear :::"rightker"::: ) (Set "(" ($#k17_bilinear :::"QForm"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_bilinear :::"rightker"::: ) (Set "(" ($#k16_bilinear :::"RQForm"::: ) (Set "(" ($#k15_bilinear :::"LQForm"::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool (Set ($#k10_bilinear :::"leftker"::: ) (Set "(" ($#k17_bilinear :::"QForm"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_bilinear :::"leftker"::: ) (Set "(" ($#k15_bilinear :::"LQForm"::: ) (Set "(" ($#k16_bilinear :::"RQForm"::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool (Set ($#k11_bilinear :::"rightker"::: ) (Set "(" ($#k17_bilinear :::"QForm"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_bilinear :::"rightker"::: ) (Set "(" ($#k15_bilinear :::"LQForm"::: ) (Set "(" ($#k16_bilinear :::"RQForm"::: ) (Set (Var "f")) ")" ) ")" ))) ")" )))) ; theorem :: BILINEAR:50 (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"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "W")) "holds" (Bool (Set ($#k8_vectsp10 :::"ker"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_bilinear :::"leftker"::: ) (Set "(" ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ))))))) ; theorem :: BILINEAR:51 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"<>"::: ) (Set ($#k7_hahnban1 :::"0Functional"::: ) (Set (Var "W"))))) "holds" (Bool (Set ($#k10_bilinear :::"leftker"::: ) (Set "(" ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_vectsp10 :::"ker"::: ) (Set (Var "f")))))))) ; theorem :: BILINEAR:52 (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"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "W")) "holds" (Bool (Set ($#k8_vectsp10 :::"ker"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k11_bilinear :::"rightker"::: ) (Set "(" ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ))))))) ; theorem :: BILINEAR:53 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"<>"::: ) (Set ($#k7_hahnban1 :::"0Functional"::: ) (Set (Var "V"))))) "holds" (Bool (Set ($#k11_bilinear :::"rightker"::: ) (Set "(" ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_vectsp10 :::"ker"::: ) (Set (Var "g")))))))) ; theorem :: BILINEAR:54 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#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" ($#~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 :::"linear-Functional":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"<>"::: ) (Set ($#k7_hahnban1 :::"0Functional"::: ) (Set (Var "W"))))) "holds" (Bool "(" (Bool (Set ($#k13_bilinear :::"LKer"::: ) (Set "(" ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_vectsp10 :::"Ker"::: ) (Set (Var "f")))) & (Bool (Set ($#k15_bilinear :::"LQForm"::: ) (Set "(" ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set "(" ($#k11_vectsp10 :::"CQFunctional"::: ) (Set (Var "f")) ")" ) "," (Set (Var "g")) ")" )) ")" )))))) ; theorem :: BILINEAR:55 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#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"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"<>"::: ) (Set ($#k7_hahnban1 :::"0Functional"::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set ($#k14_bilinear :::"RKer"::: ) (Set "(" ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_vectsp10 :::"Ker"::: ) (Set (Var "g")))) & (Bool (Set ($#k16_bilinear :::"RQForm"::: ) (Set "(" ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k11_vectsp10 :::"CQFunctional"::: ) (Set (Var "g")) ")" ) ")" )) ")" )))))) ; theorem :: BILINEAR:56 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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() ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "g")) "being" bbbadV3_FUNCT_1() ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "W")) "holds" (Bool (Set ($#k17_bilinear :::"QForm"::: ) (Set "(" ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k9_bilinear :::"FormFunctional"::: ) "(" (Set "(" ($#k11_vectsp10 :::"CQFunctional"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k11_vectsp10 :::"CQFunctional"::: ) (Set (Var "g")) ")" ) ")" )))))) ; definitionlet "K" be ($#l2_struct_0 :::"ZeroStr"::: ) ; let "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); attr "f" is :::"degenerated-on-left"::: means :: BILINEAR:def 23 (Bool (Set ($#k10_bilinear :::"leftker"::: ) "f") ($#r1_hidden :::"<>"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "V" ")" ) ($#k6_domain_1 :::"}"::: ) )); attr "f" is :::"degenerated-on-right"::: means :: BILINEAR:def 24 (Bool (Set ($#k11_bilinear :::"rightker"::: ) "f") ($#r1_hidden :::"<>"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "W" ")" ) ($#k6_domain_1 :::"}"::: ) )); end; :: deftheorem defines :::"degenerated-on-left"::: BILINEAR:def 23 : (Bool "for" (Set (Var "K")) "being" ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_bilinear :::"degenerated-on-left"::: ) ) "iff" (Bool (Set ($#k10_bilinear :::"leftker"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ")" )))); :: deftheorem defines :::"degenerated-on-right"::: BILINEAR:def 24 : (Bool "for" (Set (Var "K")) "being" ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "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 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_bilinear :::"degenerated-on-right"::: ) ) "iff" (Bool (Set ($#k11_bilinear :::"rightker"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "W")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ")" )))); 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 "W" 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_bilinear :::"additiveSAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set ($#k15_bilinear :::"LQForm"::: ) "f") -> ($#v2_bilinear :::"additiveSAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ($#~v5_bilinear "non" ($#v5_bilinear :::"degenerated-on-left"::: ) ) ; 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 ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "W" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be ($#v1_bilinear :::"additiveFAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set ($#k16_bilinear :::"RQForm"::: ) "f") -> ($#v1_bilinear :::"additiveFAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#~v6_bilinear "non" ($#v6_bilinear :::"degenerated-on-right"::: ) ) ; 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", "W" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set ($#k17_bilinear :::"QForm"::: ) "f") -> ($#~v5_bilinear "non" ($#v5_bilinear :::"degenerated-on-left"::: ) ) ($#~v6_bilinear "non" ($#v6_bilinear :::"degenerated-on-right"::: ) ) ; 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", "W" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set ($#k16_bilinear :::"RQForm"::: ) (Set "(" ($#k15_bilinear :::"LQForm"::: ) "f" ")" )) -> ($#v1_bilinear :::"additiveFAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#~v5_bilinear "non" ($#v5_bilinear :::"degenerated-on-left"::: ) ) ($#~v6_bilinear "non" ($#v6_bilinear :::"degenerated-on-right"::: ) ) ; cluster (Set ($#k15_bilinear :::"LQForm"::: ) (Set "(" ($#k16_bilinear :::"RQForm"::: ) "f" ")" )) -> ($#v2_bilinear :::"additiveSAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ($#~v5_bilinear "non" ($#v5_bilinear :::"degenerated-on-left"::: ) ) ($#~v6_bilinear "non" ($#v6_bilinear :::"degenerated-on-right"::: ) ) ; end; registrationlet "K" be ($#l6_algstr_0 :::"Field":::); let "V", "W" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "K")); let "f" be ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set (Const "V")) "," (Set (Const "W")); cluster (Set ($#k17_bilinear :::"QForm"::: ) "f") -> ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) ; end; begin definitionlet "K" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "V" be ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); attr "f" is :::"symmetric"::: means :: BILINEAR:def 25 (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "holds" (Bool (Set "f" ($#k1_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_binop_1 :::"."::: ) "(" (Set (Var "w")) "," (Set (Var "v")) ")" ))); end; :: deftheorem defines :::"symmetric"::: BILINEAR:def 25 : (Bool "for" (Set (Var "K")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_bilinear :::"symmetric"::: ) ) "iff" (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "w")) "," (Set (Var "v")) ")" ))) ")" )))); definitionlet "K" be ($#l2_struct_0 :::"ZeroStr"::: ) ; let "V" be ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); attr "f" is :::"alternating"::: means :: BILINEAR:def 26 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "holds" (Bool (Set "f" ($#k1_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "K"))); end; :: deftheorem defines :::"alternating"::: BILINEAR:def 26 : (Bool "for" (Set (Var "K")) "being" ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "K")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_bilinear :::"alternating"::: ) ) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) ")" )))); 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 ($#k1_bilinear :::"NulForm"::: ) "(" "V" "," "V" ")" ) -> ($#v7_bilinear :::"symmetric"::: ) ; cluster (Set ($#k1_bilinear :::"NulForm"::: ) "(" "V" "," "V" ")" ) -> ($#v8_bilinear :::"alternating"::: ) ; 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 ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) )) bbbadV1_FUNCT_2((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")) ($#v7_bilinear :::"symmetric"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) )) bbbadV1_FUNCT_2((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")) ($#v8_bilinear :::"alternating"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) )) bbbadV1_FUNCT_2((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")) ($#v1_bilinear :::"additiveFAF"::: ) ($#v2_bilinear :::"additiveSAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ($#v7_bilinear :::"symmetric"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) )) bbbadV1_FUNCT_2((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")) ($#v1_bilinear :::"additiveFAF"::: ) ($#v2_bilinear :::"additiveSAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ($#v8_bilinear :::"alternating"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (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_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v3_funct_1 "non" ($#v3_funct_1 :::"constant"::: ) ) bbbadV1_PARTFUN1((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) )) bbbadV1_FUNCT_2((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")) ($#v1_bilinear :::"additiveFAF"::: ) ($#v2_bilinear :::"additiveSAF"::: ) ($#v3_bilinear :::"homogeneousFAF"::: ) ($#v4_bilinear :::"homogeneousSAF"::: ) ($#v7_bilinear :::"symmetric"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (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"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) )) bbbadV1_FUNCT_2((Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")) ($#v1_bilinear :::"additiveFAF"::: ) ($#v2_bilinear :::"additiveSAF"::: ) ($#v8_bilinear :::"alternating"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "K" 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 "K")); let "f", "g" be ($#v7_bilinear :::"symmetric"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); cluster (Set "f" ($#k2_bilinear :::"+"::: ) "g") -> ($#v7_bilinear :::"symmetric"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v7_bilinear :::"symmetric"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); cluster (Set "a" ($#k3_bilinear :::"*"::: ) "f") -> ($#v7_bilinear :::"symmetric"::: ) ; end; registrationlet "K" 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 "K")); let "f" be ($#v7_bilinear :::"symmetric"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); cluster (Set ($#k4_bilinear :::"-"::: ) "f") -> ($#v7_bilinear :::"symmetric"::: ) ; end; registrationlet "K" 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 "K")); let "f", "g" be ($#v7_bilinear :::"symmetric"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); cluster (Set "f" ($#k5_bilinear :::"-"::: ) "g") -> ($#v7_bilinear :::"symmetric"::: ) ; end; 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", "g" be ($#v8_bilinear :::"alternating"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); cluster (Set "f" ($#k2_bilinear :::"+"::: ) "g") -> ($#v8_bilinear :::"alternating"::: ) ; 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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v8_bilinear :::"alternating"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); let "a" be ($#m1_subset_1 :::"Scalar":::) "of" (Set (Const "K")); cluster (Set "a" ($#k3_bilinear :::"*"::: ) "f") -> ($#v8_bilinear :::"alternating"::: ) ; 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"::: ) ($#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 ($#v8_bilinear :::"alternating"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); cluster (Set ($#k4_bilinear :::"-"::: ) "f") -> ($#v8_bilinear :::"alternating"::: ) ; 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"::: ) ($#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", "g" be ($#v8_bilinear :::"alternating"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); cluster (Set "f" ($#k5_bilinear :::"-"::: ) "g") -> ($#v8_bilinear :::"alternating"::: ) ; end; theorem :: BILINEAR:57 (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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (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" ($#v7_bilinear :::"symmetric"::: ) ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds" (Bool (Set ($#k10_bilinear :::"leftker"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k11_bilinear :::"rightker"::: ) (Set (Var "f"))))))) ; theorem :: BILINEAR:58 (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"::: ) ($#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")) "being" ($#v1_bilinear :::"additiveFAF"::: ) ($#v2_bilinear :::"additiveSAF"::: ) ($#v8_bilinear :::"alternating"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "V")) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "w")) "," (Set (Var "v")) ")" ")" ))))))) ; definitionlet "K" be ($#v12_vectsp_1 :::"Fanoian"::: ) ($#l6_algstr_0 :::"Field":::); let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "K")); let "f" be ($#v1_bilinear :::"additiveFAF"::: ) ($#v2_bilinear :::"additiveSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Const "V")) "," (Set (Const "V")); redefine attr "f" is :::"alternating"::: means :: BILINEAR:def 27 (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" "V" "holds" (Bool (Set "f" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" "f" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "w")) "," (Set (Var "v")) ")" ")" )))); end; :: deftheorem defines :::"alternating"::: BILINEAR:def 27 : (Bool "for" (Set (Var "K")) "being" ($#v12_vectsp_1 :::"Fanoian"::: ) ($#l6_algstr_0 :::"Field":::) (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" ($#v1_bilinear :::"additiveFAF"::: ) ($#v2_bilinear :::"additiveSAF"::: ) ($#m1_subset_1 :::"Form":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_bilinear :::"alternating"::: ) ) "iff" (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "w")) "," (Set (Var "v")) ")" ")" )))) ")" )))); theorem :: BILINEAR:59 (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"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (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" ($#v8_bilinear :::"alternating"::: ) ($#m1_subset_1 :::"bilinear-Form":::) "of" (Set (Var "V")) "," (Set (Var "V")) "holds" (Bool (Set ($#k10_bilinear :::"leftker"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k11_bilinear :::"rightker"::: ) (Set (Var "f"))))))) ;