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

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 ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑋 } ) )