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