Metamath Proof Explorer


Theorem lclkrslem1

Description: The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace Q is closed under scalar product. (Contributed by NM, 27-Jan-2015)

Ref Expression
Hypotheses lclkrslem1.h 𝐻 = ( LHyp ‘ 𝐾 )
lclkrslem1.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lclkrslem1.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lclkrslem1.s 𝑆 = ( LSubSp ‘ 𝑈 )
lclkrslem1.f 𝐹 = ( LFnl ‘ 𝑈 )
lclkrslem1.l 𝐿 = ( LKer ‘ 𝑈 )
lclkrslem1.d 𝐷 = ( LDual ‘ 𝑈 )
lclkrslem1.r 𝑅 = ( Scalar ‘ 𝑈 )
lclkrslem1.b 𝐵 = ( Base ‘ 𝑅 )
lclkrslem1.t · = ( ·𝑠𝐷 )
lclkrslem1.c 𝐶 = { 𝑓𝐹 ∣ ( ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( ‘ ( 𝐿𝑓 ) ) ⊆ 𝑄 ) }
lclkrslem1.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
lclkrslem1.q ( 𝜑𝑄𝑆 )
lclkrslem1.g ( 𝜑𝐺𝐶 )
lclkrslem1.x ( 𝜑𝑋𝐵 )
Assertion lclkrslem1 ( 𝜑 → ( 𝑋 · 𝐺 ) ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 lclkrslem1.h 𝐻 = ( LHyp ‘ 𝐾 )
2 lclkrslem1.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lclkrslem1.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lclkrslem1.s 𝑆 = ( LSubSp ‘ 𝑈 )
5 lclkrslem1.f 𝐹 = ( LFnl ‘ 𝑈 )
6 lclkrslem1.l 𝐿 = ( LKer ‘ 𝑈 )
7 lclkrslem1.d 𝐷 = ( LDual ‘ 𝑈 )
8 lclkrslem1.r 𝑅 = ( Scalar ‘ 𝑈 )
9 lclkrslem1.b 𝐵 = ( Base ‘ 𝑅 )
10 lclkrslem1.t · = ( ·𝑠𝐷 )
11 lclkrslem1.c 𝐶 = { 𝑓𝐹 ∣ ( ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( ‘ ( 𝐿𝑓 ) ) ⊆ 𝑄 ) }
12 lclkrslem1.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
13 lclkrslem1.q ( 𝜑𝑄𝑆 )
14 lclkrslem1.g ( 𝜑𝐺𝐶 )
15 lclkrslem1.x ( 𝜑𝑋𝐵 )
16 eqid { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) } = { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) }
17 11 16 lcfls1c ( 𝐺𝐶 ↔ ( 𝐺 ∈ { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) } ∧ ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 ) )
18 17 simplbi ( 𝐺𝐶𝐺 ∈ { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) } )
19 14 18 syl ( 𝜑𝐺 ∈ { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) } )
20 1 2 3 5 6 7 8 9 10 16 12 15 19 lclkrlem1 ( 𝜑 → ( 𝑋 · 𝐺 ) ∈ { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) } )
21 eqid ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
22 1 3 12 dvhlmod ( 𝜑𝑈 ∈ LMod )
23 11 lcfls1lem ( 𝐺𝐶 ↔ ( 𝐺𝐹 ∧ ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ∧ ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 ) )
24 14 23 sylib ( 𝜑 → ( 𝐺𝐹 ∧ ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ∧ ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 ) )
25 24 simp1d ( 𝜑𝐺𝐹 )
26 5 8 9 7 10 22 15 25 ldualvscl ( 𝜑 → ( 𝑋 · 𝐺 ) ∈ 𝐹 )
27 21 5 6 22 26 lkrssv ( 𝜑 → ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) ⊆ ( Base ‘ 𝑈 ) )
28 1 3 12 dvhlvec ( 𝜑𝑈 ∈ LVec )
29 8 9 5 6 7 10 28 25 15 lkrss ( 𝜑 → ( 𝐿𝐺 ) ⊆ ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) )
30 1 3 21 2 dochss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) ⊆ ( Base ‘ 𝑈 ) ∧ ( 𝐿𝐺 ) ⊆ ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) ) → ( ‘ ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) ) ⊆ ( ‘ ( 𝐿𝐺 ) ) )
31 12 27 29 30 syl3anc ( 𝜑 → ( ‘ ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) ) ⊆ ( ‘ ( 𝐿𝐺 ) ) )
32 24 simp3d ( 𝜑 → ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 )
33 31 32 sstrd ( 𝜑 → ( ‘ ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) ) ⊆ 𝑄 )
34 11 16 lcfls1c ( ( 𝑋 · 𝐺 ) ∈ 𝐶 ↔ ( ( 𝑋 · 𝐺 ) ∈ { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) } ∧ ( ‘ ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) ) ⊆ 𝑄 ) )
35 20 33 34 sylanbrc ( 𝜑 → ( 𝑋 · 𝐺 ) ∈ 𝐶 )