Step |
Hyp |
Ref |
Expression |
1 |
|
cpm2mf.a |
⊢ 𝐴 = ( 𝑁 Mat 𝑅 ) |
2 |
|
cpm2mf.k |
⊢ 𝐾 = ( Base ‘ 𝐴 ) |
3 |
|
cpm2mf.s |
⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 ) |
4 |
|
cpm2mf.i |
⊢ 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 ) |
5 |
4 3
|
cpm2mfval |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐼 = ( 𝑚 ∈ 𝑆 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ) |
6 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
7 |
|
simpll |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝑆 ) → 𝑁 ∈ Fin ) |
8 |
|
simplr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝑆 ) → 𝑅 ∈ Ring ) |
9 |
|
eqid |
⊢ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) = ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) |
10 |
|
eqid |
⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) ) |
11 |
|
eqid |
⊢ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) = ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) |
12 |
|
simp2 |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑥 ∈ 𝑁 ) |
13 |
|
simp3 |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑦 ∈ 𝑁 ) |
14 |
|
eqid |
⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 ) |
15 |
3 14 9 11
|
cpmatpmat |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑚 ∈ 𝑆 ) → 𝑚 ∈ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) |
16 |
15
|
3expa |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝑆 ) → 𝑚 ∈ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) |
17 |
16
|
3ad2ant1 |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑚 ∈ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) |
18 |
9 10 11 12 13 17
|
matecld |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑥 𝑚 𝑦 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) |
19 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
20 |
|
eqid |
⊢ ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) = ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) |
21 |
20 10 14 6
|
coe1fvalcl |
⊢ ( ( ( 𝑥 𝑚 𝑦 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) ) |
22 |
18 19 21
|
sylancl |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) ) |
23 |
1 6 2 7 8 22
|
matbas2d |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ∈ 𝐾 ) |
24 |
5 23
|
fmpt3d |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐼 : 𝑆 ⟶ 𝐾 ) |