Metamath Proof Explorer


Theorem lcfl6lem

Description: Lemma for lcfl6 . A functional G (whose kernel is closed by dochsnkr ) is comletely 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 ( 𝜑𝐺 = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) ) )