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 )