Theorem dochval2

Description: Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Apr-2014)

	Ref	Expression
Hypotheses	dochval2.o	|- ._|_ = ( oc ` K )
	dochval2.h	|- H = ( LHyp ` K )
	dochval2.i	|- I = ( ( DIsoH ` K ) ` W )
	dochval2.u	|- U = ( ( DVecH ` K ) ` W )
	dochval2.v	|- V = ( Base ` U )
	dochval2.n	|- N = ( ( ocH ` K ) ` W )
Assertion	dochval2	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( N ` X ) = ( I ` ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dochval2.o	|- ._|_ = ( oc ` K )
2		dochval2.h	|- H = ( LHyp ` K )
3		dochval2.i	|- I = ( ( DIsoH ` K ) ` W )
4		dochval2.u	|- U = ( ( DVecH ` K ) ` W )
5		dochval2.v	|- V = ( Base ` U )
6		dochval2.n	|- N = ( ( ocH ` K ) ` W )
7		eqid	|- ( Base ` K ) = ( Base ` K )
8		eqid	|- ( glb ` K ) = ( glb ` K )
9	7 8 1 2 3 4 5 6	dochval	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( N ` X ) = ( I ` ( ._|_ ` ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) ) ) )
10		hlclat	|- ( K e. HL -> K e. CLat )
11	10	ad2antrr	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> K e. CLat )
12		ssrab2	|- { x e. ( Base ` K ) | X C_ ( I ` x ) } C_ ( Base ` K )
13	7 8	clatglbcl	|- ( ( K e. CLat /\ { x e. ( Base ` K ) | X C_ ( I ` x ) } C_ ( Base ` K ) ) -> ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) e. ( Base ` K ) )
14	11 12 13	sylancl	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) e. ( Base ` K ) )
15	7 2 3	dihcnvid1	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) e. ( Base ` K ) ) -> ( `' I ` ( I ` ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) ) ) = ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) )
16	14 15	syldan	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( `' I ` ( I ` ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) ) ) = ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) )
17	7 8 2 3 4 5	dihglb2	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( I ` ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) ) = |^| { z e. ran I | X C_ z } )
18	17	fveq2d	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( `' I ` ( I ` ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) ) ) = ( `' I ` |^| { z e. ran I | X C_ z } ) )
19	16 18	eqtr3d	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) = ( `' I ` |^| { z e. ran I | X C_ z } ) )
20	19	fveq2d	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) ) = ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) )
21	20	fveq2d	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( I ` ( ._|_ ` ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) ) ) = ( I ` ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) )
22	9 21	eqtrd	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( N ` X ) = ( I ` ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) )