Step |
Hyp |
Ref |
Expression |
0 |
|
ctrnN |
|- Trn |
1 |
|
vk |
|- k |
2 |
|
cvv |
|- _V |
3 |
|
vd |
|- d |
4 |
|
catm |
|- Atoms |
5 |
1
|
cv |
|- k |
6 |
5 4
|
cfv |
|- ( Atoms ` k ) |
7 |
|
vf |
|- f |
8 |
|
cdilN |
|- Dil |
9 |
5 8
|
cfv |
|- ( Dil ` k ) |
10 |
3
|
cv |
|- d |
11 |
10 9
|
cfv |
|- ( ( Dil ` k ) ` d ) |
12 |
|
vq |
|- q |
13 |
|
cwpointsN |
|- WAtoms |
14 |
5 13
|
cfv |
|- ( WAtoms ` k ) |
15 |
10 14
|
cfv |
|- ( ( WAtoms ` k ) ` d ) |
16 |
|
vr |
|- r |
17 |
12
|
cv |
|- q |
18 |
|
cpadd |
|- +P |
19 |
5 18
|
cfv |
|- ( +P ` k ) |
20 |
7
|
cv |
|- f |
21 |
17 20
|
cfv |
|- ( f ` q ) |
22 |
17 21 19
|
co |
|- ( q ( +P ` k ) ( f ` q ) ) |
23 |
|
cpolN |
|- _|_P |
24 |
5 23
|
cfv |
|- ( _|_P ` k ) |
25 |
10
|
csn |
|- { d } |
26 |
25 24
|
cfv |
|- ( ( _|_P ` k ) ` { d } ) |
27 |
22 26
|
cin |
|- ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) |
28 |
16
|
cv |
|- r |
29 |
28 20
|
cfv |
|- ( f ` r ) |
30 |
28 29 19
|
co |
|- ( r ( +P ` k ) ( f ` r ) ) |
31 |
30 26
|
cin |
|- ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { d } ) ) |
32 |
27 31
|
wceq |
|- ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { d } ) ) |
33 |
32 16 15
|
wral |
|- A. r e. ( ( WAtoms ` k ) ` d ) ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { d } ) ) |
34 |
33 12 15
|
wral |
|- A. q e. ( ( WAtoms ` k ) ` d ) A. r e. ( ( WAtoms ` k ) ` d ) ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { d } ) ) |
35 |
34 7 11
|
crab |
|- { f e. ( ( Dil ` k ) ` d ) | A. q e. ( ( WAtoms ` k ) ` d ) A. r e. ( ( WAtoms ` k ) ` d ) ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { d } ) ) } |
36 |
3 6 35
|
cmpt |
|- ( d e. ( Atoms ` k ) |-> { f e. ( ( Dil ` k ) ` d ) | A. q e. ( ( WAtoms ` k ) ` d ) A. r e. ( ( WAtoms ` k ) ` d ) ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { d } ) ) } ) |
37 |
1 2 36
|
cmpt |
|- ( k e. _V |-> ( d e. ( Atoms ` k ) |-> { f e. ( ( Dil ` k ) ` d ) | A. q e. ( ( WAtoms ` k ) ` d ) A. r e. ( ( WAtoms ` k ) ` d ) ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { d } ) ) } ) ) |
38 |
0 37
|
wceq |
|- Trn = ( k e. _V |-> ( d e. ( Atoms ` k ) |-> { f e. ( ( Dil ` k ) ` d ) | A. q e. ( ( WAtoms ` k ) ` d ) A. r e. ( ( WAtoms ` k ) ` d ) ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { d } ) ) } ) ) |