Metamath Proof Explorer


Definition df-pj1

Description: Define the left projection function, which takes two subgroups t , u with trivial intersection and returns a function mapping the elements of the subgroup sum t + u to their projections onto t . (The other projection function can be obtained by swapping the roles of t and u .) (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion df-pj1
|- proj1 = ( w e. _V |-> ( t e. ~P ( Base ` w ) , u e. ~P ( Base ` w ) |-> ( z e. ( t ( LSSum ` w ) u ) |-> ( iota_ x e. t E. y e. u z = ( x ( +g ` w ) y ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpj1
 |-  proj1
1 vw
 |-  w
2 cvv
 |-  _V
3 vt
 |-  t
4 cbs
 |-  Base
5 1 cv
 |-  w
6 5 4 cfv
 |-  ( Base ` w )
7 6 cpw
 |-  ~P ( Base ` w )
8 vu
 |-  u
9 vz
 |-  z
10 3 cv
 |-  t
11 clsm
 |-  LSSum
12 5 11 cfv
 |-  ( LSSum ` w )
13 8 cv
 |-  u
14 10 13 12 co
 |-  ( t ( LSSum ` w ) u )
15 vx
 |-  x
16 vy
 |-  y
17 9 cv
 |-  z
18 15 cv
 |-  x
19 cplusg
 |-  +g
20 5 19 cfv
 |-  ( +g ` w )
21 16 cv
 |-  y
22 18 21 20 co
 |-  ( x ( +g ` w ) y )
23 17 22 wceq
 |-  z = ( x ( +g ` w ) y )
24 23 16 13 wrex
 |-  E. y e. u z = ( x ( +g ` w ) y )
25 24 15 10 crio
 |-  ( iota_ x e. t E. y e. u z = ( x ( +g ` w ) y ) )
26 9 14 25 cmpt
 |-  ( z e. ( t ( LSSum ` w ) u ) |-> ( iota_ x e. t E. y e. u z = ( x ( +g ` w ) y ) ) )
27 3 8 7 7 26 cmpo
 |-  ( t e. ~P ( Base ` w ) , u e. ~P ( Base ` w ) |-> ( z e. ( t ( LSSum ` w ) u ) |-> ( iota_ x e. t E. y e. u z = ( x ( +g ` w ) y ) ) ) )
28 1 2 27 cmpt
 |-  ( w e. _V |-> ( t e. ~P ( Base ` w ) , u e. ~P ( Base ` w ) |-> ( z e. ( t ( LSSum ` w ) u ) |-> ( iota_ x e. t E. y e. u z = ( x ( +g ` w ) y ) ) ) ) )
29 0 28 wceq
 |-  proj1 = ( w e. _V |-> ( t e. ~P ( Base ` w ) , u e. ~P ( Base ` w ) |-> ( z e. ( t ( LSSum ` w ) u ) |-> ( iota_ x e. t E. y e. u z = ( x ( +g ` w ) y ) ) ) ) )