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

Metamath Proof Explorer

Theorem resfval2

Description: Value of the functor restriction operator. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses resfval.c ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
resfval.d ⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
resfval2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑋 )
resfval2.d ⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
Assertion resfval2 ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ↾f 𝐻 ) = ⟨ ( 𝐹 ↾ 𝑆 ) , ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ( ( 𝑥 𝐺 𝑦 ) ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )

Proof

Step Hyp Ref Expression
1 resfval.c ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2 resfval.d ⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
3 resfval2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑋 )
4 resfval2.d ⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
5 opex ⊢ ⟨ 𝐹 , 𝐺 ⟩ ∈ V
6 5 a1i ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ V )
7 6 2 resfval ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ↾f 𝐻 ) = ⟨ ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ↾ dom dom 𝐻 ) , ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ )
8 op1stg ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑋 ) → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
9 1 3 8 syl2anc ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
10 4 fndmd ⊢ ( 𝜑 → dom 𝐻 = ( 𝑆 × 𝑆 ) )
11 10 dmeqd ⊢ ( 𝜑 → dom dom 𝐻 = dom ( 𝑆 × 𝑆 ) )
12 dmxpid ⊢ dom ( 𝑆 × 𝑆 ) = 𝑆
13 11 12 eqtrdi ⊢ ( 𝜑 → dom dom 𝐻 = 𝑆 )
14 9 13 reseq12d ⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ↾ dom dom 𝐻 ) = ( 𝐹 ↾ 𝑆 ) )
15 op2ndg ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑋 ) → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
16 1 3 15 syl2anc ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
17 16 fveq1d ⊢ ( 𝜑 → ( ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
18 17 reseq1d ⊢ ( 𝜑 → ( ( ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) = ( ( 𝐺 ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) )
19 10 18 mpteq12dv ⊢ ( 𝜑 → ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝑆 × 𝑆 ) ↦ ( ( 𝐺 ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) )
20 fveq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
21 df-ov ⊢ ( 𝑥 𝐺 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
22 20 21 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐺 ‘ 𝑧 ) = ( 𝑥 𝐺 𝑦 ) )
23 fveq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
24 df-ov ⊢ ( 𝑥 𝐻 𝑦 ) = ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
25 23 24 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐻 ‘ 𝑧 ) = ( 𝑥 𝐻 𝑦 ) )
26 22 25 reseq12d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐺 ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) = ( ( 𝑥 𝐺 𝑦 ) ↾ ( 𝑥 𝐻 𝑦 ) ) )
27 26 mpompt ⊢ ( 𝑧 ∈ ( 𝑆 × 𝑆 ) ↦ ( ( 𝐺 ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ( ( 𝑥 𝐺 𝑦 ) ↾ ( 𝑥 𝐻 𝑦 ) ) )
28 19 27 eqtrdi ⊢ ( 𝜑 → ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ( ( 𝑥 𝐺 𝑦 ) ↾ ( 𝑥 𝐻 𝑦 ) ) ) )
29 14 28 opeq12d ⊢ ( 𝜑 → ⟨ ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ↾ dom dom 𝐻 ) , ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑧 ) ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ = ⟨ ( 𝐹 ↾ 𝑆 ) , ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ( ( 𝑥 𝐺 𝑦 ) ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )
30 7 29 eqtrd ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ↾f 𝐻 ) = ⟨ ( 𝐹 ↾ 𝑆 ) , ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ( ( 𝑥 𝐺 𝑦 ) ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )