Step | Hyp | Ref
| Expression |
1 | | xpsds.t |
. . . . 5
 s   |
2 | | xpsds.x |
. . . . 5
     |
3 | | xpsds.y |
. . . . 5
     |
4 | | xpsds.1 |
. . . . 5
   |
5 | | xpsds.2 |
. . . . 5
   |
6 | | eqid 2451 |
. . . . 5
                     |
7 | | eqid 2451 |
. . . . 5
Scalar  Scalar   |
8 | | eqid 2451 |
. . . . 5
 Scalar   s         Scalar   s         |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsval 14612 |
. . . 4
    
        s
 Scalar   s           |
10 | 1, 2, 3, 4, 5, 6, 7, 8 | xpslem 14613 |
. . . 4
               Scalar   s           |
11 | 6 | xpsff1o2 14611 |
. . . . 5
                           |
12 | | f1ocnv 5751 |
. . . . 5
                          
                             |
13 | 11, 12 | mp1i 12 |
. . . 4
                              |
14 | | ovex 6215 |
. . . . 5
 Scalar   s         |
15 | 14 | a1i 11 |
. . . 4
  Scalar   s          |
16 | | eqid 2451 |
. . . 4
     Scalar   s                                     Scalar   s           
        

           |
17 | | xpsds.p |
. . . 4
     |
18 | | xpsds.m |
. . . . . 6
         |
19 | | xpsds.n |
. . . . . 6
         |
20 | | xpsds.3 |
. . . . . 6
        |
21 | | xpsds.4 |
. . . . . 6
        |
22 | 1, 2, 3, 4, 5, 17,
18, 19, 20, 21 | xpsxmetlem 20070 |
. . . . 5
     Scalar   s             

           |
23 | | ssid 3473 |
. . . . 5
         
           |
24 | | xmetres2 20052 |
. . . . 5
      Scalar   s             

          
        

              Scalar   s           
        

                           |
25 | 22, 23, 24 | sylancl 662 |
. . . 4
      Scalar   s           
        

                           |
26 | | df-ov 6193 |
. . . . . 6
   
                            |
27 | | xpsds.a |
. . . . . . 7
   |
28 | | xpsds.b |
. . . . . . 7
   |
29 | 6 | xpsfval 14607 |
. . . . . . 7
 
                        |
30 | 27, 28, 29 | syl2anc 661 |
. . . . . 6
                        |
31 | 26, 30 | syl5eqr 2506 |
. . . . 5
                           |
32 | | opelxpi 4969 |
. . . . . . 7
 
        |
33 | 27, 28, 32 | syl2anc 661 |
. . . . . 6
        |
34 | | f1of 5739 |
. . . . . . . 8
                          
                            |
35 | 11, 34 | ax-mp 5 |
. . . . . . 7
                           |
36 | 35 | ffvelrni 5941 |
. . . . . 6
  
  
                 

          |
37 | 33, 36 | syl 16 |
. . . . 5
                              |
38 | 31, 37 | eqeltrrd 2540 |
. . . 4
                    |
39 | | df-ov 6193 |
. . . . . 6
   
                            |
40 | | xpsds.c |
. . . . . . 7
   |
41 | | xpsds.d |
. . . . . . 7
   |
42 | 6 | xpsfval 14607 |
. . . . . . 7
 
                        |
43 | 40, 41, 42 | syl2anc 661 |
. . . . . 6
                        |
44 | 39, 43 | syl5eqr 2506 |
. . . . 5
                           |
45 | | opelxpi 4969 |
. . . . . . 7
 
        |
46 | 40, 41, 45 | syl2anc 661 |
. . . . . 6
        |
47 | 35 | ffvelrni 5941 |
. . . . . 6
  
  
                 

          |
48 | 46, 47 | syl 16 |
. . . . 5
                              |
49 | 44, 48 | eqeltrrd 2540 |
. . . 4
                    |
50 | 9, 10, 13, 15, 16, 17, 25, 38, 49 | imasdsf1o 20065 |
. . 3
                                                               Scalar   s           
        

                     |
51 | 38, 49 | ovresd 6331 |
. . 3
               Scalar   s                                                      Scalar   s                    |
52 | 50, 51 | eqtrd 2492 |
. 2
                                                              Scalar   s                    |
53 | | f1ocnvfv 6084 |
. . . . 5
   
               
             
   
                    
  

                        |
