Metamath Proof Explorer

Theorem dochsatshpb

Description: The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 29-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 dochsatshpb.h 
 |-  H = ( LHyp ` K )
2 dochsatshpb.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 dochsatshpb.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dochsatshpb.s 
 |-  S = ( LSubSp ` U )
5 dochsatshpb.a 
 |-  A = ( LSAtoms ` U )
6 dochsatshpb.y 
 |-  Y = ( LSHyp ` U )
7 dochsatshpb.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
8 dochsatshpb.q 
 |-  ( ph -> Q e. S )
9 7 adantr 
 |-  ( ( ph /\ Q e. A ) -> ( K e. HL /\ W e. H ) )
10 simpr 
 |-  ( ( ph /\ Q e. A ) -> Q e. A )
11 1 3 2 5 6 9 10 dochsatshp 
 |-  ( ( ph /\ Q e. A ) -> ( ._|_ ` Q ) e. Y )
12 eqid 
 |-  ( Base ` U ) = ( Base ` U )
13 12 4 lssss 
 |-  ( Q e. S -> Q C_ ( Base ` U ) )
14 8 13 syl 
 |-  ( ph -> Q C_ ( Base ` U ) )
15 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
16 1 15 3 12 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q C_ ( Base ` U ) ) -> ( ._|_ ` Q ) e. ran ( ( DIsoH ` K ) ` W ) )
17 7 14 16 syl2anc 
 |-  ( ph -> ( ._|_ ` Q ) e. ran ( ( DIsoH ` K ) ` W ) )
18 1 15 2 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` Q ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` Q ) ) ) = ( ._|_ ` Q ) )
19 7 17 18 syl2anc 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( ._|_ ` Q ) ) ) = ( ._|_ ` Q ) )
20 19 adantr 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` Q ) ) ) = ( ._|_ ` Q ) )
21 1 3 7 dvhlmod 
 |-  ( ph -> U e. LMod )
22 21 adantr 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> U e. LMod )
23 simpr 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> ( ._|_ ` Q ) e. Y )
24 12 6 22 23 lshpne 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> ( ._|_ ` Q ) =/= ( Base ` U ) )
25 20 24 eqnetrd 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` Q ) ) ) =/= ( Base ` U ) )
26 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
27 1 3 12 2 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q C_ ( Base ` U ) ) -> ( ._|_ ` Q ) C_ ( Base ` U ) )
28 7 14 27 syl2anc 
 |-  ( ph -> ( ._|_ ` Q ) C_ ( Base ` U ) )
29 1 2 3 12 26 7 28 dochn0nv 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` Q ) ) =/= { ( 0g ` U ) } <-> ( ._|_ ` ( ._|_ ` ( ._|_ ` Q ) ) ) =/= ( Base ` U ) ) )
30 29 adantr 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> ( ( ._|_ ` ( ._|_ ` Q ) ) =/= { ( 0g ` U ) } <-> ( ._|_ ` ( ._|_ ` ( ._|_ ` Q ) ) ) =/= ( Base ` U ) ) )
31 25 30 mpbird 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> ( ._|_ ` ( ._|_ ` Q ) ) =/= { ( 0g ` U ) } )
32 1 3 12 4 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q C_ ( Base ` U ) ) -> ( ._|_ ` Q ) e. S )
33 7 14 32 syl2anc 
 |-  ( ph -> ( ._|_ ` Q ) e. S )
34 12 4 lssss 
 |-  ( ( ._|_ ` Q ) e. S -> ( ._|_ ` Q ) C_ ( Base ` U ) )
35 33 34 syl 
 |-  ( ph -> ( ._|_ ` Q ) C_ ( Base ` U ) )
36 1 3 12 4 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` Q ) C_ ( Base ` U ) ) -> ( ._|_ ` ( ._|_ ` Q ) ) e. S )
37 7 35 36 syl2anc 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` Q ) ) e. S )
38 37 adantr 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> ( ._|_ ` ( ._|_ ` Q ) ) e. S )
39 26 4 lssne0 
 |-  ( ( ._|_ ` ( ._|_ ` Q ) ) e. S -> ( ( ._|_ ` ( ._|_ ` Q ) ) =/= { ( 0g ` U ) } <-> E. v e. ( ._|_ ` ( ._|_ ` Q ) ) v =/= ( 0g ` U ) ) )
