Theorem fvcod

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

	Ref	Expression
Hypotheses	fvcod.g	$$⊢\phi \to \mathrm{Fun}G$$
	fvcod.a	$$⊢\phi \to A\in \mathrm{dom}G$$
	fvcod.h	$$⊢H=F\circ G$$
Assertion	fvcod	$$⊢\phi \to H\left(A\right)=F\left(G\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvcod.g	$$⊢\phi \to \mathrm{Fun}G$$
2		fvcod.a	$$⊢\phi \to A\in \mathrm{dom}G$$
3		fvcod.h	$$⊢H=F\circ G$$
4	3	fveq1i	$$⊢H\left(A\right)=\left(F\circ G\right)\left(A\right)$$
5	4	a1i	$$⊢\phi \to H\left(A\right)=\left(F\circ G\right)\left(A\right)$$
6		fvco	$$⊢\left(\mathrm{Fun}G\wedge A\in \mathrm{dom}G\right)\to \left(F\circ G\right)\left(A\right)=F\left(G\left(A\right)\right)$$
7	1 2 6	syl2anc	$$⊢\phi \to \left(F\circ G\right)\left(A\right)=F\left(G\left(A\right)\right)$$
8	5 7	eqtrd	$$⊢\phi \to H\left(A\right)=F\left(G\left(A\right)\right)$$