Metamath Proof Explorer


Theorem pj2f

Description: The right projection function maps a direct subspace sum onto the right factor. (Contributed by Mario Carneiro, 15-Oct-2015)

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 pj2f
|- ( ph -> ( U P T ) : ( T .(+) U ) --> U )

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 incom
 |-  ( U i^i T ) = ( T i^i U )
11 10 7 syl5eq
 |-  ( ph -> ( U i^i T ) = { .0. } )
12 4 5 6 8 cntzrecd
 |-  ( ph -> U C_ ( Z ` T ) )
13 1 2 3 4 6 5 11 12 9 pj1f
 |-  ( ph -> ( U P T ) : ( U .(+) T ) --> U )
14 2 4 lsmcom2
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( T .(+) U ) = ( U .(+) T ) )
15 5 6 8 14 syl3anc
 |-  ( ph -> ( T .(+) U ) = ( U .(+) T ) )
16 15 feq2d
 |-  ( ph -> ( ( U P T ) : ( T .(+) U ) --> U <-> ( U P T ) : ( U .(+) T ) --> U ) )
17 13 16 mpbird
 |-  ( ph -> ( U P T ) : ( T .(+) U ) --> U )