# 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 ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 ) ) )`