Theorem hdmap1cl

Description: Convert closure theorem mapdhcl to use HDMap1 function. (Contributed by NM, 15-May-2015)

	Ref	Expression
Hypotheses	hdmap1eq2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap1eq2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap1eq2.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap1eq2.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmap1eq2.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hdmap1eq2.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap1eq2.d	$$⊢D={\mathrm{Base}}_C$$
	hdmap1eq2.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
	hdmap1eq2.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	hdmap1eq2.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
	hdmap1eq2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap1eq2.f	$$⊢\phi \to F\in D$$
	hdmap1eq2.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=L\left(\left\{F\right\}\right)$$
	hdmap1cl.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
	hdmap1cl.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap1cl.y	$$⊢\phi \to Y\in V$$
Assertion	hdmap1cl	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)\in D$$

Proof

Step	Hyp	Ref	Expression
1		hdmap1eq2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap1eq2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap1eq2.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap1eq2.o	$$⊢\underset{\dot{}}{0}=0_U$$
5		hdmap1eq2.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
6		hdmap1eq2.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
7		hdmap1eq2.d	$$⊢D={\mathrm{Base}}_C$$
8		hdmap1eq2.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
9		hdmap1eq2.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
10		hdmap1eq2.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
11		hdmap1eq2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12		hdmap1eq2.f	$$⊢\phi \to F\in D$$
13		hdmap1eq2.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=L\left(\left\{F\right\}\right)$$
14		hdmap1cl.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
15		hdmap1cl.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
16		hdmap1cl.y	$$⊢\phi \to Y\in V$$
17		eqid	$$⊢{-}_U={-}_U$$
18		eqid	$$⊢{-}_C={-}_C$$
19		eqid	$$⊢0_C=0_C$$
20		eqid	$$⊢\left(x\in \mathrm{V}⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},0_C,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=L\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_U{2}^{nd}\left(x\right)\right\}\right)\right)=L\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{C}h\right\}\right)\right)\right)\right)\right)=\left(x\in \mathrm{V}⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},0_C,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=L\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_U{2}^{nd}\left(x\right)\right\}\right)\right)=L\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{C}h\right\}\right)\right)\right)\right)\right)$$
21	1 2 3 17 4 5 6 7 18 19 8 9 10 11 15 12 16 20	hdmap1valc	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)=\left(x\in \mathrm{V}⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},0_C,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=L\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_U{2}^{nd}\left(x\right)\right\}\right)\right)=L\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{C}h\right\}\right)\right)\right)\right)\right)\left(⟨X,F,Y⟩\right)$$
22	19 20 1 9 2 3 17 4 5 6 7 18 8 11 12 13 15 16 14	mapdhcl	$$⊢\phi \to \left(x\in \mathrm{V}⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},0_C,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=L\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right){-}_U{2}^{nd}\left(x\right)\right\}\right)\right)=L\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right){-}_{C}h\right\}\right)\right)\right)\right)\right)\left(⟨X,F,Y⟩\right)\in D$$
23	21 22	eqeltrd	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)\in D$$