fuccoval

Description: Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	fucco.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fucco.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	fucco.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	fucco.o	⊢ · = ( comp ‘ 𝐷 )
	fucco.x	⊢ ∙ = ( comp ‘ 𝑄 )
	fucco.f	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) )
	fucco.g	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐺 𝑁 𝐻 ) )
	fuccoval.f	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
Assertion	fuccoval	⊢ ( 𝜑 → ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑋 ) = ( ( 𝑆 ‘ 𝑋 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑋 ) ) ( 𝑅 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucco.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		fucco.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
3		fucco.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
4		fucco.o	⊢ · = ( comp ‘ 𝐷 )
5		fucco.x	⊢ ∙ = ( comp ‘ 𝑄 )
6		fucco.f	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 𝑁 𝐺 ) )
7		fucco.g	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐺 𝑁 𝐻 ) )
8		fuccoval.f	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
9	1 2 3 4 5 6 7	fucco	⊢ ( 𝜑 → ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) ) )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
11	10	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
12	10	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) )
13	11 12	opeq12d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ⟩ )
14	10	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐻 ) ‘ 𝑋 ) )
15	13 14	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) = ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑋 ) ) )
16	10	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑋 ) )
17	10	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑋 ) )
18	15 16 17	oveq123d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 𝑆 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑥 ) ) ( 𝑅 ‘ 𝑥 ) ) = ( ( 𝑆 ‘ 𝑋 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑋 ) ) ( 𝑅 ‘ 𝑋 ) ) )
19		ovexd	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑋 ) ) ( 𝑅 ‘ 𝑋 ) ) ∈ V )
20	9 18 8 19	fvmptd	⊢ ( 𝜑 → ( ( 𝑆 ( ⟨ 𝐹 , 𝐺 ⟩ ∙ 𝐻 ) 𝑅 ) ‘ 𝑋 ) = ( ( 𝑆 ‘ 𝑋 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ⟩ · ( ( 1^st ‘ 𝐻 ) ‘ 𝑋 ) ) ( 𝑅 ‘ 𝑋 ) ) )

Metamath Proof Explorer

Theorem fuccoval

Proof