fuco23

Description: The morphism part of the functor composition bifunctor. See also fuco23a . (Contributed by Zhi Wang, 29-Sep-2025)

	Ref	Expression
Hypotheses	fuco22.o	No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
	fuco22.u	$⊢ φ \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
	fuco22.v	$⊢ φ \to V = ⟨⟨R, S⟩, ⟨M, N⟩⟩$
	fuco22.a	$⊢ φ \to A \in (⟨F, G⟩ (C Nat D) ⟨M, N⟩)$
	fuco22.b	$⊢ φ \to B \in (⟨K, L⟩ (D Nat E) ⟨R, S⟩)$
	fuco23.x	$⊢ φ \to X \in {Base}_{C}$
	fuco23.o	$⊢ φ \to \underset{˙}{*} = ⟨K (F (X)), K (M (X))⟩ comp (E) R (M (X))$
Assertion	fuco23	$⊢ φ \to (B (U P V) A) (X) = B (M (X)) \underset{˙}{*} (F (X) L M (X)) (A (X))$

Proof

Step	Hyp	Ref	Expression
1		fuco22.o	Could not format ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
2		fuco22.u	$⊢ φ \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
3		fuco22.v	$⊢ φ \to V = ⟨⟨R, S⟩, ⟨M, N⟩⟩$
4		fuco22.a	$⊢ φ \to A \in (⟨F, G⟩ (C Nat D) ⟨M, N⟩)$
5		fuco22.b	$⊢ φ \to B \in (⟨K, L⟩ (D Nat E) ⟨R, S⟩)$
6		fuco23.x	$⊢ φ \to X \in {Base}_{C}$
7		fuco23.o	$⊢ φ \to \underset{˙}{*} = ⟨K (F (X)), K (M (X))⟩ comp (E) R (M (X))$
8	1 2 3 4 5	fuco22	$⊢ φ \to B (U P V) A = (x \in {Base}_{C} ⟼ B (M (x)) (⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x))) (F (x) L M (x)) (A (x)))$
9		simpr	$⊢ (φ \land x = X) \to x = X$
10	9	fveq2d	$⊢ (φ \land x = X) \to F (x) = F (X)$
11	10	fveq2d	$⊢ (φ \land x = X) \to K (F (x)) = K (F (X))$
12	9	fveq2d	$⊢ (φ \land x = X) \to M (x) = M (X)$
13	12	fveq2d	$⊢ (φ \land x = X) \to K (M (x)) = K (M (X))$
14	11 13	opeq12d	$⊢ (φ \land x = X) \to ⟨K (F (x)), K (M (x))⟩ = ⟨K (F (X)), K (M (X))⟩$
15	12	fveq2d	$⊢ (φ \land x = X) \to R (M (x)) = R (M (X))$
16	14 15	oveq12d	$⊢ (φ \land x = X) \to ⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x)) = ⟨K (F (X)), K (M (X))⟩ comp (E) R (M (X))$
17	7	adantr	$⊢ (φ \land x = X) \to \underset{˙}{*} = ⟨K (F (X)), K (M (X))⟩ comp (E) R (M (X))$
18	16 17	eqtr4d	$⊢ (φ \land x = X) \to ⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x)) = \underset{˙}{*}$
19	12	fveq2d	$⊢ (φ \land x = X) \to B (M (x)) = B (M (X))$
20	10 12	oveq12d	$⊢ (φ \land x = X) \to F (x) L M (x) = F (X) L M (X)$
21	9	fveq2d	$⊢ (φ \land x = X) \to A (x) = A (X)$
22	20 21	fveq12d	$⊢ (φ \land x = X) \to (F (x) L M (x)) (A (x)) = (F (X) L M (X)) (A (X))$
23	18 19 22	oveq123d	$⊢ (φ \land x = X) \to B (M (x)) (⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x))) (F (x) L M (x)) (A (x)) = B (M (X)) \underset{˙}{*} (F (X) L M (X)) (A (X))$
24		ovexd	$⊢ φ \to B (M (X)) \underset{˙}{*} (F (X) L M (X)) (A (X)) \in V$
25	8 23 6 24	fvmptd	$⊢ φ \to (B (U P V) A) (X) = B (M (X)) \underset{˙}{*} (F (X) L M (X)) (A (X))$

Metamath Proof Explorer

Theorem fuco23

Proof