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

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