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

Metamath Proof Explorer

Theorem offres

Description: Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Assertion offres ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ↾ 𝐷 ) = ( ( 𝐹 ↾ 𝐷 ) ∘f 𝑅 ( 𝐺 ↾ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 elinel2 ⊢ ( 𝑥 ∈ ( ( dom 𝐹 ∩ dom 𝐺 ) ∩ 𝐷 ) → 𝑥 ∈ 𝐷 )
2 fvres ⊢ ( 𝑥 ∈ 𝐷 → ( ( 𝐹 ↾ 𝐷 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
3 fvres ⊢ ( 𝑥 ∈ 𝐷 → ( ( 𝐺 ↾ 𝐷 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
4 2 3 oveq12d ⊢ ( 𝑥 ∈ 𝐷 → ( ( ( 𝐹 ↾ 𝐷 ) ‘ 𝑥 ) 𝑅 ( ( 𝐺 ↾ 𝐷 ) ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) )
5 1 4 syl ⊢ ( 𝑥 ∈ ( ( dom 𝐹 ∩ dom 𝐺 ) ∩ 𝐷 ) → ( ( ( 𝐹 ↾ 𝐷 ) ‘ 𝑥 ) 𝑅 ( ( 𝐺 ↾ 𝐷 ) ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) )
6 5 mpteq2ia ⊢ ( 𝑥 ∈ ( ( dom 𝐹 ∩ dom 𝐺 ) ∩ 𝐷 ) ↦ ( ( ( 𝐹 ↾ 𝐷 ) ‘ 𝑥 ) 𝑅 ( ( 𝐺 ↾ 𝐷 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( ( dom 𝐹 ∩ dom 𝐺 ) ∩ 𝐷 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) )
7 inindi ⊢ ( 𝐷 ∩ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( ( 𝐷 ∩ dom 𝐹 ) ∩ ( 𝐷 ∩ dom 𝐺 ) )
8 incom ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) ∩ 𝐷 ) = ( 𝐷 ∩ ( dom 𝐹 ∩ dom 𝐺 ) )
9 dmres ⊢ dom ( 𝐹 ↾ 𝐷 ) = ( 𝐷 ∩ dom 𝐹 )
10 dmres ⊢ dom ( 𝐺 ↾ 𝐷 ) = ( 𝐷 ∩ dom 𝐺 )
11 9 10 ineq12i ⊢ ( dom ( 𝐹 ↾ 𝐷 ) ∩ dom ( 𝐺 ↾ 𝐷 ) ) = ( ( 𝐷 ∩ dom 𝐹 ) ∩ ( 𝐷 ∩ dom 𝐺 ) )
12 7 8 11 3eqtr4ri ⊢ ( dom ( 𝐹 ↾ 𝐷 ) ∩ dom ( 𝐺 ↾ 𝐷 ) ) = ( ( dom 𝐹 ∩ dom 𝐺 ) ∩ 𝐷 )
13 12 mpteq1i ⊢ ( 𝑥 ∈ ( dom ( 𝐹 ↾ 𝐷 ) ∩ dom ( 𝐺 ↾ 𝐷 ) ) ↦ ( ( ( 𝐹 ↾ 𝐷 ) ‘ 𝑥 ) 𝑅 ( ( 𝐺 ↾ 𝐷 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( ( dom 𝐹 ∩ dom 𝐺 ) ∩ 𝐷 ) ↦ ( ( ( 𝐹 ↾ 𝐷 ) ‘ 𝑥 ) 𝑅 ( ( 𝐺 ↾ 𝐷 ) ‘ 𝑥 ) ) )
14 resmpt3 ⊢ ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ↾ 𝐷 ) = ( 𝑥 ∈ ( ( dom 𝐹 ∩ dom 𝐺 ) ∩ 𝐷 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) )
15 6 13 14 3eqtr4ri ⊢ ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ↾ 𝐷 ) = ( 𝑥 ∈ ( dom ( 𝐹 ↾ 𝐷 ) ∩ dom ( 𝐺 ↾ 𝐷 ) ) ↦ ( ( ( 𝐹 ↾ 𝐷 ) ‘ 𝑥 ) 𝑅 ( ( 𝐺 ↾ 𝐷 ) ‘ 𝑥 ) ) )
16 offval3 ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )
17 16 reseq1d ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ↾ 𝐷 ) = ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ↾ 𝐷 ) )
18 resexg ⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ↾ 𝐷 ) ∈ V )
19 resexg ⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ↾ 𝐷 ) ∈ V )
20 offval3 ⊢ ( ( ( 𝐹 ↾ 𝐷 ) ∈ V ∧ ( 𝐺 ↾ 𝐷 ) ∈ V ) → ( ( 𝐹 ↾ 𝐷 ) ∘f 𝑅 ( 𝐺 ↾ 𝐷 ) ) = ( 𝑥 ∈ ( dom ( 𝐹 ↾ 𝐷 ) ∩ dom ( 𝐺 ↾ 𝐷 ) ) ↦ ( ( ( 𝐹 ↾ 𝐷 ) ‘ 𝑥 ) 𝑅 ( ( 𝐺 ↾ 𝐷 ) ‘ 𝑥 ) ) ) )
21 18 19 20 syl2an ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( 𝐹 ↾ 𝐷 ) ∘f 𝑅 ( 𝐺 ↾ 𝐷 ) ) = ( 𝑥 ∈ ( dom ( 𝐹 ↾ 𝐷 ) ∩ dom ( 𝐺 ↾ 𝐷 ) ) ↦ ( ( ( 𝐹 ↾ 𝐷 ) ‘ 𝑥 ) 𝑅 ( ( 𝐺 ↾ 𝐷 ) ‘ 𝑥 ) ) ) )
22 15 17 21 3eqtr4a ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ↾ 𝐷 ) = ( ( 𝐹 ↾ 𝐷 ) ∘f 𝑅 ( 𝐺 ↾ 𝐷 ) ) )