54 | 11, 33, 53 | sylancr 663 |
. . . 4
                                                      |
55 | 31, 54 | mpd 15 |
. . 3
                            |
56 | | f1ocnvfv 6084 |
. . . . 5
   
               
             
   
                    
  

                        |
57 | 11, 46, 56 | sylancr 663 |
. . . 4
                                                      |
58 | 44, 57 | mpd 15 |
. . 3
                            |
59 | 55, 58 | oveq12d 6208 |
. 2
                                                   
         |
60 | | eqid 2451 |
. . . 4
    Scalar   s             Scalar   s          |
61 | | fvex 5799 |
. . . . 5
Scalar   |
62 | 61 | a1i 11 |
. . . 4
 Scalar    |
63 | | 2on 7028 |
. . . . 5
 |
64 | 63 | a1i 11 |
. . . 4
   |
65 | | xpscfn 14599 |
. . . . 5
 
          |
66 | 4, 5, 65 | syl2anc 661 |
. . . 4
          |
67 | 38, 10 | eleqtrd 2541 |
. . . 4
            Scalar   s           |
68 | 49, 10 | eleqtrd 2541 |
. . . 4
            Scalar   s           |
69 | | eqid 2451 |
. . . 4
    Scalar   s             Scalar   s          |
70 | 8, 60, 62, 64, 66, 67, 68, 69 | prdsdsval 14518 |
. . 3
              Scalar   s                    
                                               
  |
71 | | df2o3 7033 |
. . . . . . . . . . 11
    |
72 | 71 | rexeqi 3018 |
. . . . . . . . . 10
                                                                                           |
73 | | 0ex 4520 |
. . . . . . . . . . 11
 |
74 | | 1on 7027 |
. . . . . . . . . . . 12
 |
75 | 74 | elexi 3078 |
. . . . . . . . . . 11
 |
76 | | fveq2 5789 |
. . . . . . . . . . . . . 14

                        |
77 | 76 | fveq2d 5793 |
. . . . . . . . . . . . 13

                                |
78 | | fveq2 5789 |
. . . . . . . . . . . . 13

                        |
79 | | fveq2 5789 |
. . . . . . . . . . . . 13

                        |
80 | 77, 78, 79 | oveq123d 6211 |
. . . . . . . . . . . 12

                                                                                    |
81 | 80 | eqeq2d 2465 |
. . . . . . . . . . 11

                                         
                                            |
82 | | fveq2 5789 |
. . . . . . . . . . . . . 14
                         |
83 | 82 | fveq2d 5793 |
. . . . . . . . . . . . 13
                                 |
84 | | fveq2 5789 |
. . . . . . . . . . . . 13
                         |
85 | | fveq2 5789 |
. . . . . . . . . . . . 13
                         |
86 | 83, 84, 85 | oveq123d 6211 |
. . . . . . . . . . . 12
                                                                                     |
87 | 86 | eqeq2d 2465 |
. . . . . . . . . . 11
                                          
                                            |
88 | 73, 75, 81, 87 | rexpr 4028 |
. . . . . . . . . 10
                                                                                                                                     |
89 | 72, 88 | bitri 249 |
. . . . . . . . 9
                                                                                                                                 |
90 | | xpsc0 14600 |
. . . . . . . . . . . . . . 15
              |
91 | 4, 90 | syl 16 |
. . . . . . . . . . . . . 14
              |
92 | 91 | fveq2d 5793 |
. . . . . . . . . . . . 13
                      |
93 | | xpsc0 14600 |
. . . . . . . . . . . . . 14
              |
94 | 27, 93 | syl 16 |
. . . . . . . . . . . . 13
              |
95 | | xpsc0 14600 |
. . . . . . . . . . . . . 14
              |
96 | 40, 95 | syl 16 |
. . . . . . . . . . . . 13
              |
97 | 92, 94, 96 | oveq123d 6211 |
. . . . . . . . . . . 12
                                                    |
98 | 18 | oveqi 6203 |
. . . . . . . . . . . . 13
                 |
99 | 27, 40 | ovresd 6331 |
. . . . . . . . . . . . 13
                       |
100 | 98, 99 | syl5eq 2504 |
. . . . . . . . . . . 12
               |
101 | 97, 100 | eqtr4d 2495 |
. . . . . . . . . . 11
                                                |
102 | 101 | eqeq2d 2465 |
. . . . . . . . . 10
                                          
       |
103 | | xpsc1 14601 |
. . . . . . . . . . . . . . 15
              |
104 | 5, 103 | syl 16 |
. . . . . . . . . . . . . 14
           
  |
105 | 104 | fveq2d 5793 |
. . . . . . . . . . . . 13
                      |
106 | | xpsc1 14601 |
. . . . . . . . . . . . . 14
              |
107 | 28, 106 | syl 16 |
. . . . . . . . . . . . 13
           
  |
108 | | xpsc1 14601 |
. . . . . . . . . . . . . 14
              |
109 | 41, 108 | syl 16 |
. . . . . . . . . . . . 13
           
  |
110 | 105, 107,
109 | oveq123d 6211 |
. . . . . . . . . . . 12
                                                    |
111 | 19 | oveqi 6203 |
. . . . . . . . . . . . 13
                 |
112 | 28, 41 | ovresd 6331 |
. . . . . . . . . . . . 13
                       |
113 | 111, 112 | syl5eq 2504 |
. . . . . . . . . . . 12
               |
114 | 110, 113 | eqtr4d 2495 |
. . . . . . . . . . 11
                                                |
115 | 114 | eqeq2d 2465 |
. . . . . . . . . 10
                                          
       |
116 | 102, 115 | orbi12d 709 |
. . . . . . . . 9
                                                                                     
             |
117 | 89, 116 | syl5bb 257 |
. . . . . . . 8
                                           
             |
118 | | vex 3071 |
. . . . . . . . 9
 |
119 | | eqid 2451 |
. . . . . . . . . 10
                                                                                       |
120 | 119 | elrnmpt 5184 |
. . . . . . . . 9
                                             
                                            |
121 | 118, 120 | ax-mp 5 |
. . . . . . . 8
                                           
                                            |
122 | 118 | elpr 3993 |
. . . . . . . 8
           
            |
123 | 117, 121,
122 | 3bitr4g 288 |
. . . . . . 7
                                            
              |
124 | 123 | eqrdv 2448 |
. . . . . 6
                                                         |
125 | 124 | uneq1d 3607 |
. . . . 5
                                                                 |
126 | | uncom 3598 |
. . . . 5
                               |
127 | 125, 126 | syl6eq 2508 |
. . . 4
                                                                 |
128 | 127 | supeq1d 7797 |
. . 3
                                                                         |
129 | | 0xr 9531 |
. . . . . 6
 |
130 | 129 | a1i 11 |
. . . . 5
   |
131 | 130 | snssd 4116 |
. . . 4
     |
132 | | xmetcl 20022 |
. . . . . 6
      

      |
133 | 20, 27, 40, 132 | syl3anc 1219 |
. . . . 5
       |
134 | | xmetcl 20022 |
. . . . . 6
      

      |
135 | 21, 28, 41, 134 | syl3anc 1219 |
. . . . 5
       |
136 | | prssi 4127 |
. . . . 5
                        |
137 | 133, 135,
136 | syl2anc 661 |
. . . 4
           
  |
138 | | xrltso 11219 |
. . . . . 6
 |
139 | | supsn 7820 |
. . . . . 6
          |
140 | 138, 129,
139 | mp2an 672 |
. . . . 5
       |
141 | | supxrcl 11378 |
. . . . . . 7
           
                 |
142 | 137, 141 | syl 16 |
. . . . . 6
                  |
143 | | xmetge0 20035 |
. . . . . . 7
      

      |
144 | 20, 27, 40, 143 | syl3anc 1219 |
. . . . . 6

      |
145 | | ovex 6215 |
. . . . . . . 8
     |
146 | 145 | prid1 4081 |
. . . . . . 7
                |
147 | | supxrub 11388 |
. . . . . . 7
            
                                     |
148 | 137, 146,
147 | sylancl 662 |
. . . . . 6
    
                 |
149 | 130, 133,
142, 144, 148 | xrletrd 11237 |
. . . . 5

                 |
150 | 140, 149 | syl5eqbr 4423 |
. . . 4
                        |
151 | | supxrun 11379 |
. . . 4
                                                                         |
152 | 131, 137,
150, 151 | syl3anc 1219 |
. . 3
                                     |
153 | 70, 128, 152 | 3eqtrd 2496 |
. 2
              Scalar   s                                   |
154 | 52, 59, 153 | 3eqtr3d 2500 |
1
                            |