fuco22natlem3

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

Proof

Step	Hyp	Ref	Expression
1		fuco22natlem1.x	$⊢ φ \to X \in {Base}_{C}$
2		fuco22natlem1.y	$⊢ φ \to Y \in {Base}_{C}$
3		fuco22natlem1.a	$⊢ φ \to A \in (⟨F, G⟩ (C Nat D) ⟨M, N⟩)$
4		fuco22natlem1.h	$⊢ φ \to H \in (X Hom (C) Y)$
5		fuco22natlem2.b	$⊢ φ \to B \in (⟨K, L⟩ (D Nat E) ⟨R, S⟩)$
6		fuco22natlem3.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 \|-
7		fuco22natlem3.u	$⊢ φ \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
8		fuco22natlem3.v	$⊢ φ \to V = ⟨⟨R, S⟩, ⟨M, N⟩⟩$
9	1 2 3 4 5	fuco22natlem2	$⊢ φ \to (B (M (Y)) (⟨K (F (Y)), K (M (Y))⟩ comp (E) R (M (Y))) (F (Y) L M (Y)) (A (Y))) (⟨K (F (X)), K (F (Y))⟩ comp (E) R (M (Y))) (F (X) L F (Y)) ((X G Y) (H)) = (M (X) S M (Y)) ((X N Y) (H)) (⟨K (F (X)), R (M (X))⟩ comp (E) R (M (Y))) (B (M (X)) (⟨K (F (X)), K (M (X))⟩ comp (E) R (M (X))) (F (X) L M (X)) (A (X)))$
10		eqid	$⊢ {Base}_{C} = {Base}_{C}$
11		eqid	$⊢ {Base}_{D} = {Base}_{D}$
12		eqid	$⊢ C Nat D = C Nat D$
13	12 3	natrcl2	$⊢ φ \to F (C Func D) G$
14	10 11 13	funcf1	$⊢ φ \to F : {Base}_{C} ⟶ {Base}_{D}$
15	14 1	fvco3d	$⊢ φ \to (K \circ F) (X) = K (F (X))$
16	14 2	fvco3d	$⊢ φ \to (K \circ F) (Y) = K (F (Y))$
17	15 16	opeq12d	$⊢ φ \to ⟨(K \circ F) (X), (K \circ F) (Y)⟩ = ⟨K (F (X)), K (F (Y))⟩$
18	12 3	natrcl3	$⊢ φ \to M (C Func D) N$
19	10 11 18	funcf1	$⊢ φ \to M : {Base}_{C} ⟶ {Base}_{D}$
20	19 2	fvco3d	$⊢ φ \to (R \circ M) (Y) = R (M (Y))$
21	17 20	oveq12d	$⊢ φ \to ⟨(K \circ F) (X), (K \circ F) (Y)⟩ comp (E) (R \circ M) (Y) = ⟨K (F (X)), K (F (Y))⟩ comp (E) R (M (Y))$
22		eqidd	$⊢ φ \to ⟨K (F (Y)), K (M (Y))⟩ comp (E) R (M (Y)) = ⟨K (F (Y)), K (M (Y))⟩ comp (E) R (M (Y))$
23	6 7 8 3 5 2 22	fuco23	$⊢ φ \to (B (U P V) A) (Y) = B (M (Y)) (⟨K (F (Y)), K (M (Y))⟩ comp (E) R (M (Y))) (F (Y) L M (Y)) (A (Y))$
24		eqid	$⊢ Hom (C) = Hom (C)$
25		eqid	$⊢ Hom (D) = Hom (D)$
26	10 24 25 13 1 2	funcf2	$⊢ φ \to (X G Y) : X Hom (C) Y ⟶ F (X) Hom (D) F (Y)$
27	26 4	fvco3d	$⊢ φ \to ((F (X) L F (Y)) \circ (X G Y)) (H) = (F (X) L F (Y)) ((X G Y) (H))$
28	21 23 27	oveq123d	$⊢ φ \to (B (U P V) A) (Y) (⟨(K \circ F) (X), (K \circ F) (Y)⟩ comp (E) (R \circ M) (Y)) ((F (X) L F (Y)) \circ (X G Y)) (H) = (B (M (Y)) (⟨K (F (Y)), K (M (Y))⟩ comp (E) R (M (Y))) (F (Y) L M (Y)) (A (Y))) (⟨K (F (X)), K (F (Y))⟩ comp (E) R (M (Y))) (F (X) L F (Y)) ((X G Y) (H))$
29	19 1	fvco3d	$⊢ φ \to (R \circ M) (X) = R (M (X))$
30	15 29	opeq12d	$⊢ φ \to ⟨(K \circ F) (X), (R \circ M) (X)⟩ = ⟨K (F (X)), R (M (X))⟩$
31	30 20	oveq12d	$⊢ φ \to ⟨(K \circ F) (X), (R \circ M) (X)⟩ comp (E) (R \circ M) (Y) = ⟨K (F (X)), R (M (X))⟩ comp (E) R (M (Y))$
32	10 24 25 18 1 2	funcf2	$⊢ φ \to (X N Y) : X Hom (C) Y ⟶ M (X) Hom (D) M (Y)$
33	32 4	fvco3d	$⊢ φ \to ((M (X) S M (Y)) \circ (X N Y)) (H) = (M (X) S M (Y)) ((X N Y) (H))$
34		eqidd	$⊢ φ \to ⟨K (F (X)), K (M (X))⟩ comp (E) R (M (X)) = ⟨K (F (X)), K (M (X))⟩ comp (E) R (M (X))$
35	6 7 8 3 5 1 34	fuco23	$⊢ φ \to (B (U P V) A) (X) = B (M (X)) (⟨K (F (X)), K (M (X))⟩ comp (E) R (M (X))) (F (X) L M (X)) (A (X))$
36	31 33 35	oveq123d	$⊢ φ \to ((M (X) S M (Y)) \circ (X N Y)) (H) (⟨(K \circ F) (X), (R \circ M) (X)⟩ comp (E) (R \circ M) (Y)) (B (U P V) A) (X) = (M (X) S M (Y)) ((X N Y) (H)) (⟨K (F (X)), R (M (X))⟩ comp (E) R (M (Y))) (B (M (X)) (⟨K (F (X)), K (M (X))⟩ comp (E) R (M (X))) (F (X) L M (X)) (A (X)))$
37	9 28 36	3eqtr4d	$⊢ φ \to (B (U P V) A) (Y) (⟨(K \circ F) (X), (K \circ F) (Y)⟩ comp (E) (R \circ M) (Y)) ((F (X) L F (Y)) \circ (X G Y)) (H) = ((M (X) S M (Y)) \circ (X N Y)) (H) (⟨(K \circ F) (X), (R \circ M) (X)⟩ comp (E) (R \circ M) (Y)) (B (U P V) A) (X)$

Metamath Proof Explorer

Theorem fuco22natlem3

Proof