Metamath Proof Explorer

Theorem lclkrs

Description: The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace R is a subspace of the dual space. TODO: This proof repeats large parts of the lclkr proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr a special case of this? (Contributed by NM, 29-Jan-2015)

Ref Expression
Hypotheses lclkrs.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lclkrs.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lclkrs.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lclkrs.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
lclkrs.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
lclkrs.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
lclkrs.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
lclkrs.t ⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
lclkrs.c ⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑅 ) }
lclkrs.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lclkrs.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
Assertion lclkrs ( 𝜑 → 𝐶 ∈ 𝑇 )

Proof

Step Hyp Ref Expression
1 lclkrs.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 lclkrs.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lclkrs.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lclkrs.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
5 lclkrs.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6 lclkrs.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
7 lclkrs.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
8 lclkrs.t ⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
9 lclkrs.c ⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑅 ) }
10 lclkrs.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11 lclkrs.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
12 ssrab2 ⊢ { 𝑓 ∈ 𝐹 ∣ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑅 ) } ⊆ 𝐹
13 12 a1i ⊢ ( 𝜑 → { 𝑓 ∈ 𝐹 ∣ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑅 ) } ⊆ 𝐹 )
14 9 a1i ⊢ ( 𝜑 → 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑅 ) } )
15 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
16 1 3 10 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
17 5 7 15 16 ldualvbase ⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = 𝐹 )
18 13 14 17 3sstr4d ⊢ ( 𝜑 → 𝐶 ⊆ ( Base ‘ 𝐷 ) )
19 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
20 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) )
21 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
22 19 20 21 5 lfl0f ⊢ ( 𝑈 ∈ LMod → ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ∈ 𝐹 )
23 16 22 syl ⊢ ( 𝜑 → ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ∈ 𝐹 )
24 1 3 2 21 10 dochoc1 ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( Base ‘ 𝑈 ) ) ) = ( Base ‘ 𝑈 ) )
25 eqidd ⊢ ( 𝜑 → ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) = ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) )
26 19 20 21 5 6 lkr0f ⊢ ( ( 𝑈 ∈ LMod ∧ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ∈ 𝐹 ) → ( ( 𝐿 ‘ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) = ( Base ‘ 𝑈 ) ↔ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) = ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) )
27 16 23 26 syl2anc ⊢ ( 𝜑 → ( ( 𝐿 ‘ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) = ( Base ‘ 𝑈 ) ↔ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) = ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) )
28 25 27 mpbird ⊢ ( 𝜑 → ( 𝐿 ‘ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) = ( Base ‘ 𝑈 ) )
29 28 fveq2d ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) ) = ( ⊥ ‘ ( Base ‘ 𝑈 ) ) )
30 29 fveq2d ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( Base ‘ 𝑈 ) ) ) )
31 24 30 28 3eqtr4d ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) ) ) = ( 𝐿 ‘ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) )
32 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
33 1 3 2 21 32 doch1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ ( Base ‘ 𝑈 ) ) = { ( 0g ‘ 𝑈 ) } )
34 10 33 syl ⊢ ( 𝜑 → ( ⊥ ‘ ( Base ‘ 𝑈 ) ) = { ( 0g ‘ 𝑈 ) } )
35 29 34 eqtrd ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) ) = { ( 0g ‘ 𝑈 ) } )
36 32 4 lss0ss ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑅 ∈ 𝑆 ) → { ( 0g ‘ 𝑈 ) } ⊆ 𝑅 )
37 16 11 36 syl2anc ⊢ ( 𝜑 → { ( 0g ‘ 𝑈 ) } ⊆ 𝑅 )
38 35 37 eqsstrd ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) ) ⊆ 𝑅 )
39 9 lcfls1lem ⊢ ( ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ∈ 𝐶 ↔ ( ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) ) ) = ( 𝐿 ‘ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) ∧ ( ⊥ ‘ ( 𝐿 ‘ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) ) ⊆ 𝑅 ) )
40 23 31 38 39 syl3anbrc ⊢ ( 𝜑 → ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ∈ 𝐶 )
41 40 ne0d ⊢ ( 𝜑 → 𝐶 ≠ ∅ )
42 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
43 eqid ⊢ ( ·𝑠 ‘ 𝐷 ) = ( ·𝑠 ‘ 𝐷 )
44 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
45 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → 𝑅 ∈ 𝑆 )
46 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → 𝑏 ∈ 𝐶 )
47 eqid ⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
48 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → 𝑎 ∈ 𝐶 )
49 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) )
50 eqid ⊢ ( Scalar ‘ 𝐷 ) = ( Scalar ‘ 𝐷 )
51 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐷 ) ) = ( Base ‘ ( Scalar ‘ 𝐷 ) )
52 19 42 7 50 51 16 ldualsbase ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐷 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
53 52 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( Base ‘ ( Scalar ‘ 𝐷 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
54 49 53 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
55 1 2 3 4 5 6 7 19 42 43 9 44 45 48 54 lclkrslem1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐷 ) 𝑎 ) ∈ 𝐶 )
56 1 2 3 4 5 6 7 19 42 43 9 44 45 46 47 55 lclkrslem2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐶 ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝐷 ) 𝑎 ) ( +g ‘ 𝐷 ) 𝑏 ) ∈ 𝐶 )
57 56 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) ∀ 𝑎 ∈ 𝐶 ∀ 𝑏 ∈ 𝐶 ( ( 𝑥 ( ·𝑠 ‘ 𝐷 ) 𝑎 ) ( +g ‘ 𝐷 ) 𝑏 ) ∈ 𝐶 )
58 50 51 15 47 43 8 islss ⊢ ( 𝐶 ∈ 𝑇 ↔ ( 𝐶 ⊆ ( Base ‘ 𝐷 ) ∧ 𝐶 ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) ∀ 𝑎 ∈ 𝐶 ∀ 𝑏 ∈ 𝐶 ( ( 𝑥 ( ·𝑠 ‘ 𝐷 ) 𝑎 ) ( +g ‘ 𝐷 ) 𝑏 ) ∈ 𝐶 ) )
59 18 41 57 58 syl3anbrc ⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )