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