Metamath Proof Explorer


Theorem offvalfv

Description: The function operation expressed as a mapping with function values. (Contributed by AV, 6-Apr-2019)

Ref Expression
Hypotheses offvalfv.a ( 𝜑𝐴𝑉 )
offvalfv.f ( 𝜑𝐹 Fn 𝐴 )
offvalfv.g ( 𝜑𝐺 Fn 𝐴 )
Assertion offvalfv ( 𝜑 → ( 𝐹f 𝑅 𝐺 ) = ( 𝑥𝐴 ↦ ( ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 offvalfv.a ( 𝜑𝐴𝑉 )
2 offvalfv.f ( 𝜑𝐹 Fn 𝐴 )
3 offvalfv.g ( 𝜑𝐺 Fn 𝐴 )
4 fnfvelrn ( ( 𝐹 Fn 𝐴𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ ran 𝐹 )
5 2 4 sylan ( ( 𝜑𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ ran 𝐹 )
6 fnfvelrn ( ( 𝐺 Fn 𝐴𝑥𝐴 ) → ( 𝐺𝑥 ) ∈ ran 𝐺 )
7 3 6 sylan ( ( 𝜑𝑥𝐴 ) → ( 𝐺𝑥 ) ∈ ran 𝐺 )
8 dffn5 ( 𝐹 Fn 𝐴𝐹 = ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) )
9 2 8 sylib ( 𝜑𝐹 = ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) )
10 dffn5 ( 𝐺 Fn 𝐴𝐺 = ( 𝑥𝐴 ↦ ( 𝐺𝑥 ) ) )
11 3 10 sylib ( 𝜑𝐺 = ( 𝑥𝐴 ↦ ( 𝐺𝑥 ) ) )
12 1 5 7 9 11 offval2 ( 𝜑 → ( 𝐹f 𝑅 𝐺 ) = ( 𝑥𝐴 ↦ ( ( 𝐹𝑥 ) 𝑅 ( 𝐺𝑥 ) ) ) )