:: LMOD_6 semantic presentation begin notationlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); synonym :::"Submodules"::: "V" for :::"Subspaces"::: "V"; end; theorem :: LMOD_6:1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M2"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "M2"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "M2"))) "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "M2"))) "#)" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "M1"))) "iff" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "M2"))) ")" )))) ; theorem :: LMOD_6:2 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "V"))) "#)" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool (Set (Set (Var "r")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "v"))))))))) ; theorem :: LMOD_6:3 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "V"))) "#)" ) "is" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V"))))) ; theorem :: LMOD_6:4 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "holds" (Bool (Set (Var "V")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "V")))))) ; begin definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); redefine attr "K" is :::"trivial"::: means :: LMOD_6:def 1 (Bool (Set ($#k4_struct_0 :::"0."::: ) "K") ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) "K")); end; :: deftheorem defines :::"trivial"::: LMOD_6:def 1 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) "holds" (Bool "(" (Bool (Set (Var "K")) "is" ($#v7_struct_0 :::"trivial"::: ) ) "iff" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K")))) ")" )); theorem :: LMOD_6:5 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "K")) "is" ($#v7_struct_0 :::"trivial"::: ) )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" ) ")" ))) ; theorem :: LMOD_6:6 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "K")) "is" ($#v7_struct_0 :::"trivial"::: ) )) "holds" (Bool (Set (Var "V")) "is" ($#v7_struct_0 :::"trivial"::: ) ))) ; theorem :: LMOD_6:7 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "V")) "is" ($#v7_struct_0 :::"trivial"::: ) ) "iff" (Bool (Set ($#g1_vectsp_1 :::"VectSpStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "V"))) "," (Set "the" ($#u1_vectsp_1 :::"lmult"::: ) "of" (Set (Var "V"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V")))) ")" ))) ; begin definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); func :::"@"::: "W" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_vectsp_5 :::"Submodules"::: ) "V") equals :: LMOD_6:def 2 "W"; end; :: deftheorem defines :::"@"::: LMOD_6:def 2 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_lmod_6 :::"@"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "W")))))); theorem :: LMOD_6:8 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "W")) "holds" (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))))))) ; definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "W")); func :::"@"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "V" equals :: LMOD_6:def 3 "A"; end; :: deftheorem defines :::"@"::: LMOD_6:def 3 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "W")) "holds" (Bool (Set ($#k2_lmod_6 :::"@"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))))); registrationlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "W" be ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Const "V")); let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "W")); cluster (Set ($#k2_lmod_6 :::"@"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: LMOD_6:9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "V")))) "iff" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "V"))) ")" )))) ; theorem :: LMOD_6:10 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_lmod_6 :::"@"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "W")) ")" ))) "iff" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W"))) ")" ))))) ; theorem :: LMOD_6:11 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k1_mod_3 :::"Lin"::: ) (Set (Var "A")) ")" )))))) ; theorem :: LMOD_6:12 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "l")) "being" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) "is" ($#v1_vectsp_4 :::"linearly-closed"::: ) )) "holds" (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "l"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))))) ; theorem :: LMOD_6:13 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) "is" ($#v1_vectsp_4 :::"linearly-closed"::: ) )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k1_mod_3 :::"Lin"::: ) (Set (Var "A")) ")" )))))) ; begin definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "V" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); let "a" be ($#m1_subset_1 :::"Vector":::) "of" (Set (Const "V")); func :::"<:":::"a":::":>"::: -> ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" "V" equals :: LMOD_6:def 4 (Set ($#k1_mod_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) "a" ($#k6_domain_1 :::"}"::: ) )); end; :: deftheorem defines :::"<:"::: LMOD_6:def 4 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k3_lmod_6 :::"<:"::: ) (Set (Var "a")) ($#k3_lmod_6 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_mod_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )))))); begin definitionlet "K" be ($#l6_algstr_0 :::"Ring":::); let "M", "N" be ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")); pred "M" :::"c="::: "N" means :: LMOD_6:def 5 (Bool "M" "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" "N"); reflexivity (Bool "for" (Set (Var "M")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Const "K")) "holds" (Bool (Set (Var "M")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "M")))) ; end; :: deftheorem defines :::"c="::: LMOD_6:def 5 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "N"))) "iff" (Bool (Set (Var "M")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "N"))) ")" ))); theorem :: LMOD_6:14 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "M")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "N")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "M")))) "implies" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set (Var "N"))) ")" & "(" (Bool (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "M")))) "implies" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "N"))) ")" ")" )))) ; theorem :: LMOD_6:15 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "M")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "N")))) "holds" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "N")))) & "(" (Bool (Bool (Set (Var "m1")) ($#r1_hidden :::"="::: ) (Set (Var "n1"))) & (Bool (Set (Var "m2")) ($#r1_hidden :::"="::: ) (Set (Var "n2")))) "implies" (Bool (Set (Set (Var "m1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "n2")))) ")" & "(" (Bool (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "implies" (Bool (Set (Set (Var "r")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "n")))) ")" & "(" (Bool (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "implies" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "m")))) ")" & "(" (Bool (Bool (Set (Var "m1")) ($#r1_hidden :::"="::: ) (Set (Var "n1"))) & (Bool (Set (Var "m2")) ($#r1_hidden :::"="::: ) (Set (Var "n2")))) "implies" (Bool (Set (Set (Var "m1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "n2")))) ")" & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "N"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "M"))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "M"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "N"))) & "(" (Bool (Bool (Set (Var "n1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "n2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "M")))) "implies" (Bool (Set (Set (Var "n1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "n2"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "M"))) ")" & "(" (Bool (Bool (Set (Var "n")) ($#r1_struct_0 :::"in"::: ) (Set (Var "M")))) "implies" (Bool (Set (Set (Var "r")) ($#k4_vectsp_1 :::"*"::: ) (Set (Var "n"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "M"))) ")" & "(" (Bool (Bool (Set (Var "n")) ($#r1_struct_0 :::"in"::: ) (Set (Var "M")))) "implies" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "n"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "M"))) ")" & "(" (Bool (Bool (Set (Var "n1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "M"))) & (Bool (Set (Var "n2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "M")))) "implies" (Bool (Set (Set (Var "n1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "n2"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "M"))) ")" ")" )))))) ; theorem :: LMOD_6:16 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "N")) "," (Set (Var "M2")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "N"))) & (Bool (Set (Var "M2")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "N")))) "holds" (Bool "(" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "M2")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "M1"))) ($#r1_struct_0 :::"in"::: ) (Set (Var "M2"))) & "(" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M2"))))) "implies" (Bool (Set (Var "M1")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "M2"))) ")" & "(" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "n")) ($#r1_struct_0 :::"in"::: ) (Set (Var "M1")))) "holds" (Bool (Set (Var "n")) ($#r1_struct_0 :::"in"::: ) (Set (Var "M2"))) ")" )) "implies" (Bool (Set (Var "M1")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "M2"))) ")" & "(" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M2")))) & (Bool (Set (Var "M1")) "is" ($#v7_vectsp_1 :::"strict"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v7_vectsp_1 :::"strict"::: ) )) "implies" (Bool (Set (Var "M1")) ($#r1_hidden :::"="::: ) (Set (Var "M2"))) ")" & (Bool (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "M1"))) ($#r1_lmod_6 :::"c="::: ) (Set (Var "M2"))) ")" ))) ; theorem :: LMOD_6:17 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "," (Set (Var "M")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "V")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "M"))) & (Bool (Set (Var "M")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "V")))) "holds" (Bool (Set (Var "V")) ($#r1_hidden :::"="::: ) (Set (Var "M"))))) ; theorem :: LMOD_6:18 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "," (Set (Var "M")) "," (Set (Var "N")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "V")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "M"))) & (Bool (Set (Var "M")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "N")))) "holds" (Bool (Set (Var "V")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "N"))))) ; theorem :: LMOD_6:19 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "M")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "M"))) ($#r1_lmod_6 :::"c="::: ) (Set (Var "N"))))) ; theorem :: LMOD_6:20 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "M")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "N"))) ($#r1_lmod_6 :::"c="::: ) (Set (Var "M"))))) ; theorem :: LMOD_6:21 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "M")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "N")))) "holds" (Bool (Set (Var "M")) ($#r1_lmod_6 :::"c="::: ) (Set ($#k2_vectsp_4 :::"(Omega)."::: ) (Set (Var "N")))))) ; theorem :: LMOD_6:22 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "W1")) ($#r1_lmod_6 :::"c="::: ) (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")))) & (Bool (Set (Var "W2")) ($#r1_lmod_6 :::"c="::: ) (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")))) ")" )))) ; theorem :: LMOD_6:23 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W1"))) & (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W2"))) ")" )))) ; theorem :: LMOD_6:24 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3"))) ($#r1_lmod_6 :::"c="::: ) (Set (Set (Var "W2")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3"))))))) ; theorem :: LMOD_6:25 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W3")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W3")))) "holds" (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W3")))))) ; theorem :: LMOD_6:26 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W2"))) & (Bool (Set (Var "W1")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W3")))) "holds" (Bool (Set (Var "W1")) ($#r1_lmod_6 :::"c="::: ) (Set (Set (Var "W2")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3"))))))) ; theorem :: LMOD_6:27 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2"))) ($#r1_lmod_6 :::"c="::: ) (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2"))))))) ; theorem :: LMOD_6:28 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k1_vectsp_5 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3")) ")" )) ($#r1_lmod_6 :::"c="::: ) (Set (Set (Var "W2")) ($#k2_vectsp_5 :::"/\"::: ) (Set "(" (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W3")) ")" )))))) ; theorem :: LMOD_6:29 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W2")) ($#k2_vectsp_5 :::"/\"::: ) (Set "(" (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W2")) ")" ) ($#k1_vectsp_5 :::"+"::: ) (Set "(" (Set (Var "W2")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3")) ")" )))))) ; theorem :: LMOD_6:30 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W2")) "," (Set (Var "W1")) "," (Set (Var "W3")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "W2")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3")) ")" )) ($#r1_lmod_6 :::"c="::: ) (Set (Set "(" (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k2_vectsp_5 :::"/\"::: ) (Set "(" (Set (Var "W2")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W3")) ")" )))))) ; theorem :: LMOD_6:31 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W2")) ($#k1_vectsp_5 :::"+"::: ) (Set "(" (Set (Var "W1")) ($#k2_vectsp_5 :::"/\"::: ) (Set (Var "W3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2")) ")" ) ($#k2_vectsp_5 :::"/\"::: ) (Set "(" (Set (Var "W2")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W3")) ")" )))))) ; theorem :: LMOD_6:32 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "," (Set (Var "W3")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Var "W1")) ($#r1_lmod_6 :::"c="::: ) (Set (Set (Var "W2")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W3"))))))) ; theorem :: LMOD_6:33 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W3")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W3"))) & (Bool (Set (Var "W2")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W3")))) "holds" (Bool (Set (Set (Var "W1")) ($#k1_vectsp_5 :::"+"::: ) (Set (Var "W2"))) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W3")))))) ; theorem :: LMOD_6:34 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k1_mod_3 :::"Lin"::: ) (Set (Var "A"))) ($#r1_lmod_6 :::"c="::: ) (Set ($#k1_mod_3 :::"Lin"::: ) (Set (Var "B"))))))) ; theorem :: LMOD_6:35 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_mod_3 :::"Lin"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" )) ($#r1_lmod_6 :::"c="::: ) (Set (Set "(" ($#k1_mod_3 :::"Lin"::: ) (Set (Var "A")) ")" ) ($#k2_vectsp_5 :::"/\"::: ) (Set "(" ($#k1_mod_3 :::"Lin"::: ) (Set (Var "B")) ")" )))))) ; theorem :: LMOD_6:36 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "M2")))) "holds" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "M1"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "M2")))))) ; theorem :: LMOD_6:37 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "W1")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W2"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1")))) "holds" (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2")))) ")" )))) ; theorem :: LMOD_6:38 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "W1")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W2"))) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "W1"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "W2")))) ")" )))) ; theorem :: LMOD_6:39 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "W1")) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W2"))) "iff" (Bool (Set ($#k2_lmod_6 :::"@"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "W1")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_lmod_6 :::"@"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "W2")) ")" ))) ")" )))) ; theorem :: LMOD_6:40 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Ring":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"LeftMod":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "W")) "," (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "W"))) ($#r1_lmod_6 :::"c="::: ) (Set (Var "V"))) & (Bool (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V"))) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W"))) & (Bool (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "W1"))) ($#r1_lmod_6 :::"c="::: ) (Set (Var "W2"))) ")" )))) ;