Step |
Hyp |
Ref |
Expression |
0 |
|
ctrnN |
⊢ Trn |
1 |
|
vk |
⊢ 𝑘 |
2 |
|
cvv |
⊢ V |
3 |
|
vd |
⊢ 𝑑 |
4 |
|
catm |
⊢ Atoms |
5 |
1
|
cv |
⊢ 𝑘 |
6 |
5 4
|
cfv |
⊢ ( Atoms ‘ 𝑘 ) |
7 |
|
vf |
⊢ 𝑓 |
8 |
|
cdilN |
⊢ Dil |
9 |
5 8
|
cfv |
⊢ ( Dil ‘ 𝑘 ) |
10 |
3
|
cv |
⊢ 𝑑 |
11 |
10 9
|
cfv |
⊢ ( ( Dil ‘ 𝑘 ) ‘ 𝑑 ) |
12 |
|
vq |
⊢ 𝑞 |
13 |
|
cwpointsN |
⊢ WAtoms |
14 |
5 13
|
cfv |
⊢ ( WAtoms ‘ 𝑘 ) |
15 |
10 14
|
cfv |
⊢ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) |
16 |
|
vr |
⊢ 𝑟 |
17 |
12
|
cv |
⊢ 𝑞 |
18 |
|
cpadd |
⊢ +𝑃 |
19 |
5 18
|
cfv |
⊢ ( +𝑃 ‘ 𝑘 ) |
20 |
7
|
cv |
⊢ 𝑓 |
21 |
17 20
|
cfv |
⊢ ( 𝑓 ‘ 𝑞 ) |
22 |
17 21 19
|
co |
⊢ ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) |
23 |
|
cpolN |
⊢ ⊥𝑃 |
24 |
5 23
|
cfv |
⊢ ( ⊥𝑃 ‘ 𝑘 ) |
25 |
10
|
csn |
⊢ { 𝑑 } |
26 |
25 24
|
cfv |
⊢ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) |
27 |
22 26
|
cin |
⊢ ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) |
28 |
16
|
cv |
⊢ 𝑟 |
29 |
28 20
|
cfv |
⊢ ( 𝑓 ‘ 𝑟 ) |
30 |
28 29 19
|
co |
⊢ ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) |
31 |
30 26
|
cin |
⊢ ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) |
32 |
27 31
|
wceq |
⊢ ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) |
33 |
32 16 15
|
wral |
⊢ ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) |
34 |
33 12 15
|
wral |
⊢ ∀ 𝑞 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) |
35 |
34 7 11
|
crab |
⊢ { 𝑓 ∈ ( ( Dil ‘ 𝑘 ) ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) } |
36 |
3 6 35
|
cmpt |
⊢ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( ( Dil ‘ 𝑘 ) ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) } ) |
37 |
1 2 36
|
cmpt |
⊢ ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( ( Dil ‘ 𝑘 ) ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) } ) ) |
38 |
0 37
|
wceq |
⊢ Trn = ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( ( Dil ‘ 𝑘 ) ‘ 𝑑 ) ∣ ∀ 𝑞 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ∀ 𝑟 ∈ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ( ( 𝑞 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑞 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) = ( ( 𝑟 ( +𝑃 ‘ 𝑘 ) ( 𝑓 ‘ 𝑟 ) ) ∩ ( ( ⊥𝑃 ‘ 𝑘 ) ‘ { 𝑑 } ) ) } ) ) |