Metamath Proof Explorer

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