Theorem lcfrlem5

Description: Lemma for lcfr . The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace Q is closed under scalar product. TODO: share hypotheses with others. Use more consistent variable names here or elsewhere when possible. (Contributed by NM, 5-Mar-2015)

	Ref	Expression
Hypotheses	lcfrlem5.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcfrlem5.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcfrlem5.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcfrlem5.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lcfrlem5.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcfrlem5.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcfrlem5.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lcfrlem5.s	⊢ 𝑆 = ( LSubSp ‘ 𝐷 )
	lcfrlem5.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcfrlem5.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
	lcfrlem5.q	⊢ 𝑄 = ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) )
	lcfrlem5.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑄 )
	lcfrlem5.c	⊢ 𝐶 = ( Scalar ‘ 𝑈 )
	lcfrlem5.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	lcfrlem5.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
	lcfrlem5.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
Assertion	lcfrlem5	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		lcfrlem5.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcfrlem5.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcfrlem5.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lcfrlem5.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		lcfrlem5.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6		lcfrlem5.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
7		lcfrlem5.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
8		lcfrlem5.s	⊢ 𝑆 = ( LSubSp ‘ 𝐷 )
9		lcfrlem5.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		lcfrlem5.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
11		lcfrlem5.q	⊢ 𝑄 = ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) )
12		lcfrlem5.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑄 )
13		lcfrlem5.c	⊢ 𝐶 = ( Scalar ‘ 𝑈 )
14		lcfrlem5.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
15		lcfrlem5.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
16		lcfrlem5.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
17	12 11	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) )
18		eliun	⊢ ( 𝑋 ∈ ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ↔ ∃ 𝑓 ∈ 𝑅 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) )
19	17 18	sylib	⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝑅 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) )
20	1 3 9	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
21	20	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑅 ) ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) → 𝑈 ∈ LMod )
22	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑅 ) ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
23		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
24	23 8	lssss	⊢ ( 𝑅 ∈ 𝑆 → 𝑅 ⊆ ( Base ‘ 𝐷 ) )
25	10 24	syl	⊢ ( 𝜑 → 𝑅 ⊆ ( Base ‘ 𝐷 ) )
26	5 7 23 20	ldualvbase	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = 𝐹 )
27	25 26	sseqtrd	⊢ ( 𝜑 → 𝑅 ⊆ 𝐹 )
28	27	sselda	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑅 ) → 𝑓 ∈ 𝐹 )
29	28	adantr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑅 ) ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) → 𝑓 ∈ 𝐹 )
30	4 5 6 21 29	lkrssv	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑅 ) ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) → ( 𝐿 ‘ 𝑓 ) ⊆ 𝑉 )
31		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
32	1 3 4 31 2	dochlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝑓 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
33	22 30 32	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑅 ) ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
34	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑅 ) ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) → 𝐴 ∈ 𝐵 )
35		simpr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑅 ) ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) → 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) )
36	13 15 14 31	lssvscl	⊢ ( ( ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) ) → ( 𝐴 · 𝑋 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) )
37	21 33 34 35 36	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑅 ) ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) → ( 𝐴 · 𝑋 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) )
38	37	ex	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑅 ) → ( 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) → ( 𝐴 · 𝑋 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) )
39	38	reximdva	⊢ ( 𝜑 → ( ∃ 𝑓 ∈ 𝑅 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) → ∃ 𝑓 ∈ 𝑅 ( 𝐴 · 𝑋 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) )
40	19 39	mpd	⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝑅 ( 𝐴 · 𝑋 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) )
41		eliun	⊢ ( ( 𝐴 · 𝑋 ) ∈ ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ↔ ∃ 𝑓 ∈ 𝑅 ( 𝐴 · 𝑋 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) )
42	40 41	sylibr	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ ∪ 𝑓 ∈ 𝑅 ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) )
43	42 11	eleqtrrdi	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ 𝑄 )