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 
|- .x. = ( .s ` D )
lclkrslem1.c 
|- C = { f e. F | ( ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) /\ ( ._|_ ` ( L ` f ) ) C_ Q ) }
lclkrslem1.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lclkrslem1.q 
|- ( ph -> Q e. S )
lclkrslem1.g 
|- ( ph -> G e. C )
lclkrslem2.p 
|- .+ = ( +g ` D )
lclkrslem2.e 
|- ( ph -> E e. C )
Assertion lclkrslem2 
|- ( ph -> ( E .+ G ) e. 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 
 |-  .x. = ( .s ` D )
11 lclkrslem1.c 
 |-  C = { f e. F | ( ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) /\ ( ._|_ ` ( L ` f ) ) C_ Q ) }
12 lclkrslem1.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
13 lclkrslem1.q 
 |-  ( ph -> Q e. S )
14 lclkrslem1.g 
 |-  ( ph -> G e. C )
15 lclkrslem2.p 
 |-  .+ = ( +g ` D )
16 lclkrslem2.e 
 |-  ( ph -> E e. C )
17 eqid 
 |-  { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
18 11 17 lcfls1c 
 |-  ( E e. C <-> ( E e. { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } /\ ( ._|_ ` ( L ` E ) ) C_ Q ) )
19 18 simplbi 
 |-  ( E e. C -> E e. { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )
20 16 19 syl 
 |-  ( ph -> E e. { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )
21 11 17 lcfls1c 
 |-  ( G e. C <-> ( G e. { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } /\ ( ._|_ ` ( L ` G ) ) C_ Q ) )
22 21 simplbi 
 |-  ( G e. C -> G e. { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )
23 14 22 syl 
 |-  ( ph -> G e. { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )
24 1 2 3 5 6 7 15 17 12 20 23 lclkrlem2 
 |-  ( ph -> ( E .+ G ) e. { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } )
25 eqid 
 |-  ( Base ` U ) = ( Base ` U )
26 1 3 12 dvhlmod 
 |-  ( ph -> U e. LMod )
27 11 lcfls1lem 
 |-  ( E e. C <-> ( E e. F /\ ( ._|_ ` ( ._|_ ` ( L ` E ) ) ) = ( L ` E ) /\ ( ._|_ ` ( L ` E ) ) C_ Q ) )
28 16 27 sylib 
 |-  ( ph -> ( E e. F /\ ( ._|_ ` ( ._|_ ` ( L ` E ) ) ) = ( L ` E ) /\ ( ._|_ ` ( L ` E ) ) C_ Q ) )
29 28 simp1d 
 |-  ( ph -> E e. F )
30 11 lcfls1lem 
 |-  ( G e. C <-> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) /\ ( ._|_ ` ( L ` G ) ) C_ Q ) )
31 14 30 sylib 
 |-  ( ph -> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) /\ ( ._|_ ` ( L ` G ) ) C_ Q ) )
32 31 simp1d 
 |-  ( ph -> G e. F )
33 5 7 15 26 29 32 ldualvaddcl 
 |-  ( ph -> ( E .+ G ) e. F )
34 25 5 6 26 33 lkrssv 
 |-  ( ph -> ( L ` ( E .+ G ) ) C_ ( Base ` U ) )
35 5 6 7 15 26 29 32 lkrin 
 |-  ( ph -> ( ( L ` E ) i^i ( L ` G ) ) C_ ( L ` ( E .+ G ) ) )
36 1 3 25 2 dochss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` ( E .+ G ) ) C_ ( Base ` U ) /\ ( ( L ` E ) i^i ( L ` G ) ) C_ ( L ` ( E .+ G ) ) ) -> ( ._|_ ` ( L ` ( E .+ G ) ) ) C_ ( ._|_ ` ( ( L ` E ) i^i ( L ` G ) ) ) )
37 12 34 35 36 syl3anc 
 |-  ( ph -> ( ._|_ ` ( L ` ( E .+ G ) ) ) C_ ( ._|_ ` ( ( L ` E ) i^i ( L ` G ) ) ) )
38 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
39 eqid 
 |-  ( ( joinH ` K ) ` W ) = ( ( joinH ` K ) ` W )
40 28 simp2d 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` E ) ) ) = ( L ` E ) )
41 1 38 2 3 5 6 12 29 lcfl5a 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` E ) ) ) = ( L ` E ) <-> ( L ` E ) e. ran ( ( DIsoH ` K ) ` W ) ) )
42 40 41 mpbid 
 |-  ( ph -> ( L ` E ) e. ran ( ( DIsoH ` K ) ` W ) )
43 31 simp2d 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
44 1 38 2 3 5 6 12 32 lcfl5a 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) <-> ( L ` G ) e. ran ( ( DIsoH ` K ) ` W ) ) )
45 43 44 mpbid 
 |-  ( ph -> ( L ` G ) e. ran ( ( DIsoH ` K ) ` W ) )
