Metamath Proof Explorer


Theorem dih0vbN

Description: A vector is zero iff its span is the isomorphism of lattice zero. (Contributed by NM, 16-Aug-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dih0vb.h H = LHyp K
dih0vb.o 0 ˙ = 0. K
dih0vb.i I = DIsoH K W
dih0vb.u U = DVecH K W
dih0vb.v V = Base U
dih0vb.z Z = 0 U
dih0vb.n N = LSpan U
dih0vb.k φ K HL W H
dih0vb.x φ X V
Assertion dih0vbN φ X = Z N X = I 0 ˙

Proof

Step Hyp Ref Expression
1 dih0vb.h H = LHyp K
2 dih0vb.o 0 ˙ = 0. K
3 dih0vb.i I = DIsoH K W
4 dih0vb.u U = DVecH K W
5 dih0vb.v V = Base U
6 dih0vb.z Z = 0 U
7 dih0vb.n N = LSpan U
8 dih0vb.k φ K HL W H
9 dih0vb.x φ X V
10 2 1 3 4 6 dih0 K HL W H I 0 ˙ = Z
11 8 10 syl φ I 0 ˙ = Z
12 11 eqeq2d φ N X = I 0 ˙ N X = Z
13 1 4 8 dvhlmod φ U LMod
14 5 6 7 lspsneq0 U LMod X V N X = Z X = Z
15 13 9 14 syl2anc φ N X = Z X = Z
16 12 15 bitr2d φ X = Z N X = I 0 ˙