Metamath Proof Explorer

Theorem dochdmj1

Description: De Morgan-like law for subspace orthocomplement. (Contributed by NM, 5-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 dochdmj1.h 
 |-  H = ( LHyp ` K )
2 dochdmj1.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 dochdmj1.v 
 |-  V = ( Base ` U )
4 dochdmj1.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
5 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( K e. HL /\ W e. H ) )
6 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> X C_ V )
7 simp3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> Y C_ V )
8 6 7 unssd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( X u. Y ) C_ V )
9 ssun1 
 |-  X C_ ( X u. Y )
10 9 a1i 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> X C_ ( X u. Y ) )
11 1 2 3 4 dochss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X u. Y ) C_ V /\ X C_ ( X u. Y ) ) -> ( ._|_ ` ( X u. Y ) ) C_ ( ._|_ ` X ) )
12 5 8 10 11 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ._|_ ` ( X u. Y ) ) C_ ( ._|_ ` X ) )
13 ssun2 
 |-  Y C_ ( X u. Y )
14 13 a1i 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> Y C_ ( X u. Y ) )
15 1 2 3 4 dochss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X u. Y ) C_ V /\ Y C_ ( X u. Y ) ) -> ( ._|_ ` ( X u. Y ) ) C_ ( ._|_ ` Y ) )
16 5 8 14 15 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ._|_ ` ( X u. Y ) ) C_ ( ._|_ ` Y ) )
17 12 16 ssind 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ._|_ ` ( X u. Y ) ) C_ ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) )
18 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
19 1 18 2 3 4 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) e. ran ( ( DIsoH ` K ) ` W ) )
20 19 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ._|_ ` X ) e. ran ( ( DIsoH ` K ) ` W ) )
21 1 18 2 3 4 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V ) -> ( ._|_ ` Y ) e. ran ( ( DIsoH ` K ) ` W ) )
22 21 3adant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ._|_ ` Y ) e. ran ( ( DIsoH ` K ) ` W ) )
23 1 18 dihmeetcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ._|_ ` X ) e. ran ( ( DIsoH ` K ) ` W ) /\ ( ._|_ ` Y ) e. ran ( ( DIsoH ` K ) ` W ) ) ) -> ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) e. ran ( ( DIsoH ` K ) ` W ) )
24 5 20 22 23 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) e. ran ( ( DIsoH ` K ) ` W ) )
25 1 18 4 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) ) = ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) )
26 5 24 25 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ._|_ ` ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) ) = ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) )
27 1 2 3 4 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) C_ V )
28 27 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ._|_ ` X ) C_ V )
29 ssinss1 
 |-  ( ( ._|_ ` X ) C_ V -> ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) C_ V )
30 28 29 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) C_ V )
31 1 2 3 4 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) C_ V ) -> ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) C_ V )
32 5 30 31 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) C_ V )
33 1 2 3 4 dochocss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )
34 33 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )
35 1 2 3 4 dochocss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V ) -> Y C_ ( ._|_ ` ( ._|_ ` Y ) ) )
36 35 3adant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> Y C_ ( ._|_ ` ( ._|_ ` Y ) ) )
37 unss12 
 |-  ( ( X C_ ( ._|_ ` ( ._|_ ` X ) ) /\ Y C_ ( ._|_ ` ( ._|_ ` Y ) ) ) -> ( X u. Y ) C_ ( ( ._|_ ` ( ._|_ ` X ) ) u. ( ._|_ ` ( ._|_ ` Y ) ) ) )
38 34 36 37 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( X u. Y ) C_ ( ( ._|_ ` ( ._|_ ` X ) ) u. ( ._|_ ` ( ._|_ ` Y ) ) ) )
39 inss1 
 |-  ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) C_ ( ._|_ ` X )
40 39 a1i 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) C_ ( ._|_ ` X ) )
41 1 2 3 4 dochss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` X ) C_ V /\ ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) C_ ( ._|_ ` X ) ) -> ( ._|_ ` ( ._|_ ` X ) ) C_ ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) )
42 5 28 40 41 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ._|_ ` ( ._|_ ` X ) ) C_ ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) )
43 1 2 3 4 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V ) -> ( ._|_ ` Y ) C_ V )
44 43 3adant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ._|_ ` Y ) C_ V )
45 inss2 
 |-  ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) C_ ( ._|_ ` Y )
46 45 a1i 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) C_ ( ._|_ ` Y ) )
47 1 2 3 4 dochss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` Y ) C_ V /\ ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) C_ ( ._|_ ` Y ) ) -> ( ._|_ ` ( ._|_ ` Y ) ) C_ ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) )
48 5 44 46 47 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ._|_ ` ( ._|_ ` Y ) ) C_ ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) )
49 42 48 unssd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ( ._|_ ` ( ._|_ ` X ) ) u. ( ._|_ ` ( ._|_ ` Y ) ) ) C_ ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) )
50 38 49 sstrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( X u. Y ) C_ ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) )
51 1 2 3 4 dochss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) C_ V /\ ( X u. Y ) C_ ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) ) -> ( ._|_ ` ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) ) C_ ( ._|_ ` ( X u. Y ) ) )
52 5 32 50 51 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ._|_ ` ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) ) C_ ( ._|_ ` ( X u. Y ) ) )
53 26 52 eqsstrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) C_ ( ._|_ ` ( X u. Y ) ) )
54 17 53 eqssd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( ._|_ ` ( X u. Y ) ) = ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) )