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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochsat0.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochsat0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochsat0.z ⊢ 0 = ( 0g ‘ 𝑈 )
dochsat0.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
dochsat0.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
dochsat0.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
dochsat0.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochsat0.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion dochsat0 ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 ∨ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = { 0 } ) )

Proof

Step Hyp Ref Expression
1 dochsat0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochsat0.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochsat0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochsat0.z ⊢ 0 = ( 0g ‘ 𝑈 )
5 dochsat0.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
6 dochsat0.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7 dochsat0.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
8 dochsat0.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 dochsat0.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
10 1 2 3 5 6 7 4 8 9 dochkrsat ⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ≠ { 0 } ↔ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 ) )
11 10 biimpd ⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ≠ { 0 } → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 ) )
12 11 necon1bd ⊢ ( 𝜑 → ( ¬ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = { 0 } ) )
13 12 orrd ⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 ∨ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = { 0 } ) )