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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochshpsat.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochshpsat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochshpsat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
dochshpsat.y ⊢ 𝑌 = ( LSHyp ‘ 𝑈 )
dochshpsat.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochshpsat.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑌 )
Assertion dochshpsat ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ↔ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 dochshpsat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochshpsat.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochshpsat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochshpsat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
5 dochshpsat.y ⊢ 𝑌 = ( LSHyp ‘ 𝑈 )
6 dochshpsat.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 dochshpsat.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑌 )
8 simpr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
9 7 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → 𝑋 ∈ 𝑌 )
10 8 9 eqeltrd ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ 𝑌 )
11 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
12 1 3 6 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
13 11 5 12 7 lshplss ⊢ ( 𝜑 → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
14 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
15 14 11 lssss ⊢ ( 𝑋 ∈ ( LSubSp ‘ 𝑈 ) → 𝑋 ⊆ ( Base ‘ 𝑈 ) )
16 13 15 syl ⊢ ( 𝜑 → 𝑋 ⊆ ( Base ‘ 𝑈 ) )
17 1 3 14 11 2 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) )
18 6 16 17 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑈 ) )
19 1 2 3 11 4 5 6 18 dochsatshpb ⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ 𝑌 ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ 𝑌 ) )
21 10 20 mpbird ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐴 )
22 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
23 12 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) → 𝑈 ∈ LMod )
24 simpr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐴 )
25 22 4 23 24 lsatn0 ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) → ( ⊥ ‘ 𝑋 ) ≠ { ( 0g ‘ 𝑈 ) } )
26 25 neneqd ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) → ¬ ( ⊥ ‘ 𝑋 ) = { ( 0g ‘ 𝑈 ) } )
27 6 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
28 1 3 2 14 22 doch0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) = ( Base ‘ 𝑈 ) )
29 27 28 syl ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) → ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) = ( Base ‘ 𝑈 ) )
30 29 eqeq2d ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( Base ‘ 𝑈 ) ) )
31 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
32 1 31 3 14 2 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
33 6 16 32 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
34 1 31 3 22 dih0rn ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → { ( 0g ‘ 𝑈 ) } ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
35 6 34 syl ⊢ ( 𝜑 → { ( 0g ‘ 𝑈 ) } ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
36 1 31 2 6 33 35 doch11 ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ↔ ( ⊥ ‘ 𝑋 ) = { ( 0g ‘ 𝑈 ) } ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) ↔ ( ⊥ ‘ 𝑋 ) = { ( 0g ‘ 𝑈 ) } ) )
38 30 37 bitr3d ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( Base ‘ 𝑈 ) ↔ ( ⊥ ‘ 𝑋 ) = { ( 0g ‘ 𝑈 ) } ) )
39 26 38 mtbird ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) → ¬ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( Base ‘ 𝑈 ) )
40 1 2 3 14 5 6 7 dochshpncl ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( Base ‘ 𝑈 ) ) )
41 40 necon1bbid ⊢ ( 𝜑 → ( ¬ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( Base ‘ 𝑈 ) ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) → ( ¬ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( Base ‘ 𝑈 ) ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) )
43 39 42 mpbid ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
44 21 43 impbida ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ↔ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) )