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

Metamath Proof Explorer

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 𝑅 𝐺 ) = 𝐻 )