Theorem mapdhvmap

Description: Relationship between mapd and HVMap , which can be used to satisfy the last hypothesis of mapdpg . Equation 10 of Baer p. 48. (Contributed by NM, 29-Mar-2015)

	Ref	Expression
Hypotheses	mapdhvmap.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdhvmap.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdhvmap.v	$$⊢V={\mathrm{Base}}_U$$
	mapdhvmap.z	$$⊢\underset{\dot{}}{0}=0_U$$
	mapdhvmap.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	mapdhvmap.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	mapdhvmap.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
	mapdhvmap.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdhvmap.p	$$⊢P=\mathrm{HVMap}\left(K\right)\left(W\right)$$
	mapdhvmap.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdhvmap.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	mapdhvmap	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{P\left(X\right)\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		mapdhvmap.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdhvmap.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		mapdhvmap.v	$$⊢V={\mathrm{Base}}_U$$
4		mapdhvmap.z	$$⊢\underset{\dot{}}{0}=0_U$$
5		mapdhvmap.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
6		mapdhvmap.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
7		mapdhvmap.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
8		mapdhvmap.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
9		mapdhvmap.p	$$⊢P=\mathrm{HVMap}\left(K\right)\left(W\right)$$
10		mapdhvmap.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
11		mapdhvmap.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
12		eqid	$$⊢\mathrm{ocH}\left(K\right)\left(W\right)=\mathrm{ocH}\left(K\right)\left(W\right)$$
13		eqid	$$⊢\mathrm{LFnl}\left(U\right)=\mathrm{LFnl}\left(U\right)$$
14		eqid	$$⊢\mathrm{LKer}\left(U\right)=\mathrm{LKer}\left(U\right)$$
15		eqid	$$⊢\mathrm{LDual}\left(U\right)=\mathrm{LDual}\left(U\right)$$
16		eqid	$$⊢\mathrm{LSpan}\left(\mathrm{LDual}\left(U\right)\right)=\mathrm{LSpan}\left(\mathrm{LDual}\left(U\right)\right)$$
17	11	eldifad	$$⊢\phi \to X\in V$$
18	1 2 3 4 13 9 10 11	hvmaplfl	$$⊢\phi \to P\left(X\right)\in \mathrm{LFnl}\left(U\right)$$
19	1 12 2 3 4 14 9 10 11	hvmaplkr	$$⊢\phi \to \mathrm{LKer}\left(U\right)\left(P\left(X\right)\right)=\mathrm{ocH}\left(K\right)\left(W\right)\left(\left\{X\right\}\right)$$
20	1 12 8 2 3 5 13 14 15 16 10 17 18 19	mapdsn3	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=\mathrm{LSpan}\left(\mathrm{LDual}\left(U\right)\right)\left(\left\{P\left(X\right)\right\}\right)$$
21		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
22		eqid	$$⊢0_C=0_C$$
23	1 2 3 4 6 21 22 9 10 11	hvmapcl2	$$⊢\phi \to P\left(X\right)\in \left({\mathrm{Base}}_C\setminus \left\{0_C\right\}\right)$$
24	23	eldifad	$$⊢\phi \to P\left(X\right)\in {\mathrm{Base}}_C$$
25	24	snssd	$$⊢\phi \to \left\{P\left(X\right)\right\}\subseteq {\mathrm{Base}}_C$$
26	1 2 15 16 6 21 7 10 25	lcdlsp	$$⊢\phi \to J\left(\left\{P\left(X\right)\right\}\right)=\mathrm{LSpan}\left(\mathrm{LDual}\left(U\right)\right)\left(\left\{P\left(X\right)\right\}\right)$$
27	20 26	eqtr4d	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{P\left(X\right)\right\}\right)$$