Metamath Proof Explorer


Theorem ofcfval

Description: Value of an operation applied to a function and a constant. (Contributed by Thierry Arnoux, 30-Jan-2017)

Ref Expression
Hypotheses ofcfval.1 ( 𝜑𝐹 Fn 𝐴 )
ofcfval.2 ( 𝜑𝐴𝑉 )
ofcfval.3 ( 𝜑𝐶𝑊 )
ofcfval.6 ( ( 𝜑𝑥𝐴 ) → ( 𝐹𝑥 ) = 𝐵 )
Assertion ofcfval ( 𝜑 → ( 𝐹f/c 𝑅 𝐶 ) = ( 𝑥𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ofcfval.1 ( 𝜑𝐹 Fn 𝐴 )
2 ofcfval.2 ( 𝜑𝐴𝑉 )
3 ofcfval.3 ( 𝜑𝐶𝑊 )
4 ofcfval.6 ( ( 𝜑𝑥𝐴 ) → ( 𝐹𝑥 ) = 𝐵 )
5 df-ofc f/c 𝑅 = ( 𝑓 ∈ V , 𝑐 ∈ V ↦ ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓𝑥 ) 𝑅 𝑐 ) ) )
6 5 a1i ( 𝜑 → ∘f/c 𝑅 = ( 𝑓 ∈ V , 𝑐 ∈ V ↦ ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓𝑥 ) 𝑅 𝑐 ) ) ) )
7 simprl ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑐 = 𝐶 ) ) → 𝑓 = 𝐹 )
8 7 dmeqd ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑐 = 𝐶 ) ) → dom 𝑓 = dom 𝐹 )
9 7 fveq1d ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑐 = 𝐶 ) ) → ( 𝑓𝑥 ) = ( 𝐹𝑥 ) )
10 simprr ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑐 = 𝐶 ) ) → 𝑐 = 𝐶 )
11 9 10 oveq12d ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑐 = 𝐶 ) ) → ( ( 𝑓𝑥 ) 𝑅 𝑐 ) = ( ( 𝐹𝑥 ) 𝑅 𝐶 ) )
12 8 11 mpteq12dv ( ( 𝜑 ∧ ( 𝑓 = 𝐹𝑐 = 𝐶 ) ) → ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓𝑥 ) 𝑅 𝑐 ) ) = ( 𝑥 ∈ dom 𝐹 ↦ ( ( 𝐹𝑥 ) 𝑅 𝐶 ) ) )
13 fnex ( ( 𝐹 Fn 𝐴𝐴𝑉 ) → 𝐹 ∈ V )
14 1 2 13 syl2anc ( 𝜑𝐹 ∈ V )
15 3 elexd ( 𝜑𝐶 ∈ V )
16 1 fndmd ( 𝜑 → dom 𝐹 = 𝐴 )
17 16 2 eqeltrd ( 𝜑 → dom 𝐹𝑉 )
18 17 mptexd ( 𝜑 → ( 𝑥 ∈ dom 𝐹 ↦ ( ( 𝐹𝑥 ) 𝑅 𝐶 ) ) ∈ V )
19 6 12 14 15 18 ovmpod ( 𝜑 → ( 𝐹f/c 𝑅 𝐶 ) = ( 𝑥 ∈ dom 𝐹 ↦ ( ( 𝐹𝑥 ) 𝑅 𝐶 ) ) )
20 16 eleq2d ( 𝜑 → ( 𝑥 ∈ dom 𝐹𝑥𝐴 ) )
21 20 pm5.32i ( ( 𝜑𝑥 ∈ dom 𝐹 ) ↔ ( 𝜑𝑥𝐴 ) )
22 21 4 sylbi ( ( 𝜑𝑥 ∈ dom 𝐹 ) → ( 𝐹𝑥 ) = 𝐵 )
23 22 oveq1d ( ( 𝜑𝑥 ∈ dom 𝐹 ) → ( ( 𝐹𝑥 ) 𝑅 𝐶 ) = ( 𝐵 𝑅 𝐶 ) )
24 16 23 mpteq12dva ( 𝜑 → ( 𝑥 ∈ dom 𝐹 ↦ ( ( 𝐹𝑥 ) 𝑅 𝐶 ) ) = ( 𝑥𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )
25 19 24 eqtrd ( 𝜑 → ( 𝐹f/c 𝑅 𝐶 ) = ( 𝑥𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )