Metamath Proof Explorer


Theorem dochkrsat

Description: The orthocomplement of a kernel is an atom iff it is nonzero. (Contributed by NM, 1-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 dochkrsat.h H = LHyp K
2 dochkrsat.o ˙ = ocH K W
3 dochkrsat.u U = DVecH K W
4 dochkrsat.a A = LSAtoms U
5 dochkrsat.f F = LFnl U
6 dochkrsat.l L = LKer U
7 dochkrsat.z 0 ˙ = 0 U
8 dochkrsat.k φ K HL W H
9 dochkrsat.g φ G F
10 eqid Base U = Base U
11 eqid LSHyp U = LSHyp U
12 1 2 3 10 11 5 6 8 9 dochkrshp φ ˙ ˙ L G Base U ˙ ˙ L G LSHyp U
13 1 3 8 dvhlmod φ U LMod
14 10 5 6 13 9 lkrssv φ L G Base U
15 1 2 3 10 7 8 14 dochn0nv φ ˙ L G 0 ˙ ˙ ˙ L G Base U
16 eqid LSubSp U = LSubSp U
17 1 3 10 16 2 dochlss K HL W H L G Base U ˙ L G LSubSp U
18 8 14 17 syl2anc φ ˙ L G LSubSp U
19 1 2 3 16 4 11 8 18 dochsatshpb φ ˙ L G A ˙ ˙ L G LSHyp U
20 12 15 19 3bitr4d φ ˙ L G 0 ˙ ˙ L G A