This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )