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

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 ⊢ 𝐻 = ( 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 ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 ) )