Metamath Proof Explorer

Theorem fucoisfunc2lem2

Description: Lemma for fucoisfunc2 . (Contributed by Zhi Wang, 14-Sep-2026) (New usage is discouraged.)

Ref Expression
Hypotheses fucoisfunc.w 
|- W = ( ( D Func E ) X. ( C Func D ) )
fucoisfunc2lem1.o 
|- O = ( o.func |` W )
fucoisfunc2lem1.b 
|- B = ( Base ` C )
fucoisfunc2lem1.r 
|- R = ( Hom ` C )
fucoisfunc2lem1.s 
|- S = ( Hom ` E )
fucoisfunc2lem1.v 
|- .xb = ( comp ` E )
fucoisfunc2.t 
|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
fucoisfunc2.q 
|- Q = ( C FuncCat E )
fucoisfunc2.h 
|- H = ( Hom ` T )
fucoisfunc2.i 
|- I = ( Id ` T )
fucoisfunc2.x 
|- .x. = ( comp ` T )
fucoisfunc2.c 
|- ( ph -> C e. Cat )
fucoisfunc2.d 
|- ( ph -> D e. Cat )
fucoisfunc2.e 
|- ( ph -> E e. Cat )
fucoisfunc2.k 
|- K = ( Id ` E )
fucoisfunc2lem2.j 
|- J = ( Id ` Q )
fucoisfunc2lem2.y 
|- .o. = ( comp ` Q )
Assertion fucoisfunc2lem2 
|- ( ph -> ( O ( T Func Q ) P <-> ( ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( ( p ( m P n ) q ) = ( x e. B |-> ( ( p ( m P n ) q ) ` x ) ) /\ A. x e. B ( ( p ( m P n ) q ) ` x ) e. ( ( ( 1st ` ( O ` m ) ) ` x ) S ( ( 1st ` ( O ` n ) ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x R y ) ( ( ( p ( m P n ) q ) ` y ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` m ) ) ` y ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( x ( 2nd ` ( O ` m ) ) y ) ` h ) ) = ( ( ( x ( 2nd ` ( O ` n ) ) y ) ` h ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` n ) ) ` x ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( p ( m P n ) q ) ` x ) ) ) ) ) /\ A. x e. W ( A. t e. B ( ( ( x P x ) ` ( I ` x ) ) ` t ) = ( K ` ( ( 1st ` ( O ` x ) ) ` t ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) A. t e. B ( ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) ` t ) = ( ( ( ( y P z ) ` n ) ` t ) ( <. ( ( 1st ` ( O ` x ) ) ` t ) , ( ( 1st ` ( O ` y ) ) ` t ) >. .xb ( ( 1st ` ( O ` z ) ) ` t ) ) ( ( ( x P y ) ` m ) ` t ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fucoisfunc.w 
 |-  W = ( ( D Func E ) X. ( C Func D ) )
2 fucoisfunc2lem1.o 
 |-  O = ( o.func |` W )
3 fucoisfunc2lem1.b 
 |-  B = ( Base ` C )
4 fucoisfunc2lem1.r 
 |-  R = ( Hom ` C )
5 fucoisfunc2lem1.s 
 |-  S = ( Hom ` E )
6 fucoisfunc2lem1.v 
 |-  .xb = ( comp ` E )
7 fucoisfunc2.t 
 |-  T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
8 fucoisfunc2.q 
 |-  Q = ( C FuncCat E )
9 fucoisfunc2.h 
 |-  H = ( Hom ` T )
10 fucoisfunc2.i 
 |-  I = ( Id ` T )
11 fucoisfunc2.x 
 |-  .x. = ( comp ` T )
12 fucoisfunc2.c 
 |-  ( ph -> C e. Cat )
13 fucoisfunc2.d 
 |-  ( ph -> D e. Cat )
14 fucoisfunc2.e 
 |-  ( ph -> E e. Cat )
15 fucoisfunc2.k 
 |-  K = ( Id ` E )
16 fucoisfunc2lem2.j 
 |-  J = ( Id ` Q )
17 fucoisfunc2lem2.y 
 |-  .o. = ( comp ` Q )
18 1 7 8 2 9 10 16 11 17 12 13 14 fucoisfunc 
 |-  ( ph -> ( O ( T Func Q ) P <-> ( ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m P n ) q ) e. ( ( O ` m ) ( C Nat E ) ( O ` n ) ) ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) )
19 7 fveq2i 
 |-  ( Hom ` T ) = ( Hom ` ( ( D FuncCat E ) Xc. ( C FuncCat D ) ) )
20 9 19 eqtri 
 |-  H = ( Hom ` ( ( D FuncCat E ) Xc. ( C FuncCat D ) ) )
21 1 20 fucofulem2 
 |-  ( P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) <-> ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m P n ) q ) e. ( ( O ` m ) ( C Nat E ) ( O ` n ) ) ) ) )
22 21 anbi1i 
 |-  ( ( P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) <-> ( ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m P n ) q ) e. ( ( O ` m ) ( C Nat E ) ( O ` n ) ) ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) )
23 18 22 bitr4di 
 |-  ( ph -> ( O ( T Func Q ) P <-> ( P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) )
24 7 xpcfucbas 
 |-  ( ( D Func E ) X. ( C Func D ) ) = ( Base ` T )
25 1 24 eqtri 
 |-  W = ( Base ` T )
26 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
27 26 13 14 fuccat 
 |-  ( ph -> ( D FuncCat E ) e. Cat )
28 eqid 
 |-  ( C FuncCat D ) = ( C FuncCat D )
29 28 12 13 fuccat 
 |-  ( ph -> ( C FuncCat D ) e. Cat )
30 7 27 29 xpccat 
 |-  ( ph -> T e. Cat )
31 30 adantr 
 |-  ( ( ph /\ P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) ) -> T e. Cat )
32 simpr 
 |-  ( ( ph /\ P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) ) -> P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) )
33 25 8 3 9 10 16 15 11 17 6 31 32 fucidcobi 
 |-  ( ( ph /\ P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) ) -> ( A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) <-> A. x e. W ( A. t e. B ( ( ( x P x ) ` ( I ` x ) ) ` t ) = ( K ` ( ( 1st ` ( O ` x ) ) ` t ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) A. t e. B ( ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) ` t ) = ( ( ( ( y P z ) ` n ) ` t ) ( <. ( ( 1st ` ( O ` x ) ) ` t ) , ( ( 1st ` ( O ` y ) ) ` t ) >. .xb ( ( 1st ` ( O ` z ) ) ` t ) ) ( ( ( x P y ) ` m ) ` t ) ) ) ) )
34 33 pm5.32da 
 |-  ( ph -> ( ( P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) <-> ( P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) /\ A. x e. W ( A. t e. B ( ( ( x P x ) ` ( I ` x ) ) ` t ) = ( K ` ( ( 1st ` ( O ` x ) ) ` t ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) A. t e. B ( ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) ` t ) = ( ( ( ( y P z ) ` n ) ` t ) ( <. ( ( 1st ` ( O ` x ) ) ` t ) , ( ( 1st ` ( O ` y ) ) ` t ) >. .xb ( ( 1st ` ( O ` z ) ) ` t ) ) ( ( ( x P y ) ` m ) ` t ) ) ) ) ) )
35 23 34 bitrd 
 |-  ( ph -> ( O ( T Func Q ) P <-> ( P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) /\ A. x e. W ( A. t e. B ( ( ( x P x ) ` ( I ` x ) ) ` t ) = ( K ` ( ( 1st ` ( O ` x ) ) ` t ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) A. t e. B ( ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) ` t ) = ( ( ( ( y P z ) ` n ) ` t ) ( <. ( ( 1st ` ( O ` x ) ) ` t ) , ( ( 1st ` ( O ` y ) ) ` t ) >. .xb ( ( 1st ` ( O ` z ) ) ` t ) ) ( ( ( x P y ) ` m ) ` t ) ) ) ) ) )
36 1 2 3 4 5 6 fucoisfunc2lem1 
 |-  ( ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m P n ) q ) e. ( ( O ` m ) ( C Nat E ) ( O ` n ) ) ) ) <-> ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( ( p ( m P n ) q ) = ( x e. B |-> ( ( p ( m P n ) q ) ` x ) ) /\ A. x e. B ( ( p ( m P n ) q ) ` x ) e. ( ( ( 1st ` ( O ` m ) ) ` x ) S ( ( 1st ` ( O ` n ) ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x R y ) ( ( ( p ( m P n ) q ) ` y ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` m ) ) ` y ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( x ( 2nd ` ( O ` m ) ) y ) ` h ) ) = ( ( ( x ( 2nd ` ( O ` n ) ) y ) ` h ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` n ) ) ` x ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( p ( m P n ) q ) ` x ) ) ) ) ) )
37 21 36 bitri 
 |-  ( P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) <-> ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( ( p ( m P n ) q ) = ( x e. B |-> ( ( p ( m P n ) q ) ` x ) ) /\ A. x e. B ( ( p ( m P n ) q ) ` x ) e. ( ( ( 1st ` ( O ` m ) ) ` x ) S ( ( 1st ` ( O ` n ) ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x R y ) ( ( ( p ( m P n ) q ) ` y ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` m ) ) ` y ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( x ( 2nd ` ( O ` m ) ) y ) ` h ) ) = ( ( ( x ( 2nd ` ( O ` n ) ) y ) ` h ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` n ) ) ` x ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( p ( m P n ) q ) ` x ) ) ) ) ) )
38 37 anbi1i 
 |-  ( ( P e. X_ w e. ( W X. W ) ( ( ( O ` ( 1st ` w ) ) ( C Nat E ) ( O ` ( 2nd ` w ) ) ) ^m ( H ` w ) ) /\ A. x e. W ( A. t e. B ( ( ( x P x ) ` ( I ` x ) ) ` t ) = ( K ` ( ( 1st ` ( O ` x ) ) ` t ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) A. t e. B ( ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) ` t ) = ( ( ( ( y P z ) ` n ) ` t ) ( <. ( ( 1st ` ( O ` x ) ) ` t ) , ( ( 1st ` ( O ` y ) ) ` t ) >. .xb ( ( 1st ` ( O ` z ) ) ` t ) ) ( ( ( x P y ) ` m ) ` t ) ) ) ) <-> ( ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( ( p ( m P n ) q ) = ( x e. B |-> ( ( p ( m P n ) q ) ` x ) ) /\ A. x e. B ( ( p ( m P n ) q ) ` x ) e. ( ( ( 1st ` ( O ` m ) ) ` x ) S ( ( 1st ` ( O ` n ) ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x R y ) ( ( ( p ( m P n ) q ) ` y ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` m ) ) ` y ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( x ( 2nd ` ( O ` m ) ) y ) ` h ) ) = ( ( ( x ( 2nd ` ( O ` n ) ) y ) ` h ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` n ) ) ` x ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( p ( m P n ) q ) ` x ) ) ) ) ) /\ A. x e. W ( A. t e. B ( ( ( x P x ) ` ( I ` x ) ) ` t ) = ( K ` ( ( 1st ` ( O ` x ) ) ` t ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) A. t e. B ( ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) ` t ) = ( ( ( ( y P z ) ` n ) ` t ) ( <. ( ( 1st ` ( O ` x ) ) ` t ) , ( ( 1st ` ( O ` y ) ) ` t ) >. .xb ( ( 1st ` ( O ` z ) ) ` t ) ) ( ( ( x P y ) ` m ) ` t ) ) ) ) )
39 35 38 bitrdi 
 |-  ( ph -> ( O ( T Func Q ) P <-> ( ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( ( p ( m P n ) q ) = ( x e. B |-> ( ( p ( m P n ) q ) ` x ) ) /\ A. x e. B ( ( p ( m P n ) q ) ` x ) e. ( ( ( 1st ` ( O ` m ) ) ` x ) S ( ( 1st ` ( O ` n ) ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x R y ) ( ( ( p ( m P n ) q ) ` y ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` m ) ) ` y ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( x ( 2nd ` ( O ` m ) ) y ) ` h ) ) = ( ( ( x ( 2nd ` ( O ` n ) ) y ) ` h ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` n ) ) ` x ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( p ( m P n ) q ) ` x ) ) ) ) ) /\ A. x e. W ( A. t e. B ( ( ( x P x ) ` ( I ` x ) ) ` t ) = ( K ` ( ( 1st ` ( O ` x ) ) ` t ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) A. t e. B ( ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) ` t ) = ( ( ( ( y P z ) ` n ) ` t ) ( <. ( ( 1st ` ( O ` x ) ) ` t ) , ( ( 1st ` ( O ` y ) ) ` t ) >. .xb ( ( 1st ` ( O ` z ) ) ` t ) ) ( ( ( x P y ) ` m ) ` t ) ) ) ) ) )