Metamath Proof Explorer


Theorem dochshpsat

Description: A hyperplane is closed iff its orthocomplement is an atom. (Contributed by NM, 29-Oct-2014)

Ref Expression
Hypotheses dochshpsat.h H = LHyp K
dochshpsat.o ˙ = ocH K W
dochshpsat.u U = DVecH K W
dochshpsat.a A = LSAtoms U
dochshpsat.y Y = LSHyp U
dochshpsat.k φ K HL W H
dochshpsat.x φ X Y
Assertion dochshpsat φ ˙ ˙ X = X ˙ X A

Proof

Step Hyp Ref Expression
1 dochshpsat.h H = LHyp K
2 dochshpsat.o ˙ = ocH K W
3 dochshpsat.u U = DVecH K W
4 dochshpsat.a A = LSAtoms U
5 dochshpsat.y Y = LSHyp U
6 dochshpsat.k φ K HL W H
7 dochshpsat.x φ X Y
8 simpr φ ˙ ˙ X = X ˙ ˙ X = X
9 7 adantr φ ˙ ˙ X = X X Y
10 8 9 eqeltrd φ ˙ ˙ X = X ˙ ˙ X Y
11 eqid LSubSp U = LSubSp U
12 1 3 6 dvhlmod φ U LMod
13 11 5 12 7 lshplss φ X LSubSp U
14 eqid Base U = Base U
15 14 11 lssss X LSubSp U X Base U
16 13 15 syl φ X Base U
17 1 3 14 11 2 dochlss K HL W H X Base U ˙ X LSubSp U
18 6 16 17 syl2anc φ ˙ X LSubSp U
19 1 2 3 11 4 5 6 18 dochsatshpb φ ˙ X A ˙ ˙ X Y
20 19 adantr φ ˙ ˙ X = X ˙ X A ˙ ˙ X Y
21 10 20 mpbird φ ˙ ˙ X = X ˙ X A
22 eqid 0 U = 0 U
23 12 adantr φ ˙ X A U LMod
24 simpr φ ˙ X A ˙ X A
25 22 4 23 24 lsatn0 φ ˙ X A ˙ X 0 U
26 25 neneqd φ ˙ X A ¬ ˙ X = 0 U
27 6 adantr φ ˙ X A K HL W H
28 1 3 2 14 22 doch0 K HL W H ˙ 0 U = Base U
29 27 28 syl φ ˙ X A ˙ 0 U = Base U
30 29 eqeq2d φ ˙ X A ˙ ˙ X = ˙ 0 U ˙ ˙ X = Base U
31 eqid DIsoH K W = DIsoH K W
32 1 31 3 14 2 dochcl K HL W H X Base U ˙ X ran DIsoH K W
33 6 16 32 syl2anc φ ˙ X ran DIsoH K W
34 1 31 3 22 dih0rn K HL W H 0 U ran DIsoH K W
35 6 34 syl φ 0 U ran DIsoH K W
36 1 31 2 6 33 35 doch11 φ ˙ ˙ X = ˙ 0 U ˙ X = 0 U
37 36 adantr φ ˙ X A ˙ ˙ X = ˙ 0 U ˙ X = 0 U
38 30 37 bitr3d φ ˙ X A ˙ ˙ X = Base U ˙ X = 0 U
39 26 38 mtbird φ ˙ X A ¬ ˙ ˙ X = Base U
40 1 2 3 14 5 6 7 dochshpncl φ ˙ ˙ X X ˙ ˙ X = Base U
41 40 necon1bbid φ ¬ ˙ ˙ X = Base U ˙ ˙ X = X
42 41 adantr φ ˙ X A ¬ ˙ ˙ X = Base U ˙ ˙ X = X
43 39 42 mpbid φ ˙ X A ˙ ˙ X = X
44 21 43 impbida φ ˙ ˙ X = X ˙ X A