Theorem fvcod

Description: Value of a function composition. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	fvcod.g	⊢ ( 𝜑 → Fun 𝐺 )
	fvcod.a	⊢ ( 𝜑 → 𝐴 ∈ dom 𝐺 )
	fvcod.h	⊢ 𝐻 = ( 𝐹 ∘ 𝐺 )
Assertion	fvcod	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fvcod.g	⊢ ( 𝜑 → Fun 𝐺 )
2		fvcod.a	⊢ ( 𝜑 → 𝐴 ∈ dom 𝐺 )
3		fvcod.h	⊢ 𝐻 = ( 𝐹 ∘ 𝐺 )
4	3	fveq1i	⊢ ( 𝐻 ‘ 𝐴 ) = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐴 )
5	4	a1i	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐴 ) = ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐴 ) )
6		fvco	⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐴 ) ) )
7	1 2 6	syl2anc	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐴 ) ) )
8	5 7	eqtrd	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐴 ) ) )