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

Metamath Proof Explorer

Theorem fvproj

Description: Value of a function on ordered pairs with values expressed as ordered pairs. Note that F and G are the projections of H to the first and second coordinate respectively. (Contributed by Thierry Arnoux, 30-Dec-2019)

Ref Expression
Hypotheses fvproj.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ )
fvproj.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
fvproj.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion fvproj ( 𝜑 → ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑌 ) ⟩ )

Proof

Step Hyp Ref Expression
1 fvproj.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ )
2 fvproj.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
3 fvproj.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
4 df-ov ⊢ ( 𝑋 𝐻 𝑌 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
5 fveq2 ⊢ ( 𝑎 = 𝑋 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑋 ) )
6 5 opeq1d ⊢ ( 𝑎 = 𝑋 → ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑏 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑏 ) ⟩ )
7 fveq2 ⊢ ( 𝑏 = 𝑌 → ( 𝐺 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑌 ) )
8 7 opeq2d ⊢ ( 𝑏 = 𝑌 → ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑏 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑌 ) ⟩ )
9 fveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑎 ) )
10 9 opeq1d ⊢ ( 𝑥 = 𝑎 → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑦 ) ⟩ )
11 fveq2 ⊢ ( 𝑦 = 𝑏 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑏 ) )
12 11 opeq2d ⊢ ( 𝑦 = 𝑏 → ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑦 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑏 ) ⟩ )
13 10 12 cbvmpov ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ) = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑏 ) ⟩ )
14 1 13 eqtri ⊢ 𝐻 = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑏 ) ⟩ )
15 opex ⊢ ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑌 ) ⟩ ∈ V
16 6 8 14 15 ovmpo ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐻 𝑌 ) = ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑌 ) ⟩ )
17 2 3 16 syl2anc ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑌 ) ⟩ )
18 4 17 eqtr3id ⊢ ( 𝜑 → ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑌 ) ⟩ )