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 ) )