Metamath Proof Explorer

Theorem dochsatshp

Description: The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 27-Jul-2014) (Revised by Mario Carneiro, 1-Oct-2014)

Ref Expression
Hypotheses dochsatshp.h 
|- H = ( LHyp ` K )
dochsatshp.u 
|- U = ( ( DVecH ` K ) ` W )
dochsatshp.o 
|- ._|_ = ( ( ocH ` K ) ` W )
dochsatshp.a 
|- A = ( LSAtoms ` U )
dochsatshp.y 
|- Y = ( LSHyp ` U )
dochsatshp.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dochsatshp.q 
|- ( ph -> Q e. A )
Assertion dochsatshp 
|- ( ph -> ( ._|_ ` Q ) e. Y )

Proof

Step Hyp Ref Expression
1 dochsatshp.h 
 |-  H = ( LHyp ` K )
2 dochsatshp.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 dochsatshp.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
4 dochsatshp.a 
 |-  A = ( LSAtoms ` U )
5 dochsatshp.y 
 |-  Y = ( LSHyp ` U )
6 dochsatshp.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
7 dochsatshp.q 
 |-  ( ph -> Q e. A )
8 eqid 
 |-  ( Base ` U ) = ( Base ` U )
9 1 2 6 dvhlmod 
 |-  ( ph -> U e. LMod )
10 8 4 9 7 lsatssv 
 |-  ( ph -> Q C_ ( Base ` U ) )
11 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
12 1 2 8 11 3 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q C_ ( Base ` U ) ) -> ( ._|_ ` Q ) e. ( LSubSp ` U ) )
13 6 10 12 syl2anc 
 |-  ( ph -> ( ._|_ ` Q ) e. ( LSubSp ` U ) )
14 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
15 14 4 9 7 lsatn0 
 |-  ( ph -> Q =/= { ( 0g ` U ) } )
16 1 2 3 8 14 doch0 
 |-  ( ( K e. HL /\ W e. H ) -> ( ._|_ ` { ( 0g ` U ) } ) = ( Base ` U ) )
17 6 16 syl 
 |-  ( ph -> ( ._|_ ` { ( 0g ` U ) } ) = ( Base ` U ) )
18 17 eqeq2d 
 |-  ( ph -> ( ( ._|_ ` Q ) = ( ._|_ ` { ( 0g ` U ) } ) <-> ( ._|_ ` Q ) = ( Base ` U ) ) )
19 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
20 1 2 19 4 dih1dimat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) -> Q e. ran ( ( DIsoH ` K ) ` W ) )
21 6 7 20 syl2anc 
 |-  ( ph -> Q e. ran ( ( DIsoH ` K ) ` W ) )
22 1 19 2 14 dih0rn 
 |-  ( ( K e. HL /\ W e. H ) -> { ( 0g ` U ) } e. ran ( ( DIsoH ` K ) ` W ) )
23 6 22 syl 
 |-  ( ph -> { ( 0g ` U ) } e. ran ( ( DIsoH ` K ) ` W ) )
24 1 19 3 6 21 23 doch11 
 |-  ( ph -> ( ( ._|_ ` Q ) = ( ._|_ ` { ( 0g ` U ) } ) <-> Q = { ( 0g ` U ) } ) )
25 18 24 bitr3d 
 |-  ( ph -> ( ( ._|_ ` Q ) = ( Base ` U ) <-> Q = { ( 0g ` U ) } ) )
26 25 necon3bid 
 |-  ( ph -> ( ( ._|_ ` Q ) =/= ( Base ` U ) <-> Q =/= { ( 0g ` U ) } ) )
27 15 26 mpbird 
 |-  ( ph -> ( ._|_ ` Q ) =/= ( Base ` U ) )
28 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
29 8 28 14 4 islsat 
 |-  ( U e. LMod -> ( Q e. A <-> E. v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) Q = ( ( LSpan ` U ) ` { v } ) ) )
30 9 29 syl 
 |-  ( ph -> ( Q e. A <-> E. v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) Q = ( ( LSpan ` U ) ` { v } ) ) )
31 7 30 mpbid 
 |-  ( ph -> E. v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) Q = ( ( LSpan ` U ) ` { v } ) )
32 eldifi 
 |-  ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) -> v e. ( Base ` U ) )
33 32 adantr 
 |-  ( ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) -> v e. ( Base ` U ) )
34 33 a1i 
 |-  ( ph -> ( ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) -> v e. ( Base ` U ) ) )
35 11 28 lspid 
 |-  ( ( U e. LMod /\ ( ._|_ ` Q ) e. ( LSubSp ` U ) ) -> ( ( LSpan ` U ) ` ( ._|_ ` Q ) ) = ( ._|_ ` Q ) )
36 9 13 35 syl2anc 
 |-  ( ph -> ( ( LSpan ` U ) ` ( ._|_ ` Q ) ) = ( ._|_ ` Q ) )
37 36 uneq1d 
 |-  ( ph -> ( ( ( LSpan ` U ) ` ( ._|_ ` Q ) ) u. ( ( LSpan ` U ) ` { v } ) ) = ( ( ._|_ ` Q ) u. ( ( LSpan ` U ) ` { v } ) ) )
38 37 fveq2d 
 |-  ( ph -> ( ( LSpan ` U ) ` ( ( ( LSpan ` U ) ` ( ._|_ ` Q ) ) u. ( ( LSpan ` U ) ` { v } ) ) ) = ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. ( ( LSpan ` U ) ` { v } ) ) ) )
39 38 adantr 
 |-  ( ( ph /\ ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) ) -> ( ( LSpan ` U ) ` ( ( ( LSpan ` U ) ` ( ._|_ ` Q ) ) u. ( ( LSpan ` U ) ` { v } ) ) ) = ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. ( ( LSpan ` U ) ` { v } ) ) ) )
40 9 adantr 
 |-  ( ( ph /\ ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) ) -> U e. LMod )
41 8 11 lssss 
 |-  ( ( ._|_ ` Q ) e. ( LSubSp ` U ) -> ( ._|_ ` Q ) C_ ( Base ` U ) )
42 13 41 syl 
 |-  ( ph -> ( ._|_ ` Q ) C_ ( Base ` U ) )
43 42 adantr 
 |-  ( ( ph /\ ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) ) -> ( ._|_ ` Q ) C_ ( Base ` U ) )
44 32 snssd 
 |-  ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) -> { v } C_ ( Base ` U ) )
45 44 adantr 
 |-  ( ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) -> { v } C_ ( Base ` U ) )
46 45 adantl 
 |-  ( ( ph /\ ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) ) -> { v } C_ ( Base ` U ) )
47 8 28 lspun 
 |-  ( ( U e. LMod /\ ( ._|_ ` Q ) C_ ( Base ` U ) /\ { v } C_ ( Base ` U ) ) -> ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. { v } ) ) = ( ( LSpan ` U ) ` ( ( ( LSpan ` U ) ` ( ._|_ ` Q ) ) u. ( ( LSpan ` U ) ` { v } ) ) ) )
48 40 43 46 47 syl3anc 
 |-  ( ( ph /\ ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) ) -> ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. { v } ) ) = ( ( LSpan ` U ) ` ( ( ( LSpan ` U ) ` ( ._|_ ` Q ) ) u. ( ( LSpan ` U ) ` { v } ) ) ) )
49 uneq2 
 |-  ( Q = ( ( LSpan ` U ) ` { v } ) -> ( ( ._|_ ` Q ) u. Q ) = ( ( ._|_ ` Q ) u. ( ( LSpan ` U ) ` { v } ) ) )
50 49 fveq2d 
 |-  ( Q = ( ( LSpan ` U ) ` { v } ) -> ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. Q ) ) = ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. ( ( LSpan ` U ) ` { v } ) ) ) )
51 50 adantl 
 |-  ( ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) -> ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. Q ) ) = ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. ( ( LSpan ` U ) ` { v } ) ) ) )
52 51 adantl 
 |-  ( ( ph /\ ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) ) -> ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. Q ) ) = ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. ( ( LSpan ` U ) ` { v } ) ) ) )
53 39 48 52 3eqtr4d 
 |-  ( ( ph /\ ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) ) -> ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. { v } ) ) = ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. Q ) ) )
