Metamath Proof Explorer

Theorem dochkrsat2

Description: The orthocomplement of a kernel is an atom iff the double orthocomplement is not the vector space. (Contributed by NM, 1-Jan-2015)

Ref Expression
Hypotheses dochkrsat2.h ⊢ H = LHyp ⁡ K
dochkrsat2.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochkrsat2.u ⊢ U = DVecH ⁡ K ⁡ W
dochkrsat2.v ⊢ V = Base U
dochkrsat2.a ⊢ A = LSAtoms ⁡ U
dochkrsat2.f ⊢ F = LFnl ⁡ U
dochkrsat2.l ⊢ L = LKer ⁡ U
dochkrsat2.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochkrsat2.g ⊢ φ → G ∈ F
Assertion dochkrsat2 ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ↔ ⊥ ˙ ⁡ L ⁡ G ∈ A

Proof

Step Hyp Ref Expression
1 dochkrsat2.h ⊢ H = LHyp ⁡ K
2 dochkrsat2.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochkrsat2.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochkrsat2.v ⊢ V = Base U
5 dochkrsat2.a ⊢ A = LSAtoms ⁡ U
6 dochkrsat2.f ⊢ F = LFnl ⁡ U
7 dochkrsat2.l ⊢ L = LKer ⁡ U
8 dochkrsat2.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 dochkrsat2.g ⊢ φ → G ∈ F
10 eqid ⊢ 0 U = 0 U
11 1 3 8 dvhlmod ⊢ φ → U ∈ LMod
12 4 6 7 11 9 lkrssv ⊢ φ → L ⁡ G ⊆ V
13 1 2 3 4 10 8 12 dochn0nv ⊢ φ → ⊥ ˙ ⁡ L ⁡ G ≠ 0 U ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V
14 1 2 3 5 6 7 10 8 9 dochkrsat ⊢ φ → ⊥ ˙ ⁡ L ⁡ G ≠ 0 U ↔ ⊥ ˙ ⁡ L ⁡ G ∈ A
15 13 14 bitr3d ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ↔ ⊥ ˙ ⁡ L ⁡ G ∈ A