Step | Hyp | Ref
| Expression |
1 | | offval.1 |
. . . . 5
⊢ (𝜑 → 𝐹 Fn 𝐴) |
2 | | offval.2 |
. . . . 5
⊢ (𝜑 → 𝐺 Fn 𝐵) |
3 | | offval.3 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
4 | | offval.4 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
5 | | offval.5 |
. . . . 5
⊢ (𝐴 ∩ 𝐵) = 𝑆 |
6 | | eqidd 2041 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
7 | | eqidd 2041 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
8 | 1, 2, 3, 4, 5, 6, 7 | offval 5719 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) |
9 | 8 | fveq1d 5180 |
. . 3
⊢ (𝜑 → ((𝐹 ∘𝑓 𝑅𝐺)‘𝑋) = ((𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))‘𝑋)) |
10 | 9 | adantr 261 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹 ∘𝑓 𝑅𝐺)‘𝑋) = ((𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))‘𝑋)) |
11 | | simpr 103 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆) |
12 | | ofval.8 |
. . . . 5
⊢ (𝜑 → 𝑅 Fn (𝑈 × 𝑉)) |
13 | 12 | adantr 261 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → 𝑅 Fn (𝑈 × 𝑉)) |
14 | | ofval.9 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑈) |
15 | 14 | adantr 261 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → 𝐶 ∈ 𝑈) |
16 | | inss1 3157 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
17 | 5, 16 | eqsstr3i 2976 |
. . . . . . . 8
⊢ 𝑆 ⊆ 𝐴 |
18 | 17 | sseli 2941 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐴) |
19 | | ofval.6 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) |
20 | 18, 19 | sylan2 270 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) = 𝐶) |
21 | 20 | eleq1d 2106 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹‘𝑋) ∈ 𝑈 ↔ 𝐶 ∈ 𝑈)) |
22 | 15, 21 | mpbird 156 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ 𝑈) |
23 | | ofval.10 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
24 | 23 | adantr 261 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → 𝐷 ∈ 𝑉) |
25 | | inss2 3158 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 |
26 | 5, 25 | eqsstr3i 2976 |
. . . . . . . 8
⊢ 𝑆 ⊆ 𝐵 |
27 | 26 | sseli 2941 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐵) |
28 | | ofval.7 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷) |
29 | 27, 28 | sylan2 270 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → (𝐺‘𝑋) = 𝐷) |
30 | 29 | eleq1d 2106 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐺‘𝑋) ∈ 𝑉 ↔ 𝐷 ∈ 𝑉)) |
31 | 24, 30 | mpbird 156 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → (𝐺‘𝑋) ∈ 𝑉) |
32 | | fnovex 5538 |
. . . 4
⊢ ((𝑅 Fn (𝑈 × 𝑉) ∧ (𝐹‘𝑋) ∈ 𝑈 ∧ (𝐺‘𝑋) ∈ 𝑉) → ((𝐹‘𝑋)𝑅(𝐺‘𝑋)) ∈ V) |
33 | 13, 22, 31, 32 | syl3anc 1135 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹‘𝑋)𝑅(𝐺‘𝑋)) ∈ V) |
34 | | fveq2 5178 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) |
35 | | fveq2 5178 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝐺‘𝑥) = (𝐺‘𝑋)) |
36 | 34, 35 | oveq12d 5530 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥)𝑅(𝐺‘𝑥)) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋))) |
37 | | eqid 2040 |
. . . 4
⊢ (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) = (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) |
38 | 36, 37 | fvmptg 5248 |
. . 3
⊢ ((𝑋 ∈ 𝑆 ∧ ((𝐹‘𝑋)𝑅(𝐺‘𝑋)) ∈ V) → ((𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))‘𝑋) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋))) |
39 | 11, 33, 38 | syl2anc 391 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))‘𝑋) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋))) |
40 | 20, 29 | oveq12d 5530 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹‘𝑋)𝑅(𝐺‘𝑋)) = (𝐶𝑅𝐷)) |
41 | 10, 39, 40 | 3eqtrd 2076 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹 ∘𝑓 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷)) |