Theorem pj1eq

Description: Any element of a direct subspace sum can be decomposed uniquely into projections onto the left and right factors. (Contributed by Mario Carneiro, 16-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 )
	pj1eq.5	|- ( ph -> X e. ( T .(+) U ) )
	pj1eq.6	|- ( ph -> B e. T )
	pj1eq.7	|- ( ph -> C e. U )
Assertion	pj1eq	|- ( ph -> ( X = ( B .+ C ) <-> ( ( ( T P U ) ` X ) = B /\ ( ( U P T ) ` X ) = C ) ) )

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		pj1eq.5	|- ( ph -> X e. ( T .(+) U ) )
11		pj1eq.6	|- ( ph -> B e. T )
12		pj1eq.7	|- ( ph -> C e. U )
13	1 2 3 4 5 6 7 8 9	pj1id	|- ( ( ph /\ X e. ( T .(+) U ) ) -> X = ( ( ( T P U ) ` X ) .+ ( ( U P T ) ` X ) ) )
14	10 13	mpdan	|- ( ph -> X = ( ( ( T P U ) ` X ) .+ ( ( U P T ) ` X ) ) )
15	14	eqeq1d	|- ( ph -> ( X = ( B .+ C ) <-> ( ( ( T P U ) ` X ) .+ ( ( U P T ) ` X ) ) = ( B .+ C ) ) )
16	1 2 3 4 5 6 7 8 9	pj1f	|- ( ph -> ( T P U ) : ( T .(+) U ) --> T )
17	16 10	ffvelrnd	|- ( ph -> ( ( T P U ) ` X ) e. T )
18	1 2 3 4 5 6 7 8 9	pj2f	|- ( ph -> ( U P T ) : ( T .(+) U ) --> U )
19	18 10	ffvelrnd	|- ( ph -> ( ( U P T ) ` X ) e. U )
20	1 3 4 5 6 7 8 17 11 19 12	subgdisjb	|- ( ph -> ( ( ( ( T P U ) ` X ) .+ ( ( U P T ) ` X ) ) = ( B .+ C ) <-> ( ( ( T P U ) ` X ) = B /\ ( ( U P T ) ` X ) = C ) ) )
21	15 20	bitrd	|- ( ph -> ( X = ( B .+ C ) <-> ( ( ( T P U ) ` X ) = B /\ ( ( U P T ) ` X ) = C ) ) )