Metamath Proof Explorer

Theorem dochsat

Description: The double orthocomplement of an atom is an atom. (Contributed by NM, 29-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 dochsat.h 
 |-  H = ( LHyp ` K )
2 dochsat.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 dochsat.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dochsat.s 
 |-  S = ( LSubSp ` U )
5 dochsat.a 
 |-  A = ( LSAtoms ` U )
6 dochsat.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
7 dochsat.q 
 |-  ( ph -> Q e. S )
8 1 3 6 dvhlmod 
 |-  ( ph -> U e. LMod )
9 8 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> U e. LMod )
10 7 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> Q e. S )
11 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
12 11 4 lss0ss 
 |-  ( ( U e. LMod /\ Q e. S ) -> { ( 0g ` U ) } C_ Q )
13 9 10 12 syl2anc 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> { ( 0g ` U ) } C_ Q )
14 simpr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> ( ._|_ ` ( ._|_ ` Q ) ) e. A )
15 11 5 9 14 lsatn0 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> ( ._|_ ` ( ._|_ ` Q ) ) =/= { ( 0g ` U ) } )
16 simpr 
 |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) /\ Q = { ( 0g ` U ) } ) -> Q = { ( 0g ` U ) } )
17 16 fveq2d 
 |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) /\ Q = { ( 0g ` U ) } ) -> ( ._|_ ` Q ) = ( ._|_ ` { ( 0g ` U ) } ) )
18 17 fveq2d 
 |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) /\ Q = { ( 0g ` U ) } ) -> ( ._|_ ` ( ._|_ ` Q ) ) = ( ._|_ ` ( ._|_ ` { ( 0g ` U ) } ) ) )
19 1 3 2 11 6 dochoc0 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` { ( 0g ` U ) } ) ) = { ( 0g ` U ) } )
20 19 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> ( ._|_ ` ( ._|_ ` { ( 0g ` U ) } ) ) = { ( 0g ` U ) } )
21 20 adantr 
 |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) /\ Q = { ( 0g ` U ) } ) -> ( ._|_ ` ( ._|_ ` { ( 0g ` U ) } ) ) = { ( 0g ` U ) } )
22 18 21 eqtrd 
 |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) /\ Q = { ( 0g ` U ) } ) -> ( ._|_ ` ( ._|_ ` Q ) ) = { ( 0g ` U ) } )
23 22 ex 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> ( Q = { ( 0g ` U ) } -> ( ._|_ ` ( ._|_ ` Q ) ) = { ( 0g ` U ) } ) )
24 23 necon3d 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> ( ( ._|_ ` ( ._|_ ` Q ) ) =/= { ( 0g ` U ) } -> Q =/= { ( 0g ` U ) } ) )
25 15 24 mpd 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> Q =/= { ( 0g ` U ) } )
26 25 necomd 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> { ( 0g ` U ) } =/= Q )
27 df-pss 
 |-  ( { ( 0g ` U ) } C. Q <-> ( { ( 0g ` U ) } C_ Q /\ { ( 0g ` U ) } =/= Q ) )
28 13 26 27 sylanbrc 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> { ( 0g ` U ) } C. Q )
29 6 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> ( K e. HL /\ W e. H ) )
30 eqid 
 |-  ( Base ` U ) = ( Base ` U )
31 30 4 lssss 
 |-  ( Q e. S -> Q C_ ( Base ` U ) )
32 7 31 syl 
 |-  ( ph -> Q C_ ( Base ` U ) )
33 32 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> Q C_ ( Base ` U ) )
34 1 3 30 2 dochocss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q C_ ( Base ` U ) ) -> Q C_ ( ._|_ ` ( ._|_ ` Q ) ) )
35 29 33 34 syl2anc 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> Q C_ ( ._|_ ` ( ._|_ ` Q ) ) )
36 4 5 9 14 lsatlssel 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> ( ._|_ ` ( ._|_ ` Q ) ) e. S )
37 4 lsssubg 
 |-  ( ( U e. LMod /\ ( ._|_ ` ( ._|_ ` Q ) ) e. S ) -> ( ._|_ ` ( ._|_ ` Q ) ) e. ( SubGrp ` U ) )
38 9 36 37 syl2anc 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> ( ._|_ ` ( ._|_ ` Q ) ) e. ( SubGrp ` U ) )
39 eqid 
 |-  ( LSSum ` U ) = ( LSSum ` U )
40 11 39 lsm02 
 |-  ( ( ._|_ ` ( ._|_ ` Q ) ) e. ( SubGrp ` U ) -> ( { ( 0g ` U ) } ( LSSum ` U ) ( ._|_ ` ( ._|_ ` Q ) ) ) = ( ._|_ ` ( ._|_ ` Q ) ) )
41 38 40 syl 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> ( { ( 0g ` U ) } ( LSSum ` U ) ( ._|_ ` ( ._|_ ` Q ) ) ) = ( ._|_ ` ( ._|_ ` Q ) ) )
42 35 41 sseqtrrd 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> Q C_ ( { ( 0g ` U ) } ( LSSum ` U ) ( ._|_ ` ( ._|_ ` Q ) ) ) )
43 1 3 6 dvhlvec 
 |-  ( ph -> U e. LVec )
44 43 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> U e. LVec )
45 11 4 lsssn0 
 |-  ( U e. LMod -> { ( 0g ` U ) } e. S )
46 9 45 syl 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> { ( 0g ` U ) } e. S )
47 4 39 5 44 46 10 14 lsmsatcv 
 |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) /\ { ( 0g ` U ) } C. Q /\ Q C_ ( { ( 0g ` U ) } ( LSSum ` U ) ( ._|_ ` ( ._|_ ` Q ) ) ) ) -> Q = ( { ( 0g ` U ) } ( LSSum ` U ) ( ._|_ ` ( ._|_ ` Q ) ) ) )
48 28 42 47 mpd3an23 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> Q = ( { ( 0g ` U ) } ( LSSum ` U ) ( ._|_ ` ( ._|_ ` Q ) ) ) )
49 48 41 eqtr2d 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> ( ._|_ ` ( ._|_ ` Q ) ) = Q )
50 49 14 eqeltrrd 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` Q ) ) e. A ) -> Q e. A )
51 6 adantr 
 |-  ( ( ph /\ Q e. A ) -> ( K e. HL /\ W e. H ) )
52 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
53 1 3 52 5 dih1dimat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) -> Q e. ran ( ( DIsoH ` K ) ` W ) )
54 6 53 sylan 
 |-  ( ( ph /\ Q e. A ) -> Q e. ran ( ( DIsoH ` K ) ` W ) )
55 1 52 2 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Q e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` Q ) ) = Q )
56 51 54 55 syl2anc 
 |-  ( ( ph /\ Q e. A ) -> ( ._|_ ` ( ._|_ ` Q ) ) = Q )
57 simpr 
 |-  ( ( ph /\ Q e. A ) -> Q e. A )
58 56 57 eqeltrd 
 |-  ( ( ph /\ Q e. A ) -> ( ._|_ ` ( ._|_ ` Q ) ) e. A )
59 50 58 impbida 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` Q ) ) e. A <-> Q e. A ) )