Metamath Proof Explorer

Theorem fucocolem2

Description: Lemma for fucoco . The composed natural transformations are mapped to composition of 4 natural transformations. (Contributed by Zhi Wang, 2-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 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 ) ) ) ) ) )

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 6 7 opeq12d 
 |-  ( ph -> <. X , Y >. = <. <. F , G >. , <. K , L >. >. )
15 14 8 oveq12d 
 |-  ( ph -> ( <. X , Y >. .x. Z ) = ( <. <. F , G >. , <. K , L >. >. .x. <. M , N >. ) )
16 15 10 9 oveq123d 
 |-  ( ph -> ( B ( <. X , Y >. .x. Z ) A ) = ( <. U , V >. ( <. <. F , G >. , <. K , L >. >. .x. <. M , N >. ) <. R , S >. ) )
17 eqid 
 |-  ( Base ` D ) = ( Base ` D )
18 eqid 
 |-  ( Base ` C ) = ( Base ` C )
19 eqid 
 |-  ( comp ` E ) = ( comp ` E )
20 11 12 1 2 3 4 17 18 19 13 xpcfucco3 
 |-  ( ph -> ( <. U , V >. ( <. <. F , G >. , <. K , L >. >. .x. <. M , N >. ) <. R , S >. ) = <. ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) , ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) >. )
21 16 20 eqtrd 
 |-  ( ph -> ( B ( <. X , Y >. .x. Z ) A ) = <. ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) , ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) >. )
22 21 fveq2d 
 |-  ( ph -> ( ( X P Z ) ` ( B ( <. X , Y >. .x. Z ) A ) ) = ( ( X P Z ) ` <. ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) , ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) >. ) )
23 df-ov 
 |-  ( ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) ( X P Z ) ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) ) = ( ( X P Z ) ` <. ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) , ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) >. )
24 22 23 eqtr4di 
 |-  ( ph -> ( ( X P Z ) ` ( B ( <. X , Y >. .x. Z ) A ) ) = ( ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) ( X P Z ) ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) ) )
25 11 12 1 2 3 4 xpcfuccocl 
 |-  ( ph -> ( <. U , V >. ( <. <. F , G >. , <. K , L >. >. .x. <. M , N >. ) <. R , S >. ) e. ( ( F ( D Nat E ) M ) X. ( G ( C Nat D ) N ) ) )
26 20 25 eqeltrrd 
 |-  ( ph -> <. ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) , ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) >. e. ( ( F ( D Nat E ) M ) X. ( G ( C Nat D ) N ) ) )
27 opelxp2 
 |-  ( <. ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) , ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) >. e. ( ( F ( D Nat E ) M ) X. ( G ( C Nat D ) N ) ) -> ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) e. ( G ( C Nat D ) N ) )
28 26 27 syl 
 |-  ( ph -> ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) e. ( G ( C Nat D ) N ) )
29 opelxp1 
 |-  ( <. ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) , ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) >. e. ( ( F ( D Nat E ) M ) X. ( G ( C Nat D ) N ) ) -> ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) e. ( F ( D Nat E ) M ) )
30 26 29 syl 
 |-  ( ph -> ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) e. ( F ( D Nat E ) M ) )
31 5 6 8 28 30 fuco22a 
 |-  ( ph -> ( ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) ( X P Z ) ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) ) = ( x e. ( Base ` C ) |-> ( ( ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) ` ( ( 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 ) ) ` ( ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) ` x ) ) ) ) )
32 eqid 
 |-  ( C Nat D ) = ( C Nat D )
33 32 natrcl 
 |-  ( V e. ( L ( C Nat D ) N ) -> ( L e. ( C Func D ) /\ N e. ( C Func D ) ) )
34 4 33 syl 
 |-  ( ph -> ( L e. ( C Func D ) /\ N e. ( C Func D ) ) )
35 34 simprd 
 |-  ( ph -> N e. ( C Func D ) )
36 35 func1st2nd 
 |-  ( ph -> ( 1st ` N ) ( C Func D ) ( 2nd ` N ) )
37 18 17 36 funcf1 
 |-  ( ph -> ( 1st ` N ) : ( Base ` C ) --> ( Base ` D ) )
38 37 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` N ) ` x ) e. ( Base ` D ) )
39 fveq2 
 |-  ( p = ( ( 1st ` N ) ` x ) -> ( ( 1st ` F ) ` p ) = ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) )
40 fveq2 
 |-  ( p = ( ( 1st ` N ) ` x ) -> ( ( 1st ` K ) ` p ) = ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) )
41 39 40 opeq12d 
 |-  ( p = ( ( 1st ` N ) ` x ) -> <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. = <. ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. )
42 fveq2 
 |-  ( p = ( ( 1st ` N ) ` x ) -> ( ( 1st ` M ) ` p ) = ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) )
43 41 42 oveq12d 
 |-  ( p = ( ( 1st ` N ) ` x ) -> ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) = ( <. ( ( 1st ` F ) ` ( ( 1st ` N ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) )
44 fveq2 
 |-  ( p = ( ( 1st ` N ) ` x ) -> ( U ` p ) = ( U ` ( ( 1st ` N ) ` x ) ) )
45 fveq2 
 |-  ( p = ( ( 1st ` N ) ` x ) -> ( R ` p ) = ( R ` ( ( 1st ` N ) ` x ) ) )
46 43 44 45 oveq123d 
 |-  ( p = ( ( 1st ` N ) ` x ) -> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) = ( ( 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 ) ) ) )
47 eqid 
 |-  ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) = ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) )
48 ovex 
 |-  ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) e. _V
49 46 47 48 fvmpt3i 
 |-  ( ( ( 1st ` N ) ` x ) e. ( Base ` D ) -> ( ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) ` ( ( 1st ` N ) ` 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 ) ) ) )
50 38 49 syl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) ` ( ( 1st ` N ) ` 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 ) ) ) )
51 fveq2 
 |-  ( p = x -> ( ( 1st ` G ) ` p ) = ( ( 1st ` G ) ` x ) )
52 fveq2 
 |-  ( p = x -> ( ( 1st ` L ) ` p ) = ( ( 1st ` L ) ` x ) )
53 51 52 opeq12d 
 |-  ( p = x -> <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. = <. ( ( 1st ` G ) ` x ) , ( ( 1st ` L ) ` x ) >. )
54 fveq2 
 |-  ( p = x -> ( ( 1st ` N ) ` p ) = ( ( 1st ` N ) ` x ) )
55 53 54 oveq12d 
 |-  ( p = x -> ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) = ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` L ) ` x ) >. .* ( ( 1st ` N ) ` x ) ) )
56 fveq2 
 |-  ( p = x -> ( V ` p ) = ( V ` x ) )
57 fveq2 
 |-  ( p = x -> ( S ` p ) = ( S ` x ) )
58 55 56 57 oveq123d 
 |-  ( p = x -> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) = ( ( V ` x ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` L ) ` x ) >. .* ( ( 1st ` N ) ` x ) ) ( S ` x ) ) )
59 eqid 
 |-  ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) = ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) )
60 ovex 
 |-  ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) e. _V
61 58 59 60 fvmpt3i 
 |-  ( x e. ( Base ` C ) -> ( ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) ` x ) = ( ( V ` x ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` L ) ` x ) >. .* ( ( 1st ` N ) ` x ) ) ( S ` x ) ) )
62 61 fveq2d 
 |-  ( x e. ( Base ` C ) -> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) ` x ) ) = ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( ( V ` x ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` L ) ` x ) >. .* ( ( 1st ` N ) ` x ) ) ( S ` x ) ) ) )
63 62 adantl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) ` x ) ) = ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( ( V ` x ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` L ) ` x ) >. .* ( ( 1st ` N ) ` x ) ) ( S ` x ) ) ) )
64 50 63 oveq12d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) ` ( ( 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 ) ) ` ( ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) ` 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 ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` N ) ` x ) ) ` ( ( V ` x ) ( <. ( ( 1st ` G ) ` x ) , ( ( 1st ` L ) ` x ) >. .* ( ( 1st ` N ) ` x ) ) ( S ` x ) ) ) ) )
65 64 mpteq2dva 
 |-  ( ph -> ( x e. ( Base ` C ) |-> ( ( ( p e. ( Base ` D ) |-> ( ( U ` p ) ( <. ( ( 1st ` F ) ` p ) , ( ( 1st ` K ) ` p ) >. ( comp ` E ) ( ( 1st ` M ) ` p ) ) ( R ` p ) ) ) ` ( ( 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 ) ) ` ( ( p e. ( Base ` C ) |-> ( ( V ` p ) ( <. ( ( 1st ` G ) ` p ) , ( ( 1st ` L ) ` p ) >. .* ( ( 1st ` N ) ` p ) ) ( S ` p ) ) ) ` x ) ) ) ) = ( 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 ) ) ) ) ) )
66 24 31 65 3eqtrd 
 |-  ( 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 ) ) ) ) ) )