46 1 38 3 25 2 39 12 42 45 dochdmm1 
 |-  ( ph -> ( ._|_ ` ( ( L ` E ) i^i ( L ` G ) ) ) = ( ( ._|_ ` ( L ` E ) ) ( ( joinH ` K ) ` W ) ( ._|_ ` ( L ` G ) ) ) )
47 eqid 
 |-  ( LSSum ` U ) = ( LSSum ` U )
48 25 5 6 26 29 lkrssv 
 |-  ( ph -> ( L ` E ) C_ ( Base ` U ) )
49 1 38 3 25 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` E ) C_ ( Base ` U ) ) -> ( ._|_ ` ( L ` E ) ) e. ran ( ( DIsoH ` K ) ` W ) )
50 12 48 49 syl2anc 
 |-  ( ph -> ( ._|_ ` ( L ` E ) ) e. ran ( ( DIsoH ` K ) ` W ) )
51 1 38 2 3 47 5 6 12 50 32 dochkrsm 
 |-  ( ph -> ( ( ._|_ ` ( L ` E ) ) ( LSSum ` U ) ( ._|_ ` ( L ` G ) ) ) e. ran ( ( DIsoH ` K ) ` W ) )
52 1 3 25 4 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` E ) C_ ( Base ` U ) ) -> ( ._|_ ` ( L ` E ) ) e. S )
53 12 48 52 syl2anc 
 |-  ( ph -> ( ._|_ ` ( L ` E ) ) e. S )
54 25 5 6 26 32 lkrssv 
 |-  ( ph -> ( L ` G ) C_ ( Base ` U ) )
55 1 3 25 4 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` G ) C_ ( Base ` U ) ) -> ( ._|_ ` ( L ` G ) ) e. S )
56 12 54 55 syl2anc 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) e. S )
57 1 3 25 4 47 38 39 12 53 56 djhlsmcl 
 |-  ( ph -> ( ( ( ._|_ ` ( L ` E ) ) ( LSSum ` U ) ( ._|_ ` ( L ` G ) ) ) e. ran ( ( DIsoH ` K ) ` W ) <-> ( ( ._|_ ` ( L ` E ) ) ( LSSum ` U ) ( ._|_ ` ( L ` G ) ) ) = ( ( ._|_ ` ( L ` E ) ) ( ( joinH ` K ) ` W ) ( ._|_ ` ( L ` G ) ) ) ) )
58 51 57 mpbid 
 |-  ( ph -> ( ( ._|_ ` ( L ` E ) ) ( LSSum ` U ) ( ._|_ ` ( L ` G ) ) ) = ( ( ._|_ ` ( L ` E ) ) ( ( joinH ` K ) ` W ) ( ._|_ ` ( L ` G ) ) ) )
59 46 58 eqtr4d 
 |-  ( ph -> ( ._|_ ` ( ( L ` E ) i^i ( L ` G ) ) ) = ( ( ._|_ ` ( L ` E ) ) ( LSSum ` U ) ( ._|_ ` ( L ` G ) ) ) )
60 28 simp3d 
 |-  ( ph -> ( ._|_ ` ( L ` E ) ) C_ Q )
61 31 simp3d 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) C_ Q )
62 4 lsssssubg 
 |-  ( U e. LMod -> S C_ ( SubGrp ` U ) )
63 26 62 syl 
 |-  ( ph -> S C_ ( SubGrp ` U ) )
64 63 53 sseldd 
 |-  ( ph -> ( ._|_ ` ( L ` E ) ) e. ( SubGrp ` U ) )
65 63 56 sseldd 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) e. ( SubGrp ` U ) )
66 63 13 sseldd 
 |-  ( ph -> Q e. ( SubGrp ` U ) )
67 47 lsmlub 
 |-  ( ( ( ._|_ ` ( L ` E ) ) e. ( SubGrp ` U ) /\ ( ._|_ ` ( L ` G ) ) e. ( SubGrp ` U ) /\ Q e. ( SubGrp ` U ) ) -> ( ( ( ._|_ ` ( L ` E ) ) C_ Q /\ ( ._|_ ` ( L ` G ) ) C_ Q ) <-> ( ( ._|_ ` ( L ` E ) ) ( LSSum ` U ) ( ._|_ ` ( L ` G ) ) ) C_ Q ) )
68 64 65 66 67 syl3anc 
 |-  ( ph -> ( ( ( ._|_ ` ( L ` E ) ) C_ Q /\ ( ._|_ ` ( L ` G ) ) C_ Q ) <-> ( ( ._|_ ` ( L ` E ) ) ( LSSum ` U ) ( ._|_ ` ( L ` G ) ) ) C_ Q ) )
69 60 61 68 mpbi2and 
 |-  ( ph -> ( ( ._|_ ` ( L ` E ) ) ( LSSum ` U ) ( ._|_ ` ( L ` G ) ) ) C_ Q )
70 59 69 eqsstrd 
 |-  ( ph -> ( ._|_ ` ( ( L ` E ) i^i ( L ` G ) ) ) C_ Q )
71 37 70 sstrd 
 |-  ( ph -> ( ._|_ ` ( L ` ( E .+ G ) ) ) C_ Q )
72 11 17 lcfls1c 
 |-  ( ( E .+ G ) e. C <-> ( ( E .+ G ) e. { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } /\ ( ._|_ ` ( L ` ( E .+ G ) ) ) C_ Q ) )
73 24 71 72 sylanbrc 
 |-  ( ph -> ( E .+ G ) e. C )