This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prdsplusg

Description: Addition in a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Mario Carneiro, 15-Aug-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)

Ref Expression
Hypotheses prdsbas.p 
|- P = ( S Xs_ R )
prdsbas.s 
|- ( ph -> S e. V )
prdsbas.r 
|- ( ph -> R e. W )
prdsbas.b 
|- B = ( Base ` P )
prdsbas.i 
|- ( ph -> dom R = I )
prdsplusg.b 
|- .+ = ( +g ` P )
Assertion prdsplusg 
|- ( ph -> .+ = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 prdsbas.p 
 |-  P = ( S Xs_ R )
2 prdsbas.s 
 |-  ( ph -> S e. V )
3 prdsbas.r 
 |-  ( ph -> R e. W )
4 prdsbas.b 
 |-  B = ( Base ` P )
5 prdsbas.i 
 |-  ( ph -> dom R = I )
6 prdsplusg.b 
 |-  .+ = ( +g ` P )
7 eqid 
 |-  ( Base ` S ) = ( Base ` S )
8 1 2 3 4 5 prdsbas 
 |-  ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )
9 eqidd 
 |-  ( ph -> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) )
10 eqidd 
 |-  ( ph -> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) )
11 eqidd 
 |-  ( ph -> ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) = ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) )
12 eqidd 
 |-  ( ph -> ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) = ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) )
13 eqidd 
 |-  ( ph -> ( Xt_ ` ( TopOpen o. R ) ) = ( Xt_ ` ( TopOpen o. R ) ) )
14 eqidd 
 |-  ( ph -> { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } = { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } )
15 eqidd 
 |-  ( ph -> ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) )
16 eqidd 
 |-  ( ph -> ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) = ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) )
17 eqidd 
 |-  ( ph -> ( a e. ( B X. B ) , c e. B |-> ( d e. ( ( 2nd ` a ) ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) = ( a e. ( B X. B ) , c e. B |-> ( d e. ( ( 2nd ` a ) ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) )
18 1 7 5 8 9 10 11 12 13 14 15 16 17 2 3 prdsval 
 |-  ( ph -> P = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. R ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) >. , <. ( comp ` ndx ) , ( a e. ( B X. B ) , c e. B |-> ( d e. ( ( 2nd ` a ) ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) )
19 plusgid 
 |-  +g = Slot ( +g ` ndx )
20 ovssunirn 
 |-  ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) C_ U. ran ( +g ` ( R ` x ) )
21 19 strfvss 
 |-  ( +g ` ( R ` x ) ) C_ U. ran ( R ` x )
22 fvssunirn 
 |-  ( R ` x ) C_ U. ran R
23 rnss 
 |-  ( ( R ` x ) C_ U. ran R -> ran ( R ` x ) C_ ran U. ran R )
24 uniss 
 |-  ( ran ( R ` x ) C_ ran U. ran R -> U. ran ( R ` x ) C_ U. ran U. ran R )
25 22 23 24 mp2b 
 |-  U. ran ( R ` x ) C_ U. ran U. ran R
26 21 25 sstri 
 |-  ( +g ` ( R ` x ) ) C_ U. ran U. ran R
27 rnss 
 |-  ( ( +g ` ( R ` x ) ) C_ U. ran U. ran R -> ran ( +g ` ( R ` x ) ) C_ ran U. ran U. ran R )
28 uniss 
 |-  ( ran ( +g ` ( R ` x ) ) C_ ran U. ran U. ran R -> U. ran ( +g ` ( R ` x ) ) C_ U. ran U. ran U. ran R )
29 26 27 28 mp2b 
 |-  U. ran ( +g ` ( R ` x ) ) C_ U. ran U. ran U. ran R
30 20 29 sstri 
 |-  ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) C_ U. ran U. ran U. ran R
31 ovex 
 |-  ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) e. _V
32 31 elpw 
 |-  ( ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) e. ~P U. ran U. ran U. ran R <-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) C_ U. ran U. ran U. ran R )
