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	⊢ ( 𝜑 → ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐺 ‘ 𝑌 ) ⟩ )