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

Metamath Proof Explorer

Theorem dochsnkrlem2

Description: Lemma for dochsnkr . (Contributed by NM, 1-Jan-2015)

Ref Expression
Hypotheses dochsnkr.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochsnkr.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochsnkr.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochsnkr.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochsnkr.z ⊢ 0 = ( 0g ‘ 𝑈 )
dochsnkr.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
dochsnkr.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
dochsnkr.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochsnkr.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
dochsnkr.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) )
dochsnkr.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
Assertion dochsnkrlem2 ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 dochsnkr.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochsnkr.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochsnkr.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochsnkr.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochsnkr.z ⊢ 0 = ( 0g ‘ 𝑈 )
6 dochsnkr.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7 dochsnkr.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
8 dochsnkr.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 dochsnkr.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
10 dochsnkr.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) )
11 dochsnkr.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
12 1 2 3 4 5 6 7 8 9 10 dochsnkrlem1 ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 )
13 1 2 3 4 11 6 7 8 9 dochkrsat2 ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 ) )
14 12 13 mpbid ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝐴 )