cofuval

Description: Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	cofuval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	cofuval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	cofuval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
Assertion	cofuval	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) = ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		cofuval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		cofuval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
3		cofuval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
4		df-cofu	⊢ ∘_func = ( 𝑔 ∈ V , 𝑓 ∈ V ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ )
5	4	a1i	⊢ ( 𝜑 → ∘_func = ( 𝑔 ∈ V , 𝑓 ∈ V ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ ) )
6		simprl	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → 𝑔 = 𝐺 )
7	6	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 1^st ‘ 𝑔 ) = ( 1^st ‘ 𝐺 ) )
8		simprr	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → 𝑓 = 𝐹 )
9	8	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 1^st ‘ 𝑓 ) = ( 1^st ‘ 𝐹 ) )
10	7 9	coeq12d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) = ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) )
11	8	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 2^nd ‘ 𝑓 ) = ( 2^nd ‘ 𝐹 ) )
12	11	dmeqd	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → dom ( 2^nd ‘ 𝑓 ) = dom ( 2^nd ‘ 𝐹 ) )
13		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
14		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
15	13 2 14	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
16	1 15	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ 𝐹 ) Fn ( 𝐵 × 𝐵 ) )
17	16	fndmd	⊢ ( 𝜑 → dom ( 2^nd ‘ 𝐹 ) = ( 𝐵 × 𝐵 ) )
18	17	adantr	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → dom ( 2^nd ‘ 𝐹 ) = ( 𝐵 × 𝐵 ) )
19	12 18	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → dom ( 2^nd ‘ 𝑓 ) = ( 𝐵 × 𝐵 ) )
20	19	dmeqd	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → dom dom ( 2^nd ‘ 𝑓 ) = dom ( 𝐵 × 𝐵 ) )
21		dmxpid	⊢ dom ( 𝐵 × 𝐵 ) = 𝐵
22	20 21	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → dom dom ( 2^nd ‘ 𝑓 ) = 𝐵 )
23	6	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 2^nd ‘ 𝑔 ) = ( 2^nd ‘ 𝐺 ) )
24	9	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) )
25	9	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) )
26	23 24 25	oveq123d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
27	11	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) = ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) )
28	26 27	coeq12d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) )
29	22 22 28	mpoeq123dv	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) )
30	10 29	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ⟨ ( ( 1^st ‘ 𝑔 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2^nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2^nd ‘ 𝑓 ) ↦ ( ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ) ) ⟩ = ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ )
31	3	elexd	⊢ ( 𝜑 → 𝐺 ∈ V )
32	2	elexd	⊢ ( 𝜑 → 𝐹 ∈ V )
33		opex	⊢ ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ ∈ V
34	33	a1i	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ ∈ V )
35	5 30 31 32 34	ovmpod	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) = ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ )

Metamath Proof Explorer

Theorem cofuval

Proof