Theorem mapdhcl

Description: Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015)

	Ref	Expression
Hypotheses	mapdh.q	$$⊢Q=0_C$$
	mapdh.i	$$⊢I=\left(x\in \mathrm{V}⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$
	mapdh.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdh.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdh.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdh.v	$$⊢V={\mathrm{Base}}_U$$
	mapdh.s	$$⊢\underset{\dot{}}{-}={-}_U$$
	mapdhc.o	$$⊢\underset{\dot{}}{0}=0_U$$
	mapdh.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	mapdh.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	mapdh.d	$$⊢D={\mathrm{Base}}_C$$
	mapdh.r	$$⊢R={-}_C$$
	mapdh.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
	mapdh.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdhc.f	$$⊢\phi \to F\in D$$
	mapdh.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{F\right\}\right)$$
	mapdhcl.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	mapdhc.y	$$⊢\phi \to Y\in V$$
	mapdh.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
Assertion	mapdhcl	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)\in D$$

Proof

Step	Hyp	Ref	Expression
1		mapdh.q	$$⊢Q=0_C$$
2		mapdh.i	$$⊢I=\left(x\in \mathrm{V}⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$
3		mapdh.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		mapdh.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
5		mapdh.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
6		mapdh.v	$$⊢V={\mathrm{Base}}_U$$
7		mapdh.s	$$⊢\underset{\dot{}}{-}={-}_U$$
8		mapdhc.o	$$⊢\underset{\dot{}}{0}=0_U$$
9		mapdh.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
10		mapdh.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
11		mapdh.d	$$⊢D={\mathrm{Base}}_C$$
12		mapdh.r	$$⊢R={-}_C$$
13		mapdh.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
14		mapdh.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
15		mapdhc.f	$$⊢\phi \to F\in D$$
16		mapdh.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{F\right\}\right)$$
17		mapdhcl.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
18		mapdhc.y	$$⊢\phi \to Y\in V$$
19		mapdh.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
20		oteq3	$$⊢Y=\underset{\dot{}}{0}\to ⟨X,F,Y⟩=⟨X,F,\underset{\dot{}}{0}⟩$$
21	20	fveq2d	$$⊢Y=\underset{\dot{}}{0}\to I\left(⟨X,F,Y⟩\right)=I\left(⟨X,F,\underset{\dot{}}{0}⟩\right)$$
22	21	eleq1d	$$⊢Y=\underset{\dot{}}{0}\to \left(I\left(⟨X,F,Y⟩\right)\in D\leftrightarrow I\left(⟨X,F,\underset{\dot{}}{0}⟩\right)\in D\right)$$
23	17	adantr	$$⊢\left(\phi \wedge Y\ne \underset{\dot{}}{0}\right)\to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
24	15	adantr	$$⊢\left(\phi \wedge Y\ne \underset{\dot{}}{0}\right)\to F\in D$$
25	18	anim1i	$$⊢\left(\phi \wedge Y\ne \underset{\dot{}}{0}\right)\to \left(Y\in V\wedge Y\ne \underset{\dot{}}{0}\right)$$
26		eldifsn	$$⊢Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(Y\in V\wedge Y\ne \underset{\dot{}}{0}\right)$$
27	25 26	sylibr	$$⊢\left(\phi \wedge Y\ne \underset{\dot{}}{0}\right)\to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
28	1 2 23 24 27	mapdhval2	$$⊢\left(\phi \wedge Y\ne \underset{\dot{}}{0}\right)\to I\left(⟨X,F,Y⟩\right)=\left(\iota h\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{FRh\right\}\right)\right)\right)$$
29	14	adantr	$$⊢\left(\phi \wedge Y\ne \underset{\dot{}}{0}\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
30	19	adantr	$$⊢\left(\phi \wedge Y\ne \underset{\dot{}}{0}\right)\to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
31	16	adantr	$$⊢\left(\phi \wedge Y\ne \underset{\dot{}}{0}\right)\to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{F\right\}\right)$$
32	3 4 5 6 7 8 9 10 11 12 13 29 23 27 24 30 31	mapdpg	$$⊢\left(\phi \wedge Y\ne \underset{\dot{}}{0}\right)\to \exists !h\in D\left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{FRh\right\}\right)\right)$$
33		riotacl	$$⊢\exists !h\in D\left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{FRh\right\}\right)\right)\to \left(\iota h\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{FRh\right\}\right)\right)\right)\in D$$
34	32 33	syl	$$⊢\left(\phi \wedge Y\ne \underset{\dot{}}{0}\right)\to \left(\iota h\in D|\left(M\left(N\left(\left\{Y\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{FRh\right\}\right)\right)\right)\in D$$
35	28 34	eqeltrd	$$⊢\left(\phi \wedge Y\ne \underset{\dot{}}{0}\right)\to I\left(⟨X,F,Y⟩\right)\in D$$
36	1 2 8 17 15	mapdhval0	$$⊢\phi \to I\left(⟨X,F,\underset{\dot{}}{0}⟩\right)=Q$$
37	3 10 11 1 14	lcd0vcl	$$⊢\phi \to Q\in D$$
38	36 37	eqeltrd	$$⊢\phi \to I\left(⟨X,F,\underset{\dot{}}{0}⟩\right)\in D$$
39	22 35 38	pm2.61ne	$$⊢\phi \to I\left(⟨X,F,Y⟩\right)\in D$$