Metamath Proof Explorer


Theorem dochsat0

Description: The orthocomplement of a kernel is either an atom or zero. (Contributed by NM, 29-Jan-2015)

Ref Expression
Hypotheses dochsat0.h H = LHyp K
dochsat0.o ˙ = ocH K W
dochsat0.u U = DVecH K W
dochsat0.z 0 ˙ = 0 U
dochsat0.a A = LSAtoms U
dochsat0.f F = LFnl U
dochsat0.l L = LKer U
dochsat0.k φ K HL W H
dochsat0.g φ G F
Assertion dochsat0 φ ˙ L G A ˙ L G = 0 ˙

Proof

Step Hyp Ref Expression
1 dochsat0.h H = LHyp K
2 dochsat0.o ˙ = ocH K W
3 dochsat0.u U = DVecH K W
4 dochsat0.z 0 ˙ = 0 U
5 dochsat0.a A = LSAtoms U
6 dochsat0.f F = LFnl U
7 dochsat0.l L = LKer U
8 dochsat0.k φ K HL W H
9 dochsat0.g φ G F
10 1 2 3 5 6 7 4 8 9 dochkrsat φ ˙ L G 0 ˙ ˙ L G A
11 10 biimpd φ ˙ L G 0 ˙ ˙ L G A
12 11 necon1bd φ ¬ ˙ L G A ˙ L G = 0 ˙
13 12 orrd φ ˙ L G A ˙ L G = 0 ˙