xpcco

Description: Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	xpccofval.t	⊢ 𝑇 = ( 𝐶 ×_c 𝐷 )
	xpccofval.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
	xpccofval.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
	xpccofval.o1	⊢ · = ( comp ‘ 𝐶 )
	xpccofval.o2	⊢ ∙ = ( comp ‘ 𝐷 )
	xpccofval.o	⊢ 𝑂 = ( comp ‘ 𝑇 )
	xpcco.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	xpcco.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	xpcco.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	xpcco.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐾 𝑌 ) )
	xpcco.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐾 𝑍 ) )
Assertion	xpcco	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) 𝐹 ) = ⟨ ( ( 1^st ‘ 𝐺 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ · ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝐹 ) ) , ( ( 2^nd ‘ 𝐺 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ∙ ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝐹 ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		xpccofval.t	⊢ 𝑇 = ( 𝐶 ×_c 𝐷 )
2		xpccofval.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
3		xpccofval.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
4		xpccofval.o1	⊢ · = ( comp ‘ 𝐶 )
5		xpccofval.o2	⊢ ∙ = ( comp ‘ 𝐷 )
6		xpccofval.o	⊢ 𝑂 = ( comp ‘ 𝑇 )
7		xpcco.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		xpcco.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9		xpcco.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
10		xpcco.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐾 𝑌 ) )
11		xpcco.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐾 𝑍 ) )
12	1 2 3 4 5 6	xpccofval	⊢ 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
13	7 8	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
14	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ) → 𝑍 ∈ 𝐵 )
15		ovex	⊢ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) ∈ V
16		fvex	⊢ ( 𝐾 ‘ 𝑥 ) ∈ V
17	15 16	mpoex	⊢ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ∈ V
18	17	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ∈ V )
19	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → 𝐺 ∈ ( 𝑌 𝐾 𝑍 ) )
20		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ )
21	20	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
22		op2ndg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
23	7 8 22	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
24	23	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
25	21 24	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → ( 2^nd ‘ 𝑥 ) = 𝑌 )
26		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → 𝑦 = 𝑍 )
27	25 26	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) = ( 𝑌 𝐾 𝑍 ) )
28	19 27	eleqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → 𝐺 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) )
29	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → 𝐹 ∈ ( 𝑋 𝐾 𝑌 ) )
30	20	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → ( 𝐾 ‘ 𝑥 ) = ( 𝐾 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
31		df-ov	⊢ ( 𝑋 𝐾 𝑌 ) = ( 𝐾 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
32	30 31	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → ( 𝐾 ‘ 𝑥 ) = ( 𝑋 𝐾 𝑌 ) )
33	29 32	eleqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → 𝐹 ∈ ( 𝐾 ‘ 𝑥 ) )
34	33	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ 𝑔 = 𝐺 ) → 𝐹 ∈ ( 𝐾 ‘ 𝑥 ) )
35		opex	⊢ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ∈ V
36	35	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ∈ V )
37	20	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → ( 1^st ‘ 𝑥 ) = ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
38		op1stg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
39	7 8 38	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
40	39	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
41	37 40	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → ( 1^st ‘ 𝑥 ) = 𝑋 )
42	41	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 1^st ‘ 𝑥 ) = 𝑋 )
43	42	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ 𝑋 ) )
44	25	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 2^nd ‘ 𝑥 ) = 𝑌 )
45	44	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) = ( 1^st ‘ 𝑌 ) )
46	43 45	opeq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ = ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ )
47		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → 𝑦 = 𝑍 )
48	47	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 1^st ‘ 𝑦 ) = ( 1^st ‘ 𝑍 ) )
49	46 48	oveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) = ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ · ( 1^st ‘ 𝑍 ) ) )
50		simprl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → 𝑔 = 𝐺 )
51	50	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 1^st ‘ 𝑔 ) = ( 1^st ‘ 𝐺 ) )
52		simprr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → 𝑓 = 𝐹 )
53	52	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 1^st ‘ 𝑓 ) = ( 1^st ‘ 𝐹 ) )
54	49 51 53	oveq123d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) = ( ( 1^st ‘ 𝐺 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ · ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝐹 ) ) )
55	42	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = ( 2^nd ‘ 𝑋 ) )
56	44	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) = ( 2^nd ‘ 𝑌 ) )
57	55 56	opeq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ = ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ )
58	47	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 2^nd ‘ 𝑦 ) = ( 2^nd ‘ 𝑍 ) )
59	57 58	oveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) = ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ∙ ( 2^nd ‘ 𝑍 ) ) )
60	50	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 2^nd ‘ 𝑔 ) = ( 2^nd ‘ 𝐺 ) )
61	52	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 2^nd ‘ 𝑓 ) = ( 2^nd ‘ 𝐹 ) )
62	59 60 61	oveq123d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) = ( ( 2^nd ‘ 𝐺 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ∙ ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝐹 ) ) )
63	54 62	opeq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ = ⟨ ( ( 1^st ‘ 𝐺 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ · ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝐹 ) ) , ( ( 2^nd ‘ 𝐺 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ∙ ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝐹 ) ) ⟩ )
64	28 34 36 63	ovmpodv2	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑦 = 𝑍 ) ) → ( ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) = ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) 𝐹 ) = ⟨ ( ( 1^st ‘ 𝐺 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ · ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝐹 ) ) , ( ( 2^nd ‘ 𝐺 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ∙ ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝐹 ) ) ⟩ ) )
65	13 14 18 64	ovmpodv	⊢ ( 𝜑 → ( 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) 𝐹 ) = ⟨ ( ( 1^st ‘ 𝐺 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ · ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝐹 ) ) , ( ( 2^nd ‘ 𝐺 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ∙ ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝐹 ) ) ⟩ ) )
66	12 65	mpi	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) 𝐹 ) = ⟨ ( ( 1^st ‘ 𝐺 ) ( ⟨ ( 1^st ‘ 𝑋 ) , ( 1^st ‘ 𝑌 ) ⟩ · ( 1^st ‘ 𝑍 ) ) ( 1^st ‘ 𝐹 ) ) , ( ( 2^nd ‘ 𝐺 ) ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 2^nd ‘ 𝑌 ) ⟩ ∙ ( 2^nd ‘ 𝑍 ) ) ( 2^nd ‘ 𝐹 ) ) ⟩ )

Metamath Proof Explorer

Theorem xpcco

Proof