This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dochsnnz

Description: The orthocomplement of a singleton is nonzero. (Contributed by NM, 13-Jun-2015)

Ref Expression
Hypotheses dochsnnz.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochsnnz.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochsnnz.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochsnnz.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochsnnz.z ⊢ 0 = ( 0g ‘ 𝑈 )
dochsnnz.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochsnnz.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion dochsnnz ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ≠ { 0 } )

Proof

Step Hyp Ref Expression
1 dochsnnz.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochsnnz.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochsnnz.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochsnnz.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochsnnz.z ⊢ 0 = ( 0g ‘ 𝑈 )
6 dochsnnz.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 dochsnnz.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
9 1 3 2 4 8 6 7 dochocsn ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) )
10 1 3 4 8 6 7 dvh2dim ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑉 ¬ 𝑦 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) )
11 eleq2 ⊢ ( ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) = 𝑉 → ( 𝑦 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ↔ 𝑦 ∈ 𝑉 ) )
12 11 biimprcd ⊢ ( 𝑦 ∈ 𝑉 → ( ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) = 𝑉 → 𝑦 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) )
13 12 necon3bd ⊢ ( 𝑦 ∈ 𝑉 → ( ¬ 𝑦 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ≠ 𝑉 ) )
14 13 rexlimiv ⊢ ( ∃ 𝑦 ∈ 𝑉 ¬ 𝑦 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ≠ 𝑉 )
15 10 14 syl ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ≠ 𝑉 )
16 9 15 eqnetrd ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) ≠ 𝑉 )
17 7 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
18 1 2 3 4 5 6 17 dochn0nv ⊢ ( 𝜑 → ( ( ⊥ ‘ { 𝑋 } ) ≠ { 0 } ↔ ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) ≠ 𝑉 ) )
19 16 18 mpbird ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ≠ { 0 } )