:: VECTSP_5 semantic presentation begin definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "GF")); let "W1", "W2" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "M")); func "W1" :::"+"::: "W2" -> ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" "M" means :: VECTSP_5:def 1 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")) ")" ) where v, u "is" ($#m1_subset_1 :::"Element":::) "of" "M" : (Bool "(" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) "W1") & (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) "W2") ")" ) "}" ); end; :: deftheorem defines :::"+"::: VECTSP_5:def 1 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "b5")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")) ")" ) where v, u "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) : (Bool "(" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) ")" ) "}" ) ")" ))))); definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "GF")); let "W1", "W2" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "M")); func "W1" :::"/\"::: "W2" -> ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" "M" means :: VECTSP_5:def 2 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W1") ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W2"))); commutativity (Bool "for" (Set (Var "b1")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "M")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "M")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W1"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W2")))))) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W2"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W1"))))))) ; end; :: deftheorem defines :::"/\"::: VECTSP_5:def 2 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "b5")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W1"))) ($#k3_xboole_0 :::"/\"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W2"))))) ")" ))))); theorem :: VECTSP_5:1 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")))) "iff" (Bool "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "v2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2")))) ")" )) ")" ))))) ; theorem :: VECTSP_5:2 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool "(" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) "or" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) ")" )) "holds" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")))))))) ; theorem :: VECTSP_5:3 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) ")" ) ")" ))))) ; theorem :: VECTSP_5:4 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "W")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W")))))) ; theorem :: VECTSP_5:5 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W1"))))))) ; theorem :: VECTSP_5:6 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W3"))))))) ; theorem :: VECTSP_5:7 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")))) & (Bool (Set (Var "W2")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")))) ")" )))) ; theorem :: VECTSP_5:8 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "W2")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2"))) "iff" (Bool (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W2"))) ")" ))))) ; theorem :: VECTSP_5:9 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "M")) ")" ) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Set (Set (Var "W")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "W"))) ")" )))) ; theorem :: VECTSP_5:10 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "M")) ")" ) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "M"))) "#)" )) & (Bool (Set (Set "(" ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "M")) ")" ) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "M"))) "#)" )) ")" ))) ; theorem :: VECTSP_5:11 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "M")) ")" ) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "M"))) "#)" )) & (Bool (Set (Set (Var "W")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "M"))) "#)" )) ")" )))) ; theorem :: VECTSP_5:12 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v7_vectsp_1 :::"strict"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) "holds" (Bool (Set (Set "(" ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "M")) ")" ) ($#k1_vectsp_5 :::"+"::: ) (Set "(" ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "M"))))) ; theorem :: VECTSP_5:13 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "W")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W")))))) ; theorem :: VECTSP_5:14 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set "(" (Set (Var "W2")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3"))))))) ; theorem :: VECTSP_5:15 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W1"))) & (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2"))) ")" )))) ; theorem :: VECTSP_5:16 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "W1")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) ")" ) & (Bool "(" "for" (Set (Var "W1")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W1")))) "holds" (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2"))) ")" ) ")" )))) ; theorem :: VECTSP_5:17 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3"))) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set (Var "W2")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3"))))))) ; theorem :: VECTSP_5:18 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W3")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W3")))) "holds" (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W3")))))) ; theorem :: VECTSP_5:19 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2"))) & (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W3")))) "holds" (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set (Var "W2")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3"))))))) ; theorem :: VECTSP_5:20 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "M")) ")" ) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "M")))) & (Bool (Set (Set (Var "W")) ($#k2_vectsp_5 :::"/\"::: ) (Set "(" ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "M")))) ")" )))) ; theorem :: VECTSP_5:21 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "M")) ")" ) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Set (Set (Var "W")) ($#k2_vectsp_5 :::"/\"::: ) (Set "(" ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "W"))) ")" )))) ; theorem :: VECTSP_5:22 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v7_vectsp_1 :::"strict"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) "holds" (Bool (Set (Set "(" ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "M")) ")" ) ($#k2_vectsp_5 :::"/\"::: ) (Set "(" ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "M"))))) ; theorem :: VECTSP_5:23 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2"))))))) ; theorem :: VECTSP_5:24 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "W2")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Set "(" (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W2"))))))) ; theorem :: VECTSP_5:25 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "W1")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set "(" (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "W1"))))))) ; theorem :: VECTSP_5:26 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Set "(" (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k1_vectsp_5 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3")) ")" )) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set (Var "W2")) ($#k2_vectsp_5 :::"/\"::: ) (Set "(" (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W3")) ")" )))))) ; theorem :: VECTSP_5:27 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W2")) ($#k2_vectsp_5 :::"/\"::: ) (Set "(" (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k1_vectsp_5 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3")) ")" )))))) ; theorem :: VECTSP_5:28 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W2")) "," (Set (Var "W1")) "," (Set (Var "W3")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "W2")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3")) ")" )) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set "(" (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k2_vectsp_5 :::"/\"::: ) (Set "(" (Set (Var "W2")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W3")) ")" )))))) ; theorem :: VECTSP_5:29 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W2")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k2_vectsp_5 :::"/\"::: ) (Set "(" (Set (Var "W2")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W3")) ")" )))))) ; theorem :: VECTSP_5:30 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W3")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "W1")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W3")))) "holds" (Bool (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3")))))))) ; theorem :: VECTSP_5:31 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W2"))) "iff" (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) ")" )))) ; theorem :: VECTSP_5:32 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W3"))) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set (Var "W2")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W3")))))))) ; theorem :: VECTSP_5:33 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Set (Var "W2")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W3"))))))) ; theorem :: VECTSP_5:34 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W3")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W3"))) & (Bool (Set (Var "W2")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W3")))) "holds" (Bool (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2"))) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W3")))))) ; theorem :: VECTSP_5:35 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W2"))) "or" (Bool (Set (Var "W2")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W1"))) ")" ) "iff" (Bool "ex" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W2")))))) ")" )))) ; definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "GF")); func :::"Subspaces"::: "M" -> ($#m1_hidden :::"set"::: ) means :: VECTSP_5:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "W")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" "M" "st" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )); end; :: deftheorem defines :::"Subspaces"::: VECTSP_5:def 3 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_vectsp_5 :::"Subspaces"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "W")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )) ")" )))); registrationlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "GF")); cluster (Set ($#k3_vectsp_5 :::"Subspaces"::: ) "M") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: VECTSP_5:36 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v7_vectsp_1 :::"strict"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) "holds" (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set ($#k3_vectsp_5 :::"Subspaces"::: ) (Set (Var "M")))))) ; definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "GF")); let "W1", "W2" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "M")); pred "M" :::"is_the_direct_sum_of"::: "W1" "," "W2" means :: VECTSP_5:def 4 (Bool "(" (Bool (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "M") "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" "M") "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" "M") "#)" ) ($#r1_hidden :::"="::: ) (Set "W1" ($#k1_vectsp_5 :::"+"::: ) "W2")) & (Bool (Set "W1" ($#k2_vectsp_5 :::"/\"::: ) "W2") ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) "M")) ")" ); end; :: deftheorem defines :::"is_the_direct_sum_of"::: VECTSP_5:def 4 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2"))) "iff" (Bool "(" (Bool (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "M"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")))) & (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "M")))) ")" ) ")" )))); definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); mode :::"Linear_Compl"::: "of" "W" -> ($#m1_vectsp_4 :::"Subspace"::: ) "of" "V" means :: VECTSP_5:def 5 (Bool "V" ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) it "," "W"); end; :: deftheorem defines :::"Linear_Compl"::: VECTSP_5:def 5 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W")) "," (Set (Var "b4")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set (Var "W"))) "iff" (Bool (Set (Var "V")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "b4")) "," (Set (Var "W"))) ")" )))); theorem :: VECTSP_5:37 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool (Set (Var "W2")) "is" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set (Var "W1")))))) ; theorem :: VECTSP_5:38 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "L")) "," (Set (Var "W"))) & (Bool (Set (Var "V")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W")) "," (Set (Var "L"))) ")" ))))) ; theorem :: VECTSP_5:39 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Set (Var "W")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "V"))) "#)" )) & (Bool (Set (Set (Var "L")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "V"))) "#)" )) ")" ))))) ; theorem :: VECTSP_5:40 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Set (Var "W")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V")))) & (Bool (Set (Set (Var "L")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V")))) ")" ))))) ; theorem :: VECTSP_5:41 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "M")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool (Set (Var "M")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W2")) "," (Set (Var "W1")))))) ; theorem :: VECTSP_5:42 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "M"))) "," (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "M")))) & (Bool (Set (Var "M")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "M"))) "," (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "M")))) ")" ))) ; theorem :: VECTSP_5:43 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set (Var "W")) "holds" (Bool (Set (Var "W")) "is" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set (Var "L"))))))) ; theorem :: VECTSP_5:44 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) "holds" (Bool "(" (Bool (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V"))) "is" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "V")))) & (Bool (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "V"))) "is" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V")))) ")" ))) ; theorem :: VECTSP_5:45 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "C1")) "being" ($#m2_vectsp_4 :::"Coset"::: ) "of" (Set (Var "W1")) (Bool "for" (Set (Var "C2")) "being" ($#m2_vectsp_4 :::"Coset"::: ) "of" (Set (Var "W2")) "st" (Bool (Bool (Set (Var "C1")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "C2")))) "holds" (Bool (Set (Set (Var "C1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C2"))) "is" ($#m2_vectsp_4 :::"Coset"::: ) "of" (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))))))))) ; theorem :: VECTSP_5:46 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2"))) "iff" (Bool "for" (Set (Var "C1")) "being" ($#m2_vectsp_4 :::"Coset"::: ) "of" (Set (Var "W1")) (Bool "for" (Set (Var "C2")) "being" ($#m2_vectsp_4 :::"Coset"::: ) "of" (Set (Var "W2")) (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Set (Set (Var "C1")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))))) ")" )))) ; theorem :: VECTSP_5:47 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v7_vectsp_1 :::"strict"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "M"))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) (Bool "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "v2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2")))) ")" ))) ")" )))) ; theorem :: VECTSP_5:48 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "u1")) "," (Set (Var "u2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "M")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2")))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u2")))) & (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "u1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "v2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) & (Bool (Set (Var "u2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2")))) "holds" (Bool "(" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "u1"))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Var "u2"))) ")" ))))) ; theorem :: VECTSP_5:49 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")))) & (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "u1")) "," (Set (Var "u2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2")))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "u1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u2")))) & (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "u1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "v2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) & (Bool (Set (Var "u2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2")))) "holds" (Bool "(" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "u1"))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Var "u2"))) ")" )))) "holds" (Bool (Set (Var "M")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))))) ; definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "GF")); let "v" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "M")); let "W1", "W2" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "M")); assume (Bool (Set (Const "M")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Const "W1")) "," (Set (Const "W2"))) ; func "v" :::"|--"::: "(" "W1" "," "W2" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k2_zfmisc_1 :::":]"::: ) ) means :: VECTSP_5:def 6 (Bool "(" (Bool "v" ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" it ($#k3_domain_1 :::"`2"::: ) ")" ))) & (Bool (Set it ($#k2_domain_1 :::"`1"::: ) ) ($#r1_struct_0 :::"in"::: ) "W1") & (Bool (Set it ($#k3_domain_1 :::"`2"::: ) ) ($#r1_struct_0 :::"in"::: ) "W2") ")" ); end; :: deftheorem defines :::"|--"::: VECTSP_5:def 6 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "M")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" )) "iff" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b6")) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b6")) ($#k3_domain_1 :::"`2"::: ) ")" ))) & (Bool (Set (Set (Var "b6")) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Set (Var "b6")) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) ")" ) ")" )))))); theorem :: VECTSP_5:50 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "M")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W2")) "," (Set (Var "W1")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) )))))) ; theorem :: VECTSP_5:51 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "M")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W2")) "," (Set (Var "W1")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) )))))) ; theorem :: VECTSP_5:52 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Set "(" (Set (Var "t")) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k3_domain_1 :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Set (Var "t")) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Set (Var "t")) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "L")))) "holds" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" )))))))) ; theorem :: VECTSP_5:53 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v")))))))) ; theorem :: VECTSP_5:54 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Set "(" (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "L"))) ")" )))))) ; theorem :: VECTSP_5:55 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "L")) "," (Set (Var "W")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ))))))) ; theorem :: VECTSP_5:56 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_vectsp_5 :::"Linear_Compl"::: ) "of" (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k4_vectsp_5 :::"|--"::: ) "(" (Set (Var "L")) "," (Set (Var "W")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) ))))))) ; definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "GF")); func :::"SubJoin"::: "M" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_vectsp_5 :::"Subspaces"::: ) "M" ")" ) means :: VECTSP_5:def 7 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_vectsp_5 :::"Subspaces"::: ) "M") (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" "M" "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")))))); end; :: deftheorem defines :::"SubJoin"::: VECTSP_5:def 7 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_vectsp_5 :::"Subspaces"::: ) (Set (Var "M")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_vectsp_5 :::"SubJoin"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_vectsp_5 :::"Subspaces"::: ) (Set (Var "M"))) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "b3")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")))))) ")" )))); definitionlet "GF" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Const "GF")); func :::"SubMeet"::: "M" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_vectsp_5 :::"Subspaces"::: ) "M" ")" ) means :: VECTSP_5:def 8 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_vectsp_5 :::"Subspaces"::: ) "M") (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" "M" "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2")))))); end; :: deftheorem defines :::"SubMeet"::: VECTSP_5:def 8 : (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_vectsp_5 :::"Subspaces"::: ) (Set (Var "M")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_vectsp_5 :::"SubMeet"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_vectsp_5 :::"Subspaces"::: ) (Set (Var "M"))) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "b3")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2")))))) ")" )))); theorem :: VECTSP_5:57 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_vectsp_5 :::"Subspaces"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k5_vectsp_5 :::"SubJoin"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k6_vectsp_5 :::"SubMeet"::: ) (Set (Var "M")) ")" ) "#)" ) "is" ($#l3_lattices :::"Lattice":::)))) ; theorem :: VECTSP_5:58 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_vectsp_5 :::"Subspaces"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k5_vectsp_5 :::"SubJoin"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k6_vectsp_5 :::"SubMeet"::: ) (Set (Var "M")) ")" ) "#)" ) "is" ($#l3_lattices :::"0_Lattice":::)))) ; theorem :: VECTSP_5:59 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_vectsp_5 :::"Subspaces"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k5_vectsp_5 :::"SubJoin"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k6_vectsp_5 :::"SubMeet"::: ) (Set (Var "M")) ")" ) "#)" ) "is" ($#l3_lattices :::"1_Lattice":::)))) ; theorem :: VECTSP_5:60 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_vectsp_5 :::"Subspaces"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k5_vectsp_5 :::"SubJoin"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k6_vectsp_5 :::"SubMeet"::: ) (Set (Var "M")) ")" ) "#)" ) "is" ($#l3_lattices :::"01_Lattice":::)))) ; theorem :: VECTSP_5:61 (Bool "for" (Set (Var "GF")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v8_vectsp_1 :::"vector-distributive"::: ) ($#v9_vectsp_1 :::"scalar-distributive"::: ) ($#v10_vectsp_1 :::"scalar-associative"::: ) ($#v11_vectsp_1 :::"scalar-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_vectsp_1 :::"VectSpStr"::: ) "over" (Set (Var "GF")) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_vectsp_5 :::"Subspaces"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k5_vectsp_5 :::"SubJoin"::: ) (Set (Var "M")) ")" ) "," (Set "(" ($#k6_vectsp_5 :::"SubMeet"::: ) (Set (Var "M")) ")" ) "#)" ) "is" ($#l3_lattices :::"M_Lattice":::)))) ; theorem :: VECTSP_5:62 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_vectsp_5 :::"Subspaces"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k5_vectsp_5 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k6_vectsp_5 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#l3_lattices :::"C_Lattice":::)))) ;