Step | Hyp | Ref
| Expression |
1 | | offval.1 |
. . . 4
⊢ (𝜑 → 𝐹 Fn 𝐴) |
2 | | offval.3 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | | fnex 5691 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
4 | 1, 2, 3 | syl2anc 409 |
. . 3
⊢ (𝜑 → 𝐹 ∈ V) |
5 | | offval.2 |
. . . 4
⊢ (𝜑 → 𝐺 Fn 𝐵) |
6 | | offval.4 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
7 | | fnex 5691 |
. . . 4
⊢ ((𝐺 Fn 𝐵 ∧ 𝐵 ∈ 𝑊) → 𝐺 ∈ V) |
8 | 5, 6, 7 | syl2anc 409 |
. . 3
⊢ (𝜑 → 𝐺 ∈ V) |
9 | | fndm 5271 |
. . . . . . . 8
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
10 | 1, 9 | syl 14 |
. . . . . . 7
⊢ (𝜑 → dom 𝐹 = 𝐴) |
11 | | fndm 5271 |
. . . . . . . 8
⊢ (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵) |
12 | 5, 11 | syl 14 |
. . . . . . 7
⊢ (𝜑 → dom 𝐺 = 𝐵) |
13 | 10, 12 | ineq12d 3310 |
. . . . . 6
⊢ (𝜑 → (dom 𝐹 ∩ dom 𝐺) = (𝐴 ∩ 𝐵)) |
14 | | offval.5 |
. . . . . 6
⊢ (𝐴 ∩ 𝐵) = 𝑆 |
15 | 13, 14 | eqtrdi 2206 |
. . . . 5
⊢ (𝜑 → (dom 𝐹 ∩ dom 𝐺) = 𝑆) |
16 | 15 | mpteq1d 4051 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) = (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) |
17 | | inex1g 4102 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V) |
18 | 14, 17 | eqeltrrid 2245 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → 𝑆 ∈ V) |
19 | | mptexg 5694 |
. . . . 5
⊢ (𝑆 ∈ V → (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) ∈ V) |
20 | 2, 18, 19 | 3syl 17 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) ∈ V) |
21 | 16, 20 | eqeltrd 2234 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) ∈ V) |
22 | | dmeq 4788 |
. . . . . 6
⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹) |
23 | | dmeq 4788 |
. . . . . 6
⊢ (𝑔 = 𝐺 → dom 𝑔 = dom 𝐺) |
24 | 22, 23 | ineqan12d 3311 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (dom 𝑓 ∩ dom 𝑔) = (dom 𝐹 ∩ dom 𝐺)) |
25 | | fveq1 5469 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥)) |
26 | | fveq1 5469 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (𝑔‘𝑥) = (𝐺‘𝑥)) |
27 | 25, 26 | oveqan12d 5845 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓‘𝑥)𝑅(𝑔‘𝑥)) = ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) |
28 | 24, 27 | mpteq12dv 4048 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓‘𝑥)𝑅(𝑔‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) |
29 | | df-of 6034 |
. . . 4
⊢
∘𝑓 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓‘𝑥)𝑅(𝑔‘𝑥)))) |
30 | 28, 29 | ovmpoga 5952 |
. . 3
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) ∈ V) → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) |
31 | 4, 8, 21, 30 | syl3anc 1220 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) |
32 | 14 | eleq2i 2224 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ 𝑥 ∈ 𝑆) |
33 | | elin 3291 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
34 | 32, 33 | bitr3i 185 |
. . . 4
⊢ (𝑥 ∈ 𝑆 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
35 | | offval.6 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶) |
36 | 35 | adantrr 471 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) → (𝐹‘𝑥) = 𝐶) |
37 | | offval.7 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) |
38 | 37 | adantrl 470 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) → (𝐺‘𝑥) = 𝐷) |
39 | 36, 38 | oveq12d 5844 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) → ((𝐹‘𝑥)𝑅(𝐺‘𝑥)) = (𝐶𝑅𝐷)) |
40 | 34, 39 | sylan2b 285 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝐹‘𝑥)𝑅(𝐺‘𝑥)) = (𝐶𝑅𝐷)) |
41 | 40 | mpteq2dva 4056 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) = (𝑥 ∈ 𝑆 ↦ (𝐶𝑅𝐷))) |
42 | 31, 16, 41 | 3eqtrd 2194 |
1
⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ 𝑆 ↦ (𝐶𝑅𝐷))) |