# Metamath Proof Explorer

## Theorem fvovco

Description: Value of the composition of an operator, with a given function. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses fvovco.1 ( 𝜑𝐹 : 𝑋 ⟶ ( 𝑉 × 𝑊 ) )
fvovco.2 ( 𝜑𝑌𝑋 )
Assertion fvovco ( 𝜑 → ( ( 𝑂𝐹 ) ‘ 𝑌 ) = ( ( 1st ‘ ( 𝐹𝑌 ) ) 𝑂 ( 2nd ‘ ( 𝐹𝑌 ) ) ) )

### Proof

Step Hyp Ref Expression
1 fvovco.1 ( 𝜑𝐹 : 𝑋 ⟶ ( 𝑉 × 𝑊 ) )
2 fvovco.2 ( 𝜑𝑌𝑋 )
3 1 2 ffvelrnd ( 𝜑 → ( 𝐹𝑌 ) ∈ ( 𝑉 × 𝑊 ) )
4 1st2nd2 ( ( 𝐹𝑌 ) ∈ ( 𝑉 × 𝑊 ) → ( 𝐹𝑌 ) = ⟨ ( 1st ‘ ( 𝐹𝑌 ) ) , ( 2nd ‘ ( 𝐹𝑌 ) ) ⟩ )
5 3 4 syl ( 𝜑 → ( 𝐹𝑌 ) = ⟨ ( 1st ‘ ( 𝐹𝑌 ) ) , ( 2nd ‘ ( 𝐹𝑌 ) ) ⟩ )
6 5 fveq2d ( 𝜑 → ( 𝑂 ‘ ( 𝐹𝑌 ) ) = ( 𝑂 ‘ ⟨ ( 1st ‘ ( 𝐹𝑌 ) ) , ( 2nd ‘ ( 𝐹𝑌 ) ) ⟩ ) )
7 fvco3 ( ( 𝐹 : 𝑋 ⟶ ( 𝑉 × 𝑊 ) ∧ 𝑌𝑋 ) → ( ( 𝑂𝐹 ) ‘ 𝑌 ) = ( 𝑂 ‘ ( 𝐹𝑌 ) ) )
8 1 2 7 syl2anc ( 𝜑 → ( ( 𝑂𝐹 ) ‘ 𝑌 ) = ( 𝑂 ‘ ( 𝐹𝑌 ) ) )
9 df-ov ( ( 1st ‘ ( 𝐹𝑌 ) ) 𝑂 ( 2nd ‘ ( 𝐹𝑌 ) ) ) = ( 𝑂 ‘ ⟨ ( 1st ‘ ( 𝐹𝑌 ) ) , ( 2nd ‘ ( 𝐹𝑌 ) ) ⟩ )
10 9 a1i ( 𝜑 → ( ( 1st ‘ ( 𝐹𝑌 ) ) 𝑂 ( 2nd ‘ ( 𝐹𝑌 ) ) ) = ( 𝑂 ‘ ⟨ ( 1st ‘ ( 𝐹𝑌 ) ) , ( 2nd ‘ ( 𝐹𝑌 ) ) ⟩ ) )
11 6 8 10 3eqtr4d ( 𝜑 → ( ( 𝑂𝐹 ) ‘ 𝑌 ) = ( ( 1st ‘ ( 𝐹𝑌 ) ) 𝑂 ( 2nd ‘ ( 𝐹𝑌 ) ) ) )