Theorem dochoc1

Description: The unit subspace (all vectors) is closed. (Contributed by NM, 16-Feb-2015)

	Ref	Expression
Hypotheses	dochoc1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dochoc1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dochoc1.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	dochoc1.v	$$⊢V={\mathrm{Base}}_U$$
	dochoc1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	dochoc1	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(V\right)\right)=V$$

Proof

Step	Hyp	Ref	Expression
1		dochoc1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dochoc1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		dochoc1.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
4		dochoc1.v	$$⊢V={\mathrm{Base}}_U$$
5		dochoc1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
6		eqid	$$⊢0_U=0_U$$
7	1 2 3 4 6	doch1	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \underset{\dot{}}{\perp }\left(V\right)=\left\{0_U\right\}$$
8	7	fveq2d	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(V\right)\right)=\underset{\dot{}}{\perp }\left(\left\{0_U\right\}\right)$$
9	1 2 3 4 6	doch0	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \underset{\dot{}}{\perp }\left(\left\{0_U\right\}\right)=V$$
10	8 9	eqtrd	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(V\right)\right)=V$$
11	5 10	syl	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(V\right)\right)=V$$