Metamath Proof Explorer

Theorem dochocss

Description: Double negative law for orthocomplement of an arbitrary set of vectors. (Contributed by NM, 16-Apr-2014)

Ref Expression
Hypotheses dochss.h 
|- H = ( LHyp ` K )
dochss.u 
|- U = ( ( DVecH ` K ) ` W )
dochss.v 
|- V = ( Base ` U )
dochss.o 
|- ._|_ = ( ( ocH ` K ) ` W )
Assertion dochocss 
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )

Proof

Step Hyp Ref Expression
1 dochss.h 
 |-  H = ( LHyp ` K )
2 dochss.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 dochss.v 
 |-  V = ( Base ` U )
4 dochss.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
5 ssintub 
 |-  X C_ |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z }
6 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
7 1 6 2 3 4 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) e. ran ( ( DIsoH ` K ) ` W ) )
8 eqid 
 |-  ( oc ` K ) = ( oc ` K )
9 8 1 6 4 dochvalr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` X ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` X ) ) = ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` X ) ) ) ) )
10 7 9 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` ( ._|_ ` X ) ) = ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` X ) ) ) ) )
11 8 1 6 2 3 4 dochval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) = ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) ) ) )
12 11 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` X ) ) = ( `' ( ( DIsoH ` K ) ` W ) ` ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) ) ) ) )
13 eqid 
 |-  ( Base ` K ) = ( Base ` K )
14 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
15 13 1 6 2 14 dihf11 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( DIsoH ` K ) ` W ) : ( Base ` K ) -1-1-> ( LSubSp ` U ) )
16 15 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( DIsoH ` K ) ` W ) : ( Base ` K ) -1-1-> ( LSubSp ` U ) )
17 f1f1orn 
 |-  ( ( ( DIsoH ` K ) ` W ) : ( Base ` K ) -1-1-> ( LSubSp ` U ) -> ( ( DIsoH ` K ) ` W ) : ( Base ` K ) -1-1-onto-> ran ( ( DIsoH ` K ) ` W ) )
18 16 17 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( DIsoH ` K ) ` W ) : ( Base ` K ) -1-1-onto-> ran ( ( DIsoH ` K ) ` W ) )
19 hlop 
 |-  ( K e. HL -> K e. OP )
20 19 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> K e. OP )
21 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( K e. HL /\ W e. H ) )
22 ssrab2 
 |-  { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } C_ ran ( ( DIsoH ` K ) ` W )
23 22 a1i 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } C_ ran ( ( DIsoH ` K ) ` W ) )
24 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
25 24 1 6 2 3 dih1 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( DIsoH ` K ) ` W ) ` ( 1. ` K ) ) = V )
26 25 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( ( DIsoH ` K ) ` W ) ` ( 1. ` K ) ) = V )
27 f1fn 
 |-  ( ( ( DIsoH ` K ) ` W ) : ( Base ` K ) -1-1-> ( LSubSp ` U ) -> ( ( DIsoH ` K ) ` W ) Fn ( Base ` K ) )
28 16 27 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( DIsoH ` K ) ` W ) Fn ( Base ` K ) )
29 13 24 op1cl 
 |-  ( K e. OP -> ( 1. ` K ) e. ( Base ` K ) )
30 20 29 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( 1. ` K ) e. ( Base ` K ) )
31 fnfvelrn 
 |-  ( ( ( ( DIsoH ` K ) ` W ) Fn ( Base ` K ) /\ ( 1. ` K ) e. ( Base ` K ) ) -> ( ( ( DIsoH ` K ) ` W ) ` ( 1. ` K ) ) e. ran ( ( DIsoH ` K ) ` W ) )
32 28 30 31 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( ( DIsoH ` K ) ` W ) ` ( 1. ` K ) ) e. ran ( ( DIsoH ` K ) ` W ) )
33 26 32 eqeltrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> V e. ran ( ( DIsoH ` K ) ` W ) )
34 simpr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> X C_ V )
35 sseq2 
 |-  ( z = V -> ( X C_ z <-> X C_ V ) )
36 35 elrab 
 |-  ( V e. { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } <-> ( V e. ran ( ( DIsoH ` K ) ` W ) /\ X C_ V ) )
37 33 34 36 sylanbrc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> V e. { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } )
38 37 ne0d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } =/= (/) )
39 1 6 dihintcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } C_ ran ( ( DIsoH ` K ) ` W ) /\ { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } =/= (/) ) ) -> |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } e. ran ( ( DIsoH ` K ) ` W ) )
40 21 23 38 39 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } e. ran ( ( DIsoH ` K ) ` W ) )
41 f1ocnvdm 
 |-  ( ( ( ( DIsoH ` K ) ` W ) : ( Base ` K ) -1-1-onto-> ran ( ( DIsoH ` K ) ` W ) /\ |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } e. ran ( ( DIsoH ` K ) ` W ) ) -> ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) e. ( Base ` K ) )
42 18 40 41 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) e. ( Base ` K ) )
43 13 8 opoccl 
 |-  ( ( K e. OP /\ ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) ) e. ( Base ` K ) )
44 20 42 43 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) ) e. ( Base ` K ) )
45 f1ocnvfv1 
 |-  ( ( ( ( DIsoH ` K ) ` W ) : ( Base ` K ) -1-1-onto-> ran ( ( DIsoH ` K ) ` W ) /\ ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) ) e. ( Base ` K ) ) -> ( `' ( ( DIsoH ` K ) ` W ) ` ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) ) ) ) = ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) ) )
46 18 44 45 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( `' ( ( DIsoH ` K ) ` W ) ` ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) ) ) ) = ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) ) )
47 12 46 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` X ) ) = ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) ) )
48 47 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` X ) ) ) = ( ( oc ` K ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) ) ) )
49 13 8 opococ 
 |-  ( ( K e. OP /\ ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) ) ) = ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) )
50 20 42 49 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( oc ` K ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) ) ) = ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) )
51 48 50 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` X ) ) ) = ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) )
52 51 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` ( ._|_ ` X ) ) ) ) = ( ( ( DIsoH ` K ) ` W ) ` ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) ) )
53 f1ocnvfv2 
 |-  ( ( ( ( DIsoH ` K ) ` W ) : ( Base ` K ) -1-1-onto-> ran ( ( DIsoH ` K ) ` W ) /\ |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ( ( DIsoH ` K ) ` W ) ` ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) ) = |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } )
54 18 40 53 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( ( DIsoH ` K ) ` W ) ` ( `' ( ( DIsoH ` K ) ` W ) ` |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } ) ) = |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } )
55 10 52 54 3eqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> |^| { z e. ran ( ( DIsoH ` K ) ` W ) | X C_ z } = ( ._|_ ` ( ._|_ ` X ) ) )
56 5 55 sseqtrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )