Step | Hyp | Ref
| Expression |
1 | | dmeq 5035 |
. . . . . . . . 9

  |
2 | 1 | dmeqd 5037 |
. . . . . . . 8
   |
3 | | oveq 6296 |
. . . . . . . . . 10
           |
4 | 3 | fveq2d 5869 |
. . . . . . . . 9
 coe1      coe1        |
5 | 4 | fveq1d 5867 |
. . . . . . . 8
  coe1          coe1           |
6 | 2, 2, 5 | mpt2eq123dv 6353 |
. . . . . . 7
  
 coe1           
 coe1            |
7 | | fveq2 5865 |
. . . . . . . 8
  coe1          coe1           |
8 | 7 | mpt2eq3dv 6357 |
. . . . . . 7
  
 coe1           
 coe1            |
9 | 6, 8 | cbvmpt2v 6371 |
. . . . . 6
   
 coe1              
 coe1            |
10 | | dmexg 6724 |
. . . . . . . . . . 11

  |
11 | | dmexg 6724 |
. . . . . . . . . . 11
   |
12 | 10, 11 | syl 17 |
. . . . . . . . . 10
   |
13 | 12, 12 | jca 535 |
. . . . . . . . 9
     |
14 | 13 | ad2antrl 734 |
. . . . . . . 8
   


  
 
    |
15 | | mpt2exga 6869 |
. . . . . . . 8
 
  
 coe1            |
16 | 14, 15 | syl 17 |
. . . . . . 7
   


  
 

  coe1            |
17 | 16 | ralrimivva 2809 |
. . . . . 6
    
  

   coe1            |
18 | | simprr 766 |
. . . . . 6
    
    |
19 | | nn0ex 10875 |
. . . . . . . 8
 |
20 | 19 | ssex 4547 |
. . . . . . 7

  |
21 | 20 | ad2antrl 734 |
. . . . . 6
    
 
  |
22 | | simp3 1010 |
. . . . . . 7
 
   |
23 | 22 | adantr 467 |
. . . . . 6
    
 
  |
24 | 9, 17, 18, 21, 23 | mpt2curryvald 7017 |
. . . . 5
    
  curry      coe1                 ![]_ ]_](_urbrack.gif)    coe1             |
25 | | fveq2 5865 |
. . . . . . . . 9
  coe1          coe1           |
26 | 25 | mpt2eq3dv 6357 |
. . . . . . . 8
  
 coe1           
 coe1            |
27 | 26 | csbeq2dv 3781 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)  
 coe1            ![]_ ]_](_urbrack.gif)  
 coe1            |
28 | | eqcom 2458 |
. . . . . . . . 9

  |
29 | | eqcom 2458 |
. . . . . . . . 9
  
 coe1           
 coe1         

  coe1           
 coe1            |
30 | 6, 28, 29 | 3imtr3i 269 |
. . . . . . . 8
  
 coe1           
 coe1            |
31 | 30 | cbvcsbv 3369 |
. . . . . . 7
  ![]_ ]_](_urbrack.gif)  
 coe1            ![]_ ]_](_urbrack.gif)  
 coe1           |
32 | 27, 31 | syl6eq 2501 |
. . . . . 6
   ![]_ ]_](_urbrack.gif)  
 coe1            ![]_ ]_](_urbrack.gif)  
 coe1            |
33 | 32 | cbvmptv 4495 |
. . . . 5
   ![]_ ]_](_urbrack.gif)  
 coe1              ![]_ ]_](_urbrack.gif)    coe1            |
34 | 24, 33 | syl6eq 2501 |
. . . 4
    
  curry      coe1                 ![]_ ]_](_urbrack.gif)    coe1             |
35 | | dmeq 5035 |
. . . . . . . . . . 11

  |
36 | 35 | dmeqd 5037 |
. . . . . . . . . 10
   |
37 | | oveq 6296 |
. . . . . . . . . . . 12
           |
38 | 37 | fveq2d 5869 |
. . . . . . . . . . 11
 coe1      coe1        |
39 | 38 | fveq1d 5867 |
. . . . . . . . . 10
  coe1          coe1           |
40 | 36, 36, 39 | mpt2eq123dv 6353 |
. . . . . . . . 9
  
 coe1             coe1            |
41 | 40 | adantl 468 |
. . . . . . . 8
      
 coe1             coe1            |
42 | 22, 41 | csbied 3390 |
. . . . . . 7
 
   ![]_ ]_](_urbrack.gif)  
 coe1           
 coe1            |
43 | | pmatcollpw.c |
. . . . . . . . . . . . 13
 Mat   |
44 | | eqid 2451 |
. . . . . . . . . . . . 13
         |
45 | | pmatcollpw.b |
. . . . . . . . . . . . 13
     |
46 | 43, 44, 45 | matbas2i 19447 |
. . . . . . . . . . . 12
     
     |
47 | | elmapi 7493 |
. . . . . . . . . . . 12
                     |
48 | | fdm 5733 |
. . . . . . . . . . . . . 14
               |
49 | 48 | dmeqd 5037 |
. . . . . . . . . . . . 13
               |
