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 ⊢ H = LHyp ⁡ K
dochexmidat.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochexmidat.u ⊢ U = DVecH ⁡ K ⁡ W
dochexmidat.v ⊢ V = Base U
dochexmidat.z ⊢ 0 ˙ = 0 U
dochexmidat.r ⊢ N = LSpan ⁡ U
dochexmidat.p ⊢ ⊕ ˙ = LSSum ⁡ U
dochexmidat.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochexmidat.x ⊢ φ → X ∈ V ∖ 0 ˙
Assertion dochexmidat ⊢ φ → ⊥ ˙ ⁡ X ⊕ ˙ N ⁡ X = V

Proof

Step Hyp Ref Expression
1 dochexmidat.h ⊢ H = LHyp ⁡ K
2 dochexmidat.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochexmidat.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochexmidat.v ⊢ V = Base U
5 dochexmidat.z ⊢ 0 ˙ = 0 U
6 dochexmidat.r ⊢ N = LSpan ⁡ U
7 dochexmidat.p ⊢ ⊕ ˙ = LSSum ⁡ U
8 dochexmidat.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 dochexmidat.x ⊢ φ → X ∈ V ∖ 0 ˙
10 1 2 3 4 5 8 9 dochnel ⊢ φ → ¬ X ∈ ⊥ ˙ ⁡ X
11 eqid ⊢ LSHyp ⁡ U = LSHyp ⁡ U
12 1 3 8 dvhlvec ⊢ φ → U ∈ LVec
13 1 2 3 4 5 11 8 9 dochsnshp ⊢ φ → ⊥ ˙ ⁡ X ∈ LSHyp ⁡ U
14 9 eldifad ⊢ φ → X ∈ V
15 4 6 7 11 12 13 14 lshpnelb ⊢ φ → ¬ X ∈ ⊥ ˙ ⁡ X ↔ ⊥ ˙ ⁡ X ⊕ ˙ N ⁡ X = V
16 10 15 mpbid ⊢ φ → ⊥ ˙ ⁡ X ⊕ ˙ N ⁡ X = V