Theorem hdmap1eq4N

Description: Convert mapdheq4 to use HDMap1 function. (Contributed by NM, 17-May-2015) (New usage is discouraged.)

	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)$$
	hdmap1eq4.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap1eq4.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap1eq4.z	$$⊢\phi \to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap1eq4.ne	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{Z\right\}\right)$$
	hdmap1eq4.xn	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
	hdmap1eq4.eg	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)=G$$
	hdmap1eq4.ee	$$⊢\phi \to I\left(⟨X,F,Z⟩\right)=B$$
Assertion	hdmap1eq4N	$$⊢\phi \to I\left(⟨Y,G,Z⟩\right)=B$$

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		hdmap1eq4.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
15		hdmap1eq4.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
16		hdmap1eq4.z	$$⊢\phi \to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
17		hdmap1eq4.ne	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{Z\right\}\right)$$
18		hdmap1eq4.xn	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
19		hdmap1eq4.eg	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)=G$$
20		hdmap1eq4.ee	$$⊢\phi \to I\left(⟨X,F,Z⟩\right)=B$$
21		eqid	$$⊢{-}_U={-}_U$$
22		eqid	$$⊢{-}_C={-}_C$$
23		eqid	$$⊢0_C=0_C$$
24	1 2 11	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
25	14	eldifad	$$⊢\phi \to X\in V$$
26	15	eldifad	$$⊢\phi \to Y\in V$$
27	16	eldifad	$$⊢\phi \to Z\in V$$
28	3 5 24 25 26 27 18	lspindpi	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)\wedge N\left(\left\{X\right\}\right)\ne N\left(\left\{Z\right\}\right)\right)$$
29	28	simpld	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
30	1 2 3 4 5 6 7 8 9 10 11 12 13 29 14 26	hdmap1cl	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)\in D$$
31	19 30	eqeltrrd	$$⊢\phi \to G\in D$$
32		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)$$
33	1 2 3 21 4 5 6 7 22 23 8 9 10 11 15 31 27 32	hdmap1valc	$$⊢\phi \to I\left(⟨Y,G,Z⟩\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,Z⟩\right)$$
34	1 2 3 21 4 5 6 7 22 23 8 9 10 11 14 12 26 32	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)$$
35	34 19	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$$
36	1 2 3 21 4 5 6 7 22 23 8 9 10 11 14 12 27 32	hdmap1valc	$$⊢\phi \to I\left(⟨X,F,Z⟩\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,Z⟩\right)$$
37	36 20	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,Z⟩\right)=B$$
38	23 32 1 9 2 3 21 4 5 6 7 22 8 11 12 13 14 15 16 18 17 35 37	mapdheq4	$$⊢\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,Z⟩\right)=B$$
39	33 38	eqtrd	$$⊢\phi \to I\left(⟨Y,G,Z⟩\right)=B$$