33 30 32 mpbir 
 |-  ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) e. ~P U. ran U. ran U. ran R
34 33 a1i 
 |-  ( ( ph /\ x e. I ) -> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) e. ~P U. ran U. ran U. ran R )
35 34 fmpttd 
 |-  ( ph -> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) : I --> ~P U. ran U. ran U. ran R )
36 rnexg 
 |-  ( R e. W -> ran R e. _V )
37 uniexg 
 |-  ( ran R e. _V -> U. ran R e. _V )
38 3 36 37 3syl 
 |-  ( ph -> U. ran R e. _V )
39 rnexg 
 |-  ( U. ran R e. _V -> ran U. ran R e. _V )
40 uniexg 
 |-  ( ran U. ran R e. _V -> U. ran U. ran R e. _V )
41 38 39 40 3syl 
 |-  ( ph -> U. ran U. ran R e. _V )
42 rnexg 
 |-  ( U. ran U. ran R e. _V -> ran U. ran U. ran R e. _V )
43 uniexg 
 |-  ( ran U. ran U. ran R e. _V -> U. ran U. ran U. ran R e. _V )
44 pwexg 
 |-  ( U. ran U. ran U. ran R e. _V -> ~P U. ran U. ran U. ran R e. _V )
45 41 42 43 44 4syl 
 |-  ( ph -> ~P U. ran U. ran U. ran R e. _V )
46 3 dmexd 
 |-  ( ph -> dom R e. _V )
47 5 46 eqeltrrd 
 |-  ( ph -> I e. _V )
48 45 47 elmapd 
 |-  ( ph -> ( ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) e. ( ~P U. ran U. ran U. ran R ^m I ) <-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) : I --> ~P U. ran U. ran U. ran R ) )
49 35 48 mpbird 
 |-  ( ph -> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) e. ( ~P U. ran U. ran U. ran R ^m I ) )
50 49 ralrimivw 
 |-  ( ph -> A. g e. B ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) e. ( ~P U. ran U. ran U. ran R ^m I ) )
51 50 ralrimivw 
 |-  ( ph -> A. f e. B A. g e. B ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) e. ( ~P U. ran U. ran U. ran R ^m I ) )
52 eqid 
 |-  ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) )
53 52 fmpo 
 |-  ( A. f e. B A. g e. B ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) e. ( ~P U. ran U. ran U. ran R ^m I ) <-> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) : ( B X. B ) --> ( ~P U. ran U. ran U. ran R ^m I ) )
54 51 53 sylib 
 |-  ( ph -> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) : ( B X. B ) --> ( ~P U. ran U. ran U. ran R ^m I ) )
55 4 fvexi 
 |-  B e. _V
56 55 55 xpex 
 |-  ( B X. B ) e. _V
57 ovex 
 |-  ( ~P U. ran U. ran U. ran R ^m I ) e. _V
58 fex2 
 |-  ( ( ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) : ( B X. B ) --> ( ~P U. ran U. ran U. ran R ^m I ) /\ ( B X. B ) e. _V /\ ( ~P U. ran U. ran U. ran R ^m I ) e. _V ) -> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) e. _V )
59 56 57 58 mp3an23 
 |-  ( ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) : ( B X. B ) --> ( ~P U. ran U. ran U. ran R ^m I ) -> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) e. _V )
60 54 59 syl 
 |-  ( ph -> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) e. _V )
61 snsstp2 
 |-  { <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. } C_ { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. }
62 ssun1 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } )
63 61 62 sstri 
 |-  { <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } )
64 ssun1 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) C_ ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. R ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) >. , <. ( comp ` ndx ) , ( a e. ( B X. B ) , c e. B |-> ( d e. ( ( 2nd ` a ) ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) )
65 63 64 sstri 
 |-  { <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. } C_ ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. R ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) >. , <. ( comp ` ndx ) , ( a e. ( B X. B ) , c e. B |-> ( d e. ( ( 2nd ` a ) ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) )
66 18 6 19 60 65 prdsbaslem 
 |-  ( ph -> .+ = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) )