Theorem mapdval3N

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

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

Proof

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