Metamath Proof Explorer

Theorem pj1lmhm

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 pj1lmhm 
|- ( ph -> ( T P U ) e. ( ( W |`s ( T .(+) U ) ) LMHom W ) )

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 eqid 
 |-  ( +g ` W ) = ( +g ` W )
10 eqid 
 |-  ( Cntz ` W ) = ( Cntz ` W )
11 1 lsssssubg 
 |-  ( W e. LMod -> L C_ ( SubGrp ` W ) )
12 5 11 syl 
 |-  ( ph -> L C_ ( SubGrp ` W ) )
13 12 6 sseldd 
 |-  ( ph -> T e. ( SubGrp ` W ) )
14 12 7 sseldd 
 |-  ( ph -> U e. ( SubGrp ` W ) )
15 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
16 5 15 syl 
 |-  ( ph -> W e. Abel )
17 10 16 13 14 ablcntzd 
 |-  ( ph -> T C_ ( ( Cntz ` W ) ` U ) )
18 9 2 3 10 13 14 8 17 4 pj1ghm 
 |-  ( ph -> ( T P U ) e. ( ( W |`s ( T .(+) U ) ) GrpHom W ) )
19 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
20 19 a1i 
 |-  ( ph -> ( Scalar ` W ) = ( Scalar ` W ) )
21 9 2 3 10 13 14 8 17 4 pj1id 
 |-  ( ( ph /\ y e. ( T .(+) U ) ) -> y = ( ( ( T P U ) ` y ) ( +g ` W ) ( ( U P T ) ` y ) ) )
22 21 adantrl 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> y = ( ( ( T P U ) ` y ) ( +g ` W ) ( ( U P T ) ` y ) ) )
23 22 oveq2d 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( x ( .s ` W ) y ) = ( x ( .s ` W ) ( ( ( T P U ) ` y ) ( +g ` W ) ( ( U P T ) ` y ) ) ) )
24 5 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> W e. LMod )
25 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> x e. ( Base ` ( Scalar ` W ) ) )
26 6 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> T e. L )
27 eqid 
 |-  ( Base ` W ) = ( Base ` W )
28 27 1 lssss 
 |-  ( T e. L -> T C_ ( Base ` W ) )
29 26 28 syl 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> T C_ ( Base ` W ) )
30 13 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> T e. ( SubGrp ` W ) )
31 14 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> U e. ( SubGrp ` W ) )
32 8 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( T i^i U ) = { .0. } )
33 17 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> T C_ ( ( Cntz ` W ) ` U ) )
34 9 2 3 10 30 31 32 33 4 pj1f 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( T P U ) : ( T .(+) U ) --> T )
35 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> y e. ( T .(+) U ) )
36 34 35 ffvelcdmd 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( ( T P U ) ` y ) e. T )
37 29 36 sseldd 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( ( T P U ) ` y ) e. ( Base ` W ) )
38 7 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> U e. L )
39 27 1 lssss 
 |-  ( U e. L -> U C_ ( Base ` W ) )
40 38 39 syl 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> U C_ ( Base ` W ) )
41 9 2 3 10 30 31 32 33 4 pj2f 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( U P T ) : ( T .(+) U ) --> U )
42 41 35 ffvelcdmd 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( ( U P T ) ` y ) e. U )
43 40 42 sseldd 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( ( U P T ) ` y ) e. ( Base ` W ) )
44 eqid 
 |-  ( .s ` W ) = ( .s ` W )
45 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
46 27 9 19 44 45 lmodvsdi 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ ( ( T P U ) ` y ) e. ( Base ` W ) /\ ( ( U P T ) ` y ) e. ( Base ` W ) ) ) -> ( x ( .s ` W ) ( ( ( T P U ) ` y ) ( +g ` W ) ( ( U P T ) ` y ) ) ) = ( ( x ( .s ` W ) ( ( T P U ) ` y ) ) ( +g ` W ) ( x ( .s ` W ) ( ( U P T ) ` y ) ) ) )
47 24 25 37 43 46 syl13anc 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( x ( .s ` W ) ( ( ( T P U ) ` y ) ( +g ` W ) ( ( U P T ) ` y ) ) ) = ( ( x ( .s ` W ) ( ( T P U ) ` y ) ) ( +g ` W ) ( x ( .s ` W ) ( ( U P T ) ` y ) ) ) )
48 23 47 eqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( x ( .s ` W ) y ) = ( ( x ( .s ` W ) ( ( T P U ) ` y ) ) ( +g ` W ) ( x ( .s ` W ) ( ( U P T ) ` y ) ) ) )
49 1 2 lsmcl 
 |-  ( ( W e. LMod /\ T e. L /\ U e. L ) -> ( T .(+) U ) e. L )
50 5 6 7 49 syl3anc 
 |-  ( ph -> ( T .(+) U ) e. L )
51 50 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( T .(+) U ) e. L )
52 19 44 45 1 lssvscl 
 |-  ( ( ( W e. LMod /\ ( T .(+) U ) e. L ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( x ( .s ` W ) y ) e. ( T .(+) U ) )
