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 φ K HL W H
dochsat.q φ Q S
Assertion dochsat φ ˙ ˙ Q A Q 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 φ K HL W H
7 dochsat.q φ Q S
8 1 3 6 dvhlmod φ U LMod
9 8 adantr φ ˙ ˙ Q A U LMod
10 7 adantr φ ˙ ˙ Q A Q S
11 eqid 0 U = 0 U
12 11 4 lss0ss U LMod Q S 0 U Q
13 9 10 12 syl2anc φ ˙ ˙ Q A 0 U Q
14 simpr φ ˙ ˙ Q A ˙ ˙ Q A
15 11 5 9 14 lsatn0 φ ˙ ˙ Q A ˙ ˙ Q 0 U
16 simpr φ ˙ ˙ Q A Q = 0 U Q = 0 U
17 16 fveq2d φ ˙ ˙ Q A Q = 0 U ˙ Q = ˙ 0 U
18 17 fveq2d φ ˙ ˙ Q A Q = 0 U ˙ ˙ Q = ˙ ˙ 0 U
19 1 3 2 11 6 dochoc0 φ ˙ ˙ 0 U = 0 U
20 19 adantr φ ˙ ˙ Q A ˙ ˙ 0 U = 0 U
21 20 adantr φ ˙ ˙ Q A Q = 0 U ˙ ˙ 0 U = 0 U
22 18 21 eqtrd φ ˙ ˙ Q A Q = 0 U ˙ ˙ Q = 0 U
23 22 ex φ ˙ ˙ Q A Q = 0 U ˙ ˙ Q = 0 U
24 23 necon3d φ ˙ ˙ Q A ˙ ˙ Q 0 U Q 0 U
25 15 24 mpd φ ˙ ˙ Q A Q 0 U
26 25 necomd φ ˙ ˙ Q A 0 U Q
27 df-pss 0 U Q 0 U Q 0 U Q
28 13 26 27 sylanbrc φ ˙ ˙ Q A 0 U Q
29 6 adantr φ ˙ ˙ Q A K HL W H
30 eqid Base U = Base U
31 30 4 lssss Q S Q Base U
32 7 31 syl φ Q Base U
33 32 adantr φ ˙ ˙ Q A Q Base U
34 1 3 30 2 dochocss K HL W H Q Base U Q ˙ ˙ Q
35 29 33 34 syl2anc φ ˙ ˙ Q A Q ˙ ˙ Q
36 4 5 9 14 lsatlssel φ ˙ ˙ Q A ˙ ˙ Q S
37 4 lsssubg U LMod ˙ ˙ Q S ˙ ˙ Q SubGrp U
38 9 36 37 syl2anc φ ˙ ˙ Q A ˙ ˙ Q SubGrp U
39 eqid LSSum U = LSSum U
40 11 39 lsm02 ˙ ˙ Q SubGrp U 0 U LSSum U ˙ ˙ Q = ˙ ˙ Q
41 38 40 syl φ ˙ ˙ Q A 0 U LSSum U ˙ ˙ Q = ˙ ˙ Q
42 35 41 sseqtrrd φ ˙ ˙ Q A Q 0 U LSSum U ˙ ˙ Q
43 1 3 6 dvhlvec φ U LVec
44 43 adantr φ ˙ ˙ Q A U LVec
45 11 4 lsssn0 U LMod 0 U S
46 9 45 syl φ ˙ ˙ Q A 0 U S
47 4 39 5 44 46 10 14 lsmsatcv φ ˙ ˙ Q A 0 U Q Q 0 U LSSum U ˙ ˙ Q Q = 0 U LSSum U ˙ ˙ Q
48 28 42 47 mpd3an23 φ ˙ ˙ Q A Q = 0 U LSSum U ˙ ˙ Q
49 48 41 eqtr2d φ ˙ ˙ Q A ˙ ˙ Q = Q
50 49 14 eqeltrrd φ ˙ ˙ Q A Q A
51 6 adantr φ Q A K HL W H
52 eqid DIsoH K W = DIsoH K W
53 1 3 52 5 dih1dimat K HL W H Q A Q ran DIsoH K W
54 6 53 sylan φ Q A Q ran DIsoH K W
55 1 52 2 dochoc K HL W H Q ran DIsoH K W ˙ ˙ Q = Q
56 51 54 55 syl2anc φ Q A ˙ ˙ Q = Q
57 simpr φ Q A Q A
58 56 57 eqeltrd φ Q A ˙ ˙ Q A
59 50 58 impbida φ ˙ ˙ Q A Q A