Step | Hyp | Ref
| Expression |
1 | | evls1fval.q |
. 2
⊢ 𝑄 = (𝑆 evalSub1 𝑅) |
2 | | elex 3460 |
. . . 4
⊢ (𝑆 ∈ 𝑉 → 𝑆 ∈ V) |
3 | 2 | adantr 482 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → 𝑆 ∈ V) |
4 | | simpr 486 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → 𝑅 ∈ 𝒫 𝐵) |
5 | | ovex 7375 |
. . . . . 6
⊢ (𝐵 ↑m (𝐵 ↑m
1o)) ∈ V |
6 | 5 | mptex 7160 |
. . . . 5
⊢ (𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∈ V |
7 | | fvex 6843 |
. . . . 5
⊢ (𝐸‘𝑅) ∈ V |
8 | 6, 7 | coex 7850 |
. . . 4
⊢ ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅)) ∈ V |
9 | 8 | a1i 11 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅)) ∈ V) |
10 | | fveq2 6830 |
. . . . . . . 8
⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆)) |
11 | 10 | adantr 482 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (Base‘𝑠) = (Base‘𝑆)) |
12 | | evls1fval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑆) |
13 | 11, 12 | eqtr4di 2795 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (Base‘𝑠) = 𝐵) |
14 | 13 | csbeq1d 3851 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o
evalSub 𝑠)‘𝑟)) = ⦋𝐵 / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o
evalSub 𝑠)‘𝑟))) |
15 | 12 | fvexi 6844 |
. . . . . . 7
⊢ 𝐵 ∈ V |
16 | 15 | a1i 11 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → 𝐵 ∈ V) |
17 | | id 22 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → 𝑏 = 𝐵) |
18 | | oveq1 7349 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → (𝑏 ↑m 1o) = (𝐵 ↑m
1o)) |
19 | 17, 18 | oveq12d 7360 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → (𝑏 ↑m (𝑏 ↑m 1o)) = (𝐵 ↑m (𝐵 ↑m
1o))) |
20 | | mpteq1 5190 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})) = (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))) |
21 | 20 | coeq2d 5809 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦}))) = (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) |
22 | 19, 21 | mpteq12dv 5188 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) = (𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦}))))) |
23 | 22 | coeq1d 5808 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → ((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o
evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ ((1o
evalSub 𝑠)‘𝑟))) |
24 | 23 | adantl 483 |
. . . . . 6
⊢ (((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) ∧ 𝑏 = 𝐵) → ((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o
evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ ((1o
evalSub 𝑠)‘𝑟))) |
25 | 16, 24 | csbied 3885 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⦋𝐵 / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o
evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ ((1o
evalSub 𝑠)‘𝑟))) |
26 | | oveq2 7350 |
. . . . . . . . 9
⊢ (𝑠 = 𝑆 → (1o evalSub 𝑠) = (1o evalSub 𝑆)) |
27 | | evls1fval.e |
. . . . . . . . 9
⊢ 𝐸 = (1o evalSub 𝑆) |
28 | 26, 27 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝑠 = 𝑆 → (1o evalSub 𝑠) = 𝐸) |
29 | 28 | adantr 482 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → (1o evalSub 𝑠) = 𝐸) |
30 | | simpr 486 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → 𝑟 = 𝑅) |
31 | 29, 30 | fveq12d 6837 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ((1o evalSub 𝑠)‘𝑟) = (𝐸‘𝑅)) |
32 | 31 | coeq2d 5809 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ ((1o
evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅))) |
33 | 14, 25, 32 | 3eqtrd 2781 |
. . . 4
⊢ ((𝑠 = 𝑆 ∧ 𝑟 = 𝑅) → ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o
evalSub 𝑠)‘𝑟)) = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅))) |
34 | 10, 12 | eqtr4di 2795 |
. . . . 5
⊢ (𝑠 = 𝑆 → (Base‘𝑠) = 𝐵) |
35 | 34 | pweqd 4569 |
. . . 4
⊢ (𝑠 = 𝑆 → 𝒫 (Base‘𝑠) = 𝒫 𝐵) |
36 | | df-evls1 21587 |
. . . 4
⊢
evalSub1 = (𝑠
∈ V, 𝑟 ∈
𝒫 (Base‘𝑠)
↦ ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o
evalSub 𝑠)‘𝑟))) |
37 | 33, 35, 36 | ovmpox 7493 |
. . 3
⊢ ((𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 𝐵 ∧ ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅)) ∈ V) → (𝑆 evalSub1 𝑅) = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅))) |
38 | 3, 4, 9, 37 | syl3anc 1371 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → (𝑆 evalSub1 𝑅) = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅))) |
39 | 1, 38 | eqtrid 2789 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝒫 𝐵) → 𝑄 = ((𝑥 ∈ (𝐵 ↑m (𝐵 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1o × {𝑦})))) ∘ (𝐸‘𝑅))) |