40 38 39 syl 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> ( ( ._|_ ` ( ._|_ ` Q ) ) =/= { ( 0g ` U ) } <-> E. v e. ( ._|_ ` ( ._|_ ` Q ) ) v =/= ( 0g ` U ) ) )
41 31 40 mpbid 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> E. v e. ( ._|_ ` ( ._|_ ` Q ) ) v =/= ( 0g ` U ) )
42 7 adantr 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> ( K e. HL /\ W e. H ) )
43 42 3ad2ant1 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
44 17 adantr 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> ( ._|_ ` Q ) e. ran ( ( DIsoH ` K ) ` W ) )
45 44 3ad2ant1 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ._|_ ` Q ) e. ran ( ( DIsoH ` K ) ` W ) )
46 43 45 18 syl2anc 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` Q ) ) ) = ( ._|_ ` Q ) )
47 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
48 22 3ad2ant1 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> U e. LMod )
49 38 3ad2ant1 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ._|_ ` ( ._|_ ` Q ) ) e. S )
50 simp2 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> v e. ( ._|_ ` ( ._|_ ` Q ) ) )
51 4 47 48 49 50 lspsnel5a 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ( LSpan ` U ) ` { v } ) C_ ( ._|_ ` ( ._|_ ` Q ) ) )
52 12 4 lssel 
 |-  ( ( ( ._|_ ` ( ._|_ ` Q ) ) e. S /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) ) -> v e. ( Base ` U ) )
53 49 50 52 syl2anc 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> v e. ( Base ` U ) )
54 1 3 12 47 15 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ v e. ( Base ` U ) ) -> ( ( LSpan ` U ) ` { v } ) e. ran ( ( DIsoH ` K ) ` W ) )
55 43 53 54 syl2anc 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ( LSpan ` U ) ` { v } ) e. ran ( ( DIsoH ` K ) ` W ) )
56 1 15 3 12 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` Q ) C_ ( Base ` U ) ) -> ( ._|_ ` ( ._|_ ` Q ) ) e. ran ( ( DIsoH ` K ) ` W ) )
57 7 35 56 syl2anc 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` Q ) ) e. ran ( ( DIsoH ` K ) ` W ) )
58 57 adantr 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> ( ._|_ ` ( ._|_ ` Q ) ) e. ran ( ( DIsoH ` K ) ` W ) )
59 58 3ad2ant1 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ._|_ ` ( ._|_ ` Q ) ) e. ran ( ( DIsoH ` K ) ` W ) )
60 1 15 2 43 55 59 dochord 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ( ( LSpan ` U ) ` { v } ) C_ ( ._|_ ` ( ._|_ ` Q ) ) <-> ( ._|_ ` ( ._|_ ` ( ._|_ ` Q ) ) ) C_ ( ._|_ ` ( ( LSpan ` U ) ` { v } ) ) ) )
61 51 60 mpbid 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` Q ) ) ) C_ ( ._|_ ` ( ( LSpan ` U ) ` { v } ) ) )
62 46 61 eqsstrrd 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ._|_ ` Q ) C_ ( ._|_ ` ( ( LSpan ` U ) ` { v } ) ) )
63 1 3 7 dvhlvec 
 |-  ( ph -> U e. LVec )
64 63 adantr 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> U e. LVec )
65 64 3ad2ant1 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> U e. LVec )
66 simp1r 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ._|_ ` Q ) e. Y )
67 simp3 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> v =/= ( 0g ` U ) )
68 12 47 26 5 lsatlspsn2 
 |-  ( ( U e. LMod /\ v e. ( Base ` U ) /\ v =/= ( 0g ` U ) ) -> ( ( LSpan ` U ) ` { v } ) e. A )
69 48 53 67 68 syl3anc 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ( LSpan ` U ) ` { v } ) e. A )
70 1 3 2 5 6 43 69 dochsatshp 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ._|_ ` ( ( LSpan ` U ) ` { v } ) ) e. Y )
71 6 65 66 70 lshpcmp 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ( ._|_ ` Q ) C_ ( ._|_ ` ( ( LSpan ` U ) ` { v } ) ) <-> ( ._|_ ` Q ) = ( ._|_ ` ( ( LSpan ` U ) ` { v } ) ) ) )
72 62 71 mpbid 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ._|_ ` Q ) = ( ._|_ ` ( ( LSpan ` U ) ` { v } ) ) )
73 72 fveq2d 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ._|_ ` ( ._|_ ` Q ) ) = ( ._|_ ` ( ._|_ ` ( ( LSpan ` U ) ` { v } ) ) ) )
74 1 15 2 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( LSpan ` U ) ` { v } ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` ( ( LSpan ` U ) ` { v } ) ) ) = ( ( LSpan ` U ) ` { v } ) )
75 43 55 74 syl2anc 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ._|_ ` ( ._|_ ` ( ( LSpan ` U ) ` { v } ) ) ) = ( ( LSpan ` U ) ` { v } ) )
76 73 75 eqtrd 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ._|_ ` ( ._|_ ` Q ) ) = ( ( LSpan ` U ) ` { v } ) )
77 76 69 eqeltrd 
 |-  ( ( ( ph /\ ( ._|_ ` Q ) e. Y ) /\ v e. ( ._|_ ` ( ._|_ ` Q ) ) /\ v =/= ( 0g ` U ) ) -> ( ._|_ ` ( ._|_ ` Q ) ) e. A )
78 77 rexlimdv3a 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> ( E. v e. ( ._|_ ` ( ._|_ ` Q ) ) v =/= ( 0g ` U ) -> ( ._|_ ` ( ._|_ ` Q ) ) e. A ) )
79 41 78 mpd 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> ( ._|_ ` ( ._|_ ` Q ) ) e. A )
80 8 adantr 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> Q e. S )
81 1 2 3 4 5 42 80 dochsat 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> ( ( ._|_ ` ( ._|_ ` Q ) ) e. A <-> Q e. A ) )
82 79 81 mpbid 
 |-  ( ( ph /\ ( ._|_ ` Q ) e. Y ) -> Q e. A )
83 11 82 impbida 
 |-  ( ph -> ( Q e. A <-> ( ._|_ ` Q ) e. Y ) )