Theorem pj1f

Description: The left projection function maps a direct subspace sum onto the left 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	pj1f	|- ( ph -> ( T P U ) : ( T .(+) U ) --> 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		subgrcl	|- ( T e. ( SubGrp ` G ) -> G e. Grp )
11	5 10	syl	|- ( ph -> G e. Grp )
12		eqid	|- ( Base ` G ) = ( Base ` G )
13	12	subgss	|- ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) )
14	5 13	syl	|- ( ph -> T C_ ( Base ` G ) )
15	12	subgss	|- ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
16	6 15	syl	|- ( ph -> U C_ ( Base ` G ) )
17	12 1 2 9	pj1fval	|- ( ( G e. Grp /\ T C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) -> ( T P U ) = ( z e. ( T .(+) U ) |-> ( iota_ x e. T E. y e. U z = ( x .+ y ) ) ) )
18	11 14 16 17	syl3anc	|- ( ph -> ( T P U ) = ( z e. ( T .(+) U ) |-> ( iota_ x e. T E. y e. U z = ( x .+ y ) ) ) )
19	1 2 3 4 5 6 7 8	pj1eu	|- ( ( ph /\ z e. ( T .(+) U ) ) -> E! x e. T E. y e. U z = ( x .+ y ) )
20		riotacl	|- ( E! x e. T E. y e. U z = ( x .+ y ) -> ( iota_ x e. T E. y e. U z = ( x .+ y ) ) e. T )
21	19 20	syl	|- ( ( ph /\ z e. ( T .(+) U ) ) -> ( iota_ x e. T E. y e. U z = ( x .+ y ) ) e. T )
22	18 21	fmpt3d	|- ( ph -> ( T P U ) : ( T .(+) U ) --> T )