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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochkrsat2.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	dochkrsat2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochkrsat2.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dochkrsat2.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
	dochkrsat2.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	dochkrsat2.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	dochkrsat2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dochkrsat2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	dochkrsat2	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		dochkrsat2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochkrsat2.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		dochkrsat2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dochkrsat2.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		dochkrsat2.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
6		dochkrsat2.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7		dochkrsat2.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
8		dochkrsat2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		dochkrsat2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
10		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
11	1 3 8	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
12	4 6 7 11 9	lkrssv	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 )
13	1 2 3 4 10 8 12	dochn0nv	⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ≠ { ( 0g ‘ 𝑈 ) } ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ) )
14	1 2 3 5 6 7 10 8 9	dochkrsat	⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ≠ { ( 0g ‘ 𝑈 ) } ↔ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 ) )
15	13 14	bitr3d	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 ) )