Metamath Proof Explorer

Theorem pjf2

Description: A projection is a function from the base set to the subspace. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses pjf.k 
|- K = ( proj ` W )
pjf.v 
|- V = ( Base ` W )
Assertion pjf2 
|- ( ( W e. PreHil /\ T e. dom K ) -> ( K ` T ) : V --> T )

Proof

Step Hyp Ref Expression
1 pjf.k 
 |-  K = ( proj ` W )
2 pjf.v 
 |-  V = ( Base ` W )
3 eqid 
 |-  ( +g ` W ) = ( +g ` W )
4 eqid 
 |-  ( LSSum ` W ) = ( LSSum ` W )
5 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
6 eqid 
 |-  ( Cntz ` W ) = ( Cntz ` W )
7 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
8 7 adantr 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> W e. LMod )
9 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
10 9 lsssssubg 
 |-  ( W e. LMod -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
11 8 10 syl 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
12 eqid 
 |-  ( ocv ` W ) = ( ocv ` W )
13 2 9 12 4 1 pjdm2 
 |-  ( W e. PreHil -> ( T e. dom K <-> ( T e. ( LSubSp ` W ) /\ ( T ( LSSum ` W ) ( ( ocv ` W ) ` T ) ) = V ) ) )
14 13 simprbda 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> T e. ( LSubSp ` W ) )
15 11 14 sseldd 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> T e. ( SubGrp ` W ) )
16 2 9 lssss 
 |-  ( T e. ( LSubSp ` W ) -> T C_ V )
17 14 16 syl 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> T C_ V )
18 2 12 9 ocvlss 
 |-  ( ( W e. PreHil /\ T C_ V ) -> ( ( ocv ` W ) ` T ) e. ( LSubSp ` W ) )
19 17 18 syldan 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( ( ocv ` W ) ` T ) e. ( LSubSp ` W ) )
20 11 19 sseldd 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( ( ocv ` W ) ` T ) e. ( SubGrp ` W ) )
21 12 9 5 ocvin 
 |-  ( ( W e. PreHil /\ T e. ( LSubSp ` W ) ) -> ( T i^i ( ( ocv ` W ) ` T ) ) = { ( 0g ` W ) } )
22 14 21 syldan 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( T i^i ( ( ocv ` W ) ` T ) ) = { ( 0g ` W ) } )
23 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
24 8 23 syl 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> W e. Abel )
25 6 24 15 20 ablcntzd 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> T C_ ( ( Cntz ` W ) ` ( ( ocv ` W ) ` T ) ) )
26 eqid 
 |-  ( proj1 ` W ) = ( proj1 ` W )
27 3 4 5 6 15 20 22 25 26 pj1f 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( T ( proj1 ` W ) ( ( ocv ` W ) ` T ) ) : ( T ( LSSum ` W ) ( ( ocv ` W ) ` T ) ) --> T )
28 12 26 1 pjval 
 |-  ( T e. dom K -> ( K ` T ) = ( T ( proj1 ` W ) ( ( ocv ` W ) ` T ) ) )
29 28 adantl 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( K ` T ) = ( T ( proj1 ` W ) ( ( ocv ` W ) ` T ) ) )
30 29 eqcomd 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( T ( proj1 ` W ) ( ( ocv ` W ) ` T ) ) = ( K ` T ) )
31 13 simplbda 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( T ( LSSum ` W ) ( ( ocv ` W ) ` T ) ) = V )
32 30 31 feq12d 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( ( T ( proj1 ` W ) ( ( ocv ` W ) ` T ) ) : ( T ( LSSum ` W ) ( ( ocv ` W ) ` T ) ) --> T <-> ( K ` T ) : V --> T ) )
33 27 32 mpbid 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( K ` T ) : V --> T )