Theorem offveq

Description: Convert an identity of the operation to the analogous identity on the function operation. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Hypotheses	offveq.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	offveq.2	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	offveq.3	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
	offveq.4	⊢ ( 𝜑 → 𝐻 Fn 𝐴 )
	offveq.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
	offveq.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = 𝐶 )
	offveq.7	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 𝑅 𝐶 ) = ( 𝐻 ‘ 𝑥 ) )
Assertion	offveq	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		offveq.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		offveq.2	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
3		offveq.3	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
4		offveq.4	⊢ ( 𝜑 → 𝐻 Fn 𝐴 )
5		offveq.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
6		offveq.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = 𝐶 )
7		offveq.7	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 𝑅 𝐶 ) = ( 𝐻 ‘ 𝑥 ) )
8		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
9	2 3 1 1 8	offn	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) Fn 𝐴 )
10	2 3 1 1 8 5 6	ofval	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑥 ) = ( 𝐵 𝑅 𝐶 ) )
11	10 7	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) )
12	9 4 11	eqfnfvd	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = 𝐻 )