50 | | dmxpid 5054 |
. . . . . . . . . . . . 13
   |
51 | 49, 50 | syl6req 2502 |
. . . . . . . . . . . 12
          
  |
52 | 46, 47, 51 | 3syl 18 |
. . . . . . . . . . 11

  |
53 | 52 | 3ad2ant3 1031 |
. . . . . . . . . 10
 

  |
54 | 53 | adantr 467 |
. . . . . . . . 9
    
  |
55 | | simpr 463 |
. . . . . . . . . . . 12
       |
56 | 55 | oveqd 6307 |
. . . . . . . . . . 11
               |
57 | 56 | fveq2d 5869 |
. . . . . . . . . 10
     coe1      coe1        |
58 | 57 | fveq1d 5867 |
. . . . . . . . 9
      coe1          coe1           |
59 | 54, 54, 58 | mpt2eq123dv 6353 |
. . . . . . . 8
        coe1             coe1            |
60 | 22, 59 | csbied 3390 |
. . . . . . 7
 
   ![]_ ]_](_urbrack.gif)    coe1             coe1            |
61 | 42, 60 | eqtr4d 2488 |
. . . . . 6
 
   ![]_ ]_](_urbrack.gif)  
 coe1            ![]_ ]_](_urbrack.gif)    coe1            |
62 | 61 | adantr 467 |
. . . . 5
    
  
 ![]_ ]_](_urbrack.gif)    coe1            ![]_ ]_](_urbrack.gif)    coe1            |
63 | 62 | mpteq2dv 4490 |
. . . 4
    
     ![]_ ]_](_urbrack.gif)    coe1              ![]_ ]_](_urbrack.gif)  
 coe1             |
64 | 34, 63 | eqtrd 2485 |
. . 3
    
  curry      coe1                 ![]_ ]_](_urbrack.gif)  
 coe1             |
65 | | oveq 6296 |
. . . . . . . . . . . 12
           |
66 | 65 | adantl 468 |
. . . . . . . . . . 11
               |
67 | 66 | fveq2d 5869 |
. . . . . . . . . 10
     coe1      coe1        |
68 | 67 | fveq1d 5867 |
. . . . . . . . 9
      coe1          coe1           |
69 | 68 | mpt2eq3dv 6357 |
. . . . . . . 8
        coe1           
 coe1            |
70 | 22, 69 | csbied 3390 |
. . . . . . 7
 
   ![]_ ]_](_urbrack.gif)    coe1             coe1            |
71 | 70 | ad2antrr 732 |
. . . . . 6
   


     ![]_ ]_](_urbrack.gif)    coe1             coe1            |
72 | | pmatcollpw3.a |
. . . . . . 7
 Mat   |
73 | | eqid 2451 |
. . . . . . 7
         |
74 | | pmatcollpw3.d |
. . . . . . 7
     |
75 | | simpll1 1047 |
. . . . . . 7
   


     |
76 | | simpll2 1048 |
. . . . . . 7
   


     |
77 | | simp2 1009 |
. . . . . . . . 9
    
 
 


  |
78 | | simp3 1010 |
. . . . . . . . 9
    
 
 


  |
79 | 23 | adantr 467 |
. . . . . . . . . 10
   


     |
80 | 79 | 3ad2ant1 1029 |
. . . . . . . . 9
    
 
 


  |
81 | 43, 44, 45, 77, 78, 80 | matecld 19451 |
. . . . . . . 8
    
 
 


          |
82 | | ssel 3426 |
. . . . . . . . . . 11

    |
83 | 82 | ad2antrl 734 |
. . . . . . . . . 10
    
      |
84 | 83 | imp 431 |
. . . . . . . . 9
   


     |
85 | 84 | 3ad2ant1 1029 |
. . . . . . . 8
    
 
 


  |
86 | | eqid 2451 |
. . . . . . . . 9
coe1      coe1       |
87 | | pmatcollpw.p |
. . . . . . . . 9
Poly1   |
88 | 86, 44, 87, 73 | coe1fvalcl 18805 |
. . . . . . . 8
            coe1               |
89 | 81, 85, 88 | syl2anc 667 |
. . . . . . 7
    
 
 


 coe1               |
90 | 72, 73, 74, 75, 76, 89 | matbas2d 19448 |
. . . . . 6
   


      coe1            |
91 | 71, 90 | eqeltrd 2529 |
. . . . 5
   


     ![]_ ]_](_urbrack.gif)    coe1            |
92 | | eqid 2451 |
. . . . 5
   ![]_ ]_](_urbrack.gif)    coe1              ![]_ ]_](_urbrack.gif)  
 coe1            |
93 | 91, 92 | fmptd 6046 |
. . . 4
    
     ![]_ ]_](_urbrack.gif)  
 coe1                 |
94 | | fvex 5875 |
. . . . . . 7
     |
95 | 74, 94 | eqeltri 2525 |
. . . . . 6
 |
96 | 95 | a1i 11 |
. . . . 5
 
   |
97 | 20 | adantr 467 |
. . . . 5
 
   |
