Step |
Hyp |
Ref |
Expression |
0 |
|
ccpmat |
⊢ ConstPolyMat |
1 |
|
vn |
⊢ 𝑛 |
2 |
|
cfn |
⊢ Fin |
3 |
|
vr |
⊢ 𝑟 |
4 |
|
cvv |
⊢ V |
5 |
|
vm |
⊢ 𝑚 |
6 |
|
cbs |
⊢ Base |
7 |
1
|
cv |
⊢ 𝑛 |
8 |
|
cmat |
⊢ Mat |
9 |
|
cpl1 |
⊢ Poly1 |
10 |
3
|
cv |
⊢ 𝑟 |
11 |
10 9
|
cfv |
⊢ ( Poly1 ‘ 𝑟 ) |
12 |
7 11 8
|
co |
⊢ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) |
13 |
12 6
|
cfv |
⊢ ( Base ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) |
14 |
|
vi |
⊢ 𝑖 |
15 |
|
vj |
⊢ 𝑗 |
16 |
|
vk |
⊢ 𝑘 |
17 |
|
cn |
⊢ ℕ |
18 |
|
cco1 |
⊢ coe1 |
19 |
14
|
cv |
⊢ 𝑖 |
20 |
5
|
cv |
⊢ 𝑚 |
21 |
15
|
cv |
⊢ 𝑗 |
22 |
19 21 20
|
co |
⊢ ( 𝑖 𝑚 𝑗 ) |
23 |
22 18
|
cfv |
⊢ ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) |
24 |
16
|
cv |
⊢ 𝑘 |
25 |
24 23
|
cfv |
⊢ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) |
26 |
|
c0g |
⊢ 0g |
27 |
10 26
|
cfv |
⊢ ( 0g ‘ 𝑟 ) |
28 |
25 27
|
wceq |
⊢ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑟 ) |
29 |
28 16 17
|
wral |
⊢ ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑟 ) |
30 |
29 15 7
|
wral |
⊢ ∀ 𝑗 ∈ 𝑛 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑟 ) |
31 |
30 14 7
|
wral |
⊢ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑟 ) |
32 |
31 5 13
|
crab |
⊢ { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑟 ) } |
33 |
1 3 2 4 32
|
cmpo |
⊢ ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑟 ) } ) |
34 |
0 33
|
wceq |
⊢ ConstPolyMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑟 ) } ) |