Metamath Proof Explorer

Theorem dochfln0

Description: The value of a functional is nonzero at a nonzero vector in the orthocomplement of its kernel. (Contributed by NM, 2-Jan-2015)

Ref Expression
Hypotheses dochfln0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochfln0.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochfln0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochfln0.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochfln0.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
dochfln0.n ⊢ 𝑁 = ( 0g ‘ 𝑅 )
dochfln0.z ⊢ 0 = ( 0g ‘ 𝑈 )
dochfln0.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
dochfln0.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
dochfln0.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochfln0.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
dochfln0.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) )
Assertion dochfln0 ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ≠ 𝑁 )

Proof

Step Hyp Ref Expression
1 dochfln0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochfln0.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochfln0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochfln0.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochfln0.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
6 dochfln0.n ⊢ 𝑁 = ( 0g ‘ 𝑅 )
7 dochfln0.z ⊢ 0 = ( 0g ‘ 𝑈 )
8 dochfln0.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
9 dochfln0.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
10 dochfln0.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11 dochfln0.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
12 dochfln0.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) )
13 1 3 10 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
14 4 8 9 13 11 lkrssv ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 )
15 1 3 4 2 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑉 )
16 10 14 15 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑉 )
17 16 ssdifd ⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ⊆ ( 𝑉 ∖ { 0 } ) )
18 17 12 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
19 1 2 3 4 7 10 18 dochnel ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘ { 𝑋 } ) )
20 12 eldifad ⊢ ( 𝜑 → 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
21 16 20 sseldd ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
22 21 biantrurd ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) = 𝑁 ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑋 ) = 𝑁 ) ) )
23 4 5 6 8 9 ellkr ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝑋 ∈ ( 𝐿 ‘ 𝐺 ) ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑋 ) = 𝑁 ) ) )
24 13 11 23 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐿 ‘ 𝐺 ) ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑋 ) = 𝑁 ) ) )
25 1 2 3 4 7 8 9 10 11 12 dochsnkr ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑋 } ) )
26 25 eleq2d ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐿 ‘ 𝐺 ) ↔ 𝑋 ∈ ( ⊥ ‘ { 𝑋 } ) ) )
27 22 24 26 3bitr2rd ⊢ ( 𝜑 → ( 𝑋 ∈ ( ⊥ ‘ { 𝑋 } ) ↔ ( 𝐺 ‘ 𝑋 ) = 𝑁 ) )
28 27 necon3bbid ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ ( ⊥ ‘ { 𝑋 } ) ↔ ( 𝐺 ‘ 𝑋 ) ≠ 𝑁 ) )
29 19 28 mpbid ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ≠ 𝑁 )