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 ‘ ( 𝐹 ‘ 𝑌 ) ) ) )