Metamath Proof Explorer

Theorem pjff

Description: A projection is a linear operator. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypothesis pjf.k 
|- K = ( proj ` W )
Assertion pjff 
|- ( W e. PreHil -> K : dom K --> ( W LMHom W ) )

Proof

Step Hyp Ref Expression
1 pjf.k 
 |-  K = ( proj ` W )
2 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
3 eqid 
 |-  ( LSSum ` W ) = ( LSSum ` W )
4 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
5 eqid 
 |-  ( proj1 ` W ) = ( proj1 ` W )
6 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
7 6 adantr 
 |-  ( ( W e. PreHil /\ x e. dom K ) -> W e. LMod )
8 eqid 
 |-  ( Base ` W ) = ( Base ` W )
9 eqid 
 |-  ( ocv ` W ) = ( ocv ` W )
10 8 2 9 3 1 pjdm2 
 |-  ( W e. PreHil -> ( x e. dom K <-> ( x e. ( LSubSp ` W ) /\ ( x ( LSSum ` W ) ( ( ocv ` W ) ` x ) ) = ( Base ` W ) ) ) )
11 10 simprbda 
 |-  ( ( W e. PreHil /\ x e. dom K ) -> x e. ( LSubSp ` W ) )
12 8 2 lssss 
 |-  ( x e. ( LSubSp ` W ) -> x C_ ( Base ` W ) )
13 11 12 syl 
 |-  ( ( W e. PreHil /\ x e. dom K ) -> x C_ ( Base ` W ) )
14 8 9 2 ocvlss 
 |-  ( ( W e. PreHil /\ x C_ ( Base ` W ) ) -> ( ( ocv ` W ) ` x ) e. ( LSubSp ` W ) )
15 13 14 syldan 
 |-  ( ( W e. PreHil /\ x e. dom K ) -> ( ( ocv ` W ) ` x ) e. ( LSubSp ` W ) )
16 9 2 4 ocvin 
 |-  ( ( W e. PreHil /\ x e. ( LSubSp ` W ) ) -> ( x i^i ( ( ocv ` W ) ` x ) ) = { ( 0g ` W ) } )
17 11 16 syldan 
 |-  ( ( W e. PreHil /\ x e. dom K ) -> ( x i^i ( ( ocv ` W ) ` x ) ) = { ( 0g ` W ) } )
18 2 3 4 5 7 11 15 17 pj1lmhm 
 |-  ( ( W e. PreHil /\ x e. dom K ) -> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) e. ( ( W |`s ( x ( LSSum ` W ) ( ( ocv ` W ) ` x ) ) ) LMHom W ) )
19 10 simplbda 
 |-  ( ( W e. PreHil /\ x e. dom K ) -> ( x ( LSSum ` W ) ( ( ocv ` W ) ` x ) ) = ( Base ` W ) )
20 19 oveq2d 
 |-  ( ( W e. PreHil /\ x e. dom K ) -> ( W |`s ( x ( LSSum ` W ) ( ( ocv ` W ) ` x ) ) ) = ( W |`s ( Base ` W ) ) )
21 8 ressid 
 |-  ( W e. PreHil -> ( W |`s ( Base ` W ) ) = W )
22 21 adantr 
 |-  ( ( W e. PreHil /\ x e. dom K ) -> ( W |`s ( Base ` W ) ) = W )
23 20 22 eqtrd 
 |-  ( ( W e. PreHil /\ x e. dom K ) -> ( W |`s ( x ( LSSum ` W ) ( ( ocv ` W ) ` x ) ) ) = W )
24 23 oveq1d 
 |-  ( ( W e. PreHil /\ x e. dom K ) -> ( ( W |`s ( x ( LSSum ` W ) ( ( ocv ` W ) ` x ) ) ) LMHom W ) = ( W LMHom W ) )
25 18 24 eleqtrd 
 |-  ( ( W e. PreHil /\ x e. dom K ) -> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) e. ( W LMHom W ) )
26 9 5 1 pjfval2 
 |-  K = ( x e. dom K |-> ( x ( proj1 ` W ) ( ( ocv ` W ) ` x ) ) )
27 25 26 fmptd 
 |-  ( W e. PreHil -> K : dom K --> ( W LMHom W ) )