54 eqid 
 |-  ( ( joinH ` K ) ` W ) = ( ( joinH ` K ) ` W )
55 eqid 
 |-  ( LSSum ` U ) = ( LSSum ` U )
56 1 19 2 8 3 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q C_ ( Base ` U ) ) -> ( ._|_ ` Q ) e. ran ( ( DIsoH ` K ) ` W ) )
57 6 10 56 syl2anc 
 |-  ( ph -> ( ._|_ ` Q ) e. ran ( ( DIsoH ` K ) ` W ) )
58 1 19 54 2 55 4 6 57 7 dihjat2 
 |-  ( ph -> ( ( ._|_ ` Q ) ( ( joinH ` K ) ` W ) Q ) = ( ( ._|_ ` Q ) ( LSSum ` U ) Q ) )
59 1 2 8 54 6 42 10 djhcom 
 |-  ( ph -> ( ( ._|_ ` Q ) ( ( joinH ` K ) ` W ) Q ) = ( Q ( ( joinH ` K ) ` W ) ( ._|_ ` Q ) ) )
60 11 4 9 7 lsatlssel 
 |-  ( ph -> Q e. ( LSubSp ` U ) )
61 11 28 55 lsmsp 
 |-  ( ( U e. LMod /\ ( ._|_ ` Q ) e. ( LSubSp ` U ) /\ Q e. ( LSubSp ` U ) ) -> ( ( ._|_ ` Q ) ( LSSum ` U ) Q ) = ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. Q ) ) )
62 9 13 60 61 syl3anc 
 |-  ( ph -> ( ( ._|_ ` Q ) ( LSSum ` U ) Q ) = ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. Q ) ) )
63 58 59 62 3eqtr3rd 
 |-  ( ph -> ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. Q ) ) = ( Q ( ( joinH ` K ) ` W ) ( ._|_ ` Q ) ) )
64 1 2 8 3 54 djhexmid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q C_ ( Base ` U ) ) -> ( Q ( ( joinH ` K ) ` W ) ( ._|_ ` Q ) ) = ( Base ` U ) )
65 6 10 64 syl2anc 
 |-  ( ph -> ( Q ( ( joinH ` K ) ` W ) ( ._|_ ` Q ) ) = ( Base ` U ) )
66 63 65 eqtrd 
 |-  ( ph -> ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. Q ) ) = ( Base ` U ) )
67 66 adantr 
 |-  ( ( ph /\ ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) ) -> ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. Q ) ) = ( Base ` U ) )
68 53 67 eqtrd 
 |-  ( ( ph /\ ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) ) -> ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. { v } ) ) = ( Base ` U ) )
69 68 ex 
 |-  ( ph -> ( ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) -> ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. { v } ) ) = ( Base ` U ) ) )
70 34 69 jcad 
 |-  ( ph -> ( ( v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) /\ Q = ( ( LSpan ` U ) ` { v } ) ) -> ( v e. ( Base ` U ) /\ ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. { v } ) ) = ( Base ` U ) ) ) )
71 70 reximdv2 
 |-  ( ph -> ( E. v e. ( ( Base ` U ) \ { ( 0g ` U ) } ) Q = ( ( LSpan ` U ) ` { v } ) -> E. v e. ( Base ` U ) ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. { v } ) ) = ( Base ` U ) ) )
72 31 71 mpd 
 |-  ( ph -> E. v e. ( Base ` U ) ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. { v } ) ) = ( Base ` U ) )
73 1 2 6 dvhlvec 
 |-  ( ph -> U e. LVec )
74 8 28 11 5 islshp 
 |-  ( U e. LVec -> ( ( ._|_ ` Q ) e. Y <-> ( ( ._|_ ` Q ) e. ( LSubSp ` U ) /\ ( ._|_ ` Q ) =/= ( Base ` U ) /\ E. v e. ( Base ` U ) ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. { v } ) ) = ( Base ` U ) ) ) )
75 73 74 syl 
 |-  ( ph -> ( ( ._|_ ` Q ) e. Y <-> ( ( ._|_ ` Q ) e. ( LSubSp ` U ) /\ ( ._|_ ` Q ) =/= ( Base ` U ) /\ E. v e. ( Base ` U ) ( ( LSpan ` U ) ` ( ( ._|_ ` Q ) u. { v } ) ) = ( Base ` U ) ) ) )
76 13 27 72 75 mpbir3and 
 |-  ( ph -> ( ._|_ ` Q ) e. Y )