Theorem lcfl6lem

Description: Lemma for lcfl6 . A functional G (whose kernel is closed by dochsnkr ) is completely determined by a vector X in the orthocomplement in its kernel at which the functional value is 1. Note that the \ { .0. } in the X hypothesis is redundant by the last hypothesis but allows easier use of other theorems. (Contributed by NM, 3-Jan-2015)

	Ref	Expression
Hypotheses	lcfl6lem.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcfl6lem.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcfl6lem.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcfl6lem.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lcfl6lem.a	⊢ + = ( +g ‘ 𝑈 )
	lcfl6lem.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
	lcfl6lem.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
	lcfl6lem.i	⊢ 1 = ( 1r ‘ 𝑆 )
	lcfl6lem.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
	lcfl6lem.z	⊢ 0 = ( 0g ‘ 𝑈 )
	lcfl6lem.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcfl6lem.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcfl6lem.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcfl6lem.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	lcfl6lem.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) )
	lcfl6lem.y	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = 1 )
Assertion	lcfl6lem	⊢ ( 𝜑 → 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcfl6lem.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcfl6lem.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcfl6lem.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lcfl6lem.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		lcfl6lem.a	⊢ + = ( +g ‘ 𝑈 )
6		lcfl6lem.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
7		lcfl6lem.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
8		lcfl6lem.i	⊢ 1 = ( 1r ‘ 𝑆 )
9		lcfl6lem.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
10		lcfl6lem.z	⊢ 0 = ( 0g ‘ 𝑈 )
11		lcfl6lem.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
12		lcfl6lem.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
13		lcfl6lem.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14		lcfl6lem.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
15		lcfl6lem.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) )
16		lcfl6lem.y	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = 1 )
17		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
18	1 3 13	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
19	1 3 13	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
20	4 11 12 19 14	lkrssv	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 )
21	1 3 4 2	dochssv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑉 )
22	13 20 21	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑉 )
23	15	eldifad	⊢ ( 𝜑 → 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
24	22 23	sseldd	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
25		eqid	⊢ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
26		eldifsni	⊢ ( 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) → 𝑋 ≠ 0 )
27	15 26	syl	⊢ ( 𝜑 → 𝑋 ≠ 0 )
28		eldifsn	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) ↔ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) )
29	24 27 28	sylanbrc	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
30	1 2 3 4 10 5 6 11 7 9 25 13 29	dochflcl	⊢ ( 𝜑 → ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) ) ∈ 𝐹 )
31	1 2 3 4 10 11 12 13 14 15	dochsnkr	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑋 } ) )
32	1 2 3 4 10 5 6 12 7 9 25 13 29	dochsnkr2	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) ) ) = ( ⊥ ‘ { 𝑋 } ) )
33	31 32	eqtr4d	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) ) ) )
34	1 2 3 4 5 6 10 7 9 8 13 29 25	dochfl1	⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) ) ‘ 𝑋 ) = 1 )
35	16 34	eqtr4d	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) ) ‘ 𝑋 ) )
36	1 2 3 4 7 17 10 11 12 13 14 15	dochfln0	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ≠ ( 0g ‘ 𝑆 ) )
37	4 7 9 17 11 12 18 24 14 30 33 35 36	eqlkr3	⊢ ( 𝜑 → 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) ) )