98 | | elmapg 7485 |
. . . . 5
 
     ![]_ ]_](_urbrack.gif)  
 coe1            

  ![]_ ]_](_urbrack.gif)    coe1                  |
99 | 96, 97, 98 | syl2an 480 |
. . . 4
    
      ![]_ ]_](_urbrack.gif)  
 coe1            

  ![]_ ]_](_urbrack.gif)    coe1                  |
100 | 93, 99 | mpbird 236 |
. . 3
    
     ![]_ ]_](_urbrack.gif)  
 coe1               |
101 | 64, 100 | eqeltrd 2529 |
. 2
    
  curry      coe1                  |
102 | | fveq1 5864 |
. . . . . . . . . . 11
 curry    
 coe1             
     curry      coe1                   |
103 | 102 | adantl 468 |
. . . . . . . . . 10
   


  curry      coe1                    curry      coe1                   |
104 | 103 | adantr 467 |
. . . . . . . . 9
    
 
 
curry    
 coe1              
      curry  
   coe1                   |
105 | | eqid 2451 |
. . . . . . . . . . . 12
   
 coe1              
 coe1            |
106 | | dmexg 6724 |
. . . . . . . . . . . . . . . . 17

  |
107 | | dmexg 6724 |
. . . . . . . . . . . . . . . . 17
   |
108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . 16
   |
109 | 108, 108 | jca 535 |
. . . . . . . . . . . . . . 15
     |
110 | 109 | ad2antrl 734 |
. . . . . . . . . . . . . 14
    
 
 
 
      |
111 | | mpt2exga 6869 |
. . . . . . . . . . . . . 14
 
  
 coe1            |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . 13
    
 
 
 
   
 coe1            |
113 | 112 | ralrimivva 2809 |
. . . . . . . . . . . 12
   


   


  coe1            |
114 | 21 | adantr 467 |
. . . . . . . . . . . 12
   


     |
115 | 23 | adantr 467 |
. . . . . . . . . . . 12
   


     |
116 | | simpr 463 |
. . . . . . . . . . . 12
   


     |
117 | 105, 113,
114, 115, 116 | fvmpt2curryd 7018 |
. . . . . . . . . . 11
   


    curry      coe1                        coe1               |
118 | | df-decpmat 19787 |
. . . . . . . . . . . . . 14
decompPMat    
 coe1            |
119 | 118 | reseq1i 5101 |
. . . . . . . . . . . . 13
decompPMat      
 
 coe1               |
120 | | ssv 3452 |
. . . . . . . . . . . . . . . . 17
 |
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
   |
122 | | simpl 459 |
. . . . . . . . . . . . . . . 16
 
   |
123 | 121, 122 | anim12i 570 |
. . . . . . . . . . . . . . 15
    
  
   |
124 | 123 | adantr 467 |
. . . . . . . . . . . . . 14
   


       |
125 | | resmpt2 6394 |
. . . . . . . . . . . . . 14
 
   
   coe1           
     
 coe1             |
126 | 124, 125 | syl 17 |
. . . . . . . . . . . . 13
   


     
   coe1           
     
 coe1             |
127 | 119, 126 | syl5req 2498 |
. . . . . . . . . . . 12
   


      
 coe1           decompPMat      |
128 | 127 | oveqd 6307 |
. . . . . . . . . . 11
   


          coe1               decompPMat
       |
129 | 117, 128 | eqtrd 2485 |
. . . . . . . . . 10
   


    curry      coe1                   decompPMat
       |
130 | 129 | adantlr 721 |
. . . . . . . . 9
    
 
 
curry    
 coe1              
  curry    
 coe1                   decompPMat        |
131 | 104, 130 | eqtrd 2485 |
. . . . . . . 8
    
 
 
curry    
 coe1              
       decompPMat        |
132 | 131 | fveq2d 5869 |
. . . . . . 7
    
 
 
curry    
 coe1              
              decompPMat         |
133 | 22 | ad2antrr 732 |
. . . . . . . . 9
   


  curry      coe1                 |
134 | | ovres 6436 |
. . . . . . . . 9
 
   decompPMat       decompPMat    |
135 | 133, 134 | sylan 474 |
. . . . . . . 8
    
 
 
curry    
 coe1              
   decompPMat       decompPMat    |
136 | 135 | fveq2d 5869 |
. . . . . . 7
    
 
 
curry    
 coe1              
     
decompPMat
          decompPMat     |
137 | 132, 136 | eqtrd 2485 |
. . . . . 6
    
 
 
curry    
 coe1              
             decompPMat     |
138 | 137 | oveq2d 6306 |
. . . . 5
    
 
 
curry    
 coe1              
                    decompPMat      |
139 | 138 | mpteq2dva 4489 |
. . . 4
   


  curry      coe1                                     decompPMat       |
140 | 139 | oveq2d 6306 |
. . 3
   


  curry      coe1                g   
             g   
     decompPMat        |
141 | 140 | eqeq2d 2461 |
. 2
   


  curry      coe1                 g               

g         decompPMat         |
142 | 101, 141 | rspcedv 3154 |
1
    
    g         decompPMat     
     g                   |