Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dochshpsat Structured version   Unicode version

Theorem dochshpsat 32314
 Description: A hyperplane is closed iff its orthocomplement is an atom. (Contributed by NM, 29-Oct-2014.)
Hypotheses
Ref Expression
dochshpsat.h
dochshpsat.o
dochshpsat.u
dochshpsat.a LSAtoms
dochshpsat.y LSHyp
dochshpsat.k
dochshpsat.x
Assertion
Ref Expression
dochshpsat

Proof of Theorem dochshpsat
StepHypRef Expression
1 simpr 449 . . . 4
2 dochshpsat.x . . . . 5
32adantr 453 . . . 4
41, 3eqeltrd 2512 . . 3
5 dochshpsat.h . . . . 5
6 dochshpsat.o . . . . 5
7 dochshpsat.u . . . . 5
8 eqid 2438 . . . . 5
9 dochshpsat.a . . . . 5 LSAtoms
10 dochshpsat.y . . . . 5 LSHyp
11 dochshpsat.k . . . . 5
125, 7, 11dvhlmod 31970 . . . . . . . 8
138, 10, 12, 2lshplss 29841 . . . . . . 7
14 eqid 2438 . . . . . . . 8
1514, 8lssss 16015 . . . . . . 7
1613, 15syl 16 . . . . . 6
175, 7, 14, 8, 6dochlss 32214 . . . . . 6
1811, 16, 17syl2anc 644 . . . . 5
195, 6, 7, 8, 9, 10, 11, 18dochsatshpb 32312 . . . 4
214, 20mpbird 225 . 2
22 eqid 2438 . . . . . 6
2312adantr 453 . . . . . 6
24 simpr 449 . . . . . 6
2522, 9, 23, 24lsatn0 29859 . . . . 5
2625neneqd 2619 . . . 4
2711adantr 453 . . . . . . 7
285, 7, 6, 14, 22doch0 32218 . . . . . . 7
2927, 28syl 16 . . . . . 6
3029eqeq2d 2449 . . . . 5
31 eqid 2438 . . . . . . 7
325, 31, 7, 14, 6dochcl 32213 . . . . . . . 8
3311, 16, 32syl2anc 644 . . . . . . 7
345, 31, 7, 22dih0rn 32144 . . . . . . . 8
3511, 34syl 16 . . . . . . 7
365, 31, 6, 11, 33, 35doch11 32233 . . . . . 6
3736adantr 453 . . . . 5
3830, 37bitr3d 248 . . . 4
3926, 38mtbird 294 . . 3
405, 6, 7, 14, 10, 11, 2dochshpncl 32244 . . . . 5
4140necon1bbid 2660 . . . 4