:: RMOD_3 semantic presentation begin definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Const "R")); let "W1", "W2" be ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Const "V")); func "W1" :::"+"::: "W2" -> ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" "V" means :: RMOD_3: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 :::"+"::: RMOD_3:def 1 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b5")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (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 :::"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 "R" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Const "R")); let "W1", "W2" be ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Const "V")); func "W1" :::"/\"::: "W2" -> ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" "V" means :: RMOD_3: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 :::"/\"::: RMOD_3:def 2 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "b5")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (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 :: RMOD_3:1 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "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_rmod_3 :::"+"::: ) (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 :: RMOD_3:2 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "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_rmod_3 :::"+"::: ) (Set (Var "W2")))))))) ; theorem :: RMOD_3:3 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "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_rmod_3 :::"/\"::: ) (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 :: RMOD_3:4 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W")))))) ; theorem :: RMOD_3:5 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W1"))))))) ; theorem :: RMOD_3:6 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W3"))))))) ; theorem :: RMOD_3:7 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W2")))) & (Bool (Set (Var "W2")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W2")))) ")" )))) ; theorem :: RMOD_3:8 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W2")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W2"))) "iff" (Bool (Set (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W2"))) ")" ))))) ; theorem :: RMOD_3:9 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_rmod_2 :::"(0)."::: ) (Set (Var "V")) ")" ) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Set (Set (Var "W")) ($#k1_rmod_3 :::"+"::: ) (Set "(" ($#k1_rmod_2 :::"(0)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "W"))) ")" )))) ; theorem :: RMOD_3:10 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_rmod_2 :::"(0)."::: ) (Set (Var "V")) ")" ) ($#k1_rmod_3 :::"+"::: ) (Set "(" ($#k2_rmod_2 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "V"))) & (Bool (Set (Set "(" ($#k2_rmod_2 :::"(Omega)."::: ) (Set (Var "V")) ")" ) ($#k1_rmod_3 :::"+"::: ) (Set "(" ($#k1_rmod_2 :::"(0)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "V"))) ")" ))) ; theorem :: RMOD_3:11 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_rmod_2 :::"(Omega)."::: ) (Set (Var "V")) ")" ) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_2 :::"RightModStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"U7"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_vectsp_2 :::"rmult"::: ) "of" (Set (Var "V"))) "#)" )) & (Bool (Set (Set (Var "W")) ($#k1_rmod_3 :::"+"::: ) (Set "(" ($#k2_rmod_2 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_2 :::"RightModStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"U7"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_vectsp_2 :::"rmult"::: ) "of" (Set (Var "V"))) "#)" )) ")" )))) ; theorem :: RMOD_3:12 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set "(" ($#k2_rmod_2 :::"(Omega)."::: ) (Set (Var "V")) ")" ) ($#k1_rmod_3 :::"+"::: ) (Set "(" ($#k2_rmod_2 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "V"))))) ; theorem :: RMOD_3:13 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W")))))) ; theorem :: RMOD_3:14 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W1"))))))) ; theorem :: RMOD_3:15 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set "(" (Set (Var "W2")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W3"))))))) ; theorem :: RMOD_3:16 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W2"))) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W1"))) & (Bool (Set (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W2"))) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W2"))) ")" )))) ; theorem :: RMOD_3:17 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "W1")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) ")" ) & (Bool "(" "for" (Set (Var "W1")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W1")))) "holds" (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W2"))) ")" ) ")" )))) ; theorem :: RMOD_3:18 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W3"))) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Set (Var "W2")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W3"))))))) ; theorem :: RMOD_3:19 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W3")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W3")))) "holds" (Bool (Set (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W2"))) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W3")))))) ; theorem :: RMOD_3:20 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W2"))) & (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W3")))) "holds" (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Set (Var "W2")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W3"))))))) ; theorem :: RMOD_3:21 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_rmod_2 :::"(0)."::: ) (Set (Var "V")) ")" ) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rmod_2 :::"(0)."::: ) (Set (Var "V")))) & (Bool (Set (Set (Var "W")) ($#k2_rmod_3 :::"/\"::: ) (Set "(" ($#k1_rmod_2 :::"(0)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rmod_2 :::"(0)."::: ) (Set (Var "V")))) ")" )))) ; theorem :: RMOD_3:22 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_rmod_2 :::"(Omega)."::: ) (Set (Var "V")) ")" ) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Set (Set (Var "W")) ($#k2_rmod_3 :::"/\"::: ) (Set "(" ($#k2_rmod_2 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "W"))) ")" )))) ; theorem :: RMOD_3:23 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set "(" ($#k2_rmod_2 :::"(Omega)."::: ) (Set (Var "V")) ")" ) ($#k2_rmod_3 :::"/\"::: ) (Set "(" ($#k2_rmod_2 :::"(Omega)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "V"))))) ; theorem :: RMOD_3:24 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W2"))) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W2"))))))) ; theorem :: RMOD_3:25 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W2")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W2"))))))) ; theorem :: RMOD_3:26 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W1")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set "(" (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "W1"))))))) ; theorem :: RMOD_3:27 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k1_rmod_3 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W3")) ")" )) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Set (Var "W2")) ($#k2_rmod_3 :::"/\"::: ) (Set "(" (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W3")) ")" )))))) ; theorem :: RMOD_3:28 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W2")) ($#k2_rmod_3 :::"/\"::: ) (Set "(" (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k1_rmod_3 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W3")) ")" )))))) ; theorem :: RMOD_3:29 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W2")) "," (Set (Var "W1")) "," (Set (Var "W3")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W2")) ($#k1_rmod_3 :::"+"::: ) (Set "(" (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W3")) ")" )) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Set "(" (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k2_rmod_3 :::"/\"::: ) (Set "(" (Set (Var "W2")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W3")) ")" )))))) ; theorem :: RMOD_3:30 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W2")) ($#k1_rmod_3 :::"+"::: ) (Set "(" (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k2_rmod_3 :::"/\"::: ) (Set "(" (Set (Var "W2")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W3")) ")" )))))) ; theorem :: RMOD_3:31 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W3")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W1")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W3")))) "holds" (Bool (Set (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W3")))))))) ; theorem :: RMOD_3:32 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W2"))) "iff" (Bool (Set (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) ")" )))) ; theorem :: RMOD_3:33 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W3"))) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Set (Var "W2")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W3")))))))) ; theorem :: RMOD_3:34 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Set (Var "W2")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W3"))))))) ; theorem :: RMOD_3:35 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W3")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W3"))) & (Bool (Set (Var "W2")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W3")))) "holds" (Bool (Set (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W2"))) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W3")))))) ; theorem :: RMOD_3:36 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "W1")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W2"))) "or" (Bool (Set (Var "W2")) "is" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "W1"))) ")" ) "iff" (Bool "ex" (Set (Var "W")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "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 "R" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Const "R")); func :::"Submodules"::: "V" -> ($#m1_hidden :::"set"::: ) means :: RMOD_3: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" ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" "V" "st" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )); end; :: deftheorem defines :::"Submodules"::: RMOD_3:def 3 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_rmod_3 :::"Submodules"::: ) (Set (Var "V")))) "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" ($#v2_vectsp_2 :::"strict"::: ) ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ")" )) ")" )))); registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Const "R")); cluster (Set ($#k3_rmod_3 :::"Submodules"::: ) "V") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: RMOD_3:37 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) "holds" (Bool (Set (Var "V")) ($#r2_hidden :::"in"::: ) (Set ($#k3_rmod_3 :::"Submodules"::: ) (Set (Var "V")))))) ; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Const "R")); let "W1", "W2" be ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Const "V")); pred "V" :::"is_the_direct_sum_of"::: "W1" "," "W2" means :: RMOD_3:def 4 (Bool "(" (Bool (Set ($#g1_vectsp_2 :::"RightModStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_algstr_0 :::"U7"::: ) "of" "V") "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" "V") "," (Set "the" ($#u1_vectsp_2 :::"rmult"::: ) "of" "V") "#)" ) ($#r1_hidden :::"="::: ) (Set "W1" ($#k1_rmod_3 :::"+"::: ) "W2")) & (Bool (Set "W1" ($#k2_rmod_3 :::"/\"::: ) "W2") ($#r1_hidden :::"="::: ) (Set ($#k1_rmod_2 :::"(0)."::: ) "V")) ")" ); end; :: deftheorem defines :::"is_the_direct_sum_of"::: RMOD_3:def 4 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r1_rmod_3 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2"))) "iff" (Bool "(" (Bool (Set ($#g1_vectsp_2 :::"RightModStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"U7"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_vectsp_2 :::"rmult"::: ) "of" (Set (Var "V"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W2")))) & (Bool (Set (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rmod_2 :::"(0)."::: ) (Set (Var "V")))) ")" ) ")" )))); theorem :: RMOD_3:38 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_rmod_3 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool (Set (Var "V")) ($#r1_rmod_3 :::"is_the_direct_sum_of"::: ) (Set (Var "W2")) "," (Set (Var "W1")))))) ; theorem :: RMOD_3:39 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r1_rmod_3 :::"is_the_direct_sum_of"::: ) (Set ($#k1_rmod_2 :::"(0)."::: ) (Set (Var "V"))) "," (Set ($#k2_rmod_2 :::"(Omega)."::: ) (Set (Var "V")))) & (Bool (Set (Var "V")) ($#r1_rmod_3 :::"is_the_direct_sum_of"::: ) (Set ($#k2_rmod_2 :::"(Omega)."::: ) (Set (Var "V"))) "," (Set ($#k1_rmod_2 :::"(0)."::: ) (Set (Var "V")))) ")" ))) ; theorem :: RMOD_3:40 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "C1")) "being" ($#m2_rmod_2 :::"Coset"::: ) "of" (Set (Var "W1")) (Bool "for" (Set (Var "C2")) "being" ($#m2_rmod_2 :::"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_rmod_2 :::"Coset"::: ) "of" (Set (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W2"))))))))) ; theorem :: RMOD_3:41 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "V")) ($#r1_rmod_3 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2"))) "iff" (Bool "for" (Set (Var "C1")) "being" ($#m2_rmod_2 :::"Coset"::: ) "of" (Set (Var "W1")) (Bool "for" (Set (Var "C2")) "being" ($#m2_rmod_2 :::"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 :: RMOD_3:42 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#v2_vectsp_2 :::"strict"::: ) ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (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 :: RMOD_3:43 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "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_rmod_3 :::"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 :: RMOD_3:44 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (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_rmod_3 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))))) ; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Const "R")); let "v" be ($#m1_subset_1 :::"Vector":::) "of" (Set (Const "V")); let "W1", "W2" be ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Const "V")); assume (Bool (Set (Const "V")) ($#r1_rmod_3 :::"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 :: RMOD_3:def 5 (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 :::"|--"::: RMOD_3:def 5 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_rmod_3 :::"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 "V"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k4_rmod_3 :::"|--"::: ) "(" (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 :: RMOD_3:45 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "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_rmod_3 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k4_rmod_3 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k4_rmod_3 :::"|--"::: ) "(" (Set (Var "W2")) "," (Set (Var "W1")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) )))))) ; theorem :: RMOD_3:46 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "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_rmod_3 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k4_rmod_3 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ")" ) ($#k3_domain_1 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k4_rmod_3 :::"|--"::: ) "(" (Set (Var "W2")) "," (Set (Var "W1")) ")" ")" ) ($#k2_domain_1 :::"`1"::: ) )))))) ; definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Const "R")); func :::"SubJoin"::: "V" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_rmod_3 :::"Submodules"::: ) "V" ")" ) means :: RMOD_3:def 6 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_rmod_3 :::"Submodules"::: ) "V") (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "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_rmod_3 :::"+"::: ) (Set (Var "W2")))))); end; :: deftheorem defines :::"SubJoin"::: RMOD_3:def 6 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_rmod_3 :::"Submodules"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_rmod_3 :::"SubJoin"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_rmod_3 :::"Submodules"::: ) (Set (Var "V"))) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "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 "b3")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k1_rmod_3 :::"+"::: ) (Set (Var "W2")))))) ")" )))); definitionlet "R" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Const "R")); func :::"SubMeet"::: "V" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_rmod_3 :::"Submodules"::: ) "V" ")" ) means :: RMOD_3:def 7 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_rmod_3 :::"Submodules"::: ) "V") (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "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_rmod_3 :::"/\"::: ) (Set (Var "W2")))))); end; :: deftheorem defines :::"SubMeet"::: RMOD_3:def 7 : (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_rmod_3 :::"Submodules"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_rmod_3 :::"SubMeet"::: ) (Set (Var "V")))) "iff" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_rmod_3 :::"Submodules"::: ) (Set (Var "V"))) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rmod_2 :::"Submodule"::: ) "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 "b3")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "A1")) "," (Set (Var "A2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k2_rmod_3 :::"/\"::: ) (Set (Var "W2")))))) ")" )))); theorem :: RMOD_3:47 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_rmod_3 :::"Submodules"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k5_rmod_3 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k6_rmod_3 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#l3_lattices :::"Lattice":::)))) ; theorem :: RMOD_3:48 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_rmod_3 :::"Submodules"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k5_rmod_3 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k6_rmod_3 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#l3_lattices :::"0_Lattice":::)))) ; theorem :: RMOD_3:49 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_rmod_3 :::"Submodules"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k5_rmod_3 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k6_rmod_3 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#l3_lattices :::"1_Lattice":::)))) ; theorem :: RMOD_3:50 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_rmod_3 :::"Submodules"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k5_rmod_3 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k6_rmod_3 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#l3_lattices :::"01_Lattice":::)))) ; theorem :: RMOD_3:51 (Bool "for" (Set (Var "R")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_2 :::"RightMod":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#g3_lattices :::"LattStr"::: ) "(#" (Set "(" ($#k3_rmod_3 :::"Submodules"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k5_rmod_3 :::"SubJoin"::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k6_rmod_3 :::"SubMeet"::: ) (Set (Var "V")) ")" ) "#)" ) "is" ($#l3_lattices :::"M_Lattice":::)))) ;