53 24 51 25 35 52 syl22anc 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( x ( .s ` W ) y ) e. ( T .(+) U ) )
54 19 44 45 1 lssvscl 
 |-  ( ( ( W e. LMod /\ T e. L ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ ( ( T P U ) ` y ) e. T ) ) -> ( x ( .s ` W ) ( ( T P U ) ` y ) ) e. T )
55 24 26 25 36 54 syl22anc 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( x ( .s ` W ) ( ( T P U ) ` y ) ) e. T )
56 19 44 45 1 lssvscl 
 |-  ( ( ( W e. LMod /\ U e. L ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ ( ( U P T ) ` y ) e. U ) ) -> ( x ( .s ` W ) ( ( U P T ) ` y ) ) e. U )
57 24 38 25 42 56 syl22anc 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( x ( .s ` W ) ( ( U P T ) ` y ) ) e. U )
58 9 2 3 10 30 31 32 33 4 53 55 57 pj1eq 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( ( x ( .s ` W ) y ) = ( ( x ( .s ` W ) ( ( T P U ) ` y ) ) ( +g ` W ) ( x ( .s ` W ) ( ( U P T ) ` y ) ) ) <-> ( ( ( T P U ) ` ( x ( .s ` W ) y ) ) = ( x ( .s ` W ) ( ( T P U ) ` y ) ) /\ ( ( U P T ) ` ( x ( .s ` W ) y ) ) = ( x ( .s ` W ) ( ( U P T ) ` y ) ) ) ) )
59 48 58 mpbid 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( ( ( T P U ) ` ( x ( .s ` W ) y ) ) = ( x ( .s ` W ) ( ( T P U ) ` y ) ) /\ ( ( U P T ) ` ( x ( .s ` W ) y ) ) = ( x ( .s ` W ) ( ( U P T ) ` y ) ) ) )
60 59 simpld 
 |-  ( ( ph /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ y e. ( T .(+) U ) ) ) -> ( ( T P U ) ` ( x ( .s ` W ) y ) ) = ( x ( .s ` W ) ( ( T P U ) ` y ) ) )
61 60 ralrimivva 
 |-  ( ph -> A. x e. ( Base ` ( Scalar ` W ) ) A. y e. ( T .(+) U ) ( ( T P U ) ` ( x ( .s ` W ) y ) ) = ( x ( .s ` W ) ( ( T P U ) ` y ) ) )
62 12 50 sseldd 
 |-  ( ph -> ( T .(+) U ) e. ( SubGrp ` W ) )
63 eqid 
 |-  ( W |`s ( T .(+) U ) ) = ( W |`s ( T .(+) U ) )
64 63 subgbas 
 |-  ( ( T .(+) U ) e. ( SubGrp ` W ) -> ( T .(+) U ) = ( Base ` ( W |`s ( T .(+) U ) ) ) )
65 62 64 syl 
 |-  ( ph -> ( T .(+) U ) = ( Base ` ( W |`s ( T .(+) U ) ) ) )
66 65 raleqdv 
 |-  ( ph -> ( A. y e. ( T .(+) U ) ( ( T P U ) ` ( x ( .s ` W ) y ) ) = ( x ( .s ` W ) ( ( T P U ) ` y ) ) <-> A. y e. ( Base ` ( W |`s ( T .(+) U ) ) ) ( ( T P U ) ` ( x ( .s ` W ) y ) ) = ( x ( .s ` W ) ( ( T P U ) ` y ) ) ) )
67 66 ralbidv 
 |-  ( ph -> ( A. x e. ( Base ` ( Scalar ` W ) ) A. y e. ( T .(+) U ) ( ( T P U ) ` ( x ( .s ` W ) y ) ) = ( x ( .s ` W ) ( ( T P U ) ` y ) ) <-> A. x e. ( Base ` ( Scalar ` W ) ) A. y e. ( Base ` ( W |`s ( T .(+) U ) ) ) ( ( T P U ) ` ( x ( .s ` W ) y ) ) = ( x ( .s ` W ) ( ( T P U ) ` y ) ) ) )
68 61 67 mpbid 
 |-  ( ph -> A. x e. ( Base ` ( Scalar ` W ) ) A. y e. ( Base ` ( W |`s ( T .(+) U ) ) ) ( ( T P U ) ` ( x ( .s ` W ) y ) ) = ( x ( .s ` W ) ( ( T P U ) ` y ) ) )
69 63 1 lsslmod 
 |-  ( ( W e. LMod /\ ( T .(+) U ) e. L ) -> ( W |`s ( T .(+) U ) ) e. LMod )
70 5 50 69 syl2anc 
 |-  ( ph -> ( W |`s ( T .(+) U ) ) e. LMod )
71 ovex 
 |-  ( T .(+) U ) e. _V
72 63 19 resssca 
 |-  ( ( T .(+) U ) e. _V -> ( Scalar ` W ) = ( Scalar ` ( W |`s ( T .(+) U ) ) ) )
73 71 72 ax-mp 
 |-  ( Scalar ` W ) = ( Scalar ` ( W |`s ( T .(+) U ) ) )
74 eqid 
 |-  ( Base ` ( W |`s ( T .(+) U ) ) ) = ( Base ` ( W |`s ( T .(+) U ) ) )
75 63 44 ressvsca 
 |-  ( ( T .(+) U ) e. _V -> ( .s ` W ) = ( .s ` ( W |`s ( T .(+) U ) ) ) )
76 71 75 ax-mp 
 |-  ( .s ` W ) = ( .s ` ( W |`s ( T .(+) U ) ) )
77 73 19 45 74 76 44 islmhm3 
 |-  ( ( ( W |`s ( T .(+) U ) ) e. LMod /\ W e. LMod ) -> ( ( T P U ) e. ( ( W |`s ( T .(+) U ) ) LMHom W ) <-> ( ( T P U ) e. ( ( W |`s ( T .(+) U ) ) GrpHom W ) /\ ( Scalar ` W ) = ( Scalar ` W ) /\ A. x e. ( Base ` ( Scalar ` W ) ) A. y e. ( Base ` ( W |`s ( T .(+) U ) ) ) ( ( T P U ) ` ( x ( .s ` W ) y ) ) = ( x ( .s ` W ) ( ( T P U ) ` y ) ) ) ) )
78 70 5 77 syl2anc 
 |-  ( ph -> ( ( T P U ) e. ( ( W |`s ( T .(+) U ) ) LMHom W ) <-> ( ( T P U ) e. ( ( W |`s ( T .(+) U ) ) GrpHom W ) /\ ( Scalar ` W ) = ( Scalar ` W ) /\ A. x e. ( Base ` ( Scalar ` W ) ) A. y e. ( Base ` ( W |`s ( T .(+) U ) ) ) ( ( T P U ) ` ( x ( .s ` W ) y ) ) = ( x ( .s ` W ) ( ( T P U ) ` y ) ) ) ) )
79 18 20 68 78 mpbir3and 
 |-  ( ph -> ( T P U ) e. ( ( W |`s ( T .(+) U ) ) LMHom W ) )