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	⊢ ( 𝜑 → ( 𝑋 · 𝐺 ) ∈ 𝐶 )