Theorem doch2val2

Description: Double orthocomplement for DVecH vector space. (Contributed by NM, 26-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		doch2val2.h	|- H = ( LHyp ` K )
2		doch2val2.i	|- I = ( ( DIsoH ` K ) ` W )
3		doch2val2.u	|- U = ( ( DVecH ` K ) ` W )
4		doch2val2.v	|- V = ( Base ` U )
5		doch2val2.o	|- ._|_ = ( ( ocH ` K ) ` W )
6		doch2val2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		doch2val2.x	|- ( ph -> X C_ V )
8		eqid	|- ( oc ` K ) = ( oc ` K )
9	8 1 2 3 4 5	dochval2	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) = ( I ` ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) )
10	6 7 9	syl2anc	|- ( ph -> ( ._|_ ` X ) = ( I ` ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) )
11	10	fveq2d	|- ( ph -> ( ._|_ ` ( ._|_ ` X ) ) = ( ._|_ ` ( I ` ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) ) )
12	6	simpld	|- ( ph -> K e. HL )
13		hlop	|- ( K e. HL -> K e. OP )
14	12 13	syl	|- ( ph -> K e. OP )
15		ssrab2	|- { z e. ran I | X C_ z } C_ ran I
16	15	a1i	|- ( ph -> { z e. ran I | X C_ z } C_ ran I )
17	1 2 3 4	dih1rn	|- ( ( K e. HL /\ W e. H ) -> V e. ran I )
18	6 17	syl	|- ( ph -> V e. ran I )
19		sseq2	|- ( z = V -> ( X C_ z <-> X C_ V ) )
20	19	elrab	|- ( V e. { z e. ran I | X C_ z } <-> ( V e. ran I /\ X C_ V ) )
21	18 7 20	sylanbrc	|- ( ph -> V e. { z e. ran I | X C_ z } )
22	21	ne0d	|- ( ph -> { z e. ran I | X C_ z } =/= (/) )
23	1 2	dihintcl	|- ( ( ( K e. HL /\ W e. H ) /\ ( { z e. ran I | X C_ z } C_ ran I /\ { z e. ran I | X C_ z } =/= (/) ) ) -> |^| { z e. ran I | X C_ z } e. ran I )
24	6 16 22 23	syl12anc	|- ( ph -> |^| { z e. ran I | X C_ z } e. ran I )
25		eqid	|- ( Base ` K ) = ( Base ` K )
26	25 1 2	dihcnvcl	|- ( ( ( K e. HL /\ W e. H ) /\ |^| { z e. ran I | X C_ z } e. ran I ) -> ( `' I ` |^| { z e. ran I | X C_ z } ) e. ( Base ` K ) )
27	6 24 26	syl2anc	|- ( ph -> ( `' I ` |^| { z e. ran I | X C_ z } ) e. ( Base ` K ) )
28	25 8	opoccl	|- ( ( K e. OP /\ ( `' I ` |^| { z e. ran I | X C_ z } ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) e. ( Base ` K ) )
29	14 27 28	syl2anc	|- ( ph -> ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) e. ( Base ` K ) )
30	25 8 1 2 5	dochvalr2	|- ( ( ( K e. HL /\ W e. H ) /\ ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) e. ( Base ` K ) ) -> ( ._|_ ` ( I ` ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) ) = ( I ` ( ( oc ` K ) ` ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) ) )
31	6 29 30	syl2anc	|- ( ph -> ( ._|_ ` ( I ` ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) ) = ( I ` ( ( oc ` K ) ` ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) ) )
32	25 8	opococ	|- ( ( K e. OP /\ ( `' I ` |^| { z e. ran I | X C_ z } ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) = ( `' I ` |^| { z e. ran I | X C_ z } ) )
33	14 27 32	syl2anc	|- ( ph -> ( ( oc ` K ) ` ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) = ( `' I ` |^| { z e. ran I | X C_ z } ) )
34	33	fveq2d	|- ( ph -> ( I ` ( ( oc ` K ) ` ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) ) = ( I ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) )
35	1 2	dihcnvid2	|- ( ( ( K e. HL /\ W e. H ) /\ |^| { z e. ran I | X C_ z } e. ran I ) -> ( I ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) = |^| { z e. ran I | X C_ z } )
36	6 24 35	syl2anc	|- ( ph -> ( I ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) = |^| { z e. ran I | X C_ z } )
37	34 36	eqtrd	|- ( ph -> ( I ` ( ( oc ` K ) ` ( ( oc ` K ) ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) ) = |^| { z e. ran I | X C_ z } )
38	11 31 37	3eqtrd	|- ( ph -> ( ._|_ ` ( ._|_ ` X ) ) = |^| { z e. ran I | X C_ z } )