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

Metamath Proof Explorer

Theorem ofresid

Description: Applying an operation restricted to the range of the functions does not change the function operation. (Contributed by Thierry Arnoux, 14-Feb-2018)

Ref Expression
Hypotheses ofresid.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
ofresid.2 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
ofresid.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion ofresid ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝐹 ∘f ( 𝑅 ↾ ( 𝐵 × 𝐵 ) ) 𝐺 ) )

Proof

Step Hyp Ref Expression
1 ofresid.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 ofresid.2 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
3 ofresid.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 1 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
5 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐵 )
6 4 5 opelxpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ ( 𝐵 × 𝐵 ) )
7 6 fvresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑅 ↾ ( 𝐵 × 𝐵 ) ) ‘ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) = ( 𝑅 ‘ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) )
8 7 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅 ‘ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) = ( ( 𝑅 ↾ ( 𝐵 × 𝐵 ) ) ‘ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) )
9 df-ov ⊢ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) = ( 𝑅 ‘ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ )
10 df-ov ⊢ ( ( 𝐹 ‘ 𝑥 ) ( 𝑅 ↾ ( 𝐵 × 𝐵 ) ) ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝑅 ↾ ( 𝐵 × 𝐵 ) ) ‘ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ )
11 8 9 10 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 𝑅 ↾ ( 𝐵 × 𝐵 ) ) ( 𝐺 ‘ 𝑥 ) ) )
12 11 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ( 𝑅 ↾ ( 𝐵 × 𝐵 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )
13 1 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
14 2 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
15 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
16 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
17 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
18 13 14 3 3 15 16 17 offval ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )
19 13 14 3 3 15 16 17 offval ⊢ ( 𝜑 → ( 𝐹 ∘f ( 𝑅 ↾ ( 𝐵 × 𝐵 ) ) 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ( 𝑅 ↾ ( 𝐵 × 𝐵 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )
20 12 18 19 3eqtr4d ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝐹 ∘f ( 𝑅 ↾ ( 𝐵 × 𝐵 ) ) 𝐺 ) )