Theorem dih0sb

Description: A subspace is zero iff the converse of its isomorphism is lattice zero. (Contributed by NM, 17-Aug-2014)

	Ref	Expression
Hypotheses	dih0sb.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dih0sb.o	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	dih0sb.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dih0sb.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dih0sb.v	$$⊢V={\mathrm{Base}}_U$$
	dih0sb.z	$$⊢Z=0_U$$
	dih0sb.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	dih0sb.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dih0sb.x	$$⊢\phi \to X\in \mathrm{ran}I$$
Assertion	dih0sb	$$⊢\phi \to \left(X=\left\{Z\right\}\leftrightarrow I^{-1}\left(X\right)=\underset{\dot{}}{0}\right)$$

Proof

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