Theorem pj1val

Description: The left projection function (for a direct product of group subspaces). (Contributed by Mario Carneiro, 15-Oct-2015) (Revised by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	pj1fval.v	|- B = ( Base ` G )
	pj1fval.a	|- .+ = ( +g ` G )
	pj1fval.s	|- .(+) = ( LSSum ` G )
	pj1fval.p	|- P = ( proj1 ` G )
Assertion	pj1val	|- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ X e. ( T .(+) U ) ) -> ( ( T P U ) ` X ) = ( iota_ x e. T E. y e. U X = ( x .+ y ) ) )

Proof

Step	Hyp	Ref	Expression
1		pj1fval.v	|- B = ( Base ` G )
2		pj1fval.a	|- .+ = ( +g ` G )
3		pj1fval.s	|- .(+) = ( LSSum ` G )
4		pj1fval.p	|- P = ( proj1 ` G )
5	1 2 3 4	pj1fval	|- ( ( G e. V /\ T C_ B /\ U C_ B ) -> ( T P U ) = ( z e. ( T .(+) U ) |-> ( iota_ x e. T E. y e. U z = ( x .+ y ) ) ) )
6	5	adantr	|- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ X e. ( T .(+) U ) ) -> ( T P U ) = ( z e. ( T .(+) U ) |-> ( iota_ x e. T E. y e. U z = ( x .+ y ) ) ) )
7		simpr	|- ( ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ X e. ( T .(+) U ) ) /\ z = X ) -> z = X )
8	7	eqeq1d	|- ( ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ X e. ( T .(+) U ) ) /\ z = X ) -> ( z = ( x .+ y ) <-> X = ( x .+ y ) ) )
9	8	rexbidv	|- ( ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ X e. ( T .(+) U ) ) /\ z = X ) -> ( E. y e. U z = ( x .+ y ) <-> E. y e. U X = ( x .+ y ) ) )
10	9	riotabidv	|- ( ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ X e. ( T .(+) U ) ) /\ z = X ) -> ( iota_ x e. T E. y e. U z = ( x .+ y ) ) = ( iota_ x e. T E. y e. U X = ( x .+ y ) ) )
11		simpr	|- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ X e. ( T .(+) U ) ) -> X e. ( T .(+) U ) )
12		riotaex	|- ( iota_ x e. T E. y e. U X = ( x .+ y ) ) e. _V
13	12	a1i	|- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ X e. ( T .(+) U ) ) -> ( iota_ x e. T E. y e. U X = ( x .+ y ) ) e. _V )
14	6 10 11 13	fvmptd	|- ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ X e. ( T .(+) U ) ) -> ( ( T P U ) ` X ) = ( iota_ x e. T E. y e. U X = ( x .+ y ) ) )