Step | Hyp | Ref
| Expression |
1 | | evls1fval.q |
. 2
⊢ 𝑄 = (𝑆 evalSub1 𝑅) |
2 | | elex 3212 |
. . . 4
⊢ (𝑆 ∈ 𝑉 → 𝑆 ∈ V) |
3 | 2 | adantr 481 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → 𝑆 ∈ V) |
4 | | simpr 477 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → 𝑅 ∈ 𝒫 𝐵) |
5 | | ovex 6678 |
. . . . . 6
⊢ (𝐵 ↑𝑚
(𝐵
↑𝑚 1𝑜)) ∈ V |
6 | 5 | mptex 6486 |
. . . . 5
⊢ (𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∈
V |
7 | | fvex 6201 |
. . . . 5
⊢ (𝐸‘𝑅) ∈ V |
8 | 6, 7 | coex 7118 |
. . . 4
⊢ ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ (𝐸‘𝑅)) ∈ V |
9 | 8 | a1i 11 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ (𝐸‘𝑅)) ∈ V) |
10 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆)) |
11 | 10 | adantr 481 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (Base‘𝑠) = (Base‘𝑆)) |
12 | | evls1fval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑆) |
13 | 11, 12 | syl6eqr 2674 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (Base‘𝑠) = 𝐵) |
14 | 13 | csbeq1d 3540 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑠)‘𝑟)) = ⦋𝐵 / 𝑏⦌((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑠)‘𝑟))) |
15 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘𝑆)
∈ V |
16 | 12, 15 | eqeltri 2697 |
. . . . . . 7
⊢ 𝐵 ∈ V |
17 | 16 | a1i 11 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → 𝐵 ∈ V) |
18 | | id 22 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → 𝑏 = 𝐵) |
19 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → (𝑏 ↑𝑚
1𝑜) = (𝐵
↑𝑚 1𝑜)) |
20 | 18, 19 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) = (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜))) |
21 | | mpteq1 4737 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})) = (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))) |
22 | 21 | coeq2d 5284 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦}))) = (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) |
23 | 20, 22 | mpteq12dv 4733 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) = (𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))))) |
24 | 23 | coeq1d 5283 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → ((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑠)‘𝑟))) |
25 | 24 | adantl 482 |
. . . . . 6
⊢ (((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) ∧ 𝑏 = 𝐵) → ((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑠)‘𝑟))) |
26 | 17, 25 | csbied 3560 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⦋𝐵 / 𝑏⦌((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑠)‘𝑟))) |
27 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑠 = 𝑆 → (1𝑜 evalSub 𝑠) = (1𝑜
evalSub 𝑆)) |
28 | | evls1fval.e |
. . . . . . . . 9
⊢ 𝐸 = (1𝑜
evalSub 𝑆) |
29 | 27, 28 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝑠 = 𝑆 → (1𝑜 evalSub 𝑠) = 𝐸) |
30 | 29 | adantr 481 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (1𝑜 evalSub
𝑠) = 𝐸) |
31 | | simpr 477 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → 𝑟 = 𝑅) |
32 | 30, 31 | fveq12d 6197 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ((1𝑜 evalSub
𝑠)‘𝑟) = (𝐸‘𝑅)) |
33 | 32 | coeq2d 5284 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ (𝐸‘𝑅))) |
34 | 14, 26, 33 | 3eqtrd 2660 |
. . . 4
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ (𝐸‘𝑅))) |
35 | 10, 12 | syl6eqr 2674 |
. . . . 5
⊢ (𝑠 = 𝑆 → (Base‘𝑠) = 𝐵) |
36 | 35 | pweqd 4163 |
. . . 4
⊢ (𝑠 = 𝑆 → 𝒫 (Base‘𝑠) = 𝒫 𝐵) |
37 | | df-evls1 19680 |
. . . 4
⊢
evalSub1 = (𝑠
∈ V, 𝑟 ∈
𝒫 (Base‘𝑠)
↦ ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) ∘
((1𝑜 evalSub 𝑠)‘𝑟))) |
38 | 34, 36, 37 | ovmpt2x 6789 |
. . 3
⊢ ((𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 𝐵 ∧ ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ (𝐸‘𝑅)) ∈ V) → (𝑆 evalSub1 𝑅) = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ (𝐸‘𝑅))) |
39 | 3, 4, 9, 38 | syl3anc 1326 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → (𝑆 evalSub1 𝑅) = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ (𝐸‘𝑅))) |
40 | 1, 39 | syl5eq 2668 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → 𝑄 = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ (𝐸‘𝑅))) |