Theorem mapdrn

Description: Range of the map defined by df-mapd . (Contributed by NM, 12-Mar-2015)

	Ref	Expression
Hypotheses	mapdrn.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdrn.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	mapdrn.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdrn.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdrn.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	mapdrn.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	mapdrn.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	mapdrn.t	$$⊢T=\mathrm{LSubSp}\left(D\right)$$
	mapdrn.c	$$⊢C=\left\{g\in F|O\left(O\left(L\left(g\right)\right)\right)=L\left(g\right)\right\}$$
	mapdrn.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	mapdrn	$$⊢\phi \to \mathrm{ran}M=T\cap 𝒫C$$

Proof

Step	Hyp	Ref	Expression
1		mapdrn.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdrn.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		mapdrn.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
4		mapdrn.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		mapdrn.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
6		mapdrn.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
7		mapdrn.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
8		mapdrn.t	$$⊢T=\mathrm{LSubSp}\left(D\right)$$
9		mapdrn.c	$$⊢C=\left\{g\in F|O\left(O\left(L\left(g\right)\right)\right)=L\left(g\right)\right\}$$
10		mapdrn.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
11		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
12	1 2 3 4 11 5 6 7 8 9 10	mapd1o	$$⊢\phi \to M:\mathrm{LSubSp}\left(U\right)\underset{1-1\; onto}{⟶}T\cap 𝒫C$$
13		f1ofo	$$⊢M:\mathrm{LSubSp}\left(U\right)\underset{1-1\; onto}{⟶}T\cap 𝒫C\to M:\mathrm{LSubSp}\left(U\right)\underset{onto}{⟶}T\cap 𝒫C$$
14		forn	$$⊢M:\mathrm{LSubSp}\left(U\right)\underset{onto}{⟶}T\cap 𝒫C\to \mathrm{ran}M=T\cap 𝒫C$$
15	12 13 14	3syl	$$⊢\phi \to \mathrm{ran}M=T\cap 𝒫C$$