Theorem dih0cnv

Description: The isomorphism H converse value of the zero subspace is the lattice zero. (Contributed by NM, 19-Jun-2014)

	Ref	Expression
Hypotheses	dih0cnv.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dih0cnv.o	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	dih0cnv.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dih0cnv.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dih0cnv.z	$$⊢Z=0_U$$
Assertion	dih0cnv	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to I^{-1}\left(\left\{Z\right\}\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		dih0cnv.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dih0cnv.o	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
3		dih0cnv.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
4		dih0cnv.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		dih0cnv.z	$$⊢Z=0_U$$
6	2 1 3 4 5	dih0	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to I\left(\underset{\dot{}}{0}\right)=\left\{Z\right\}$$
7	6	fveq2d	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to I^{-1}\left(I\left(\underset{\dot{}}{0}\right)\right)=I^{-1}\left(\left\{Z\right\}\right)$$
8		hlatl	$$⊢K\in \mathrm{HL}\to K\in \mathrm{AtLat}$$
9	8	adantr	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to K\in \mathrm{AtLat}$$
10		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
11	10 2	atl0cl	$$⊢K\in \mathrm{AtLat}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_K$$
12	9 11	syl	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \underset{\dot{}}{0}\in {\mathrm{Base}}_K$$
13	10 1 3	dihcnvid1	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_K\right)\to I^{-1}\left(I\left(\underset{\dot{}}{0}\right)\right)=\underset{\dot{}}{0}$$
14	12 13	mpdan	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to I^{-1}\left(I\left(\underset{\dot{}}{0}\right)\right)=\underset{\dot{}}{0}$$
15	7 14	eqtr3d	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to I^{-1}\left(\left\{Z\right\}\right)=\underset{\dot{}}{0}$$