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 𝑅 𝐺 ) = ( 𝑥𝑆 ↦ ( 𝐶 𝑅 𝐷 ) ) )