# Metamath Proof Explorer

## Theorem dochsnkr

Description: A (closed) kernel expressed in terms of a nonzero vector in its orthocomplement. TODO: consolidate lemmas unless they're needed for something else (in which case break out as theorems). (Contributed by NM, 2-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 dochsnkr ( 𝜑 → ( 𝐿𝐺 ) = ( ‘ { 𝑋 } ) )

### 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 eqid ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
12 eqid ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
13 1 3 8 dvhlvec ( 𝜑𝑈 ∈ LVec )
14 1 2 3 4 5 6 7 8 9 10 12 dochsnkrlem2 ( 𝜑 → ( ‘ ( 𝐿𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) )
15 10 eldifad ( 𝜑𝑋 ∈ ( ‘ ( 𝐿𝐺 ) ) )
16 eldifsni ( 𝑋 ∈ ( ( ‘ ( 𝐿𝐺 ) ) ∖ { 0 } ) → 𝑋0 )
17 10 16 syl ( 𝜑𝑋0 )
18 5 11 12 13 14 15 17 lsatel ( 𝜑 → ( ‘ ( 𝐿𝐺 ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) )
19 18 fveq2d ( 𝜑 → ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) )
20 1 2 3 4 5 6 7 8 9 10 dochsnkrlem3 ( 𝜑 → ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) )
21 1 3 8 dvhlmod ( 𝜑𝑈 ∈ LMod )
22 4 6 7 21 9 lkrssv ( 𝜑 → ( 𝐿𝐺 ) ⊆ 𝑉 )
23 1 3 4 2 dochssv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐿𝐺 ) ⊆ 𝑉 ) → ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑉 )
24 8 22 23 syl2anc ( 𝜑 → ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑉 )
25 24 ssdifssd ( 𝜑 → ( ( ‘ ( 𝐿𝐺 ) ) ∖ { 0 } ) ⊆ 𝑉 )
26 25 10 sseldd ( 𝜑𝑋𝑉 )
27 26 snssd ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
28 1 3 2 4 11 8 27 dochocsp ( 𝜑 → ( ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) = ( ‘ { 𝑋 } ) )
29 19 20 28 3eqtr3d ( 𝜑 → ( 𝐿𝐺 ) = ( ‘ { 𝑋 } ) )