Metamath Proof Explorer

Theorem fucocolem3

Description: Lemma for fucoco . The composed natural transformations are mapped to composition of 4 natural transformations. (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 >. )
fucocolem2.t 
|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
fucocolem2.ot 
|- .x. = ( comp ` T )
fucocolem2.od 
|- .* = ( comp ` D )
Assertion fucocolem3 
|- ( ph -> ( ( X P Z ) ` ( B ( <. X , Y >. .x. Z ) A ) ) = ( x e. ( Base ` C ) |-> ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( R ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` L ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` L ) ` x ) ) ` ( S ` x ) ) ) ) ) )

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 fucocolem2.t 
 |-  T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
12 fucocolem2.ot 
 |-  .x. = ( comp ` T )
13 fucocolem2.od 
 |-  .* = ( comp ` D )
14 1 2 3 4 5 6 7 8 9 10 11 12 13 fucocolem2 
 |-  ( ph -> ( ( X P Z ) ` ( B ( <. X , Y >. .x. Z ) A ) ) = ( x e. ( Base ` C ) |-> ( ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( R ` ( ( 1st ` N ) ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( ( V ` x ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` L ) ` x ) >. .* ( ( 1st ` N ) ` x ) ) ( S ` x ) ) ) ) ) )
15 eqid 
 |-  ( Base ` D ) = ( Base ` D )
16 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
17 eqid 
 |-  ( comp ` E ) = ( comp ` E )
18 relfunc 
 |-  Rel ( D Func E )
19 eqid 
 |-  ( D Nat E ) = ( D Nat E )
20 19 natrcl 
 |-  ( R e. ( F ( D Nat E ) K ) -> ( F e. ( D Func E ) /\ K e. ( D Func E ) ) )
21 1 20 syl 
 |-  ( ph -> ( F e. ( D Func E ) /\ K e. ( D Func E ) ) )
22 21 simpld 
 |-  ( ph -> F e. ( D Func E ) )
23 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ F e. ( D Func E ) ) -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
24 18 22 23 sylancr 
 |-  ( ph -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
25 24 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
26 eqid 
 |-  ( Base ` C ) = ( Base ` C )
27 relfunc 
 |-  Rel ( C Func D )
28 eqid 
 |-  ( C Nat D ) = ( C Nat D )
29 28 natrcl 
 |-  ( S e. ( G ( C Nat D ) L ) -> ( G e. ( C Func D ) /\ L e. ( C Func D ) ) )
30 2 29 syl 
 |-  ( ph -> ( G e. ( C Func D ) /\ L e. ( C Func D ) ) )
31 30 simpld 
 |-  ( ph -> G e. ( C Func D ) )
32 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
33 27 31 32 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
34 26 15 33 funcf1 
 |-  ( ph -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) )
35 34 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` G ) ` x ) e. ( Base ` D ) )
36 30 simprd 
 |-  ( ph -> L e. ( C Func D ) )
37 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ L e. ( C Func D ) ) -> ( 1st ` L ) ( C Func D ) ( 2nd ` L ) )
38 27 36 37 sylancr 
 |-  ( ph -> ( 1st ` L ) ( C Func D ) ( 2nd ` L ) )
39 26 15 38 funcf1 
 |-  ( ph -> ( 1st ` L ) : ( Base ` C ) --> ( Base ` D ) )
40 39 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` L ) ` x ) e. ( Base ` D ) )
41 28 natrcl 
 |-  ( V e. ( L ( C Nat D ) N ) -> ( L e. ( C Func D ) /\ N e. ( C Func D ) ) )
42 4 41 syl 
 |-  ( ph -> ( L e. ( C Func D ) /\ N e. ( C Func D ) ) )
43 42 simprd 
 |-  ( ph -> N e. ( C Func D ) )
44 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ N e. ( C Func D ) ) -> ( 1st ` N ) ( C Func D ) ( 2nd ` N ) )
45 27 43 44 sylancr 
 |-  ( ph -> ( 1st ` N ) ( C Func D ) ( 2nd ` N ) )
46 26 15 45 funcf1 
 |-  ( ph -> ( 1st ` N ) : ( Base ` C ) --> ( Base ` D ) )
47 46 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` N ) ` x ) e. ( Base ` D ) )
48 28 2 nat1st2nd 
 |-  ( ph -> S e. ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C Nat D ) <. ( 1st ` L ) , ( 2nd ` L ) >. ) )
49 48 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> S e. ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C Nat D ) <. ( 1st ` L ) , ( 2nd ` L ) >. ) )
50 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
51 28 49 26 16 50 natcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( S ` x ) e. ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` L ) ` x ) ) )
52 28 4 nat1st2nd 
 |-  ( ph -> V e. ( <. ( 1st ` L ) , ( 2nd ` L ) >. ( C Nat D ) <. ( 1st ` N ) , ( 2nd ` N ) >. ) )
53 52 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> V e. ( <. ( 1st ` L ) , ( 2nd ` L ) >. ( C Nat D ) <. ( 1st ` N ) , ( 2nd ` N ) >. ) )
54 28 53 26 16 50 natcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( V ` x ) e. ( ( ( 1st ` L ) ` x ) ( Hom ` D ) ( ( 1st ` N ) ` x ) ) )
55 15 16 13 17 25 35 40 47 51 54 funcco 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( ( V ` x ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` L ) ` x ) >. .* ( ( 1st ` N ) ` x ) ) ( S ` x ) ) ) = ( ( ( ( ( 1st ` L ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` L ) ` x ) ) ` ( S ` x ) ) ) )
56 55 oveq2d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( R ` ( ( 1st ` N ) ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( ( V ` x ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` L ) ` x ) >. .* ( ( 1st ` N ) ` x ) ) ( S ` x ) ) ) ) = ( ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( R ` ( ( 1st ` N ) ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( ( 1st ` L ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` L ) ` x ) ) ` ( S ` x ) ) ) ) )
57 1 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> R e. ( F ( D Nat E ) K ) )
58 2 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> S e. ( G ( C Nat D ) L ) )
59 3 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> U e. ( K ( D Nat E ) M ) )
60 4 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> V e. ( L ( C Nat D ) N ) )
61 22 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> F e. ( D Func E ) )
62 43 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> N e. ( C Func D ) )
63 19 1 nat1st2nd 
 |-  ( ph -> R e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D Nat E ) <. ( 1st ` K ) , ( 2nd ` K ) >. ) )
64 63 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> R e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D Nat E ) <. ( 1st ` K ) , ( 2nd ` K ) >. ) )
65 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
66 19 64 15 65 47 natcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( R ` ( ( 1st ` N ) ` x ) ) e. ( ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) ( Hom ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) ) )
67 15 16 65 25 40 47 funcf2 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( 1st ` L ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) : ( ( ( 1st ` L ) ` x ) ( Hom ` D ) ( ( 1st ` N ) ` x ) ) --> ( ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) ( Hom ` E ) ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) ) )
68 67 54 ffvelcdmd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( ( 1st ` L ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) e. ( ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) ( Hom ` E ) ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) ) )
69 57 58 59 60 50 61 62 66 68 fucocolem1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( R ` ( ( 1st ` N ) ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( ( 1st ` L ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` L ) ` x ) ) ` ( S ` x ) ) ) ) = ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( R ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` L ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` L ) ` x ) ) ` ( S ` x ) ) ) ) )
70 56 69 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( R ` ( ( 1st ` N ) ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( ( V ` x ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` L ) ` x ) >. .* ( ( 1st ` N ) ` x ) ) ( S ` x ) ) ) ) = ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( R ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` L ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` L ) ` x ) ) ` ( S ` x ) ) ) ) )
71 70 mpteq2dva 
 |-  ( ph -> ( x e. ( Base ` C ) |-> ( ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( R ` ( ( 1st ` N ) ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( ( V ` x ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` L ) ` x ) >. .* ( ( 1st ` N ) ` x ) ) ( S ` x ) ) ) ) ) = ( x e. ( Base ` C ) |-> ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( R ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` L ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` L ) ` x ) ) ` ( S ` x ) ) ) ) ) )
72 14 71 eqtrd 
 |-  ( ph -> ( ( X P Z ) ` ( B ( <. X , Y >. .x. Z ) A ) ) = ( x e. ( Base ` C ) |-> ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( R ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` L ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` L ) ` x ) ) ` ( S ` x ) ) ) ) ) )