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 eqid 
 |-  ( C Nat D ) = ( C Nat D )
28 27 natrcl 
 |-  ( S e. ( G ( C Nat D ) L ) -> ( G e. ( C Func D ) /\ L e. ( C Func D ) ) )
29 2 28 syl 
 |-  ( ph -> ( G e. ( C Func D ) /\ L e. ( C Func D ) ) )
30 29 simpld 
 |-  ( ph -> G e. ( C Func D ) )
31 30 func1st2nd 
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
32 eqid 
 |-  ( D Nat E ) = ( D Nat E )
33 32 natrcl 
 |-  ( R e. ( F ( D Nat E ) K ) -> ( F e. ( D Func E ) /\ K e. ( D Func E ) ) )
34 1 33 syl 
 |-  ( ph -> ( F e. ( D Func E ) /\ K e. ( D Func E ) ) )
35 34 simpld 
 |-  ( ph -> F e. ( D Func E ) )
36 35 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
37 relfunc 
 |-  Rel ( D Func E )
38 1st2nd 
 |-  ( ( Rel ( D Func E ) /\ F e. ( D Func E ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
39 37 35 38 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
40 relfunc 
 |-  Rel ( C Func D )
41 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
42 40 30 41 sylancr 
 |-  ( ph -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
43 39 42 opeq12d 
 |-  ( ph -> <. F , G >. = <. <. ( 1st ` F ) , ( 2nd ` F ) >. , <. ( 1st ` G ) , ( 2nd ` G ) >. >. )
44 6 43 eqtrd 
 |-  ( ph -> X = <. <. ( 1st ` F ) , ( 2nd ` F ) >. , <. ( 1st ` G ) , ( 2nd ` G ) >. >. )
45 5 31 36 44 fuco111 
 |-  ( ph -> ( 1st ` ( O ` X ) ) = ( ( 1st ` F ) o. ( 1st ` G ) ) )
46 45 fveq1d 
 |-  ( ph -> ( ( 1st ` ( O ` X ) ) ` x ) = ( ( ( 1st ` F ) o. ( 1st ` G ) ) ` x ) )
47 46 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( O ` X ) ) ` x ) = ( ( ( 1st ` F ) o. ( 1st ` G ) ) ` x ) )
48 eqid 
 |-  ( Base ` D ) = ( Base ` D )
49 14 48 31 funcf1 
 |-  ( ph -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) )
50 49 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) )
51 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
52 50 51 fvco3d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( 1st ` F ) o. ( 1st ` G ) ) ` x ) = ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) )
53 47 52 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( O ` X ) ) ` x ) = ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) )
54 29 simprd 
 |-  ( ph -> L e. ( C Func D ) )
55 54 func1st2nd 
 |-  ( ph -> ( 1st ` L ) ( C Func D ) ( 2nd ` L ) )
56 34 simprd 
 |-  ( ph -> K e. ( D Func E ) )
57 56 func1st2nd 
 |-  ( ph -> ( 1st ` K ) ( D Func E ) ( 2nd ` K ) )
58 1st2nd 
 |-  ( ( Rel ( D Func E ) /\ K e. ( D Func E ) ) -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
59 37 56 58 sylancr 
 |-  ( ph -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
60 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ L e. ( C Func D ) ) -> L = <. ( 1st ` L ) , ( 2nd ` L ) >. )
61 40 54 60 sylancr 
 |-  ( ph -> L = <. ( 1st ` L ) , ( 2nd ` L ) >. )
62 59 61 opeq12d 
 |-  ( ph -> <. K , L >. = <. <. ( 1st ` K ) , ( 2nd ` K ) >. , <. ( 1st ` L ) , ( 2nd ` L ) >. >. )
63 7 62 eqtrd 
 |-  ( ph -> Y = <. <. ( 1st ` K ) , ( 2nd ` K ) >. , <. ( 1st ` L ) , ( 2nd ` L ) >. >. )
64 5 55 57 63 fuco111 
 |-  ( ph -> ( 1st ` ( O ` Y ) ) = ( ( 1st ` K ) o. ( 1st ` L ) ) )
65 64 fveq1d 
 |-  ( ph -> ( ( 1st ` ( O ` Y ) ) ` x ) = ( ( ( 1st ` K ) o. ( 1st ` L ) ) ` x ) )
66 65 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( O ` Y ) ) ` x ) = ( ( ( 1st ` K ) o. ( 1st ` L ) ) ` x ) )
67 14 48 55 funcf1 
 |-  ( ph -> ( 1st ` L ) : ( Base ` C ) --> ( Base ` D ) )
68 67 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` L ) : ( Base ` C ) --> ( Base ` D ) )
69 68 51 fvco3d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( 1st ` K ) o. ( 1st ` L ) ) ` x ) = ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) )
70 66 69 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( O ` Y ) ) ` x ) = ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) )
71 53 70 opeq12d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> <. ( ( 1st ` ( O ` X ) ) ` x ) , ( ( 1st ` ( O ` Y ) ) ` x ) >. = <. ( ( 1st ` F ) ` ( ( 1st ` G ) ` x ) ) , ( ( 1st ` K ) ` ( ( 1st ` L ) ` x ) ) >. )
72 27 natrcl 
 |-  ( V e. ( L ( C Nat D ) N ) -> ( L e. ( C Func D ) /\ N e. ( C Func D ) ) )
73 4 72 syl 
 |-  ( ph -> ( L e. ( C Func D ) /\ N e. ( C Func D ) ) )
74 73 simprd 
 |-  ( ph -> N e. ( C Func D ) )
75 74 func1st2nd 
 |-  ( ph -> ( 1st ` N ) ( C Func D ) ( 2nd ` N ) )
76 32 natrcl 
 |-  ( U e. ( K ( D Nat E ) M ) -> ( K e. ( D Func E ) /\ M e. ( D Func E ) ) )
77 3 76 syl 
 |-  ( ph -> ( K e. ( D Func E ) /\ M e. ( D Func E ) ) )
78 77 simprd 
 |-  ( ph -> M e. ( D Func E ) )
79 78 func1st2nd 
 |-  ( ph -> ( 1st ` M ) ( D Func E ) ( 2nd ` M ) )
80 1st2nd 
 |-  ( ( Rel ( D Func E ) /\ M e. ( D Func E ) ) -> M = <. ( 1st ` M ) , ( 2nd ` M ) >. )
81 37 78 80 sylancr 
 |-  ( ph -> M = <. ( 1st ` M ) , ( 2nd ` M ) >. )
82 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ N e. ( C Func D ) ) -> N = <. ( 1st ` N ) , ( 2nd ` N ) >. )
83 40 74 82 sylancr 
 |-  ( ph -> N = <. ( 1st ` N ) , ( 2nd ` N ) >. )
84 81 83 opeq12d 
 |-  ( ph -> <. M , N >. = <. <. ( 1st ` M ) , ( 2nd ` M ) >. , <. ( 1st ` N ) , ( 2nd ` N ) >. >. )
85 8 84 eqtrd 
 |-  ( ph -> Z = <. <. ( 1st ` M ) , ( 2nd ` M ) >. , <. ( 1st ` N ) , ( 2nd ` N ) >. >. )
86 5 75 79 85 fuco111 
 |-  ( ph -> ( 1st ` ( O ` Z ) ) = ( ( 1st ` M ) o. ( 1st ` N ) ) )
87 86 fveq1d 
 |-  ( ph -> ( ( 1st ` ( O ` Z ) ) ` x ) = ( ( ( 1st ` M ) o. ( 1st ` N ) ) ` x ) )
88 87 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( O ` Z ) ) ` x ) = ( ( ( 1st ` M ) o. ( 1st ` N ) ) ` x ) )
89 14 48 75 funcf1 
 |-  ( ph -> ( 1st ` N ) : ( Base ` C ) --> ( Base ` D ) )
90 89 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` N ) : ( Base ` C ) --> ( Base ` D ) )
91 90 51 fvco3d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( 1st ` M ) o. ( 1st ` N ) ) ` x ) = ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) )
92 88 91 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( O ` Z ) ) ` x ) = ( ( 1st ` M ) ` ( ( 1st ` N ) ` x ) ) )
93 71 92 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 ) ) ) )
94 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 ) ) ) ) )
95 23 94 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 ) ) ) ) )
96 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 )
97 95 96 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 ) ) ) )
98 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 ) ) ) ) )
99 18 98 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 ) ) ) ) )
100 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 )
101 99 100 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 ) ) ) )
102 93 97 101 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 ) ) ) ) )
103 102 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 ) ) ) ) ) )
104 26 103 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 ) ) ) ) ) )