This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ˙