:: VECTSP_8 semantic presentation begin definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "VS" be ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); func :::"lattice"::: "VS" -> ($#v3_lattices :::"strict"::: ) ($#v15_lattices :::"bounded"::: ) ($#l3_lattices :::"Lattice":::) equals :: VECTSP_8:def 1 (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_vectsp_5 :::"Subspaces"::: ) "VS" ")" ) "," (Set "(" ($#k5_vectsp_5 :::"SubJoin"::: ) "VS" ")" ) "," (Set "(" ($#k6_vectsp_5 :::"SubMeet"::: ) "VS" ")" ) "#)" ); end; :: deftheorem defines :::"lattice"::: VECTSP_8:def 1 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "VS")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) "holds" (Bool (Set ($#k1_vectsp_8 :::"lattice"::: ) (Set (Var "VS"))) ($#r1_hidden :::"="::: ) (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_vectsp_5 :::"Subspaces"::: ) (Set (Var "VS")) ")" ) "," (Set "(" ($#k5_vectsp_5 :::"SubJoin"::: ) (Set (Var "VS")) ")" ) "," (Set "(" ($#k6_vectsp_5 :::"SubMeet"::: ) (Set (Var "VS")) ")" ) "#)" )))); definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "VS" be ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); mode :::"SubVS-Family"::: "of" "VS" -> ($#m1_hidden :::"set"::: ) means :: VECTSP_8:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Var "x")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" "VS")); end; :: deftheorem defines :::"SubVS-Family"::: VECTSP_8:def 2 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "VS")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_vectsp_8 :::"SubVS-Family"::: ) "of" (Set (Var "VS"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "VS")))) ")" )))); registrationlet "F" be ($#l6_algstr_0 :::"Field":::); let "VS" be ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_vectsp_8 :::"SubVS-Family"::: ) "of" "VS"; end; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "VS" be ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); :: original: :::"Subspaces"::: redefine func :::"Subspaces"::: "VS" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_vectsp_8 :::"SubVS-Family"::: ) "of" "VS"; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_vectsp_8 :::"SubVS-Family"::: ) "of" (Set (Const "VS")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "X" -> ($#m1_vectsp_4 :::"Subspace"::: ) "of" "VS"; end; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "VS" be ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "x" be ($#m2_vectsp_8 :::"Element"::: ) "of" (Set ($#k2_vectsp_8 :::"Subspaces"::: ) (Set (Const "VS"))); func :::"carr"::: "x" -> ($#m1_subset_1 :::"Subset":::) "of" "VS" means :: VECTSP_8:def 3 (Bool "ex" (Set (Var "X")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" "VS" "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool it ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ")" )); end; :: deftheorem defines :::"carr"::: VECTSP_8:def 3 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "VS")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "x")) "being" ($#m2_vectsp_8 :::"Element"::: ) "of" (Set ($#k2_vectsp_8 :::"Subspaces"::: ) (Set (Var "VS"))) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "VS")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_vectsp_8 :::"carr"::: ) (Set (Var "x")))) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "VS")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ")" )) ")" ))))); definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "VS" be ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); func :::"carr"::: "VS" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_vectsp_8 :::"Subspaces"::: ) "VS" ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "VS") ")" ) means :: VECTSP_8:def 4 (Bool "for" (Set (Var "h")) "being" ($#m2_vectsp_8 :::"Element"::: ) "of" (Set ($#k2_vectsp_8 :::"Subspaces"::: ) "VS") (Bool "for" (Set (Var "H")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" "VS" "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "H")))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H")))))); end; :: deftheorem defines :::"carr"::: VECTSP_8:def 4 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "VS")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_vectsp_8 :::"Subspaces"::: ) (Set (Var "VS")) ")" ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "VS"))) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_vectsp_8 :::"carr"::: ) (Set (Var "VS")))) "iff" (Bool "for" (Set (Var "h")) "being" ($#m2_vectsp_8 :::"Element"::: ) "of" (Set ($#k2_vectsp_8 :::"Subspaces"::: ) (Set (Var "VS"))) (Bool "for" (Set (Var "H")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "VS")) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "H")))) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H")))))) ")" )))); theorem :: VECTSP_8:1 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "VS")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "H")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_vectsp_8 :::"Subspaces"::: ) (Set (Var "VS")) ")" ) "holds" (Bool (Bool "not" (Set (Set "(" ($#k4_vectsp_8 :::"carr"::: ) (Set (Var "VS")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "H"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))))) ; theorem :: VECTSP_8:2 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "VS")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "H")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "VS")) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "VS"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_vectsp_8 :::"carr"::: ) (Set (Var "VS")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "H"))))))) ; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "VS" be ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "G" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_vectsp_8 :::"Subspaces"::: ) (Set (Const "VS")) ")" ); func :::"meet"::: "G" -> ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" "VS" means :: VECTSP_8:def 5 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" (Set "(" ($#k4_vectsp_8 :::"carr"::: ) "VS" ")" ) ($#k7_relset_1 :::".:"::: ) "G" ")" ))); end; :: deftheorem defines :::"meet"::: VECTSP_8:def 5 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "VS")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "G")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_vectsp_8 :::"Subspaces"::: ) (Set (Var "VS")) ")" ) (Bool "for" (Set (Var "b4")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "VS")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_vectsp_8 :::"meet"::: ) (Set (Var "G")))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" (Set "(" ($#k4_vectsp_8 :::"carr"::: ) (Set (Var "VS")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "G")) ")" ))) ")" ))))); theorem :: VECTSP_8:3 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "VS")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) "holds" (Bool (Set ($#k2_vectsp_8 :::"Subspaces"::: ) (Set (Var "VS"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_vectsp_8 :::"lattice"::: ) (Set (Var "VS")) ")" ))))) ; theorem :: VECTSP_8:4 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "VS")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) "holds" (Bool (Set "the" ($#u1_lattices :::"L_meet"::: ) "of" (Set "(" ($#k1_vectsp_8 :::"lattice"::: ) (Set (Var "VS")) ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k6_vectsp_5 :::"SubMeet"::: ) (Set (Var "VS")))))) ; theorem :: VECTSP_8:5 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "VS")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) "holds" (Bool (Set "the" ($#u2_lattices :::"L_join"::: ) "of" (Set "(" ($#k1_vectsp_8 :::"lattice"::: ) (Set (Var "VS")) ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k5_vectsp_5 :::"SubJoin"::: ) (Set (Var "VS")))))) ; theorem :: VECTSP_8:6 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "VS")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_vectsp_8 :::"lattice"::: ) (Set (Var "VS")) ")" ) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "VS")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "H2")))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_lattices :::"[="::: ) (Set (Var "q"))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2")))) ")" ))))) ; theorem :: VECTSP_8:7 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "VS")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_vectsp_8 :::"lattice"::: ) (Set (Var "VS")) ")" ) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "VS")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "H2")))) "holds" (Bool (Set (Set (Var "p")) ($#k3_lattices :::""\/""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "H2")))))))) ; theorem :: VECTSP_8:8 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "VS")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_vectsp_8 :::"lattice"::: ) (Set (Var "VS")) ")" ) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "VS")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "H1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "H2")))) "holds" (Bool (Set (Set (Var "p")) ($#k4_lattices :::""/\""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "H2")))))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) ; redefine attr "L" is :::"complete"::: means :: VECTSP_8:def 6 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" "L" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "a")) ($#r3_lattice3 :::"is_less_than"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Bool (Set (Var "b")) ($#r3_lattice3 :::"is_less_than"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "b")) ($#r1_lattices :::"[="::: ) (Set (Var "a"))) ")" ) ")" ))); end; :: deftheorem defines :::"complete"::: VECTSP_8:def 6 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_lattices :::"LattStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v4_lattice3 :::"complete"::: ) ) "iff" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r3_lattice3 :::"is_less_than"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "b")) ($#r3_lattice3 :::"is_less_than"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "b")) ($#r1_lattices :::"[="::: ) (Set (Var "a"))) ")" ) ")" ))) ")" )); theorem :: VECTSP_8:9 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "VS")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) "holds" (Bool (Set ($#k1_vectsp_8 :::"lattice"::: ) (Set (Var "VS"))) "is" ($#v4_lattice3 :::"complete"::: ) ))) ; theorem :: VECTSP_8:10 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "VS")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "VS")) "st" (Bool (Bool (Bool "not" (Set (Var "S")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "S")) "is" ($#v1_vectsp_4 :::"linearly-closed"::: ) ) & (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))))))) ; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "A", "B" be ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "A"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "B"))); func :::"FuncLatt"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_vectsp_8 :::"lattice"::: ) "A" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_vectsp_8 :::"lattice"::: ) "B" ")" )) means :: VECTSP_8:def 7 (Bool "for" (Set (Var "S")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" "A" (Bool "for" (Set (Var "B0")) "being" ($#m1_subset_1 :::"Subset":::) "of" "B" "st" (Bool (Bool (Set (Var "B0")) ($#r1_hidden :::"="::: ) (Set "f" ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set (Var "B0")))))); end; :: deftheorem defines :::"FuncLatt"::: VECTSP_8:def 7 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B"))) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_vectsp_8 :::"lattice"::: ) (Set (Var "A")) ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_vectsp_8 :::"lattice"::: ) (Set (Var "B")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_vectsp_8 :::"FuncLatt"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "S")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "B0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "B0")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set (Var "B0")))))) ")" ))))); definitionlet "L1", "L2" be ($#l3_lattices :::"Lattice":::); mode :::"Semilattice-Homomorphism"::: "of" "L1" "," "L2" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L2") means :: VECTSP_8:def 8 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "L1" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" )))); end; :: deftheorem defines :::"Semilattice-Homomorphism"::: VECTSP_8:def 8 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m3_vectsp_8 :::"Semilattice-Homomorphism"::: ) "of" (Set (Var "L1")) "," (Set (Var "L2"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k4_lattices :::""/\""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k4_lattices :::""/\""::: ) (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" )))) ")" ))); definitionlet "L1", "L2" be ($#l3_lattices :::"Lattice":::); mode :::"sup-Semilattice-Homomorphism"::: "of" "L1" "," "L2" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L2") means :: VECTSP_8:def 9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "L1" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" )))); end; :: deftheorem defines :::"sup-Semilattice-Homomorphism"::: VECTSP_8:def 9 : (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m4_vectsp_8 :::"sup-Semilattice-Homomorphism"::: ) "of" (Set (Var "L1")) "," (Set (Var "L2"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L1")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "a")) ($#k3_lattices :::""\/""::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) ($#k3_lattices :::""\/""::: ) (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" )))) ")" ))); theorem :: VECTSP_8:11 (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#l3_lattices :::"Lattice":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L2"))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set (Var "L1")) "," (Set (Var "L2"))) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#m4_vectsp_8 :::"sup-Semilattice-Homomorphism"::: ) "of" (Set (Var "L1")) "," (Set (Var "L2"))) & (Bool (Set (Var "f")) "is" ($#m3_vectsp_8 :::"Semilattice-Homomorphism"::: ) "of" (Set (Var "L1")) "," (Set (Var "L2"))) ")" ) ")" ))) ; theorem :: VECTSP_8:12 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_mod_2 :::"homogeneous"::: ) )) "holds" (Bool (Set ($#k6_vectsp_8 :::"FuncLatt"::: ) (Set (Var "f"))) "is" ($#m4_vectsp_8 :::"sup-Semilattice-Homomorphism"::: ) "of" (Set ($#k1_vectsp_8 :::"lattice"::: ) (Set (Var "A"))) "," (Set ($#k1_vectsp_8 :::"lattice"::: ) (Set (Var "B"))))))) ; theorem :: VECTSP_8:13 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "f")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_mod_2 :::"homogeneous"::: ) )) "holds" (Bool (Set ($#k6_vectsp_8 :::"FuncLatt"::: ) (Set (Var "f"))) "is" ($#m1_lattice4 :::"Homomorphism"::: ) "of" (Set ($#k1_vectsp_8 :::"lattice"::: ) (Set (Var "A"))) "," (Set ($#k1_vectsp_8 :::"lattice"::: ) (Set (Var "B"))))))) ; theorem :: VECTSP_8:14 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v13_vectsp_1 :::"additive"::: ) ) & (Bool (Set (Var "f")) "is" ($#v1_mod_2 :::"homogeneous"::: ) ) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k6_vectsp_8 :::"FuncLatt"::: ) (Set (Var "f"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) )))) ; theorem :: VECTSP_8:15 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "A")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) "holds" (Bool (Set ($#k6_vectsp_8 :::"FuncLatt"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_vectsp_8 :::"lattice"::: ) (Set (Var "A")) ")" )))))) ;