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