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 H = LHyp K
lclkrslem1.o ˙ = ocH K W
lclkrslem1.u U = DVecH K W
lclkrslem1.s S = LSubSp U
lclkrslem1.f F = LFnl U
lclkrslem1.l L = LKer U
lclkrslem1.d D = LDual U
lclkrslem1.r R = Scalar U
lclkrslem1.b B = Base R
lclkrslem1.t · ˙ = D
lclkrslem1.c C = f F | ˙ ˙ L f = L f ˙ L f Q
lclkrslem1.k φ K HL W H
lclkrslem1.q φ Q S
lclkrslem1.g φ G C
lclkrslem2.p + ˙ = + D
lclkrslem2.e φ E C
Assertion lclkrslem2 φ E + ˙ G C

Proof

Step Hyp Ref Expression
1 lclkrslem1.h H = LHyp K
2 lclkrslem1.o ˙ = ocH K W
3 lclkrslem1.u U = DVecH K W
4 lclkrslem1.s S = LSubSp U
5 lclkrslem1.f F = LFnl U
6 lclkrslem1.l L = LKer U
7 lclkrslem1.d D = LDual U
8 lclkrslem1.r R = Scalar U
9 lclkrslem1.b B = Base R
10 lclkrslem1.t · ˙ = D
11 lclkrslem1.c C = f F | ˙ ˙ L f = L f ˙ L f Q
12 lclkrslem1.k φ K HL W H
13 lclkrslem1.q φ Q S
14 lclkrslem1.g φ G C
15 lclkrslem2.p + ˙ = + D
16 lclkrslem2.e φ E C
17 eqid f F | ˙ ˙ L f = L f = f F | ˙ ˙ L f = L f
18 11 17 lcfls1c E C E f F | ˙ ˙ L f = L f ˙ L E Q
19 18 simplbi E C E f F | ˙ ˙ L f = L f
20 16 19 syl φ E f F | ˙ ˙ L f = L f
21 11 17 lcfls1c G C G f F | ˙ ˙ L f = L f ˙ L G Q
22 21 simplbi G C G f F | ˙ ˙ L f = L f
23 14 22 syl φ G f F | ˙ ˙ L f = L f
24 1 2 3 5 6 7 15 17 12 20 23 lclkrlem2 φ E + ˙ G f F | ˙ ˙ L f = L f
25 eqid Base U = Base U
26 1 3 12 dvhlmod φ U LMod
27 11 lcfls1lem E C E F ˙ ˙ L E = L E ˙ L E Q
28 16 27 sylib φ E F ˙ ˙ L E = L E ˙ L E Q
29 28 simp1d φ E F
30 11 lcfls1lem G C G F ˙ ˙ L G = L G ˙ L G Q
31 14 30 sylib φ G F ˙ ˙ L G = L G ˙ L G Q
32 31 simp1d φ G F
33 5 7 15 26 29 32 ldualvaddcl φ E + ˙ G F
34 25 5 6 26 33 lkrssv φ L E + ˙ G Base U
35 5 6 7 15 26 29 32 lkrin φ L E L G L E + ˙ G
36 1 3 25 2 dochss K HL W H L E + ˙ G Base U L E L G L E + ˙ G ˙ L E + ˙ G ˙ L E L G
37 12 34 35 36 syl3anc φ ˙ L E + ˙ G ˙ L E L G
38 eqid DIsoH K W = DIsoH K W
39 eqid joinH K W = joinH K W
40 28 simp2d φ ˙ ˙ L E = L E
41 1 38 2 3 5 6 12 29 lcfl5a φ ˙ ˙ L E = L E L E ran DIsoH K W
42 40 41 mpbid φ L E ran DIsoH K W
43 31 simp2d φ ˙ ˙ L G = L G
44 1 38 2 3 5 6 12 32 lcfl5a φ ˙ ˙ L G = L G L G ran DIsoH K W
45 43 44 mpbid φ L G ran DIsoH K W
46 1 38 3 25 2 39 12 42 45 dochdmm1 φ ˙ L E L G = ˙ L E joinH K W ˙ L G
47 eqid LSSum U = LSSum U
48 25 5 6 26 29 lkrssv φ L E Base U
49 1 38 3 25 2 dochcl K HL W H L E Base U ˙ L E ran DIsoH K W
50 12 48 49 syl2anc φ ˙ L E ran DIsoH K W
51 1 38 2 3 47 5 6 12 50 32 dochkrsm φ ˙ L E LSSum U ˙ L G ran DIsoH K W
52 1 3 25 4 2 dochlss K HL W H L E Base U ˙ L E S
53 12 48 52 syl2anc φ ˙ L E S
54 25 5 6 26 32 lkrssv φ L G Base U
55 1 3 25 4 2 dochlss K HL W H L G Base U ˙ L G S
56 12 54 55 syl2anc φ ˙ L G S
57 1 3 25 4 47 38 39 12 53 56 djhlsmcl φ ˙ L E LSSum U ˙ L G ran DIsoH K W ˙ L E LSSum U ˙ L G = ˙ L E joinH K W ˙ L G
58 51 57 mpbid φ ˙ L E LSSum U ˙ L G = ˙ L E joinH K W ˙ L G
59 46 58 eqtr4d φ ˙ L E L G = ˙ L E LSSum U ˙ L G
60 28 simp3d φ ˙ L E Q
61 31 simp3d φ ˙ L G Q
62 4 lsssssubg U LMod S SubGrp U
63 26 62 syl φ S SubGrp U
64 63 53 sseldd φ ˙ L E SubGrp U
65 63 56 sseldd φ ˙ L G SubGrp U
66 63 13 sseldd φ Q SubGrp U
67 47 lsmlub ˙ L E SubGrp U ˙ L G SubGrp U Q SubGrp U ˙ L E Q ˙ L G Q ˙ L E LSSum U ˙ L G Q
68 64 65 66 67 syl3anc φ ˙ L E Q ˙ L G Q ˙ L E LSSum U ˙ L G Q
69 60 61 68 mpbi2and φ ˙ L E LSSum U ˙ L G Q
70 59 69 eqsstrd φ ˙ L E L G Q
71 37 70 sstrd φ ˙ L E + ˙ G Q
72 11 17 lcfls1c E + ˙ G C E + ˙ G f F | ˙ ˙ L f = L f ˙ L E + ˙ G Q
73 24 71 72 sylanbrc φ E + ˙ G C