Metamath Proof Explorer

Theorem fucocolem4

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 >. )
fucoco.q 
|- Q = ( C FuncCat E )
fucoco.oq 
|- .xb = ( comp ` Q )
Assertion fucocolem4 
|- ( ph -> ( ( ( Y P Z ) ` B ) ( <. ( O ` X ) , ( O ` Y ) >. .xb ( O ` Z ) ) ( ( X P Y ) ` A ) ) = ( x e. ( Base ` C ) |-> ( ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` L ) ` x ) ( 2nd ` K ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( R ` ( ( 1st ` L ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` L ) ` 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 fucoco.q 
 |-  Q = ( C FuncCat E )
12 fucoco.oq 
 |-  .xb = ( comp ` Q )
13 eqid 
 |-  ( C Nat E ) = ( C Nat E )
14 eqid 
 |-  ( Base ` C ) = ( Base ` C )
15 eqid 
 |-  ( comp ` E ) = ( comp ` E )
16 9 fveq2d 
 |-  ( ph -> ( ( X P Y ) ` A ) = ( ( X P Y ) ` <. R , S >. ) )
17 df-ov 
 |-  ( R ( X P Y ) S ) = ( ( X P Y ) ` <. R , S >. )
18 16 17 eqtr4di 
 |-  ( ph -> ( ( X P Y ) ` A ) = ( R ( X P Y ) S ) )
19 5 2 1 6 7 fuco22nat 
 |-  ( ph -> ( R ( X P Y ) S ) e. ( ( O ` X ) ( C Nat E ) ( O ` Y ) ) )
20 18 19 eqeltrd 
 |-  ( ph -> ( ( X P Y ) ` A ) e. ( ( O ` X ) ( C Nat E ) ( O ` Y ) ) )
21 10 fveq2d 
 |-  ( ph -> ( ( Y P Z ) ` B ) = ( ( Y P Z ) ` <. U , V >. ) )
22 df-ov 
 |-  ( U ( Y P Z ) V ) = ( ( Y P Z ) ` <. U , V >. )
23 21 22 eqtr4di 
 |-  ( ph -> ( ( Y P Z ) ` B ) = ( U ( Y P Z ) V ) )
24 5 4 3 7 8 fuco22nat 
 |-  ( ph -> ( U ( Y P Z ) V ) e. ( ( O ` Y ) ( C Nat E ) ( O ` Z ) ) )
25 23 24 eqeltrd 
 |-  ( ph -> ( ( Y P Z ) ` B ) e. ( ( O ` Y ) ( C Nat E ) ( O ` Z ) ) )
26 11 13 14 15 12 20 25 fucco 
 |-  ( ph -> ( ( ( Y P Z ) ` B ) ( <. ( O ` X ) , ( O ` Y ) >. .xb ( O ` Z ) ) ( ( X P Y ) ` A ) ) = ( x e. ( Base ` C ) |-> ( ( ( ( Y P Z ) ` B ) ` x ) ( <. ( ( 1st ` ( O ` X ) ) ` x ) , ( ( 1st ` ( O ` Y ) ) ` x ) >. ( comp ` E ) ( ( 1st ` ( O ` Z ) ) ` x ) ) ( ( ( X P Y ) ` A ) ` x ) ) ) )
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 relfunc 
 |-  Rel ( D Func E )
35 eqid 
 |-  ( D Nat E ) = ( D Nat E )
36 35 natrcl 
 |-  ( R e. ( F ( D Nat E ) K ) -> ( F e. ( D Func E ) /\ K e. ( D Func E ) ) )
37 1 36 syl 
 |-  ( ph -> ( F e. ( D Func E ) /\ K e. ( D Func E ) ) )
38 37 simpld 
 |-  ( ph -> F e. ( D Func E ) )
39 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ F e. ( D Func E ) ) -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
40 34 38 39 sylancr 
 |-  ( ph -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
41 1st2nd 
 |-  ( ( Rel ( D Func E ) /\ F e. ( D Func E ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
42 34 38 41 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
43 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
44 27 31 43 sylancr 
 |-  ( ph -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
45 42 44 opeq12d 
 |-  ( ph -> <. F , G >. = <. <. ( 1st ` F ) , ( 2nd ` F ) >. , <. ( 1st ` G ) , ( 2nd ` G ) >. >. )
46 6 45 eqtrd 
 |-  ( ph -> X = <. <. ( 1st ` F ) , ( 2nd ` F ) >. , <. ( 1st ` G ) , ( 2nd ` G ) >. >. )
47 5 33 40 46 fuco111 
 |-  ( ph -> ( 1st ` ( O ` X ) ) = ( ( 1st ` F ) o. ( 1st ` G ) ) )
48 47 fveq1d 
 |-  ( ph -> ( ( 1st ` ( O ` X ) ) ` x ) = ( ( ( 1st ` F ) o. ( 1st ` G ) ) ` x ) )
49 48 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( O ` X ) ) ` x ) = ( ( ( 1st ` F ) o. ( 1st ` G ) ) ` x ) )
50 eqid 
 |-  ( Base ` D ) = ( Base ` D )
51 14 50 33 funcf1 
 |-  ( ph -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) )
52 51 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) )
53 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
54 52 53 fvco3d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( 1st ` F ) o. ( 1st ` G ) ) ` x ) = ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) )
55 49 54 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( O ` X ) ) ` x ) = ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) )
56 30 simprd 
 |-  ( ph -> L e. ( C Func D ) )
57 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ L e. ( C Func D ) ) -> ( 1st ` L ) ( C Func D ) ( 2nd ` L ) )
58 27 56 57 sylancr 
 |-  ( ph -> ( 1st ` L ) ( C Func D ) ( 2nd ` L ) )
59 37 simprd 
 |-  ( ph -> K e. ( D Func E ) )
60 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ K e. ( D Func E ) ) -> ( 1st ` K ) ( D Func E ) ( 2nd ` K ) )
61 34 59 60 sylancr 
 |-  ( ph -> ( 1st ` K ) ( D Func E ) ( 2nd ` K ) )
62 1st2nd 
 |-  ( ( Rel ( D Func E ) /\ K e. ( D Func E ) ) -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
63 34 59 62 sylancr 
 |-  ( ph -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
64 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ L e. ( C Func D ) ) -> L = <. ( 1st ` L ) , ( 2nd ` L ) >. )
65 27 56 64 sylancr 
 |-  ( ph -> L = <. ( 1st ` L ) , ( 2nd ` L ) >. )
66 63 65 opeq12d 
 |-  ( ph -> <. K , L >. = <. <. ( 1st ` K ) , ( 2nd ` K ) >. , <. ( 1st ` L ) , ( 2nd ` L ) >. >. )
67 7 66 eqtrd 
 |-  ( ph -> Y = <. <. ( 1st ` K ) , ( 2nd ` K ) >. , <. ( 1st ` L ) , ( 2nd ` L ) >. >. )
68 5 58 61 67 fuco111 
 |-  ( ph -> ( 1st ` ( O ` Y ) ) = ( ( 1st ` K ) o. ( 1st ` L ) ) )
69 68 fveq1d 
 |-  ( ph -> ( ( 1st ` ( O ` Y ) ) ` x ) = ( ( ( 1st ` K ) o. ( 1st ` L ) ) ` x ) )
70 69 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( O ` Y ) ) ` x ) = ( ( ( 1st ` K ) o. ( 1st ` L ) ) ` x ) )
71 14 50 58 funcf1 
 |-  ( ph -> ( 1st ` L ) : ( Base ` C ) --> ( Base ` D ) )
72 71 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` L ) : ( Base ` C ) --> ( Base ` D ) )
73 72 53 fvco3d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( 1st ` K ) o. ( 1st ` L ) ) ` x ) = ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) )
74 70 73 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( O ` Y ) ) ` x ) = ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) )
75 55 74 opeq12d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> <. ( ( 1st ` ( O ` X ) ) ` x ) , ( ( 1st ` ( O ` Y ) ) ` x ) >. = <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) >. )
76 28 natrcl 
 |-  ( V e. ( L ( C Nat D ) N ) -> ( L e. ( C Func D ) /\ N e. ( C Func D ) ) )
77 4 76 syl 
 |-  ( ph -> ( L e. ( C Func D ) /\ N e. ( C Func D ) ) )
78 77 simprd 
 |-  ( ph -> N e. ( C Func D ) )
79 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ N e. ( C Func D ) ) -> ( 1st ` N ) ( C Func D ) ( 2nd ` N ) )
80 27 78 79 sylancr 
 |-  ( ph -> ( 1st ` N ) ( C Func D ) ( 2nd ` N ) )
81 35 natrcl 
 |-  ( U e. ( K ( D Nat E ) M ) -> ( K e. ( D Func E ) /\ M e. ( D Func E ) ) )
82 3 81 syl 
 |-  ( ph -> ( K e. ( D Func E ) /\ M e. ( D Func E ) ) )
83 82 simprd 
 |-  ( ph -> M e. ( D Func E ) )
84 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ M e. ( D Func E ) ) -> ( 1st ` M ) ( D Func E ) ( 2nd ` M ) )
85 34 83 84 sylancr 
 |-  ( ph -> ( 1st ` M ) ( D Func E ) ( 2nd ` M ) )
86 1st2nd 
 |-  ( ( Rel ( D Func E ) /\ M e. ( D Func E ) ) -> M = <. ( 1st ` M ) , ( 2nd ` M ) >. )
87 34 83 86 sylancr 
 |-  ( ph -> M = <. ( 1st ` M ) , ( 2nd ` M ) >. )
88 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ N e. ( C Func D ) ) -> N = <. ( 1st ` N ) , ( 2nd ` N ) >. )
89 27 78 88 sylancr 
 |-  ( ph -> N = <. ( 1st ` N ) , ( 2nd ` N ) >. )
90 87 89 opeq12d 
 |-  ( ph -> <. M , N >. = <. <. ( 1st ` M ) , ( 2nd ` M ) >. , <. ( 1st ` N ) , ( 2nd ` N ) >. >. )
91 8 90 eqtrd 
 |-  ( ph -> Z = <. <. ( 1st ` M ) , ( 2nd ` M ) >. , <. ( 1st ` N ) , ( 2nd ` N ) >. >. )
92 5 80 85 91 fuco111 
 |-  ( ph -> ( 1st ` ( O ` Z ) ) = ( ( 1st ` M ) o. ( 1st ` N ) ) )
93 92 fveq1d 
 |-  ( ph -> ( ( 1st ` ( O ` Z ) ) ` x ) = ( ( ( 1st ` M ) o. ( 1st ` N ) ) ` x ) )
94 93 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( O ` Z ) ) ` x ) = ( ( ( 1st ` M ) o. ( 1st ` N ) ) ` x ) )
95 14 50 80 funcf1 
 |-  ( ph -> ( 1st ` N ) : ( Base ` C ) --> ( Base ` D ) )
96 95 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` N ) : ( Base ` C ) --> ( Base ` D ) )
97 96 53 fvco3d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( 1st ` M ) o. ( 1st ` N ) ) ` x ) = ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) )
98 94 97 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( O ` Z ) ) ` x ) = ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) )
99 75 98 oveq12d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( <. ( ( 1st ` ( O ` X ) ) ` x ) , ( ( 1st ` ( O ` Y ) ) ` x ) >. ( comp ` E ) ( ( 1st ` ( O ` Z ) ) ` x ) ) = ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) )
100 5 7 8 4 3 fuco22a 
 |-  ( ph -> ( U ( Y P Z ) V ) = ( x e. ( Base ` C ) |-> ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` L ) ` x ) ( 2nd ` K ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) ) ) )
101 23 100 eqtrd 
 |-  ( ph -> ( ( Y P Z ) ` B ) = ( x e. ( Base ` C ) |-> ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` L ) ` x ) ( 2nd ` K ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) ) ) )
102 ovexd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` L ) ` x ) ( 2nd ` K ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) ) e. _V )
103 101 102 fvmpt2d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( Y P Z ) ` B ) ` x ) = ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` L ) ` x ) ( 2nd ` K ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) ) )
104 5 6 7 2 1 fuco22a 
 |-  ( ph -> ( R ( X P Y ) S ) = ( x e. ( Base ` C ) |-> ( ( R ` ( ( 1st ` L ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` L ) ` x ) ) ` ( S ` x ) ) ) ) )
105 18 104 eqtrd 
 |-  ( ph -> ( ( X P Y ) ` A ) = ( x e. ( Base ` C ) |-> ( ( R ` ( ( 1st ` L ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` L ) ` x ) ) ` ( S ` x ) ) ) ) )
106 ovexd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( R ` ( ( 1st ` L ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` L ) ` x ) ) ` ( S ` x ) ) ) e. _V )
107 105 106 fvmpt2d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( X P Y ) ` A ) ` x ) = ( ( R ` ( ( 1st ` L ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` L ) ` x ) ) ` ( S ` x ) ) ) )
108 99 103 107 oveq123d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( ( Y P Z ) ` B ) ` x ) ( <. ( ( 1st ` ( O ` X ) ) ` x ) , ( ( 1st ` ( O ` Y ) ) ` x ) >. ( comp ` E ) ( ( 1st ` ( O ` Z ) ) ` x ) ) ( ( ( X P Y ) ` A ) ` x ) ) = ( ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` L ) ` x ) ( 2nd ` K ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( R ` ( ( 1st ` L ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` L ) ` x ) ) ` ( S ` x ) ) ) ) )
109 108 mpteq2dva 
 |-  ( ph -> ( x e. ( Base ` C ) |-> ( ( ( ( Y P Z ) ` B ) ` x ) ( <. ( ( 1st ` ( O ` X ) ) ` x ) , ( ( 1st ` ( O ` Y ) ) ` x ) >. ( comp ` E ) ( ( 1st ` ( O ` Z ) ) ` x ) ) ( ( ( X P Y ) ` A ) ` x ) ) ) = ( x e. ( Base ` C ) |-> ( ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` L ) ` x ) ( 2nd ` K ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( R ` ( ( 1st ` L ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` L ) ` x ) ) ` ( S ` x ) ) ) ) ) )
110 26 109 eqtrd 
 |-  ( ph -> ( ( ( Y P Z ) ` B ) ( <. ( O ` X ) , ( O ` Y ) >. .xb ( O ` Z ) ) ( ( X P Y ) ` A ) ) = ( x e. ( Base ` C ) |-> ( ( ( U ` ( ( 1st ` N ) ` x ) ) ( <. ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` N ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( ( ( 1st ` L ) ` x ) ( 2nd ` K ) ( ( 1st ` N ) ` x ) ) ` ( V ` x ) ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) ) ( ( R ` ( ( 1st ` L ) ` x ) ) ( <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` F ) ` ( ( 1st ` L ) ` x ) ) >. ( comp ` E ) ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) ) ( ( ( ( 1st ` G ) ` x ) ( 2nd ` F ) ( ( 1st ` L ) ` x ) ) ` ( S ` x ) ) ) ) ) )