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

Metamath Proof Explorer

Theorem dochexmidat

Description: Special case of excluded middle for the singleton of a vector. (Contributed by NM, 27-Oct-2014)

Ref Expression
Hypotheses dochexmidat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochexmidat.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochexmidat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochexmidat.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochexmidat.z ⊢ 0 = ( 0g ‘ 𝑈 )
dochexmidat.r ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dochexmidat.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dochexmidat.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochexmidat.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion dochexmidat ( 𝜑 → ( ( ⊥ ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )

Proof

Step Hyp Ref Expression
1 dochexmidat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochexmidat.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochexmidat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochexmidat.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochexmidat.z ⊢ 0 = ( 0g ‘ 𝑈 )
6 dochexmidat.r ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
7 dochexmidat.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
8 dochexmidat.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 dochexmidat.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
10 1 2 3 4 5 8 9 dochnel ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘ { 𝑋 } ) )
11 eqid ⊢ ( LSHyp ‘ 𝑈 ) = ( LSHyp ‘ 𝑈 )
12 1 3 8 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
13 1 2 3 4 5 11 8 9 dochsnshp ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ∈ ( LSHyp ‘ 𝑈 ) )
14 9 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
15 4 6 7 11 12 13 14 lshpnelb ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( ⊥ ‘ { 𝑋 } ) ↔ ( ( ⊥ ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 ) )
16 10 15 mpbid ⊢ ( 𝜑 → ( ( ⊥ ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) = 𝑉 )