:: LOPBAN_2 semantic presentation begin theorem :: LOPBAN_2:1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "holds" (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Z")))))) ; theorem :: LOPBAN_2:2 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "holds" (Bool "(" (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "Z"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k15_lopban_1 :::"BoundedLinearOperatorsNorm"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "g")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k15_lopban_1 :::"BoundedLinearOperatorsNorm"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "f")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ))) & (Bool (Set (Set "(" ($#k15_lopban_1 :::"BoundedLinearOperatorsNorm"::: ) "(" (Set (Var "X")) "," (Set (Var "Z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k15_lopban_1 :::"BoundedLinearOperatorsNorm"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "g")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k15_lopban_1 :::"BoundedLinearOperatorsNorm"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "f")) ")" ))) ")" ) ")" ) ")" )))) ; definitionlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); let "f", "g" be ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Const "X")) "," (Set (Const "X")); :: original: :::"*"::: redefine func "g" :::"*"::: "f" -> ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" "X" "," "X"; end; definitionlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); let "f", "g" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Const "X")) "," (Set (Const "X")) ")" ); func "f" :::"+"::: "g" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ) equals :: LOPBAN_2:def 1 (Set (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" "X" "," "X" ")" ")" ) ")" ")" ) ($#k5_binop_1 :::"."::: ) "(" "f" "," "g" ")" ); end; :: deftheorem defines :::"+"::: LOPBAN_2:def 1 : (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k2_lopban_2 :::"+"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) ")" ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )))); definitionlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); let "f", "g" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Const "X")) "," (Set (Const "X")) ")" ); func "g" :::"*"::: "f" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ) equals :: LOPBAN_2:def 2 (Set (Set "(" ($#k13_lopban_1 :::"modetrans"::: ) "(" "g" "," "X" "," "X" ")" ")" ) ($#k1_lopban_2 :::"*"::: ) (Set "(" ($#k13_lopban_1 :::"modetrans"::: ) "(" "f" "," "X" "," "X" ")" ")" )); end; :: deftheorem defines :::"*"::: LOPBAN_2:def 2 : (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) "holds" (Bool (Set (Set (Var "g")) ($#k3_lopban_2 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_lopban_1 :::"modetrans"::: ) "(" (Set (Var "g")) "," (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) ($#k1_lopban_2 :::"*"::: ) (Set "(" ($#k13_lopban_1 :::"modetrans"::: ) "(" (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "X")) ")" ")" ))))); definitionlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); let "f" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Const "X")) "," (Set (Const "X")) ")" ); let "a" be ($#m1_subset_1 :::"Real":::); func "a" :::"*"::: "f" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ) equals :: LOPBAN_2:def 3 (Set (Set "(" ($#k9_rsspace :::"Mult_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" "X" "," "X" ")" ")" ) ")" ")" ) ($#k2_binop_1 :::"."::: ) "(" "a" "," "f" ")" ); end; :: deftheorem defines :::"*"::: LOPBAN_2:def 3 : (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "a")) ($#k4_lopban_2 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_rsspace :::"Mult_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) ")" ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" ))))); definitionlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); func :::"FuncMult"::: "X" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ")" ) means :: LOPBAN_2:def 4 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_lopban_2 :::"*"::: ) (Set (Var "g"))))); end; :: deftheorem defines :::"FuncMult"::: LOPBAN_2:def 4 : (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_lopban_2 :::"FuncMult"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_lopban_2 :::"*"::: ) (Set (Var "g"))))) ")" ))); theorem :: LOPBAN_2:3 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) "is" ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "X")))) ; definitionlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); func :::"FuncUnit"::: "X" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ) equals :: LOPBAN_2:def 5 (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")); end; :: deftheorem defines :::"FuncUnit"::: LOPBAN_2:def 5 : (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool (Set ($#k6_lopban_2 :::"FuncUnit"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))))); theorem :: LOPBAN_2:4 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k1_lopban_2 :::"*"::: ) (Set (Var "g")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))) ; theorem :: LOPBAN_2:5 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set (Set (Var "f")) ($#k1_lopban_2 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k1_lopban_2 :::"*"::: ) (Set (Var "h")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_lopban_2 :::"*"::: ) (Set (Var "g")) ")" ) ($#k1_lopban_2 :::"*"::: ) (Set (Var "h")))))) ; theorem :: LOPBAN_2:6 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#v2_lopban_1 :::"Lipschitzian"::: ) ($#m1_subset_1 :::"LinearOperator":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))) & (Bool (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))) ")" ))) ; theorem :: LOPBAN_2:7 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k3_lopban_2 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k3_lopban_2 :::"*"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_lopban_2 :::"*"::: ) (Set (Var "g")) ")" ) ($#k3_lopban_2 :::"*"::: ) (Set (Var "h")))))) ; theorem :: LOPBAN_2:8 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_lopban_2 :::"*"::: ) (Set "(" ($#k6_lopban_2 :::"FuncUnit"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Set "(" ($#k6_lopban_2 :::"FuncUnit"::: ) (Set (Var "X")) ")" ) ($#k3_lopban_2 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ))) ; theorem :: LOPBAN_2:9 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k3_lopban_2 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k2_lopban_2 :::"+"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_lopban_2 :::"*"::: ) (Set (Var "g")) ")" ) ($#k2_lopban_2 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k3_lopban_2 :::"*"::: ) (Set (Var "h")) ")" ))))) ; theorem :: LOPBAN_2:10 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k2_lopban_2 :::"+"::: ) (Set (Var "h")) ")" ) ($#k3_lopban_2 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k3_lopban_2 :::"*"::: ) (Set (Var "f")) ")" ) ($#k2_lopban_2 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k3_lopban_2 :::"*"::: ) (Set (Var "f")) ")" ))))) ; theorem :: LOPBAN_2:11 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k4_lopban_2 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k3_lopban_2 :::"*"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k4_lopban_2 :::"*"::: ) (Set (Var "f")) ")" ) ($#k3_lopban_2 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k4_lopban_2 :::"*"::: ) (Set (Var "g")) ")" )))))) ; theorem :: LOPBAN_2:12 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "a")) ($#k4_lopban_2 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k3_lopban_2 :::"*"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k4_lopban_2 :::"*"::: ) (Set (Var "f")) ")" ) ($#k3_lopban_2 :::"*"::: ) (Set (Var "g"))))))) ; definitionlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); func :::"Ring_of_BoundedLinearOperators"::: "X" -> ($#l6_algstr_0 :::"doubleLoopStr"::: ) equals :: LOPBAN_2:def 6 (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ")" ) "," (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" "X" "," "X" ")" ")" ) ")" ")" ) "," (Set "(" ($#k5_lopban_2 :::"FuncMult"::: ) "X" ")" ) "," (Set "(" ($#k6_lopban_2 :::"FuncUnit"::: ) "X" ")" ) "," (Set "(" ($#k10_rsspace :::"Zero_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" "X" "," "X" ")" ")" ) ")" ")" ) "#)" ); end; :: deftheorem defines :::"Ring_of_BoundedLinearOperators"::: LOPBAN_2:def 6 : (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool (Set ($#k7_lopban_2 :::"Ring_of_BoundedLinearOperators"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) ")" ")" ) "," (Set "(" ($#k5_lopban_2 :::"FuncMult"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k6_lopban_2 :::"FuncUnit"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k10_rsspace :::"Zero_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) ")" ")" ) "#)" ))); registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster (Set ($#k7_lopban_2 :::"Ring_of_BoundedLinearOperators"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ; end; registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster (Set ($#k7_lopban_2 :::"Ring_of_BoundedLinearOperators"::: ) "X") -> ($#v1_group_1 :::"unital"::: ) ; end; theorem :: LOPBAN_2:13 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k7_lopban_2 :::"Ring_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k7_lopban_2 :::"Ring_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k7_lopban_2 :::"Ring_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" ) "st" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k7_lopban_2 :::"Ring_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" )))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k7_lopban_2 :::"Ring_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k7_lopban_2 :::"Ring_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" ))) ")" ))) ; theorem :: LOPBAN_2:14 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool (Set ($#k7_lopban_2 :::"Ring_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#l6_algstr_0 :::"Ring":::))) ; registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster (Set ($#k7_lopban_2 :::"Ring_of_BoundedLinearOperators"::: ) "X") -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ; end; definitionlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); func :::"R_Algebra_of_BoundedLinearOperators"::: "X" -> ($#l1_funcsdom :::"AlgebraStr"::: ) equals :: LOPBAN_2:def 7 (Set ($#g1_funcsdom :::"AlgebraStr"::: ) "(#" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ")" ) "," (Set "(" ($#k5_lopban_2 :::"FuncMult"::: ) "X" ")" ) "," (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" "X" "," "X" ")" ")" ) ")" ")" ) "," (Set "(" ($#k9_rsspace :::"Mult_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" "X" "," "X" ")" ")" ) ")" ")" ) "," (Set "(" ($#k6_lopban_2 :::"FuncUnit"::: ) "X" ")" ) "," (Set "(" ($#k10_rsspace :::"Zero_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" "X" "," "X" ")" ")" ) ")" ")" ) "#)" ); end; :: deftheorem defines :::"R_Algebra_of_BoundedLinearOperators"::: LOPBAN_2:def 7 : (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool (Set ($#k8_lopban_2 :::"R_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g1_funcsdom :::"AlgebraStr"::: ) "(#" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k5_lopban_2 :::"FuncMult"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) ")" ")" ) "," (Set "(" ($#k9_rsspace :::"Mult_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) ")" ")" ) "," (Set "(" ($#k6_lopban_2 :::"FuncUnit"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k10_rsspace :::"Zero_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) ")" ")" ) "#)" ))); registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster (Set ($#k8_lopban_2 :::"R_Algebra_of_BoundedLinearOperators"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_funcsdom :::"strict"::: ) ; end; registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster (Set ($#k8_lopban_2 :::"R_Algebra_of_BoundedLinearOperators"::: ) "X") -> ($#v1_group_1 :::"unital"::: ) ; end; theorem :: LOPBAN_2:15 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k8_lopban_2 :::"R_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k8_lopban_2 :::"R_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k8_lopban_2 :::"R_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" ) "st" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k8_lopban_2 :::"R_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" )))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k8_lopban_2 :::"R_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k8_lopban_2 :::"R_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")))) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k7_real_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ))) ")" )))) ; definitionmode BLAlgebra is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v2_funcsdom :::"vector-associative"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#l1_funcsdom :::"AlgebraStr"::: ) ; end; registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster (Set ($#k8_lopban_2 :::"R_Algebra_of_BoundedLinearOperators"::: ) "X") -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v1_funcsdom :::"strict"::: ) ($#v2_funcsdom :::"vector-associative"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ; end; theorem :: LOPBAN_2:16 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool (Set ($#k8_lopban_2 :::"R_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#l1_funcsdom :::"BLAlgebra":::))) ; registration cluster (Set ($#k3_rsspace3 :::"l1_Space"::: ) ) -> ($#v3_lopban_1 :::"complete"::: ) ; end; registration cluster (Set ($#k3_rsspace3 :::"l1_Space"::: ) ) -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v12_algstr_0 :::"left_complementable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v14_algstr_0 :::"complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) bbbadV9_RLVECT_1() ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ($#v3_lopban_1 :::"complete"::: ) for ($#l1_normsp_1 :::"NORMSTR"::: ) ; end; theorem :: LOPBAN_2:17 (Bool "for" (Set (Var "X")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) "st" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "w")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: LOPBAN_2:18 (Bool "for" (Set (Var "X")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool (Set (Set "(" ($#k15_lopban_1 :::"BoundedLinearOperatorsNorm"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; definitionattr "c1" is :::"strict"::: ; struct :::"Normed_AlgebraStr"::: -> ($#l1_funcsdom :::"AlgebraStr"::: ) "," ($#l1_normsp_1 :::"NORMSTR"::: ) ; aggr :::"Normed_AlgebraStr":::(# :::"carrier":::, :::"multF":::, :::"addF":::, :::"Mult":::, :::"OneF":::, :::"ZeroF":::, :::"normF"::: #) -> ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) ; end; definitionlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); func :::"R_Normed_Algebra_of_BoundedLinearOperators"::: "X" -> ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) equals :: LOPBAN_2:def 8 (Set ($#g1_lopban_2 :::"Normed_AlgebraStr"::: ) "(#" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ")" ) "," (Set "(" ($#k5_lopban_2 :::"FuncMult"::: ) "X" ")" ) "," (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" "X" "," "X" ")" ")" ) ")" ")" ) "," (Set "(" ($#k9_rsspace :::"Mult_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" "X" "," "X" ")" ")" ) ")" ")" ) "," (Set "(" ($#k6_lopban_2 :::"FuncUnit"::: ) "X" ")" ) "," (Set "(" ($#k10_rsspace :::"Zero_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" "X" "," "X" ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" "X" "," "X" ")" ")" ) ")" ")" ) "," (Set "(" ($#k15_lopban_1 :::"BoundedLinearOperatorsNorm"::: ) "(" "X" "," "X" ")" ")" ) "#)" ); end; :: deftheorem defines :::"R_Normed_Algebra_of_BoundedLinearOperators"::: LOPBAN_2:def 8 : (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#g1_lopban_2 :::"Normed_AlgebraStr"::: ) "(#" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k5_lopban_2 :::"FuncMult"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k8_rsspace :::"Add_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) ")" ")" ) "," (Set "(" ($#k9_rsspace :::"Mult_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) ")" ")" ) "," (Set "(" ($#k6_lopban_2 :::"FuncUnit"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k10_rsspace :::"Zero_"::: ) "(" (Set "(" ($#k10_lopban_1 :::"BoundedLinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k8_lopban_1 :::"R_VectorSpace_of_LinearOperators"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) ")" ")" ) "," (Set "(" ($#k15_lopban_1 :::"BoundedLinearOperatorsNorm"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) "#)" ))); registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) "X") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_lopban_2 :::"strict"::: ) ; end; registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) "X") -> ($#v1_group_1 :::"unital"::: ) ; end; theorem :: LOPBAN_2:19 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" ) "st" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" )))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Num 1) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )))) ; theorem :: LOPBAN_2:20 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool "(" (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v4_normsp_0 :::"reflexive"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v3_normsp_0 :::"discerning"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v2_rlvect_1 :::"Abelian"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v13_algstr_0 :::"right_complementable"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v3_group_1 :::"associative"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v3_vectsp_1 :::"right_unital"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v1_vectsp_1 :::"right-distributive"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v5_rlvect_1 :::"vector-distributive"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v6_rlvect_1 :::"scalar-distributive"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v7_rlvect_1 :::"scalar-associative"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v2_funcsdom :::"vector-associative"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v5_rlvect_1 :::"vector-distributive"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v6_rlvect_1 :::"scalar-distributive"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v7_rlvect_1 :::"scalar-associative"::: ) ) & (Bool (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X"))) "is" ($#v8_rlvect_1 :::"scalar-unital"::: ) ) ")" )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v2_funcsdom :::"vector-associative"::: ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v1_lopban_2 :::"strict"::: ) for ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) ; end; definitionmode Normed_Algebra is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v2_funcsdom :::"vector-associative"::: ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) ; end; registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) "X") -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v2_funcsdom :::"vector-associative"::: ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ; end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) ; attr "X" is :::"Banach_Algebra-like_1"::: means :: LOPBAN_2:def 9 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "y")) ($#k1_normsp_0 :::".||"::: ) )))); attr "X" is :::"Banach_Algebra-like_2"::: means :: LOPBAN_2:def 10 (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) "X" ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)); attr "X" is :::"Banach_Algebra-like_3"::: means :: LOPBAN_2:def 11 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ))))); end; :: deftheorem defines :::"Banach_Algebra-like_1"::: LOPBAN_2:def 9 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_lopban_2 :::"Banach_Algebra-like_1"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "y")) ($#k1_normsp_0 :::".||"::: ) )))) ")" )); :: deftheorem defines :::"Banach_Algebra-like_2"::: LOPBAN_2:def 10 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_lopban_2 :::"Banach_Algebra-like_2"::: ) ) "iff" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "X")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ")" )); :: deftheorem defines :::"Banach_Algebra-like_3"::: LOPBAN_2:def 11 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_lopban_2 :::"Banach_Algebra-like_3"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ))))) ")" )); definitionlet "X" be ($#l1_lopban_2 :::"Normed_Algebra":::); attr "X" is :::"Banach_Algebra-like"::: means :: LOPBAN_2:def 12 (Bool "(" (Bool "X" "is" ($#v2_lopban_2 :::"Banach_Algebra-like_1"::: ) ) & (Bool "X" "is" ($#v3_lopban_2 :::"Banach_Algebra-like_2"::: ) ) & (Bool "X" "is" ($#v4_lopban_2 :::"Banach_Algebra-like_3"::: ) ) & (Bool "X" "is" ($#v6_vectsp_1 :::"left_unital"::: ) ) & (Bool "X" "is" ($#v2_vectsp_1 :::"left-distributive"::: ) ) & (Bool "X" "is" ($#v3_lopban_1 :::"complete"::: ) ) ")" ); end; :: deftheorem defines :::"Banach_Algebra-like"::: LOPBAN_2:def 12 : (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"Normed_Algebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v5_lopban_2 :::"Banach_Algebra-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_lopban_2 :::"Banach_Algebra-like_1"::: ) ) & (Bool (Set (Var "X")) "is" ($#v3_lopban_2 :::"Banach_Algebra-like_2"::: ) ) & (Bool (Set (Var "X")) "is" ($#v4_lopban_2 :::"Banach_Algebra-like_3"::: ) ) & (Bool (Set (Var "X")) "is" ($#v6_vectsp_1 :::"left_unital"::: ) ) & (Bool (Set (Var "X")) "is" ($#v2_vectsp_1 :::"left-distributive"::: ) ) & (Bool (Set (Var "X")) "is" ($#v3_lopban_1 :::"complete"::: ) ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v2_funcsdom :::"vector-associative"::: ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_lopban_2 :::"Banach_Algebra-like"::: ) -> ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v3_lopban_1 :::"complete"::: ) ($#v2_lopban_2 :::"Banach_Algebra-like_1"::: ) ($#v3_lopban_2 :::"Banach_Algebra-like_2"::: ) ($#v4_lopban_2 :::"Banach_Algebra-like_3"::: ) for ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v2_funcsdom :::"vector-associative"::: ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v3_lopban_1 :::"complete"::: ) ($#v2_lopban_2 :::"Banach_Algebra-like_1"::: ) ($#v3_lopban_2 :::"Banach_Algebra-like_2"::: ) ($#v4_lopban_2 :::"Banach_Algebra-like_3"::: ) -> ($#v5_lopban_2 :::"Banach_Algebra-like"::: ) for ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) ; end; registrationlet "X" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l1_normsp_1 :::"RealBanachSpace":::); cluster (Set ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) "X") -> ($#v5_lopban_2 :::"Banach_Algebra-like"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_algstr_0 :::"left_complementable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v14_algstr_0 :::"complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) bbbadV9_RLVECT_1() ($#v2_funcsdom :::"vector-associative"::: ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_lopban_2 :::"Banach_Algebra-like"::: ) for ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) ; end; definitionmode Banach_Algebra is ($#v5_lopban_2 :::"Banach_Algebra-like"::: ) ($#l1_lopban_2 :::"Normed_Algebra":::); end; theorem :: LOPBAN_2:21 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k7_lopban_2 :::"Ring_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_lopban_2 :::"FuncUnit"::: ) (Set (Var "X"))))) ; theorem :: LOPBAN_2:22 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k8_lopban_2 :::"R_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_lopban_2 :::"FuncUnit"::: ) (Set (Var "X"))))) ; theorem :: LOPBAN_2:23 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k9_lopban_2 :::"R_Normed_Algebra_of_BoundedLinearOperators"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_lopban_2 :::"FuncUnit"::: ) (Set (Var "X"))))) ;