Theorem dochfN

Description: Domain and codomain of the subspace orthocomplement for the DVecH vector space. (Contributed by NM, 27-Dec-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dochf.h	|- H = ( LHyp ` K )
	dochf.i	|- I = ( ( DIsoH ` K ) ` W )
	dochf.u	|- U = ( ( DVecH ` K ) ` W )
	dochf.v	|- V = ( Base ` U )
	dochf.o	|- ._|_ = ( ( ocH ` K ) ` W )
	dochf.k	|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion	dochfN	|- ( ph -> ._|_ : ~P V --> ran I )

Proof

Step	Hyp	Ref	Expression
1		dochf.h	|- H = ( LHyp ` K )
2		dochf.i	|- I = ( ( DIsoH ` K ) ` W )
3		dochf.u	|- U = ( ( DVecH ` K ) ` W )
4		dochf.v	|- V = ( Base ` U )
5		dochf.o	|- ._|_ = ( ( ocH ` K ) ` W )
6		dochf.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		fvexd	|- ( ( ph /\ x e. ~P V ) -> ( I ` ( ( oc ` K ) ` ( ( glb ` K ) ` { y e. ( Base ` K ) | x C_ ( I ` y ) } ) ) ) e. _V )
8		eqid	|- ( Base ` K ) = ( Base ` K )
9		eqid	|- ( glb ` K ) = ( glb ` K )
10		eqid	|- ( oc ` K ) = ( oc ` K )
11	8 9 10 1 2 3 4 5	dochfval	|- ( ( K e. HL /\ W e. H ) -> ._|_ = ( x e. ~P V |-> ( I ` ( ( oc ` K ) ` ( ( glb ` K ) ` { y e. ( Base ` K ) | x C_ ( I ` y ) } ) ) ) ) )
12	6 11	syl	|- ( ph -> ._|_ = ( x e. ~P V |-> ( I ` ( ( oc ` K ) ` ( ( glb ` K ) ` { y e. ( Base ` K ) | x C_ ( I ` y ) } ) ) ) ) )
13		elpwi	|- ( y e. ~P V -> y C_ V )
14	1 2 3 4 5	dochcl	|- ( ( ( K e. HL /\ W e. H ) /\ y C_ V ) -> ( ._|_ ` y ) e. ran I )
15	6 13 14	syl2an	|- ( ( ph /\ y e. ~P V ) -> ( ._|_ ` y ) e. ran I )
16	7 12 15	fmpt2d	|- ( ph -> ._|_ : ~P V --> ran I )