Metamath Proof Explorer

Theorem pjfo

Description: A projection is a surjection onto the subspace. (Contributed by Mario Carneiro, 16-Oct-2015)

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

Proof

Step Hyp Ref Expression
1 pjf.k 
 |-  K = ( proj ` W )
2 pjf.v 
 |-  V = ( Base ` W )
3 1 2 pjf2 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( K ` T ) : V --> T )
4 3 frnd 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ran ( K ` T ) C_ T )
5 eqid 
 |-  ( ocv ` W ) = ( ocv ` W )
6 eqid 
 |-  ( proj1 ` W ) = ( proj1 ` W )
7 5 6 1 pjval 
 |-  ( T e. dom K -> ( K ` T ) = ( T ( proj1 ` W ) ( ( ocv ` W ) ` T ) ) )
8 7 ad2antlr 
 |-  ( ( ( W e. PreHil /\ T e. dom K ) /\ x e. T ) -> ( K ` T ) = ( T ( proj1 ` W ) ( ( ocv ` W ) ` T ) ) )
9 8 fveq1d 
 |-  ( ( ( W e. PreHil /\ T e. dom K ) /\ x e. T ) -> ( ( K ` T ) ` x ) = ( ( T ( proj1 ` W ) ( ( ocv ` W ) ` T ) ) ` x ) )
10 eqid 
 |-  ( +g ` W ) = ( +g ` W )
11 eqid 
 |-  ( LSSum ` W ) = ( LSSum ` W )
12 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
13 eqid 
 |-  ( Cntz ` W ) = ( Cntz ` W )
14 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
15 14 adantr 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> W e. LMod )
16 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
17 16 lsssssubg 
 |-  ( W e. LMod -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
18 15 17 syl 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
19 2 16 5 11 1 pjdm2 
 |-  ( W e. PreHil -> ( T e. dom K <-> ( T e. ( LSubSp ` W ) /\ ( T ( LSSum ` W ) ( ( ocv ` W ) ` T ) ) = V ) ) )
20 19 simprbda 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> T e. ( LSubSp ` W ) )
21 18 20 sseldd 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> T e. ( SubGrp ` W ) )
22 2 16 lssss 
 |-  ( T e. ( LSubSp ` W ) -> T C_ V )
23 20 22 syl 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> T C_ V )
24 2 5 16 ocvlss 
 |-  ( ( W e. PreHil /\ T C_ V ) -> ( ( ocv ` W ) ` T ) e. ( LSubSp ` W ) )
25 23 24 syldan 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( ( ocv ` W ) ` T ) e. ( LSubSp ` W ) )
26 18 25 sseldd 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( ( ocv ` W ) ` T ) e. ( SubGrp ` W ) )
27 5 16 12 ocvin 
 |-  ( ( W e. PreHil /\ T e. ( LSubSp ` W ) ) -> ( T i^i ( ( ocv ` W ) ` T ) ) = { ( 0g ` W ) } )
28 20 27 syldan 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( T i^i ( ( ocv ` W ) ` T ) ) = { ( 0g ` W ) } )
29 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
30 15 29 syl 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> W e. Abel )
31 13 30 21 26 ablcntzd 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> T C_ ( ( Cntz ` W ) ` ( ( ocv ` W ) ` T ) ) )
32 10 11 12 13 21 26 28 31 6 pj1lid 
 |-  ( ( ( W e. PreHil /\ T e. dom K ) /\ x e. T ) -> ( ( T ( proj1 ` W ) ( ( ocv ` W ) ` T ) ) ` x ) = x )
33 9 32 eqtrd 
 |-  ( ( ( W e. PreHil /\ T e. dom K ) /\ x e. T ) -> ( ( K ` T ) ` x ) = x )
34 3 ffnd 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( K ` T ) Fn V )
35 23 sselda 
 |-  ( ( ( W e. PreHil /\ T e. dom K ) /\ x e. T ) -> x e. V )
36 fnfvelrn 
 |-  ( ( ( K ` T ) Fn V /\ x e. V ) -> ( ( K ` T ) ` x ) e. ran ( K ` T ) )
37 34 35 36 syl2an2r 
 |-  ( ( ( W e. PreHil /\ T e. dom K ) /\ x e. T ) -> ( ( K ` T ) ` x ) e. ran ( K ` T ) )
38 33 37 eqeltrrd 
 |-  ( ( ( W e. PreHil /\ T e. dom K ) /\ x e. T ) -> x e. ran ( K ` T ) )
39 4 38 eqelssd 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ran ( K ` T ) = T )
40 dffo2 
 |-  ( ( K ` T ) : V -onto-> T <-> ( ( K ` T ) : V --> T /\ ran ( K ` T ) = T ) )
41 3 39 40 sylanbrc 
 |-  ( ( W e. PreHil /\ T e. dom K ) -> ( K ` T ) : V -onto-> T )