Metamath Proof Explorer

Theorem pj1fval

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

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 elex 
 |-  ( G e. V -> G e. _V )
6 5 3ad2ant1 
 |-  ( ( G e. V /\ T C_ B /\ U C_ B ) -> G e. _V )
7 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
8 7 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = B )
9 8 pweqd 
 |-  ( g = G -> ~P ( Base ` g ) = ~P B )
10 fveq2 
 |-  ( g = G -> ( LSSum ` g ) = ( LSSum ` G ) )
11 10 3 eqtr4di 
 |-  ( g = G -> ( LSSum ` g ) = .(+) )
12 11 oveqd 
 |-  ( g = G -> ( t ( LSSum ` g ) u ) = ( t .(+) u ) )
13 fveq2 
 |-  ( g = G -> ( +g ` g ) = ( +g ` G ) )
14 13 2 eqtr4di 
 |-  ( g = G -> ( +g ` g ) = .+ )
15 14 oveqd 
 |-  ( g = G -> ( x ( +g ` g ) y ) = ( x .+ y ) )
16 15 eqeq2d 
 |-  ( g = G -> ( z = ( x ( +g ` g ) y ) <-> z = ( x .+ y ) ) )
17 16 rexbidv 
 |-  ( g = G -> ( E. y e. u z = ( x ( +g ` g ) y ) <-> E. y e. u z = ( x .+ y ) ) )
18 17 riotabidv 
 |-  ( g = G -> ( iota_ x e. t E. y e. u z = ( x ( +g ` g ) y ) ) = ( iota_ x e. t E. y e. u z = ( x .+ y ) ) )
19 12 18 mpteq12dv 
 |-  ( g = G -> ( z e. ( t ( LSSum ` g ) u ) |-> ( iota_ x e. t E. y e. u z = ( x ( +g ` g ) y ) ) ) = ( z e. ( t .(+) u ) |-> ( iota_ x e. t E. y e. u z = ( x .+ y ) ) ) )
20 9 9 19 mpoeq123dv 
 |-  ( g = G -> ( t e. ~P ( Base ` g ) , u e. ~P ( Base ` g ) |-> ( z e. ( t ( LSSum ` g ) u ) |-> ( iota_ x e. t E. y e. u z = ( x ( +g ` g ) y ) ) ) ) = ( t e. ~P B , u e. ~P B |-> ( z e. ( t .(+) u ) |-> ( iota_ x e. t E. y e. u z = ( x .+ y ) ) ) ) )
21 df-pj1 
 |-  proj1 = ( g e. _V |-> ( t e. ~P ( Base ` g ) , u e. ~P ( Base ` g ) |-> ( z e. ( t ( LSSum ` g ) u ) |-> ( iota_ x e. t E. y e. u z = ( x ( +g ` g ) y ) ) ) ) )
22 1 fvexi 
 |-  B e. _V
23 22 pwex 
 |-  ~P B e. _V
24 23 23 mpoex 
 |-  ( t e. ~P B , u e. ~P B |-> ( z e. ( t .(+) u ) |-> ( iota_ x e. t E. y e. u z = ( x .+ y ) ) ) ) e. _V
25 20 21 24 fvmpt 
 |-  ( G e. _V -> ( proj1 ` G ) = ( t e. ~P B , u e. ~P B |-> ( z e. ( t .(+) u ) |-> ( iota_ x e. t E. y e. u z = ( x .+ y ) ) ) ) )
26 6 25 syl 
 |-  ( ( G e. V /\ T C_ B /\ U C_ B ) -> ( proj1 ` G ) = ( t e. ~P B , u e. ~P B |-> ( z e. ( t .(+) u ) |-> ( iota_ x e. t E. y e. u z = ( x .+ y ) ) ) ) )
27 4 26 eqtrid 
 |-  ( ( G e. V /\ T C_ B /\ U C_ B ) -> P = ( t e. ~P B , u e. ~P B |-> ( z e. ( t .(+) u ) |-> ( iota_ x e. t E. y e. u z = ( x .+ y ) ) ) ) )
28 oveq12 
 |-  ( ( t = T /\ u = U ) -> ( t .(+) u ) = ( T .(+) U ) )
29 28 adantl 
 |-  ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ ( t = T /\ u = U ) ) -> ( t .(+) u ) = ( T .(+) U ) )
30 simprl 
 |-  ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ ( t = T /\ u = U ) ) -> t = T )
31 simprr 
 |-  ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ ( t = T /\ u = U ) ) -> u = U )
32 31 rexeqdv 
 |-  ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ ( t = T /\ u = U ) ) -> ( E. y e. u z = ( x .+ y ) <-> E. y e. U z = ( x .+ y ) ) )
33 30 32 riotaeqbidv 
 |-  ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ ( t = T /\ u = U ) ) -> ( iota_ x e. t E. y e. u z = ( x .+ y ) ) = ( iota_ x e. T E. y e. U z = ( x .+ y ) ) )
34 29 33 mpteq12dv 
 |-  ( ( ( G e. V /\ T C_ B /\ U C_ B ) /\ ( t = T /\ u = U ) ) -> ( z e. ( t .(+) u ) |-> ( iota_ x e. t E. y e. u z = ( x .+ y ) ) ) = ( z e. ( T .(+) U ) |-> ( iota_ x e. T E. y e. U z = ( x .+ y ) ) ) )
35 simp2 
 |-  ( ( G e. V /\ T C_ B /\ U C_ B ) -> T C_ B )
36 22 elpw2 
 |-  ( T e. ~P B <-> T C_ B )
37 35 36 sylibr 
 |-  ( ( G e. V /\ T C_ B /\ U C_ B ) -> T e. ~P B )
38 simp3 
 |-  ( ( G e. V /\ T C_ B /\ U C_ B ) -> U C_ B )
39 22 elpw2 
 |-  ( U e. ~P B <-> U C_ B )
40 38 39 sylibr 
 |-  ( ( G e. V /\ T C_ B /\ U C_ B ) -> U e. ~P B )
41 ovex 
 |-  ( T .(+) U ) e. _V
42 41 mptex 
 |-  ( z e. ( T .(+) U ) |-> ( iota_ x e. T E. y e. U z = ( x .+ y ) ) ) e. _V
43 42 a1i 
 |-  ( ( G e. V /\ T C_ B /\ U C_ B ) -> ( z e. ( T .(+) U ) |-> ( iota_ x e. T E. y e. U z = ( x .+ y ) ) ) e. _V )
44 27 34 37 40 43 ovmpod 
 |-  ( ( 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 ) ) ) )