This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑅 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )