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 eqid 
 |-  ( D Nat E ) = ( D Nat E )
19 18 natrcl 
 |-  ( R e. ( F ( D Nat E ) K ) -> ( F e. ( D Func E ) /\ K e. ( D Func E ) ) )
20 1 19 syl 
 |-  ( ph -> ( F e. ( D Func E ) /\ K e. ( D Func E ) ) )
21 20 simpld 
 |-  ( ph -> F e. ( D Func E ) )
22 21 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
23 22 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
24 eqid 
 |-  ( Base ` C ) = ( Base ` C )
25 eqid 
 |-  ( C Nat D ) = ( C Nat D )
26 25 natrcl 
 |-  ( S e. ( G ( C Nat D ) L ) -> ( G e. ( C Func D ) /\ L e. ( C Func D ) ) )
27 2 26 syl 
 |-  ( ph -> ( G e. ( C Func D ) /\ L e. ( C Func D ) ) )
28 27 simpld 
 |-  ( ph -> G e. ( C Func D ) )
29 28 func1st2nd 
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
30 24 15 29 funcf1 
 |-  ( ph -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) )
31 30 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` G ) ` x ) e. ( Base ` D ) )
32 27 simprd 
 |-  ( ph -> L e. ( C Func D ) )
33 32 func1st2nd 
 |-  ( ph -> ( 1st ` L ) ( C Func D ) ( 2nd ` L ) )
34 24 15 33 funcf1 
 |-  ( ph -> ( 1st ` L ) : ( Base ` C ) --> ( Base ` D ) )
35 34 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` L ) ` x ) e. ( Base ` D ) )
36 25 natrcl 
 |-  ( V e. ( L ( C Nat D ) N ) -> ( L e. ( C Func D ) /\ N e. ( C Func D ) ) )
37 4 36 syl 
 |-  ( ph -> ( L e. ( C Func D ) /\ N e. ( C Func D ) ) )
38 37 simprd 
 |-  ( ph -> N e. ( C Func D ) )
39 38 func1st2nd 
 |-  ( ph -> ( 1st ` N ) ( C Func D ) ( 2nd ` N ) )
40 24 15 39 funcf1 
 |-  ( ph -> ( 1st ` N ) : ( Base ` C ) --> ( Base ` D ) )
41 40 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` N ) ` x ) e. ( Base ` D ) )
42 25 2 nat1st2nd 
 |-  ( ph -> S e. ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C Nat D ) <. ( 1st ` L ) , ( 2nd ` L ) >. ) )
43 42 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> S e. ( <. ( 1st ` G ) , ( 2nd ` G ) >. ( C Nat D ) <. ( 1st ` L ) , ( 2nd ` L ) >. ) )
44 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
45 25 43 24 16 44 natcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( S ` x ) e. ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` L ) ` x ) ) )
46 25 4 nat1st2nd 
 |-  ( ph -> V e. ( <. ( 1st ` L ) , ( 2nd ` L ) >. ( C Nat D ) <. ( 1st ` N ) , ( 2nd ` N ) >. ) )
47 46 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> V e. ( <. ( 1st ` L ) , ( 2nd ` L ) >. ( C Nat D ) <. ( 1st ` N ) , ( 2nd ` N ) >. ) )
48 25 47 24 16 44 natcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( V ` x ) e. ( ( ( 1st ` L ) ` x ) ( Hom ` D ) ( ( 1st ` N ) ` x ) ) )
49 15 16 13 17 23 31 35 41 45 48 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 ) ) ) )
50 49 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 ) ) ) ) )
51 1 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> R e. ( F ( D Nat E ) K ) )
52 2 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> S e. ( G ( C Nat D ) L ) )
53 3 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> U e. ( K ( D Nat E ) M ) )
54 4 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> V e. ( L ( C Nat D ) N ) )
55 21 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> F e. ( D Func E ) )
56 38 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> N e. ( C Func D ) )
57 18 1 nat1st2nd 
 |-  ( ph -> R e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D Nat E ) <. ( 1st ` K ) , ( 2nd ` K ) >. ) )
58 57 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> R e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D Nat E ) <. ( 1st ` K ) , ( 2nd ` K ) >. ) )
59 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
60 18 58 15 59 41 natcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( R ` ( ( 1st ` N ) ` x ) ) e. ( ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) ( Hom ` E ) ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) ) )
61 15 16 59 23 35 41 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 ) ) ) )
62 61 48 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 ) ) ) )
63 51 52 53 54 44 55 56 60 62 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 ) ) ) ) )
64 50 63 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 ) ) ) ) )
65 64 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 ) ) ) ) ) )
66 14 65 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 ) ) ) ) ) )