Theorem mapdval5N

Description: Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapdval4.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdval4.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdval4.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
	mapdval4.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	mapdval4.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	mapdval4.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	mapdval4.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdval4.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdval4.t	$$⊢\phi \to T\in S$$
Assertion	mapdval5N	$$⊢\phi \to M\left(T\right)=\bigcup _{v\in T}\left\{f\in F|O\left(\left\{v\right\}\right)=L\left(f\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		mapdval4.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdval4.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		mapdval4.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
4		mapdval4.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
5		mapdval4.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
6		mapdval4.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
7		mapdval4.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
8		mapdval4.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		mapdval4.t	$$⊢\phi \to T\in S$$
10	1 2 3 4 5 6 7 8 9	mapdval4N	$$⊢\phi \to M\left(T\right)=\left\{f\in F|\exists v\in TO\left(\left\{v\right\}\right)=L\left(f\right)\right\}$$
11		iunrab	$$⊢\bigcup _{v\in T}\left\{f\in F|O\left(\left\{v\right\}\right)=L\left(f\right)\right\}=\left\{f\in F|\exists v\in TO\left(\left\{v\right\}\right)=L\left(f\right)\right\}$$
12	10 11	eqtr4di	$$⊢\phi \to M\left(T\right)=\bigcup _{v\in T}\left\{f\in F|O\left(\left\{v\right\}\right)=L\left(f\right)\right\}$$