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

Metamath Proof Explorer

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