Step |
Hyp |
Ref |
Expression |
1 |
|
mplascl.p |
⊢ 𝑃 = ( 𝐼 mPoly 𝑅 ) |
2 |
|
mplascl.d |
⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } |
3 |
|
mplascl.z |
⊢ 0 = ( 0g ‘ 𝑅 ) |
4 |
|
mplascl.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
5 |
|
mplascl.a |
⊢ 𝐴 = ( algSc ‘ 𝑃 ) |
6 |
|
mplascl.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑊 ) |
7 |
|
mplascl.r |
⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
8 |
|
mplascl.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
9 |
1 6 7
|
mplsca |
⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) ) |
10 |
9
|
fveq2d |
⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) |
11 |
4 10
|
syl5eq |
⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) |
12 |
8 11
|
eleqtrd |
⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) |
13 |
|
eqid |
⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 ) |
14 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) |
15 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 ) |
16 |
|
eqid |
⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 ) |
17 |
5 13 14 15 16
|
asclval |
⊢ ( 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) ) |
18 |
12 17
|
syl |
⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) ) |
19 |
|
eqid |
⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) |
20 |
1 2 3 19 16 6 7
|
mpl1 |
⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) |
21 |
20
|
oveq2d |
⊢ ( 𝜑 → ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) ) |
22 |
2
|
psrbag0 |
⊢ ( 𝐼 ∈ 𝑊 → ( 𝐼 × { 0 } ) ∈ 𝐷 ) |
23 |
6 22
|
syl |
⊢ ( 𝜑 → ( 𝐼 × { 0 } ) ∈ 𝐷 ) |
24 |
1 15 2 19 3 4 6 7 23 8
|
mplmon2 |
⊢ ( 𝜑 → ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) ) ) |
25 |
18 21 24
|
3eqtrd |
⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) ) ) |