:: RLSUB_2 semantic presentation begin definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "W1", "W2" be ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Const "V")); func "W1" :::"+"::: "W2" -> ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" "V" means :: RLSUB_2: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 :::"VECTOR":::) "of" "V" : (Bool "(" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) "W1") & (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) "W2") ")" ) "}" ); end; :: deftheorem defines :::"+"::: RLSUB_2:def 1 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b4")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")) ")" ) where v, u "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) : (Bool "(" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "u")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) ")" ) "}" ) ")" )))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "W1", "W2" be ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Const "V")); func "W1" :::"/\"::: "W2" -> ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" "V" means :: RLSUB_2: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"))); end; :: deftheorem defines :::"/\"::: RLSUB_2:def 2 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b4")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W2")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#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 :: RLSUB_2:1 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2")))) "iff" (Bool "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "v2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2")))) ")" )) ")" )))) ; theorem :: RLSUB_2:2 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "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_rlsub_2 :::"+"::: ) (Set (Var "W2"))))))) ; theorem :: RLSUB_2:3 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (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 :: RLSUB_2:4 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W"))))) ; theorem :: RLSUB_2:5 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W1")))))) ; theorem :: RLSUB_2:6 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W3")))))) ; theorem :: RLSUB_2:7 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2")))) & (Bool (Set (Var "W2")) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2")))) ")" ))) ; theorem :: RLSUB_2:8 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W2")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "W2"))) "iff" (Bool (Set (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W2"))) ")" )))) ; theorem :: RLSUB_2:9 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")) ")" ) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Set (Set (Var "W")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "W"))) ")" ))) ; theorem :: RLSUB_2:10 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")) ")" ) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k2_rlsub_1 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "V"))) "#)" )) & (Bool (Set (Set "(" ($#k2_rlsub_1 :::"(Omega)."::: ) (Set (Var "V")) ")" ) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "V"))) "#)" )) ")" )) ; theorem :: RLSUB_2:11 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_rlsub_1 :::"(Omega)."::: ) (Set (Var "V")) ")" ) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "V"))) "#)" )) & (Bool (Set (Set (Var "W")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k2_rlsub_1 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "V"))) "#)" )) ")" ))) ; theorem :: RLSUB_2:12 (Bool "for" (Set (Var "V")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set (Set "(" ($#k2_rlsub_1 :::"(Omega)."::: ) (Set (Var "V")) ")" ) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k2_rlsub_1 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "V")))) ; theorem :: RLSUB_2:13 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W"))))) ; theorem :: RLSUB_2:14 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W1")))))) ; theorem :: RLSUB_2:15 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set "(" (Set (Var "W2")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W3")))))) ; theorem :: RLSUB_2:16 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W2"))) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "W1"))) & (Bool (Set (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W2"))) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "W2"))) ")" ))) ; theorem :: RLSUB_2:17 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W1")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "W2"))) "iff" (Bool (Set (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) ")" )))) ; theorem :: RLSUB_2:18 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")) ")" ) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")))) & (Bool (Set (Set (Var "W")) ($#k2_rlsub_2 :::"/\"::: ) (Set "(" ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")))) ")" ))) ; theorem :: RLSUB_2:19 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")) ")" ) ($#k2_rlsub_2 :::"/\"::: ) (Set "(" ($#k2_rlsub_1 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")))) & (Bool (Set (Set "(" ($#k2_rlsub_1 :::"(Omega)."::: ) (Set (Var "V")) ")" ) ($#k2_rlsub_2 :::"/\"::: ) (Set "(" ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")))) ")" )) ; theorem :: RLSUB_2:20 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_rlsub_1 :::"(Omega)."::: ) (Set (Var "V")) ")" ) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Set (Set (Var "W")) ($#k2_rlsub_2 :::"/\"::: ) (Set "(" ($#k2_rlsub_1 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "W"))) ")" ))) ; theorem :: RLSUB_2:21 (Bool "for" (Set (Var "V")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set (Set "(" ($#k2_rlsub_1 :::"(Omega)."::: ) (Set (Var "V")) ")" ) ($#k2_rlsub_2 :::"/\"::: ) (Set "(" ($#k2_rlsub_1 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "V")))) ; theorem :: RLSUB_2:22 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W2"))) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2")))))) ; theorem :: RLSUB_2:23 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W2")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W2")))))) ; theorem :: RLSUB_2:24 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W1")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set "(" (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "W1")))))) ; theorem :: RLSUB_2:25 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k1_rlsub_2 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W3")) ")" )) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Set (Var "W2")) ($#k2_rlsub_2 :::"/\"::: ) (Set "(" (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W3")) ")" ))))) ; theorem :: RLSUB_2:26 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W2")) ($#k2_rlsub_2 :::"/\"::: ) (Set "(" (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k1_rlsub_2 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W3")) ")" ))))) ; theorem :: RLSUB_2:27 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W2")) "," (Set (Var "W1")) "," (Set (Var "W3")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W2")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W3")) ")" )) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Set "(" (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k2_rlsub_2 :::"/\"::: ) (Set "(" (Set (Var "W2")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W3")) ")" ))))) ; theorem :: RLSUB_2:28 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W2")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k2_rlsub_2 :::"/\"::: ) (Set "(" (Set (Var "W2")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W3")) ")" ))))) ; theorem :: RLSUB_2:29 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W3")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "W3")))) "holds" (Bool (Set (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W3")))))) ; theorem :: RLSUB_2:30 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W2"))) "iff" (Bool (Set (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) ")" ))) ; theorem :: RLSUB_2:31 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W3"))) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Set (Var "W2")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W3"))))))) ; theorem :: RLSUB_2:32 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "W2"))) "or" (Bool (Set (Var "W2")) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "W1"))) ")" ) "iff" (Bool "ex" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "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 "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); func :::"Subspaces"::: "V" -> ($#m1_hidden :::"set"::: ) means :: RLSUB_2:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" "V") ")" )); end; :: deftheorem defines :::"Subspaces"::: RLSUB_2:def 3 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_rlsub_2 :::"Subspaces"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) "is" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V"))) ")" )) ")" ))); registrationlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster (Set ($#k3_rlsub_2 :::"Subspaces"::: ) "V") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: RLSUB_2:33 (Bool "for" (Set (Var "V")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set ($#k3_rlsub_2 :::"Subspaces"::: ) (Set (Var "V"))))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "W1", "W2" be ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Const "V")); pred "V" :::"is_the_direct_sum_of"::: "W1" "," "W2" means :: RLSUB_2:def 4 (Bool "(" (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" "V") "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "V") "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" "V") "#)" ) ($#r1_hidden :::"="::: ) (Set "W1" ($#k1_rlsub_2 :::"+"::: ) "W2")) & (Bool (Set "W1" ($#k2_rlsub_2 :::"/\"::: ) "W2") ($#r1_hidden :::"="::: ) (Set ($#k1_rlsub_1 :::"(0)."::: ) "V")) ")" ); end; :: deftheorem defines :::"is_the_direct_sum_of"::: RLSUB_2:def 4 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2"))) "iff" (Bool "(" (Bool (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "V"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2")))) & (Bool (Set (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")))) ")" ) ")" ))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "W" be ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Const "V")); mode :::"Linear_Compl"::: "of" "W" -> ($#m1_rlsub_1 :::"Subspace"::: ) "of" "V" means :: RLSUB_2:def 5 (Bool "V" ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) it "," "W"); end; :: deftheorem defines :::"Linear_Compl"::: RLSUB_2:def 5 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "," (Set (Var "b3")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_rlsub_2 :::"Linear_Compl"::: ) "of" (Set (Var "W"))) "iff" (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "b3")) "," (Set (Var "W"))) ")" ))); registrationlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "W" be ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Const "V")); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_algstr_0 :::"left_complementable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_rlvect_1 :::"strict"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) bbbadV9_RLVECT_1() for ($#m1_rlsub_2 :::"Linear_Compl"::: ) "of" "W"; end; theorem :: RLSUB_2:34 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool (Set (Var "W2")) "is" ($#m1_rlsub_2 :::"Linear_Compl"::: ) "of" (Set (Var "W1"))))) ; theorem :: RLSUB_2:35 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_rlsub_2 :::"Linear_Compl"::: ) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "L")) "," (Set (Var "W"))) & (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W")) "," (Set (Var "L"))) ")" )))) ; theorem :: RLSUB_2:36 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_rlsub_2 :::"Linear_Compl"::: ) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Set (Var "W")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "V"))) "#)" )) & (Bool (Set (Set (Var "L")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "V"))) "#)" )) ")" )))) ; theorem :: RLSUB_2:37 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_rlsub_2 :::"Linear_Compl"::: ) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Set (Var "W")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")))) & (Bool (Set (Set (Var "L")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")))) ")" )))) ; theorem :: RLSUB_2:38 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W2")) "," (Set (Var "W1"))))) ; theorem :: RLSUB_2:39 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V"))) "," (Set ($#k2_rlsub_1 :::"(Omega)."::: ) (Set (Var "V")))) & (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set ($#k2_rlsub_1 :::"(Omega)."::: ) (Set (Var "V"))) "," (Set ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")))) ")" )) ; theorem :: RLSUB_2:40 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_rlsub_2 :::"Linear_Compl"::: ) "of" (Set (Var "W")) "holds" (Bool (Set (Var "W")) "is" ($#m1_rlsub_2 :::"Linear_Compl"::: ) "of" (Set (Var "L")))))) ; theorem :: RLSUB_2:41 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool "(" (Bool (Set ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V"))) "is" ($#m1_rlsub_2 :::"Linear_Compl"::: ) "of" (Set ($#k2_rlsub_1 :::"(Omega)."::: ) (Set (Var "V")))) & (Bool (Set ($#k2_rlsub_1 :::"(Omega)."::: ) (Set (Var "V"))) "is" ($#m1_rlsub_2 :::"Linear_Compl"::: ) "of" (Set ($#k1_rlsub_1 :::"(0)."::: ) (Set (Var "V")))) ")" )) ; theorem :: RLSUB_2:42 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "C1")) "being" ($#m2_rlsub_1 :::"Coset"::: ) "of" (Set (Var "W1")) (Bool "for" (Set (Var "C2")) "being" ($#m2_rlsub_1 :::"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_rlsub_1 :::"Coset"::: ) "of" (Set (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W2")))))))) ; theorem :: RLSUB_2:43 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2"))) "iff" (Bool "for" (Set (Var "C1")) "being" ($#m2_rlsub_1 :::"Coset"::: ) "of" (Set (Var "W1")) (Bool "for" (Set (Var "C2")) "being" ($#m2_rlsub_1 :::"Coset"::: ) "of" (Set (Var "W2")) (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "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 :: RLSUB_2:44 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "V"))) "#)" )) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "v2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2")))) ")" ))) ")" ))) ; theorem :: RLSUB_2:45 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "u1")) "," (Set (Var "u2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"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 :: RLSUB_2:46 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2")))) & (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "u1")) "," (Set (Var "u2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "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 "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2"))))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "v" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); let "W1", "W2" be ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Const "V")); assume (Bool (Set (Const "V")) ($#r1_rlsub_2 :::"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" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#k2_zfmisc_1 :::":]"::: ) ) means :: RLSUB_2: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 :::"|--"::: RLSUB_2:def 6 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "b5")) "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 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" )) "iff" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b5")) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b5")) ($#k3_domain_1 :::"`2"::: ) ")" ))) & (Bool (Set (Set (Var "b5")) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Set (Var "b5")) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) ")" ) ")" ))))); theorem :: RLSUB_2:47 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W2")) "," (Set (Var "W1")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ))))) ; theorem :: RLSUB_2:48 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W2")) "," (Set (Var "W1")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) ))))) ; theorem :: RLSUB_2:49 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_rlsub_2 :::"Linear_Compl"::: ) "of" (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "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_rlsub_2 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ))))))) ; theorem :: RLSUB_2:50 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_rlsub_2 :::"Linear_Compl"::: ) "of" (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))))))) ; theorem :: RLSUB_2:51 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_rlsub_2 :::"Linear_Compl"::: ) "of" (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) & (Bool (Set (Set "(" (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_struct_0 :::"in"::: ) (Set (Var "L"))) ")" ))))) ; theorem :: RLSUB_2:52 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_rlsub_2 :::"Linear_Compl"::: ) "of" (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "L")) "," (Set (Var "W")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) )))))) ; theorem :: RLSUB_2:53 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m1_rlsub_2 :::"Linear_Compl"::: ) "of" (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W")) "," (Set (Var "L")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "L")) "," (Set (Var "W")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) )))))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); func :::"SubJoin"::: "V" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_rlsub_2 :::"Subspaces"::: ) "V" ")" ) means :: RLSUB_2:def 7 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_rlsub_2 :::"Subspaces"::: ) "V") (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" "V" "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_rlsub_2 :::"+"::: ) (Set (Var "W2")))))); end; :: deftheorem defines :::"SubJoin"::: RLSUB_2:def 7 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_rlsub_2 :::"Subspaces"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_rlsub_2 :::"SubJoin"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_rlsub_2 :::"Subspaces"::: ) (Set (Var "V"))) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "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 "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2")))))) ")" ))); definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); func :::"SubMeet"::: "V" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_rlsub_2 :::"Subspaces"::: ) "V" ")" ) means :: RLSUB_2:def 8 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_rlsub_2 :::"Subspaces"::: ) "V") (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" "V" "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_rlsub_2 :::"/\"::: ) (Set (Var "W2")))))); end; :: deftheorem defines :::"SubMeet"::: RLSUB_2:def 8 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_rlsub_2 :::"Subspaces"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_rlsub_2 :::"SubMeet"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_rlsub_2 :::"Subspaces"::: ) (Set (Var "V"))) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "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 "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W2")))))) ")" ))); theorem :: RLSUB_2:54 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_rlsub_2 :::"Subspaces"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k5_rlsub_2 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k6_rlsub_2 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#l3_lattices :::"Lattice":::))) ; registrationlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_rlsub_2 :::"Subspaces"::: ) "V" ")" ) "," (Set "(" ($#k5_rlsub_2 :::"SubJoin"::: ) "V" ")" ) "," (Set "(" ($#k6_rlsub_2 :::"SubMeet"::: ) "V" ")" ) "#)" ) -> ($#v10_lattices :::"Lattice-like"::: ) ; end; theorem :: RLSUB_2:55 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_rlsub_2 :::"Subspaces"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k5_rlsub_2 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k6_rlsub_2 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#v13_lattices :::"lower-bounded"::: ) )) ; theorem :: RLSUB_2:56 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_rlsub_2 :::"Subspaces"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k5_rlsub_2 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k6_rlsub_2 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#v14_lattices :::"upper-bounded"::: ) )) ; theorem :: RLSUB_2:57 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_rlsub_2 :::"Subspaces"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k5_rlsub_2 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k6_rlsub_2 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#l3_lattices :::"01_Lattice":::))) ; theorem :: RLSUB_2:58 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_rlsub_2 :::"Subspaces"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k5_rlsub_2 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k6_rlsub_2 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#v12_lattices :::"modular"::: ) )) ; theorem :: RLSUB_2:59 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_rlsub_2 :::"Subspaces"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k5_rlsub_2 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k6_rlsub_2 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#v16_lattices :::"complemented"::: ) )) ; registrationlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_rlsub_2 :::"Subspaces"::: ) "V" ")" ) "," (Set "(" ($#k5_rlsub_2 :::"SubJoin"::: ) "V" ")" ) "," (Set "(" ($#k6_rlsub_2 :::"SubMeet"::: ) "V" ")" ) "#)" ) -> ($#v12_lattices :::"modular"::: ) ($#v13_lattices :::"lower-bounded"::: ) ($#v14_lattices :::"upper-bounded"::: ) ($#v16_lattices :::"complemented"::: ) ; end; theorem :: RLSUB_2:60 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W3"))) "is" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Set (Var "W2")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W3")))))) ; theorem :: RLSUB_2:61 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v2")))) "iff" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v2")))) ")" ))) ; theorem :: RLSUB_2:62 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) ")" )) "holds" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "V"))) "#)" )))) ; theorem :: RLSUB_2:63 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "C")) "being" ($#m2_rlsub_1 :::"Coset"::: ) "of" (Set (Var "W")) "st" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))))))) ; theorem :: RLSUB_2:64 (Bool "for" (Set (Var "l")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "l")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "l")) "holds" (Bool (Set (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" )) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k5_lattices :::"Bottom"::: ) (Set (Var "l")))))) ; theorem :: RLSUB_2:65 (Bool "for" (Set (Var "l")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "l")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "l")) "holds" (Bool (Set (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" )) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_lattices :::"Top"::: ) (Set (Var "l")))))) ;