Step | Hyp | Ref
| Expression |
1 | | df-fm 22262 |
. . . . 5
⊢ FilMap =
(𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦))))) |
2 | 1 | a1i 11 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)))))) |
3 | | dmeq 5618 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹) |
4 | 3 | fveq2d 6500 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (fBas‘dom 𝑓) = (fBas‘dom 𝐹)) |
5 | 4 | adantl 474 |
. . . . . 6
⊢ ((𝑥 = 𝑋 ∧ 𝑓 = 𝐹) → (fBas‘dom 𝑓) = (fBas‘dom 𝐹)) |
6 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) |
7 | | imaeq1 5762 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝑓 “ 𝑦) = (𝐹 “ 𝑦)) |
8 | 7 | mpteq2dv 5019 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)) = (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))) |
9 | 8 | rneqd 5648 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → ran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)) = ran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))) |
10 | 6, 9 | oveqan12d 6993 |
. . . . . 6
⊢ ((𝑥 = 𝑋 ∧ 𝑓 = 𝐹) → (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦))) = (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) |
11 | 5, 10 | mpteq12dv 5008 |
. . . . 5
⊢ ((𝑥 = 𝑋 ∧ 𝑓 = 𝐹) → (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)))) = (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))) |
12 | | fdm 6349 |
. . . . . . . 8
⊢ (𝐹:𝑌⟶𝑋 → dom 𝐹 = 𝑌) |
13 | 12 | fveq2d 6500 |
. . . . . . 7
⊢ (𝐹:𝑌⟶𝑋 → (fBas‘dom 𝐹) = (fBas‘𝑌)) |
14 | 13 | mpteq1d 5012 |
. . . . . 6
⊢ (𝐹:𝑌⟶𝑋 → (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))) |
15 | 14 | 3ad2ant3 1115 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))) |
16 | 11, 15 | sylan9eqr 2830 |
. . . 4
⊢ (((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑥 = 𝑋 ∧ 𝑓 = 𝐹)) → (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))) |
17 | | elex 3427 |
. . . . 5
⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ V) |
18 | 17 | 3ad2ant1 1113 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝑋 ∈ V) |
19 | | simp3 1118 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝐹:𝑌⟶𝑋) |
20 | | elfvdm 6528 |
. . . . . 6
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas) |
21 | 20 | 3ad2ant2 1114 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝑌 ∈ dom fBas) |
22 | | simp1 1116 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝑋 ∈ 𝐴) |
23 | | fex2 7451 |
. . . . 5
⊢ ((𝐹:𝑌⟶𝑋 ∧ 𝑌 ∈ dom fBas ∧ 𝑋 ∈ 𝐴) → 𝐹 ∈ V) |
24 | 19, 21, 22, 23 | syl3anc 1351 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝐹 ∈ V) |
25 | | fvex 6509 |
. . . . . 6
⊢
(fBas‘𝑌)
∈ V |
26 | 25 | mptex 6810 |
. . . . 5
⊢ (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) ∈ V |
27 | 26 | a1i 11 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) ∈ V) |
28 | 2, 16, 18, 24, 27 | ovmpod 7116 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑋 FilMap 𝐹) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))) |
29 | 28 | fveq1d 6498 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) = ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))‘𝐵)) |
30 | | mpteq1 5011 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)) = (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))) |
31 | 30 | rneqd 5648 |
. . . . 5
⊢ (𝑏 = 𝐵 → ran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)) = ran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))) |
32 | 31 | oveq2d 6990 |
. . . 4
⊢ (𝑏 = 𝐵 → (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦)))) |
33 | | eqid 2772 |
. . . 4
⊢ (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) |
34 | | ovex 7006 |
. . . 4
⊢ (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))) ∈ V |
35 | 32, 33, 34 | fvmpt 6593 |
. . 3
⊢ (𝐵 ∈ (fBas‘𝑌) → ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))‘𝐵) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦)))) |
36 | 35 | 3ad2ant2 1114 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))‘𝐵) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦)))) |
37 | 29, 36 | eqtrd 2808 |
1
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦)))) |