Theorem hdmap1eu

Description: Convert mapdh9a to use the HDMap1 notation. (Contributed by NM, 15-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		hdmap1eu.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap1eu.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap1eu.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap1eu.o	$$⊢\underset{\dot{}}{0}=0_U$$
5		hdmap1eu.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
6		hdmap1eu.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
7		hdmap1eu.d	$$⊢D={\mathrm{Base}}_C$$
8		hdmap1eu.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
9		hdmap1eu.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
10		hdmap1eu.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
11		hdmap1eu.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12		hdmap1eu.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=L\left(\left\{F\right\}\right)$$
13		hdmap1eu.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
14		hdmap1eu.f	$$⊢\phi \to F\in D$$
15		hdmap1eu.t	$$⊢\phi \to T\in V$$
16		eqid	$$⊢{-}_U={-}_U$$
17		eqid	$$⊢{-}_C={-}_C$$
18		eqid	$$⊢0_C=0_C$$
19		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)$$
20	19	hdmap1cbv	$$⊢\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(w\in \mathrm{V}⟼if\left(2^{nd}\left(w\right)=\underset{\dot{}}{0},0_C,\left(\iota g\in D|\left(M\left(N\left(\left\{2^{nd}\left(w\right)\right\}\right)\right)=L\left(\left\{g\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(w\right)\right){-}_U{2}^{nd}\left(w\right)\right\}\right)\right)=L\left(\left\{2^{nd}\left(1^{st}\left(w\right)\right){-}_{C}g\right\}\right)\right)\right)\right)\right)$$
21	1 2 3 16 4 5 6 7 17 18 8 9 10 11 12 13 14 15 20	hdmap1eulem	$$⊢\phi \to \exists !y\in D\forall z\in V\left(\neg z\in \left(N\left(\left\{X\right\}\right)\cup N\left(\left\{T\right\}\right)\right)\to y=I\left(⟨z,I\left(⟨X,F,z⟩\right),T⟩\right)\right)$$