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=\mathrm{LHyp}\left(K\right)$$
	dih0vb.o	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	dih0vb.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dih0vb.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dih0vb.v	$$⊢V={\mathrm{Base}}_U$$
	dih0vb.z	$$⊢Z=0_U$$
	dih0vb.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	dih0vb.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dih0vb.x	$$⊢\phi \to X\in V$$
Assertion	dih0vbN	$$⊢\phi \to \left(X=Z\leftrightarrow N\left(\left\{X\right\}\right)=I\left(\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dih0vb.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dih0vb.o	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
3		dih0vb.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
4		dih0vb.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		dih0vb.v	$$⊢V={\mathrm{Base}}_U$$
6		dih0vb.z	$$⊢Z=0_U$$
7		dih0vb.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
8		dih0vb.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		dih0vb.x	$$⊢\phi \to X\in V$$
10	2 1 3 4 6	dih0	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to I\left(\underset{\dot{}}{0}\right)=\left\{Z\right\}$$
11	8 10	syl	$$⊢\phi \to I\left(\underset{\dot{}}{0}\right)=\left\{Z\right\}$$
12	11	eqeq2d	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)=I\left(\underset{\dot{}}{0}\right)\leftrightarrow N\left(\left\{X\right\}\right)=\left\{Z\right\}\right)$$
13	1 4 8	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
14	5 6 7	lspsneq0	$$⊢\left(U\in \mathrm{LMod}\wedge X\in V\right)\to \left(N\left(\left\{X\right\}\right)=\left\{Z\right\}\leftrightarrow X=Z\right)$$
15	13 9 14	syl2anc	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)=\left\{Z\right\}\leftrightarrow X=Z\right)$$
16	12 15	bitr2d	$$⊢\phi \to \left(X=Z\leftrightarrow N\left(\left\{X\right\}\right)=I\left(\underset{\dot{}}{0}\right)\right)$$