This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ˙