:: RANKNULL semantic presentation begin theorem :: RANKNULL:1 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g")) ")" )) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) ; theorem :: RANKNULL:2 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))) ; theorem :: RANKNULL:3 (Bool "for" (Set (Var "V")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "Y"))) "iff" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) ")" ))) ; registrationlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); cluster ($#v1_finset_1 :::"finite"::: ) for ($#m1_vectsp_7 :::"Basis"::: ) "of" "V"; end; registrationlet "F" be ($#l6_algstr_0 :::"Field":::); let "V", "W" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v13_vectsp_1 :::"additive"::: ) ($#v1_mod_2 :::"homogeneous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "W"))))); end; theorem :: RANKNULL:4 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "V"))) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set (Var "V")) "is" ($#v1_matrlin :::"finite-dimensional"::: ) ))) ; theorem :: RANKNULL:5 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )))) ; theorem :: RANKNULL:6 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Num 1)))) ; begin definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V", "W" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); mode linear-transformation of "V" "," "W" is ($#v13_vectsp_1 :::"additive"::: ) ($#v1_mod_2 :::"homogeneous"::: ) ($#m1_subset_1 :::"Function":::) "of" "V" "," "W"; end; theorem :: RANKNULL:7 (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "V")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "T"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "W")))) ")" ))) ; theorem :: RANKNULL:8 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ))))))) ; theorem :: RANKNULL:9 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "W"))))))) ; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V", "W" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "T" be ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Const "V")) "," (Set (Const "W")); func :::"ker"::: "T" -> ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" "V" means :: RANKNULL:def 1 (Bool (Set ($#k2_struct_0 :::"[#]"::: ) it) ($#r1_hidden :::"="::: ) "{" (Set (Var "u")) where u "is" ($#m1_subset_1 :::"Element":::) "of" "V" : (Bool (Set "T" ($#k3_funct_2 :::"."::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "W")) "}" ); end; :: deftheorem defines :::"ker"::: RANKNULL:def 1 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "b5")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_ranknull :::"ker"::: ) (Set (Var "T")))) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "u")) where u "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) : (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "W")))) "}" ) ")" ))))); theorem :: RANKNULL:10 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_ranknull :::"ker"::: ) (Set (Var "T")))) "iff" (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "W")))) ")" ))))) ; definitionlet "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "T" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "V")) "," (Set (Const "W")); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); :: original: :::".:"::: redefine func "T" :::".:"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "W"; end; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V", "W" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "T" be ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Const "V")) "," (Set (Const "W")); func :::"im"::: "T" -> ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" "W" means :: RANKNULL:def 2 (Bool (Set ($#k2_struct_0 :::"[#]"::: ) it) ($#r1_hidden :::"="::: ) (Set "T" ($#k2_ranknull :::".:"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) "V" ")" ))); end; :: deftheorem defines :::"im"::: RANKNULL:def 2 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "b5")) "being" ($#v7_vectsp_1 :::"strict"::: ) ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_ranknull :::"im"::: ) (Set (Var "T")))) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k2_ranknull :::".:"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "V")) ")" ))) ")" ))))); theorem :: RANKNULL:11 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_ranknull :::"ker"::: ) (Set (Var "T"))))))) ; theorem :: RANKNULL:12 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "T")) ($#k2_ranknull :::".:"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_ranknull :::"im"::: ) (Set (Var "T")) ")" )))))) ; theorem :: RANKNULL:13 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r1_struct_0 :::"in"::: ) (Set ($#k3_ranknull :::"im"::: ) (Set (Var "T")))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))) ")" ))))) ; theorem :: RANKNULL:14 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k1_ranknull :::"ker"::: ) (Set (Var "T")) ")" ) "holds" (Bool (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "W")))))))) ; theorem :: RANKNULL:15 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k1_ranknull :::"ker"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V"))))))) ; theorem :: RANKNULL:16 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) "holds" (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set "(" ($#k1_vectsp_4 :::"(0)."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"0"::: ) )))) ; theorem :: RANKNULL:17 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y"))) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_ranknull :::"ker"::: ) (Set (Var "T")))))))) ; theorem :: RANKNULL:18 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y"))) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ))))))) ; begin theorem :: RANKNULL:19 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) "is" ($#m1_vectsp_4 :::"Subspace"::: ) "of" (Set (Var "W")))) "holds" (Bool (Set (Var "X")) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "W")))))) ; theorem :: RANKNULL:20 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_vectsp_7 :::"linearly-independent"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#m1_vectsp_7 :::"Basis"::: ) "of" (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set (Var "A"))))))) ; theorem :: RANKNULL:21 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "x")) ($#r1_struct_0 :::"in"::: ) (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set (Var "A")))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) "is" ($#v1_vectsp_7 :::"linearly-dependent"::: ) ))))) ; theorem :: RANKNULL:22 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "B")) "being" ($#m1_vectsp_7 :::"Basis"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) "is" ($#m1_vectsp_7 :::"Basis"::: ) "of" (Set ($#k1_ranknull :::"ker"::: ) (Set (Var "T")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "T")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "B")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")) ")" )) "is" ($#v2_funct_1 :::"one-to-one"::: ) )))))) ; theorem :: RANKNULL:23 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "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")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F")) "holds" (Bool (Set (Set (Var "l")) ($#k15_funct_7 :::"+*"::: ) "(" (Set (Var "x")) "," (Set (Var "a")) ")" ) "is" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ))))))))) ; definitionlet "V" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); func "V" :::"\"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "V" equals :: RANKNULL:def 3 (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) "V" ")" ) ($#k7_subset_1 :::"\"::: ) "X"); end; :: deftheorem defines :::"\"::: RANKNULL:def 3 : (Bool "for" (Set (Var "V")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "V")) ($#k4_ranknull :::"\"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set (Var "V")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "X")))))); definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "l" be ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Const "V")); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); :: original: :::".:"::: redefine func "l" :::".:"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "F"; end; registrationlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); cluster ($#v1_vectsp_7 :::"linearly-dependent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V"))); end; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "l" be ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Const "V")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); func "l" :::"!"::: "A" -> ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" "A" equals :: RANKNULL:def 4 (Set (Set "(" "l" ($#k2_partfun1 :::"|"::: ) "A" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" "V" ($#k4_ranknull :::"\"::: ) "A" ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "F" ")" ) ")" )); end; :: deftheorem defines :::"!"::: RANKNULL:def 4 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "l")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "l")) ($#k6_ranknull :::"!"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "l")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set (Var "V")) ($#k4_ranknull :::"\"::: ) (Set (Var "A")) ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" ) ")" ))))))); theorem :: RANKNULL:24 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "l")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Var "l")) ($#r1_vectsp_6 :::"="::: ) (Set (Set (Var "l")) ($#k6_ranknull :::"!"::: ) (Set "(" ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l")) ")" )))))) ; theorem :: RANKNULL:25 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "l")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" (Set (Var "l")) ($#k6_ranknull :::"!"::: ) (Set (Var "A")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))))))))) ; theorem :: RANKNULL:26 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "l")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Set "(" (Set (Var "l")) ($#k6_ranknull :::"!"::: ) (Set (Var "A")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "F"))))))))) ; theorem :: RANKNULL:27 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "l")) "being" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "l")) ($#r1_vectsp_6 :::"="::: ) (Set (Set "(" (Set (Var "l")) ($#k6_ranknull :::"!"::: ) (Set (Var "A")) ")" ) ($#k5_vectsp_6 :::"+"::: ) (Set "(" (Set (Var "l")) ($#k6_ranknull :::"!"::: ) (Set "(" (Set (Var "B")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")) ")" ) ")" ))))))) ; registrationlet "F" be ($#l6_algstr_0 :::"Field":::); let "V" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "l" be ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Const "V")); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); cluster (Set "l" ($#k7_relat_1 :::".:"::: ) "X") -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "V", "W" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "T" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "V")) "," (Set (Const "W")); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "W")); :: original: :::"""::: redefine func "T" :::"""::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "V"; end; theorem :: RANKNULL:28 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "l")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l"))))) "holds" (Bool (Set (Set (Var "l")) ($#k5_ranknull :::".:"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" ) ($#k6_domain_1 :::"}"::: ) )))))) ; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V", "W" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "l" be ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Const "V")); let "T" be ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Const "V")) "," (Set (Const "W")); func "T" :::"@"::: "l" -> ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" "W" means :: RANKNULL:def 5 (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" "W" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" "l" ($#k5_ranknull :::".:"::: ) (Set "(" "T" ($#k7_ranknull :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" )))); end; :: deftheorem defines :::"@"::: RANKNULL:def 5 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "l")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "b6")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k8_ranknull :::"@"::: ) (Set (Var "l")))) "iff" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "W")) "holds" (Bool (Set (Set (Var "b6")) ($#k3_funct_2 :::"."::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rlvect_2 :::"Sum"::: ) (Set "(" (Set (Var "l")) ($#k5_ranknull :::".:"::: ) (Set "(" (Set (Var "T")) ($#k7_ranknull :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" )))) ")" )))))); theorem :: RANKNULL:29 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "l")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "T")) ($#k8_ranknull :::"@"::: ) (Set (Var "l"))) "is" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Set (Var "T")) ($#k2_ranknull :::".:"::: ) (Set "(" ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l")) ")" ))))))) ; theorem :: RANKNULL:30 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "l")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set "(" (Set (Var "T")) ($#k8_ranknull :::"@"::: ) (Set (Var "l")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "T")) ($#k2_ranknull :::".:"::: ) (Set "(" ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l")) ")" ))))))) ; theorem :: RANKNULL:31 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "l")) "," (Set (Var "m")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "m"))))) "holds" (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set "(" (Set (Var "l")) ($#k5_vectsp_6 :::"+"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "m")) ")" )))))) ; theorem :: RANKNULL:32 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "l")) "," (Set (Var "m")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "m"))))) "holds" (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set "(" (Set (Var "l")) ($#k8_vectsp_6 :::"-"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "m")) ")" )))))) ; theorem :: RANKNULL:33 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "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"))) & (Bool (Set (Var "B")) "is" ($#m1_vectsp_7 :::"Basis"::: ) "of" (Set (Var "V")))) "holds" (Bool (Set (Var "V")) ($#r1_vectsp_5 :::"is_the_direct_sum_of"::: ) (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set (Var "A"))) "," (Set ($#k1_vectsp_7 :::"Lin"::: ) (Set "(" (Set (Var "B")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")) ")" )))))) ; theorem :: RANKNULL:34 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (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")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "T")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "ex" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "T")) ($#k7_ranknull :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set (Var "X")))) ")" )))))))) ; theorem :: RANKNULL:35 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "l")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l")))) & (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "l")) ($#k5_ranknull :::".:"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" ) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: RANKNULL:36 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "l")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set "(" (Set (Var "T")) ($#k8_ranknull :::"@"::: ) (Set (Var "l")) ")" )))) "holds" (Bool (Set (Set (Var "T")) ($#k7_ranknull :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l"))))))))) ; theorem :: RANKNULL:37 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "l")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "T")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l")) ")" )) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l"))))) "holds" (Bool (Set (Set "(" (Set (Var "T")) ($#k8_ranknull :::"@"::: ) (Set (Var "l")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))))))))) ; theorem :: RANKNULL:38 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "l")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l")))) & (Bool (Set (Set (Var "T")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l")) ")" )) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set (Var "T")) ($#k4_finseqop :::"*"::: ) (Set "(" (Set (Var "l")) ($#k3_vectsp_6 :::"(#)"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "T")) ($#k8_ranknull :::"@"::: ) (Set (Var "l")) ")" ) ($#k3_vectsp_6 :::"(#)"::: ) (Set "(" (Set (Var "T")) ($#k4_finseqop :::"*"::: ) (Set (Var "G")) ")" )))))))) ; theorem :: RANKNULL:39 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "l")) "being" ($#m1_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "T")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l")) ")" )) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set (Var "T")) ($#k2_ranknull :::".:"::: ) (Set "(" ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set "(" (Set (Var "T")) ($#k8_ranknull :::"@"::: ) (Set (Var "l")) ")" ))))))) ; theorem :: RANKNULL:40 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "B")) "being" ($#m1_vectsp_7 :::"Basis"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "l")) "being" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Set (Var "B")) ($#k7_subset_1 :::"\"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set (Var "A")) "is" ($#m1_vectsp_7 :::"Basis"::: ) "of" (Set ($#k1_ranknull :::"ker"::: ) (Set (Var "T")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "l")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set "(" (Set (Var "T")) ($#k8_ranknull :::"@"::: ) (Set (Var "l")) ")" ))))))))) ; theorem :: RANKNULL:41 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_vectsp_7 :::"linearly-dependent"::: ) )) "holds" (Bool "ex" (Set (Var "l")) "being" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set ($#k1_vectsp_6 :::"Carrier"::: ) (Set (Var "l"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_vectsp_6 :::"Sum"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" ))))) ; definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V", "W" be ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); let "T" be ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Const "V")) "," (Set (Const "W")); let "l" be ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Set (Const "T")) ($#k2_ranknull :::".:"::: ) (Set (Const "X"))); assume (Bool (Set (Set (Const "T")) ($#k2_partfun1 :::"|"::: ) (Set (Const "X"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ; func "T" :::"#"::: "l" -> ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" "X" equals :: RANKNULL:def 6 (Set (Set "(" "l" ($#k1_partfun1 :::"*"::: ) "T" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" "V" ($#k4_ranknull :::"\"::: ) "X" ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "F" ")" ) ")" )); end; :: deftheorem defines :::"#"::: RANKNULL:def 6 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "l")) "being" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Set (Var "T")) ($#k2_ranknull :::".:"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Set (Var "T")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set (Var "T")) ($#k9_ranknull :::"#"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "l")) ($#k1_partfun1 :::"*"::: ) (Set (Var "T")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set (Var "V")) ($#k4_ranknull :::"\"::: ) (Set (Var "X")) ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" ) ")" )))))))); theorem :: RANKNULL:42 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "l")) "being" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Set (Var "T")) ($#k2_ranknull :::".:"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "T")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "T")) ($#k9_ranknull :::"#"::: ) (Set (Var "l")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "l")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ))))))))) ; theorem :: RANKNULL:43 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "W")) "," (Set (Var "V")) "being" ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "l")) "being" ($#m2_vectsp_6 :::"Linear_Combination"::: ) "of" (Set (Set (Var "T")) ($#k2_ranknull :::".:"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Set (Var "T")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set (Var "T")) ($#k8_ranknull :::"@"::: ) (Set "(" (Set (Var "T")) ($#k9_ranknull :::"#"::: ) (Set (Var "l")) ")" )) ($#r1_vectsp_6 :::"="::: ) (Set (Var "l")))))))) ; begin definitionlet "F" be ($#l6_algstr_0 :::"Field":::); let "V", "W" be ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Const "F")); let "T" be ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Const "V")) "," (Set (Const "W")); func :::"rank"::: "T" -> ($#m1_hidden :::"Nat":::) equals :: RANKNULL:def 7 (Set ($#k1_vectsp_9 :::"dim"::: ) (Set "(" ($#k3_ranknull :::"im"::: ) "T" ")" )); func :::"nullity"::: "T" -> ($#m1_hidden :::"Nat":::) equals :: RANKNULL:def 8 (Set ($#k1_vectsp_9 :::"dim"::: ) (Set "(" ($#k1_ranknull :::"ker"::: ) "T" ")" )); end; :: deftheorem defines :::"rank"::: RANKNULL:def 7 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set ($#k10_ranknull :::"rank"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set "(" ($#k3_ranknull :::"im"::: ) (Set (Var "T")) ")" )))))); :: deftheorem defines :::"nullity"::: RANKNULL:def 8 : (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set ($#k11_ranknull :::"nullity"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_vectsp_9 :::"dim"::: ) (Set "(" ($#k1_ranknull :::"ker"::: ) (Set (Var "T")) ")" )))))); theorem :: RANKNULL:44 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) "holds" (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_ranknull :::"rank"::: ) (Set (Var "T")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k11_ranknull :::"nullity"::: ) (Set (Var "T")) ")" )))))) ; theorem :: RANKNULL:45 (Bool "for" (Set (Var "F")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "V")) "," (Set (Var "W")) "being" ($#v1_matrlin :::"finite-dimensional"::: ) ($#l1_vectsp_1 :::"VectSp":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"linear-transformation":::) "of" (Set (Var "V")) "," (Set (Var "W")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k1_vectsp_9 :::"dim"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set ($#k10_ranknull :::"rank"::: ) (Set (Var "T"))))))) ;