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

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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) ∈ ( 𝑉 × 𝑊 ) )
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 ‘ ( 𝐹 ‘ 𝑌 ) ) ) )