tirix

$theorem dimkerim

* Given a homomorphism of vector spaces ` F ` over ` W ` , the dimension of
  the vector space ` W ` is the sum of the dimension of ` F ` 's kernel and
  the dimension of ` F ` 's image.  Second part of theorem 5.3 in [Lang] p. 141

h1::dimkerim.1                                      |- .0. = ( 0g ` U )
h2::dimkerim.k                                        |- K = ( V |`s ( `' F " { .0. } ) )
h3::dimkerim.i                    |- I = ( U |`s ran F )
4:1,2:kerlmhm              |- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> K e. LVec )

tirix

$theorem f1ghm0to0

* If a group homomorphism ` F ` is injective, it maps the zero of one
       group (and only the zero) to the zero of the other group.  (Contributed
       by AV, 24-Oct-2019.)  (Revised by Thierry Arnoux, 13-May-2023.)

h1::f1ghm0to0.a          |- A = ( Base ` R )
h2::f1ghm0to0.b    |- B = ( Base ` S )
h3::f1ghm0to0.n         |- N = ( 0g ` S )
h4::f1ghm0to0.1          |- .0. = ( 0g ` R )

tirix

$theorem crash

* MissingComment

10::                |- ( ph <-> ( ps /\ th ) )
20:10:biimpar      
qed::              |- ( et -> ph )