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