Metamath Proof Explorer

Theorem pj1lmhm2

Description: The left projection function is a linear operator. (Contributed by Mario Carneiro, 15-Oct-2015) (Revised by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses pj1lmhm.l 
|- L = ( LSubSp ` W )
pj1lmhm.s 
|- .(+) = ( LSSum ` W )
pj1lmhm.z 
|- .0. = ( 0g ` W )
pj1lmhm.p 
|- P = ( proj1 ` W )
pj1lmhm.1 
|- ( ph -> W e. LMod )
pj1lmhm.2 
|- ( ph -> T e. L )
pj1lmhm.3 
|- ( ph -> U e. L )
pj1lmhm.4 
|- ( ph -> ( T i^i U ) = { .0. } )
Assertion pj1lmhm2 
|- ( ph -> ( T P U ) e. ( ( W |`s ( T .(+) U ) ) LMHom ( W |`s T ) ) )

Proof

Step Hyp Ref Expression
1 pj1lmhm.l 
 |-  L = ( LSubSp ` W )
2 pj1lmhm.s 
 |-  .(+) = ( LSSum ` W )
3 pj1lmhm.z 
 |-  .0. = ( 0g ` W )
4 pj1lmhm.p 
 |-  P = ( proj1 ` W )
5 pj1lmhm.1 
 |-  ( ph -> W e. LMod )
6 pj1lmhm.2 
 |-  ( ph -> T e. L )
7 pj1lmhm.3 
 |-  ( ph -> U e. L )
8 pj1lmhm.4 
 |-  ( ph -> ( T i^i U ) = { .0. } )
9 1 2 3 4 5 6 7 8 pj1lmhm 
 |-  ( ph -> ( T P U ) e. ( ( W |`s ( T .(+) U ) ) LMHom W ) )
10 eqid 
 |-  ( +g ` W ) = ( +g ` W )
11 eqid 
 |-  ( Cntz ` W ) = ( Cntz ` W )
12 1 lsssssubg 
 |-  ( W e. LMod -> L C_ ( SubGrp ` W ) )
13 5 12 syl 
 |-  ( ph -> L C_ ( SubGrp ` W ) )
14 13 6 sseldd 
 |-  ( ph -> T e. ( SubGrp ` W ) )
15 13 7 sseldd 
 |-  ( ph -> U e. ( SubGrp ` W ) )
16 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
17 5 16 syl 
 |-  ( ph -> W e. Abel )
18 11 17 14 15 ablcntzd 
 |-  ( ph -> T C_ ( ( Cntz ` W ) ` U ) )
19 10 2 3 11 14 15 8 18 4 pj1f 
 |-  ( ph -> ( T P U ) : ( T .(+) U ) --> T )
20 19 frnd 
 |-  ( ph -> ran ( T P U ) C_ T )
21 eqid 
 |-  ( W |`s T ) = ( W |`s T )
22 21 1 reslmhm2b 
 |-  ( ( W e. LMod /\ T e. L /\ ran ( T P U ) C_ T ) -> ( ( T P U ) e. ( ( W |`s ( T .(+) U ) ) LMHom W ) <-> ( T P U ) e. ( ( W |`s ( T .(+) U ) ) LMHom ( W |`s T ) ) ) )
23 5 6 20 22 syl3anc 
 |-  ( ph -> ( ( T P U ) e. ( ( W |`s ( T .(+) U ) ) LMHom W ) <-> ( T P U ) e. ( ( W |`s ( T .(+) U ) ) LMHom ( W |`s T ) ) ) )
24 9 23 mpbid 
 |-  ( ph -> ( T P U ) e. ( ( W |`s ( T .(+) U ) ) LMHom ( W |`s T ) ) )