Metamath Proof Explorer

Theorem offval

Description: Value of an operation applied to two functions. (Contributed by Mario Carneiro, 20-Jul-2014)

Ref Expression
Hypotheses offval.1 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
offval.2 ⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
offval.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
offval.4 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
offval.5 ⊢ ( 𝐴 ∩ 𝐵 ) = 𝑆
offval.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 )
offval.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑥 ) = 𝐷 )
Assertion offval ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝑆 ↦ ( 𝐶 𝑅 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 offval.1 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2 offval.2 ⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
3 offval.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 offval.4 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
5 offval.5 ⊢ ( 𝐴 ∩ 𝐵 ) = 𝑆
6 offval.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 )
7 offval.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑥 ) = 𝐷 )
8 fnex ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
9 1 3 8 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ V )
10 fnex ⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐵 ∈ 𝑊 ) → 𝐺 ∈ V )
11 2 4 10 syl2anc ⊢ ( 𝜑 → 𝐺 ∈ V )
12 1 fndmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
13 2 fndmd ⊢ ( 𝜑 → dom 𝐺 = 𝐵 )
14 12 13 ineq12d ⊢ ( 𝜑 → ( dom 𝐹 ∩ dom 𝐺 ) = ( 𝐴 ∩ 𝐵 ) )
15 14 5 eqtrdi ⊢ ( 𝜑 → ( dom 𝐹 ∩ dom 𝐺 ) = 𝑆 )
16 15 mpteq1d ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )
17 inex1g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ 𝐵 ) ∈ V )
18 5 17 eqeltrrid ⊢ ( 𝐴 ∈ 𝑉 → 𝑆 ∈ V )
19 mptexg ⊢ ( 𝑆 ∈ V → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ∈ V )
20 3 18 19 3syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ∈ V )
21 16 20 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ∈ V )
22 dmeq ⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
23 dmeq ⊢ ( 𝑔 = 𝐺 → dom 𝑔 = dom 𝐺 )
24 22 23 ineqan12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( dom 𝑓 ∩ dom 𝑔 ) = ( dom 𝐹 ∩ dom 𝐺 ) )
25 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
26 fveq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
27 25 26 oveqan12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) )
28 24 27 mpteq12dv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )
29 df-of ⊢ ∘f 𝑅 = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
30 28 29 ovmpoga ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ∧ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ∈ V ) → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )
31 9 11 21 30 syl3anc ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )
32 5 eleq2i ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ 𝑥 ∈ 𝑆 )
33 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
34 32 33 bitr3i ⊢ ( 𝑥 ∈ 𝑆 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
35 6 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 )
36 7 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝐺 ‘ 𝑥 ) = 𝐷 )
37 35 36 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) = ( 𝐶 𝑅 𝐷 ) )
38 34 37 sylan2b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) = ( 𝐶 𝑅 𝐷 ) )
39 38 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( 𝐶 𝑅 𝐷 ) ) )
40 31 16 39 3eqtrd ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝑆 ↦ ( 𝐶 𝑅 𝐷 ) ) )