Step |
Hyp |
Ref |
Expression |
1 |
|
cpm2mfval.i |
⊢ 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 ) |
2 |
|
cpm2mfval.s |
⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 ) |
3 |
1 2
|
cpm2mval |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆 ) → ( 𝐼 ‘ 𝑀 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) |
4 |
3
|
adantr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ) → ( 𝐼 ‘ 𝑀 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) |
5 |
|
oveq12 |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑥 𝑀 𝑦 ) = ( 𝑋 𝑀 𝑌 ) ) |
6 |
5
|
fveq2d |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) = ( coe1 ‘ ( 𝑋 𝑀 𝑌 ) ) ) |
7 |
6
|
fveq1d |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝑋 𝑀 𝑌 ) ) ‘ 0 ) ) |
8 |
7
|
adantl |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ) ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ( coe1 ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝑋 𝑀 𝑌 ) ) ‘ 0 ) ) |
9 |
|
simprl |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ) → 𝑋 ∈ 𝑁 ) |
10 |
|
simprr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ) → 𝑌 ∈ 𝑁 ) |
11 |
|
fvexd |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ) → ( ( coe1 ‘ ( 𝑋 𝑀 𝑌 ) ) ‘ 0 ) ∈ V ) |
12 |
4 8 9 10 11
|
ovmpod |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ) → ( 𝑋 ( 𝐼 ‘ 𝑀 ) 𝑌 ) = ( ( coe1 ‘ ( 𝑋 𝑀 𝑌 ) ) ‘ 0 ) ) |