Step |
Hyp |
Ref |
Expression |
1 |
|
evlvar.q |
⊢ 𝑄 = ( 𝐼 eval 𝑆 ) |
2 |
|
evlvar.v |
⊢ 𝑉 = ( 𝐼 mVar 𝑆 ) |
3 |
|
evlvar.b |
⊢ 𝐵 = ( Base ‘ 𝑆 ) |
4 |
|
evlvar.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑊 ) |
5 |
|
evlvar.s |
⊢ ( 𝜑 → 𝑆 ∈ CRing ) |
6 |
|
evlvar.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐼 ) |
7 |
|
eqid |
⊢ ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) |
8 |
|
eqid |
⊢ ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) = ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) |
9 |
|
eqid |
⊢ ( 𝑆 ↾s 𝐵 ) = ( 𝑆 ↾s 𝐵 ) |
10 |
|
crngring |
⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring ) |
11 |
3
|
subrgid |
⊢ ( 𝑆 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) |
12 |
5 10 11
|
3syl |
⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) |
13 |
7 1 8 9 3 4 5 12 6
|
evlsvarsrng |
⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) = ( 𝑄 ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) ) |
14 |
7 8 9 3 4 5 12 6
|
evlsvar |
⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) ) |
15 |
2 4 12 9
|
subrgmvr |
⊢ ( 𝜑 → 𝑉 = ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ) |
16 |
15
|
fveq1d |
⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) = ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) |
17 |
16
|
eqcomd |
⊢ ( 𝜑 → ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) = ( 𝑉 ‘ 𝑋 ) ) |
18 |
17
|
fveq2d |
⊢ ( 𝜑 → ( 𝑄 ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) = ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) ) |
19 |
13 14 18
|
3eqtr3rd |
⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) ) |