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 } ) )