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

Metamath Proof Explorer

Theorem dochsnkrlem1

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 } ) )
Assertion dochsnkrlem1 ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 )

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 eldif ⊢ ( 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ↔ ( 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ¬ 𝑋 ∈ { 0 } ) )
12 nelne1 ⊢ ( ( 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ¬ 𝑋 ∈ { 0 } ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ≠ { 0 } )
13 11 12 sylbi ⊢ ( 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ≠ { 0 } )
14 10 13 syl ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ≠ { 0 } )
15 1 3 8 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
16 4 6 7 15 9 lkrssv ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 )
17 1 2 3 4 5 8 16 dochn0nv ⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ≠ { 0 } ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ) )
18 14 17 mpbid ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 )