Metamath Proof Explorer

Theorem dochshpncl

Description: If a hyperplane is not closed, its closure equals the vector space. (Contributed by NM, 29-Oct-2014)

Ref Expression
Hypotheses dochshpncl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochshpncl.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochshpncl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochshpncl.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochshpncl.y ⊢ 𝑌 = ( LSHyp ‘ 𝑈 )
dochshpncl.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochshpncl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑌 )
Assertion dochshpncl ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑉 ) )

Proof

Step Hyp Ref Expression
1 dochshpncl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochshpncl.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochshpncl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochshpncl.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochshpncl.y ⊢ 𝑌 = ( LSHyp ‘ 𝑈 )
6 dochshpncl.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 dochshpncl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑌 )
8 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
9 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
10 eqid ⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
11 1 3 6 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
12 4 8 9 10 5 11 islshpsm ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑌 ↔ ( 𝑋 ∈ ( LSubSp ‘ 𝑈 ) ∧ 𝑋 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) ) )
13 7 12 mpbid ⊢ ( 𝜑 → ( 𝑋 ∈ ( LSubSp ‘ 𝑈 ) ∧ 𝑋 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) )
14 13 simp3d ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑉 ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 )
15 14 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ) → ∃ 𝑣 ∈ 𝑉 ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 )
16 id ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) )
17 16 adantlr ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) )
18 17 3adant3 ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) )
19 9 5 11 7 lshplss ⊢ ( 𝜑 → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
20 4 9 lssss ⊢ ( 𝑋 ∈ ( LSubSp ‘ 𝑈 ) → 𝑋 ⊆ 𝑉 )
21 19 20 syl ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
22 1 3 4 2 dochocss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
23 6 21 22 syl2anc ⊢ ( 𝜑 → 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ) → 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
25 24 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
26 simp1r ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 )
27 26 necomd ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → 𝑋 ≠ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
28 df-pss ⊢ ( 𝑋 ⊊ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ↔ ( 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∧ 𝑋 ≠ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) )
29 25 27 28 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → 𝑋 ⊊ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
30 1 3 4 2 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 )
31 6 21 30 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 )
32 1 3 4 2 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 )
33 6 31 32 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 )
34 33 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 )
35 34 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑉 )
36 simp3 ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 )
37 35 36 sseqtrrd ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
38 6 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
39 1 3 38 dvhlvec ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑈 ∈ LVec )
40 19 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
41 1 3 4 9 2 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
42 6 31 41 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
44 simpr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
45 4 9 8 10 39 40 43 44 lsmcv ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑋 ⊊ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
46 18 29 37 45 syl3anc ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
47 46 36 eqtrd ⊢ ( ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑉 )
48 47 rexlimdv3a ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ) → ( ∃ 𝑣 ∈ 𝑉 ( 𝑋 ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = 𝑉 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑉 ) )
49 15 48 mpd ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑉 )
50 simpr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑉 )
51 4 5 11 7 lshpne ⊢ ( 𝜑 → 𝑋 ≠ 𝑉 )
52 51 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑉 ) → 𝑋 ≠ 𝑉 )
53 52 necomd ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑉 ) → 𝑉 ≠ 𝑋 )
54 50 53 eqnetrd ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 )
55 49 54 impbida ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑋 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑉 ) )