Theorem hdmap1eq2

Description: Convert mapdheq2 to use HDMap1 function. (Contributed by NM, 16-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)$$
	hdmap1eq2.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
	hdmap1eq2.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap1eq2.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap1eq2.e	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)=G$$
Assertion	hdmap1eq2	$$⊢\phi \to I\left(⟨Y,G,X⟩\right)=F$$

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		hdmap1eq2.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
15		hdmap1eq2.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
16		hdmap1eq2.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
17		hdmap1eq2.e	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)=G$$
18		eqid	$$⊢{-}_U={-}_U$$
19		eqid	$$⊢{-}_C={-}_C$$
20		eqid	$$⊢0_C=0_C$$
21	16	eldifad	$$⊢\phi \to Y\in V$$
22	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 21	hdmap1cl	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)\in D$$
23	17 22	eqeltrrd	$$⊢\phi \to G\in D$$
24	15	eldifad	$$⊢\phi \to X\in V$$
25		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)$$
26	1 2 3 18 4 5 6 7 19 20 8 9 10 11 16 23 24 25	hdmap1valc	$$⊢\phi \to I\left(⟨Y,G,X⟩\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(⟨Y,G,X⟩\right)$$
27	1 2 3 18 4 5 6 7 19 20 8 9 10 11 15 12 21 25	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)$$
28	27 17	eqtr3d	$$⊢\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)=G$$
29	1 2 3 18 4 5 6 7 19 20 8 9 25 11 12 13 28 14 15 16	mapdh75e	$$⊢\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(⟨Y,G,X⟩\right)=F$$
30	26 29	eqtrd	$$⊢\phi \to I\left(⟨Y,G,X⟩\right)=F$$