xpcfucco3

Description: Value of composition in the binary product of categories of functors; expressed explicitly. (Contributed by Zhi Wang, 1-Oct-2025)

	Ref	Expression
Hypotheses	xpcfuchom2.t	⊢ 𝑇 = ( ( 𝐵 FuncCat 𝐶 ) ×_c ( 𝐷 FuncCat 𝐸 ) )
	xpcfucco2.o	⊢ 𝑂 = ( comp ‘ 𝑇 )
	xpcfucco2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑀 ( 𝐵 Nat 𝐶 ) 𝑃 ) )
	xpcfucco2.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑁 ( 𝐷 Nat 𝐸 ) 𝑄 ) )
	xpcfucco2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 ( 𝐵 Nat 𝐶 ) 𝑅 ) )
	xpcfucco2.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝑄 ( 𝐷 Nat 𝐸 ) 𝑆 ) )
	xpcfucco3.x	⊢ 𝑋 = ( Base ‘ 𝐵 )
	xpcfucco3.y	⊢ 𝑌 = ( Base ‘ 𝐷 )
	xpcfucco3.o1	⊢ · = ( comp ‘ 𝐶 )
	xpcfucco3.o2	⊢ ∙ = ( comp ‘ 𝐸 )
Assertion	xpcfucco3	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ( ⟨ ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑃 , 𝑄 ⟩ ⟩ 𝑂 ⟨ 𝑅 , 𝑆 ⟩ ) ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐾 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑀 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝑅 ) ‘ 𝑥 ) ) ( 𝐹 ‘ 𝑥 ) ) ) , ( 𝑦 ∈ 𝑌 ↦ ( ( 𝐿 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝑁 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝑄 ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ 𝑆 ) ‘ 𝑦 ) ) ( 𝐺 ‘ 𝑦 ) ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		xpcfuchom2.t	⊢ 𝑇 = ( ( 𝐵 FuncCat 𝐶 ) ×_c ( 𝐷 FuncCat 𝐸 ) )
2		xpcfucco2.o	⊢ 𝑂 = ( comp ‘ 𝑇 )
3		xpcfucco2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑀 ( 𝐵 Nat 𝐶 ) 𝑃 ) )
4		xpcfucco2.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑁 ( 𝐷 Nat 𝐸 ) 𝑄 ) )
5		xpcfucco2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 ( 𝐵 Nat 𝐶 ) 𝑅 ) )
6		xpcfucco2.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝑄 ( 𝐷 Nat 𝐸 ) 𝑆 ) )
7		xpcfucco3.x	⊢ 𝑋 = ( Base ‘ 𝐵 )
8		xpcfucco3.y	⊢ 𝑌 = ( Base ‘ 𝐷 )
9		xpcfucco3.o1	⊢ · = ( comp ‘ 𝐶 )
10		xpcfucco3.o2	⊢ ∙ = ( comp ‘ 𝐸 )
11	1 2 3 4 5 6	xpcfucco2	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ( ⟨ ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑃 , 𝑄 ⟩ ⟩ 𝑂 ⟨ 𝑅 , 𝑆 ⟩ ) ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝐾 ( ⟨ 𝑀 , 𝑃 ⟩ ( comp ‘ ( 𝐵 FuncCat 𝐶 ) ) 𝑅 ) 𝐹 ) , ( 𝐿 ( ⟨ 𝑁 , 𝑄 ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐸 ) ) 𝑆 ) 𝐺 ) ⟩ )
12		eqid	⊢ ( 𝐵 FuncCat 𝐶 ) = ( 𝐵 FuncCat 𝐶 )
13		eqid	⊢ ( 𝐵 Nat 𝐶 ) = ( 𝐵 Nat 𝐶 )
14		eqid	⊢ ( comp ‘ ( 𝐵 FuncCat 𝐶 ) ) = ( comp ‘ ( 𝐵 FuncCat 𝐶 ) )
15	12 13 7 9 14 3 5	fucco	⊢ ( 𝜑 → ( 𝐾 ( ⟨ 𝑀 , 𝑃 ⟩ ( comp ‘ ( 𝐵 FuncCat 𝐶 ) ) 𝑅 ) 𝐹 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐾 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑀 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝑅 ) ‘ 𝑥 ) ) ( 𝐹 ‘ 𝑥 ) ) ) )
16		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
17		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
18		eqid	⊢ ( comp ‘ ( 𝐷 FuncCat 𝐸 ) ) = ( comp ‘ ( 𝐷 FuncCat 𝐸 ) )
19	16 17 8 10 18 4 6	fucco	⊢ ( 𝜑 → ( 𝐿 ( ⟨ 𝑁 , 𝑄 ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐸 ) ) 𝑆 ) 𝐺 ) = ( 𝑦 ∈ 𝑌 ↦ ( ( 𝐿 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝑁 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝑄 ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ 𝑆 ) ‘ 𝑦 ) ) ( 𝐺 ‘ 𝑦 ) ) ) )
20	15 19	opeq12d	⊢ ( 𝜑 → ⟨ ( 𝐾 ( ⟨ 𝑀 , 𝑃 ⟩ ( comp ‘ ( 𝐵 FuncCat 𝐶 ) ) 𝑅 ) 𝐹 ) , ( 𝐿 ( ⟨ 𝑁 , 𝑄 ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐸 ) ) 𝑆 ) 𝐺 ) ⟩ = ⟨ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐾 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑀 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝑅 ) ‘ 𝑥 ) ) ( 𝐹 ‘ 𝑥 ) ) ) , ( 𝑦 ∈ 𝑌 ↦ ( ( 𝐿 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝑁 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝑄 ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ 𝑆 ) ‘ 𝑦 ) ) ( 𝐺 ‘ 𝑦 ) ) ) ⟩ )
21	11 20	eqtrd	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ( ⟨ ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑃 , 𝑄 ⟩ ⟩ 𝑂 ⟨ 𝑅 , 𝑆 ⟩ ) ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐾 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑀 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝑅 ) ‘ 𝑥 ) ) ( 𝐹 ‘ 𝑥 ) ) ) , ( 𝑦 ∈ 𝑌 ↦ ( ( 𝐿 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝑁 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝑄 ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ 𝑆 ) ‘ 𝑦 ) ) ( 𝐺 ‘ 𝑦 ) ) ) ⟩ )

Metamath Proof Explorer

Theorem xpcfucco3

Proof