Theorem fucoco

Description: Composition in the source category is mapped to composition in the target. See also fucoco2 . (Contributed by Zhi Wang, 3-Oct-2025)

	Ref	Expression
Hypotheses	fucoco.r	|- ( ph -> R e. ( F ( D Nat E ) K ) )
	fucoco.s	|- ( ph -> S e. ( G ( C Nat D ) L ) )
	fucoco.u	|- ( ph -> U e. ( K ( D Nat E ) M ) )
	fucoco.v	|- ( ph -> V e. ( L ( C Nat D ) N ) )
	fucoco.o	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
	fucoco.x	|- ( ph -> X = <. F , G >. )
	fucoco.y	|- ( ph -> Y = <. K , L >. )
	fucoco.z	|- ( ph -> Z = <. M , N >. )
	fucoco.a	|- ( ph -> A = <. R , S >. )
	fucoco.b	|- ( ph -> B = <. U , V >. )
	fucoco.q	|- Q = ( C FuncCat E )
	fucoco.oq	|- .xb = ( comp ` Q )
	fucoco.t	|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
	fucoco.ot	|- .x. = ( comp ` T )
Assertion	fucoco	|- ( ph -> ( ( X P Z ) ` ( B ( <. X , Y >. .x. Z ) A ) ) = ( ( ( Y P Z ) ` B ) ( <. ( O ` X ) , ( O ` Y ) >. .xb ( O ` Z ) ) ( ( X P Y ) ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucoco.r	|- ( ph -> R e. ( F ( D Nat E ) K ) )
2		fucoco.s	|- ( ph -> S e. ( G ( C Nat D ) L ) )
3		fucoco.u	|- ( ph -> U e. ( K ( D Nat E ) M ) )
4		fucoco.v	|- ( ph -> V e. ( L ( C Nat D ) N ) )
5		fucoco.o	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
6		fucoco.x	|- ( ph -> X = <. F , G >. )
7		fucoco.y	|- ( ph -> Y = <. K , L >. )
8		fucoco.z	|- ( ph -> Z = <. M , N >. )
9		fucoco.a	|- ( ph -> A = <. R , S >. )
10		fucoco.b	|- ( ph -> B = <. U , V >. )
11		fucoco.q	|- Q = ( C FuncCat E )
12		fucoco.oq	|- .xb = ( comp ` Q )
13		fucoco.t	|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
14		fucoco.ot	|- .x. = ( comp ` T )
15		eqid	|- ( C Nat D ) = ( C Nat D )
16	15 4	nat1st2nd	|- ( ph -> V e. ( <. ( 1st ` L ) , ( 2nd ` L ) >. ( C Nat D ) <. ( 1st ` N ) , ( 2nd ` N ) >. ) )
17	16	adantr	|- ( ( ph /\ p e. ( Base ` C ) ) -> V e. ( <. ( 1st ` L ) , ( 2nd ` L ) >. ( C Nat D ) <. ( 1st ` N ) , ( 2nd ` N ) >. ) )
18		eqid	|- ( D Nat E ) = ( D Nat E )
19	18 1	nat1st2nd	|- ( ph -> R e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D Nat E ) <. ( 1st ` K ) , ( 2nd ` K ) >. ) )
20	19	adantr	|- ( ( ph /\ p e. ( Base ` C ) ) -> R e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D Nat E ) <. ( 1st ` K ) , ( 2nd ` K ) >. ) )
21		simpr	|- ( ( ph /\ p e. ( Base ` C ) ) -> p e. ( Base ` C ) )
22		eqid	|- ( comp ` E ) = ( comp ` E )
23	17 20 21 22	fuco23alem	|- ( ( ph /\ p e. ( Base ` C ) ) -> ( ( R ` ( ( 1st ` N ) ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` L ) ` p ) ( 2nd ` F ) ( ( 1st ` N ) ` p ) ) ` ( V ` p ) ) ) = ( ( ( ( ( 1st ` L ) ` p ) ( 2nd ` K ) ( ( 1st ` N ) ` p ) ) ` ( V ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( R ` ( ( 1st ` L ) ` p ) ) ) )
24	23	oveq1d	|- ( ( ph /\ p e. ( Base ` C ) ) -> ( ( ( R ` ( ( 1st ` N ) ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` L ) ` p ) ( 2nd ` F ) ( ( 1st ` N ) ` p ) ) ` ( V ` p ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` G ) ` p ) ( 2nd ` F ) ( ( 1st ` L ) ` p ) ) ` ( S ` p ) ) ) = ( ( ( ( ( ( 1st ` L ) ` p ) ( 2nd ` K ) ( ( 1st ` N ) ` p ) ) ` ( V ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( R ` ( ( 1st ` L ) ` p ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` G ) ` p ) ( 2nd ` F ) ( ( 1st ` L ) ` p ) ) ` ( S ` p ) ) ) )
25	24	oveq2d	|- ( ( ph /\ p e. ( Base ` C ) ) -> ( ( U ` ( ( 1st ` N ) ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( R ` ( ( 1st ` N ) ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` L ) ` p ) ( 2nd ` F ) ( ( 1st ` N ) ` p ) ) ` ( V ` p ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` G ) ` p ) ( 2nd ` F ) ( ( 1st ` L ) ` p ) ) ` ( S ` p ) ) ) ) = ( ( U ` ( ( 1st ` N ) ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( ( ( 1st ` L ) ` p ) ( 2nd ` K ) ( ( 1st ` N ) ` p ) ) ` ( V ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( R ` ( ( 1st ` L ) ` p ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` G ) ` p ) ( 2nd ` F ) ( ( 1st ` L ) ` p ) ) ` ( S ` p ) ) ) ) )
26	1	adantr	|- ( ( ph /\ p e. ( Base ` C ) ) -> R e. ( F ( D Nat E ) K ) )
27	2	adantr	|- ( ( ph /\ p e. ( Base ` C ) ) -> S e. ( G ( C Nat D ) L ) )
28	3	adantr	|- ( ( ph /\ p e. ( Base ` C ) ) -> U e. ( K ( D Nat E ) M ) )
29	4	adantr	|- ( ( ph /\ p e. ( Base ` C ) ) -> V e. ( L ( C Nat D ) N ) )
30	18	natrcl	|- ( R e. ( F ( D Nat E ) K ) -> ( F e. ( D Func E ) /\ K e. ( D Func E ) ) )
31	1 30	syl	|- ( ph -> ( F e. ( D Func E ) /\ K e. ( D Func E ) ) )
32	31	simprd	|- ( ph -> K e. ( D Func E ) )
33	32	adantr	|- ( ( ph /\ p e. ( Base ` C ) ) -> K e. ( D Func E ) )
34	15	natrcl	|- ( S e. ( G ( C Nat D ) L ) -> ( G e. ( C Func D ) /\ L e. ( C Func D ) ) )
35	2 34	syl	|- ( ph -> ( G e. ( C Func D ) /\ L e. ( C Func D ) ) )
36	35	simprd	|- ( ph -> L e. ( C Func D ) )
37	36	adantr	|- ( ( ph /\ p e. ( Base ` C ) ) -> L e. ( C Func D ) )
38		eqid	|- ( Base ` D ) = ( Base ` D )
39		eqid	|- ( Hom ` D ) = ( Hom ` D )
40		eqid	|- ( Hom ` E ) = ( Hom ` E )
41	32	func1st2nd	|- ( ph -> ( 1st ` K ) ( D Func E ) ( 2nd ` K ) )
42	41	adantr	|- ( ( ph /\ p e. ( Base ` C ) ) -> ( 1st ` K ) ( D Func E ) ( 2nd ` K ) )
43		eqid	|- ( Base ` C ) = ( Base ` C )
44	36	func1st2nd	|- ( ph -> ( 1st ` L ) ( C Func D ) ( 2nd ` L ) )
45	43 38 44	funcf1	|- ( ph -> ( 1st ` L ) : ( Base ` C ) --> ( Base ` D ) )
46	45	ffvelcdmda	|- ( ( ph /\ p e. ( Base ` C ) ) -> ( ( 1st ` L ) ` p ) e. ( Base ` D ) )
47	15	natrcl	|- ( V e. ( L ( C Nat D ) N ) -> ( L e. ( C Func D ) /\ N e. ( C Func D ) ) )
48	4 47	syl	|- ( ph -> ( L e. ( C Func D ) /\ N e. ( C Func D ) ) )
49	48	simprd	|- ( ph -> N e. ( C Func D ) )
50	49	func1st2nd	|- ( ph -> ( 1st ` N ) ( C Func D ) ( 2nd ` N ) )
51	43 38 50	funcf1	|- ( ph -> ( 1st ` N ) : ( Base ` C ) --> ( Base ` D ) )
52	51	ffvelcdmda	|- ( ( ph /\ p e. ( Base ` C ) ) -> ( ( 1st ` N ) ` p ) e. ( Base ` D ) )
53	38 39 40 42 46 52	funcf2	|- ( ( ph /\ p e. ( Base ` C ) ) -> ( ( ( 1st ` L ) ` p ) ( 2nd ` K ) ( ( 1st ` N ) ` p ) ) : ( ( ( 1st ` L ) ` p ) ( Hom ` D ) ( ( 1st ` N ) ` p ) ) --> ( ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) ( Hom ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) )
54	15 17 43 39 21	natcl	|- ( ( ph /\ p e. ( Base ` C ) ) -> ( V ` p ) e. ( ( ( 1st ` L ) ` p ) ( Hom ` D ) ( ( 1st ` N ) ` p ) ) )
55	53 54	ffvelcdmd	|- ( ( ph /\ p e. ( Base ` C ) ) -> ( ( ( ( 1st ` L ) ` p ) ( 2nd ` K ) ( ( 1st ` N ) ` p ) ) ` ( V ` p ) ) e. ( ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) ( Hom ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) )
56	18 20 38 40 46	natcl	|- ( ( ph /\ p e. ( Base ` C ) ) -> ( R ` ( ( 1st ` L ) ` p ) ) e. ( ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) ( Hom ` E ) ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) ) )
57	26 27 28 29 21 33 37 55 56	fucocolem1	|- ( ( ph /\ p e. ( Base ` C ) ) -> ( ( ( U ` ( ( 1st ` N ) ` p ) ) ( <. ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` L ) ` p ) ( 2nd ` K ) ( ( 1st ` N ) ` p ) ) ` ( V ` p ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` p ) ) ) ( ( R ` ( ( 1st ` L ) ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) ) ( ( ( ( 1st ` G ) ` p ) ( 2nd ` F ) ( ( 1st ` L ) ` p ) ) ` ( S ` p ) ) ) ) = ( ( U ` ( ( 1st ` N ) ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( ( ( 1st ` L ) ` p ) ( 2nd ` K ) ( ( 1st ` N ) ` p ) ) ` ( V ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( R ` ( ( 1st ` L ) ` p ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` G ) ` p ) ( 2nd ` F ) ( ( 1st ` L ) ` p ) ) ` ( S ` p ) ) ) ) )
58	25 57	eqtr4d	|- ( ( ph /\ p e. ( Base ` C ) ) -> ( ( U ` ( ( 1st ` N ) ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( R ` ( ( 1st ` N ) ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` L ) ` p ) ( 2nd ` F ) ( ( 1st ` N ) ` p ) ) ` ( V ` p ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` G ) ` p ) ( 2nd ` F ) ( ( 1st ` L ) ` p ) ) ` ( S ` p ) ) ) ) = ( ( ( U ` ( ( 1st ` N ) ` p ) ) ( <. ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` L ) ` p ) ( 2nd ` K ) ( ( 1st ` N ) ` p ) ) ` ( V ` p ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` p ) ) ) ( ( R ` ( ( 1st ` L ) ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) ) ( ( ( ( 1st ` G ) ` p ) ( 2nd ` F ) ( ( 1st ` L ) ` p ) ) ` ( S ` p ) ) ) ) )
59	58	mpteq2dva	|- ( ph -> ( p e. ( Base ` C ) |-> ( ( U ` ( ( 1st ` N ) ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( R ` ( ( 1st ` N ) ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` L ) ` p ) ( 2nd ` F ) ( ( 1st ` N ) ` p ) ) ` ( V ` p ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` G ) ` p ) ( 2nd ` F ) ( ( 1st ` L ) ` p ) ) ` ( S ` p ) ) ) ) ) = ( p e. ( Base ` C ) |-> ( ( ( U ` ( ( 1st ` N ) ` p ) ) ( <. ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` L ) ` p ) ( 2nd ` K ) ( ( 1st ` N ) ` p ) ) ` ( V ` p ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` p ) ) ) ( ( R ` ( ( 1st ` L ) ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) ) ( ( ( ( 1st ` G ) ` p ) ( 2nd ` F ) ( ( 1st ` L ) ` p ) ) ` ( S ` p ) ) ) ) ) )
60		eqid	|- ( comp ` D ) = ( comp ` D )
61	1 2 3 4 5 6 7 8 9 10 13 14 60	fucocolem3	|- ( ph -> ( ( X P Z ) ` ( B ( <. X , Y >. .x. Z ) A ) ) = ( p e. ( Base ` C ) |-> ( ( U ` ( ( 1st ` N ) ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( R ` ( ( 1st ` N ) ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` L ) ` p ) ( 2nd ` F ) ( ( 1st ` N ) ` p ) ) ` ( V ` p ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` G ) ` p ) ( 2nd ` F ) ( ( 1st ` L ) ` p ) ) ` ( S ` p ) ) ) ) ) )
62	1 2 3 4 5 6 7 8 9 10 11 12	fucocolem4	|- ( ph -> ( ( ( Y P Z ) ` B ) ( <. ( O ` X ) , ( O ` Y ) >. .xb ( O ` Z ) ) ( ( X P Y ) ` A ) ) = ( p e. ( Base ` C ) |-> ( ( ( U ` ( ( 1st ` N ) ` p ) ) ( <. ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` p ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` p ) ) ) ( ( ( ( 1st ` L ) ` p ) ( 2nd ` K ) ( ( 1st ` N ) ` p ) ) ` ( V ` p ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` p ) ) ) ( ( R ` ( ( 1st ` L ) ` p ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` p ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` p ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` L ) ` p ) ) ) ( ( ( ( 1st ` G ) ` p ) ( 2nd ` F ) ( ( 1st ` L ) ` p ) ) ` ( S ` p ) ) ) ) ) )
63	59 61 62	3eqtr4d	|- ( ph -> ( ( X P Z ) ` ( B ( <. X , Y >. .x. Z ) A ) ) = ( ( ( Y P Z ) ` B ) ( <. ( O ` X ) , ( O ` Y ) >. .xb ( O ` Z ) ) ( ( X P Y ) ` A ) ) )