This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid 
 |-  ( 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 )