Metamath Proof Explorer


Theorem lclkrslem2

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, 28-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 ( 𝜑𝐺𝐶 )
lclkrslem2.p + = ( +g𝐷 )
lclkrslem2.e ( 𝜑𝐸𝐶 )
Assertion lclkrslem2 ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐶 )

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 lclkrslem2.p + = ( +g𝐷 )
16 lclkrslem2.e ( 𝜑𝐸𝐶 )
17 eqid { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) } = { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) }
18 11 17 lcfls1c ( 𝐸𝐶 ↔ ( 𝐸 ∈ { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) } ∧ ( ‘ ( 𝐿𝐸 ) ) ⊆ 𝑄 ) )
19 18 simplbi ( 𝐸𝐶𝐸 ∈ { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) } )
20 16 19 syl ( 𝜑𝐸 ∈ { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) } )
21 11 17 lcfls1c ( 𝐺𝐶 ↔ ( 𝐺 ∈ { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) } ∧ ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 ) )
22 21 simplbi ( 𝐺𝐶𝐺 ∈ { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) } )
23 14 22 syl ( 𝜑𝐺 ∈ { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) } )
24 1 2 3 5 6 7 15 17 12 20 23 lclkrlem2 ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) } )
25 eqid ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
26 1 3 12 dvhlmod ( 𝜑𝑈 ∈ LMod )
27 11 lcfls1lem ( 𝐸𝐶 ↔ ( 𝐸𝐹 ∧ ( ‘ ( ‘ ( 𝐿𝐸 ) ) ) = ( 𝐿𝐸 ) ∧ ( ‘ ( 𝐿𝐸 ) ) ⊆ 𝑄 ) )
28 16 27 sylib ( 𝜑 → ( 𝐸𝐹 ∧ ( ‘ ( ‘ ( 𝐿𝐸 ) ) ) = ( 𝐿𝐸 ) ∧ ( ‘ ( 𝐿𝐸 ) ) ⊆ 𝑄 ) )
29 28 simp1d ( 𝜑𝐸𝐹 )
30 11 lcfls1lem ( 𝐺𝐶 ↔ ( 𝐺𝐹 ∧ ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ∧ ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 ) )
31 14 30 sylib ( 𝜑 → ( 𝐺𝐹 ∧ ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ∧ ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 ) )
32 31 simp1d ( 𝜑𝐺𝐹 )
33 5 7 15 26 29 32 ldualvaddcl ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐹 )
34 25 5 6 26 33 lkrssv ( 𝜑 → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ⊆ ( Base ‘ 𝑈 ) )
35 5 6 7 15 26 29 32 lkrin ( 𝜑 → ( ( 𝐿𝐸 ) ∩ ( 𝐿𝐺 ) ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
36 1 3 25 2 dochss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ⊆ ( Base ‘ 𝑈 ) ∧ ( ( 𝐿𝐸 ) ∩ ( 𝐿𝐺 ) ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) → ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ⊆ ( ‘ ( ( 𝐿𝐸 ) ∩ ( 𝐿𝐺 ) ) ) )
37 12 34 35 36 syl3anc ( 𝜑 → ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ⊆ ( ‘ ( ( 𝐿𝐸 ) ∩ ( 𝐿𝐺 ) ) ) )
38 eqid ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
39 eqid ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
40 28 simp2d ( 𝜑 → ( ‘ ( ‘ ( 𝐿𝐸 ) ) ) = ( 𝐿𝐸 ) )
41 1 38 2 3 5 6 12 29 lcfl5a ( 𝜑 → ( ( ‘ ( ‘ ( 𝐿𝐸 ) ) ) = ( 𝐿𝐸 ) ↔ ( 𝐿𝐸 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) )
42 40 41 mpbid ( 𝜑 → ( 𝐿𝐸 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
43 31 simp2d ( 𝜑 → ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) )
44 1 38 2 3 5 6 12 32 lcfl5a ( 𝜑 → ( ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ↔ ( 𝐿𝐺 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) )
45 43 44 mpbid ( 𝜑 → ( 𝐿𝐺 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
46 1 38 3 25 2 39 12 42 45 dochdmm1 ( 𝜑 → ( ‘ ( ( 𝐿𝐸 ) ∩ ( 𝐿𝐺 ) ) ) = ( ( ‘ ( 𝐿𝐸 ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ‘ ( 𝐿𝐺 ) ) ) )
47 eqid ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
48 25 5 6 26 29 lkrssv ( 𝜑 → ( 𝐿𝐸 ) ⊆ ( Base ‘ 𝑈 ) )
49 1 38 3 25 2 dochcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐿𝐸 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ‘ ( 𝐿𝐸 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
50 12 48 49 syl2anc ( 𝜑 → ( ‘ ( 𝐿𝐸 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
51 1 38 2 3 47 5 6 12 50 32 dochkrsm ( 𝜑 → ( ( ‘ ( 𝐿𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ‘ ( 𝐿𝐺 ) ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
52 1 3 25 4 2 dochlss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐿𝐸 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ‘ ( 𝐿𝐸 ) ) ∈ 𝑆 )
53 12 48 52 syl2anc ( 𝜑 → ( ‘ ( 𝐿𝐸 ) ) ∈ 𝑆 )
54 25 5 6 26 32 lkrssv ( 𝜑 → ( 𝐿𝐺 ) ⊆ ( Base ‘ 𝑈 ) )
55 1 3 25 4 2 dochlss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐿𝐺 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ‘ ( 𝐿𝐺 ) ) ∈ 𝑆 )
56 12 54 55 syl2anc ( 𝜑 → ( ‘ ( 𝐿𝐺 ) ) ∈ 𝑆 )
57 1 3 25 4 47 38 39 12 53 56 djhlsmcl ( 𝜑 → ( ( ( ‘ ( 𝐿𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ‘ ( 𝐿𝐺 ) ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ↔ ( ( ‘ ( 𝐿𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ‘ ( 𝐿𝐺 ) ) ) = ( ( ‘ ( 𝐿𝐸 ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ‘ ( 𝐿𝐺 ) ) ) ) )
58 51 57 mpbid ( 𝜑 → ( ( ‘ ( 𝐿𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ‘ ( 𝐿𝐺 ) ) ) = ( ( ‘ ( 𝐿𝐸 ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ‘ ( 𝐿𝐺 ) ) ) )
59 46 58 eqtr4d ( 𝜑 → ( ‘ ( ( 𝐿𝐸 ) ∩ ( 𝐿𝐺 ) ) ) = ( ( ‘ ( 𝐿𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ‘ ( 𝐿𝐺 ) ) ) )
60 28 simp3d ( 𝜑 → ( ‘ ( 𝐿𝐸 ) ) ⊆ 𝑄 )
61 31 simp3d ( 𝜑 → ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 )
62 4 lsssssubg ( 𝑈 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑈 ) )
63 26 62 syl ( 𝜑𝑆 ⊆ ( SubGrp ‘ 𝑈 ) )
64 63 53 sseldd ( 𝜑 → ( ‘ ( 𝐿𝐸 ) ) ∈ ( SubGrp ‘ 𝑈 ) )
65 63 56 sseldd ( 𝜑 → ( ‘ ( 𝐿𝐺 ) ) ∈ ( SubGrp ‘ 𝑈 ) )
66 63 13 sseldd ( 𝜑𝑄 ∈ ( SubGrp ‘ 𝑈 ) )
67 47 lsmlub ( ( ( ‘ ( 𝐿𝐸 ) ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( ‘ ( 𝐿𝐺 ) ) ∈ ( SubGrp ‘ 𝑈 ) ∧ 𝑄 ∈ ( SubGrp ‘ 𝑈 ) ) → ( ( ( ‘ ( 𝐿𝐸 ) ) ⊆ 𝑄 ∧ ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 ) ↔ ( ( ‘ ( 𝐿𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ‘ ( 𝐿𝐺 ) ) ) ⊆ 𝑄 ) )
68 64 65 66 67 syl3anc ( 𝜑 → ( ( ( ‘ ( 𝐿𝐸 ) ) ⊆ 𝑄 ∧ ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 ) ↔ ( ( ‘ ( 𝐿𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ‘ ( 𝐿𝐺 ) ) ) ⊆ 𝑄 ) )
69 60 61 68 mpbi2and ( 𝜑 → ( ( ‘ ( 𝐿𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ‘ ( 𝐿𝐺 ) ) ) ⊆ 𝑄 )
70 59 69 eqsstrd ( 𝜑 → ( ‘ ( ( 𝐿𝐸 ) ∩ ( 𝐿𝐺 ) ) ) ⊆ 𝑄 )
71 37 70 sstrd ( 𝜑 → ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ⊆ 𝑄 )
72 11 17 lcfls1c ( ( 𝐸 + 𝐺 ) ∈ 𝐶 ↔ ( ( 𝐸 + 𝐺 ) ∈ { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) } ∧ ( ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ⊆ 𝑄 ) )
73 24 71 72 sylanbrc ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐶 )