Step |
Hyp |
Ref |
Expression |
1 |
|
mpladd.p |
⊢ 𝑃 = ( 𝐼 mPoly 𝑅 ) |
2 |
|
mpladd.b |
⊢ 𝐵 = ( Base ‘ 𝑃 ) |
3 |
|
mpladd.a |
⊢ + = ( +g ‘ 𝑅 ) |
4 |
|
mpladd.g |
⊢ ✚ = ( +g ‘ 𝑃 ) |
5 |
|
mpladd.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
6 |
|
mpladd.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) |
7 |
|
eqid |
⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 ) |
8 |
|
eqid |
⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) |
9 |
2
|
fvexi |
⊢ 𝐵 ∈ V |
10 |
1 7 2
|
mplval2 |
⊢ 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s 𝐵 ) |
11 |
|
eqid |
⊢ ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) |
12 |
10 11
|
ressplusg |
⊢ ( 𝐵 ∈ V → ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ 𝑃 ) ) |
13 |
9 12
|
ax-mp |
⊢ ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ 𝑃 ) |
14 |
4 13
|
eqtr4i |
⊢ ✚ = ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) |
15 |
1 7 2 8
|
mplbasss |
⊢ 𝐵 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) |
16 |
15 5
|
sselid |
⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) |
17 |
15 6
|
sselid |
⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) |
18 |
7 8 3 14 16 17
|
psradd |
⊢ ( 𝜑 → ( 𝑋 ✚ 𝑌 ) = ( 𝑋 ∘f + 𝑌 ) ) |