Metamath Proof Explorer


Theorem dochnel2

Description: A nonzero member of a subspace doesn't belong to the orthocomplement of the subspace. (Contributed by NM, 28-Feb-2015)

Ref Expression
Hypotheses dochnoncon.h H = LHyp K
dochnoncon.u U = DVecH K W
dochnoncon.s S = LSubSp U
dochnoncon.z 0 ˙ = 0 U
dochnoncon.o ˙ = ocH K W
dochnel2.k φ K HL W H
dochnel2.t φ T S
dochnel2.x φ X T 0 ˙
Assertion dochnel2 φ ¬ X ˙ T

Proof

Step Hyp Ref Expression
1 dochnoncon.h H = LHyp K
2 dochnoncon.u U = DVecH K W
3 dochnoncon.s S = LSubSp U
4 dochnoncon.z 0 ˙ = 0 U
5 dochnoncon.o ˙ = ocH K W
6 dochnel2.k φ K HL W H
7 dochnel2.t φ T S
8 dochnel2.x φ X T 0 ˙
9 8 eldifbd φ ¬ X 0 ˙
10 8 eldifad φ X T
11 elin X T ˙ T X T X ˙ T
12 1 2 3 4 5 dochnoncon K HL W H T S T ˙ T = 0 ˙
13 6 7 12 syl2anc φ T ˙ T = 0 ˙
14 13 eleq2d φ X T ˙ T X 0 ˙
15 11 14 bitr3id φ X T X ˙ T X 0 ˙
16 15 biimpd φ X T X ˙ T X 0 ˙
17 10 16 mpand φ X ˙ T X 0 ˙
18 9 17 mtod φ ¬ X ˙ T