Metamath Proof Explorer

Theorem pj1ghm2

Description: The left projection function is a group homomorphism. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses pj1eu.a 
|- .+ = ( +g ` G )
pj1eu.s 
|- .(+) = ( LSSum ` G )
pj1eu.o 
|- .0. = ( 0g ` G )
pj1eu.z 
|- Z = ( Cntz ` G )
pj1eu.2 
|- ( ph -> T e. ( SubGrp ` G ) )
pj1eu.3 
|- ( ph -> U e. ( SubGrp ` G ) )
pj1eu.4 
|- ( ph -> ( T i^i U ) = { .0. } )
pj1eu.5 
|- ( ph -> T C_ ( Z ` U ) )
pj1f.p 
|- P = ( proj1 ` G )
Assertion pj1ghm2 
|- ( ph -> ( T P U ) e. ( ( G |`s ( T .(+) U ) ) GrpHom ( G |`s T ) ) )

Proof

Step Hyp Ref Expression
1 pj1eu.a 
 |-  .+ = ( +g ` G )
2 pj1eu.s 
 |-  .(+) = ( LSSum ` G )
3 pj1eu.o 
 |-  .0. = ( 0g ` G )
4 pj1eu.z 
 |-  Z = ( Cntz ` G )
5 pj1eu.2 
 |-  ( ph -> T e. ( SubGrp ` G ) )
6 pj1eu.3 
 |-  ( ph -> U e. ( SubGrp ` G ) )
7 pj1eu.4 
 |-  ( ph -> ( T i^i U ) = { .0. } )
8 pj1eu.5 
 |-  ( ph -> T C_ ( Z ` U ) )
9 pj1f.p 
 |-  P = ( proj1 ` G )
10 1 2 3 4 5 6 7 8 9 pj1ghm 
 |-  ( ph -> ( T P U ) e. ( ( G |`s ( T .(+) U ) ) GrpHom G ) )
11 1 2 3 4 5 6 7 8 9 pj1f 
 |-  ( ph -> ( T P U ) : ( T .(+) U ) --> T )
12 11 frnd 
 |-  ( ph -> ran ( T P U ) C_ T )
13 eqid 
 |-  ( G |`s T ) = ( G |`s T )
14 13 resghm2b 
 |-  ( ( T e. ( SubGrp ` G ) /\ ran ( T P U ) C_ T ) -> ( ( T P U ) e. ( ( G |`s ( T .(+) U ) ) GrpHom G ) <-> ( T P U ) e. ( ( G |`s ( T .(+) U ) ) GrpHom ( G |`s T ) ) ) )
15 5 12 14 syl2anc 
 |-  ( ph -> ( ( T P U ) e. ( ( G |`s ( T .(+) U ) ) GrpHom G ) <-> ( T P U ) e. ( ( G |`s ( T .(+) U ) ) GrpHom ( G |`s T ) ) ) )
16 10 15 mpbid 
 |-  ( ph -> ( T P U ) e. ( ( G |`s ( T .(+) U ) ) GrpHom ( G |`s T ) ) )