Step | Hyp | Ref
| Expression |
1 | | dmeq 5324 |
. . . . . . . . 9
|
2 | 1 | dmeqd 5326 |
. . . . . . . 8
|
3 | | oveq 6656 |
. . . . . . . . . 10
|
4 | 3 | fveq2d 6195 |
. . . . . . . . 9
coe1 coe1 |
5 | 4 | fveq1d 6193 |
. . . . . . . 8
coe1 coe1 |
6 | 2, 2, 5 | mpt2eq123dv 6717 |
. . . . . . 7
coe1
coe1 |
7 | | fveq2 6191 |
. . . . . . . 8
coe1 coe1 |
8 | 7 | mpt2eq3dv 6721 |
. . . . . . 7
coe1
coe1 |
9 | 6, 8 | cbvmpt2v 6735 |
. . . . . 6
coe1
coe1 |
10 | | dmexg 7097 |
. . . . . . . . . . 11
|
11 | | dmexg 7097 |
. . . . . . . . . . 11
|
12 | 10, 11 | syl 17 |
. . . . . . . . . 10
|
13 | 12, 12 | jca 554 |
. . . . . . . . 9
|
14 | 13 | ad2antrl 764 |
. . . . . . . 8
|
15 | | mpt2exga 7246 |
. . . . . . . 8
coe1 |
16 | 14, 15 | syl 17 |
. . . . . . 7
coe1 |
17 | 16 | ralrimivva 2971 |
. . . . . 6
coe1 |
18 | | simprr 796 |
. . . . . 6
|
19 | | nn0ex 11298 |
. . . . . . . 8
|
20 | 19 | ssex 4802 |
. . . . . . 7
|
21 | 20 | ad2antrl 764 |
. . . . . 6
|
22 | | simp3 1063 |
. . . . . . 7
|
23 | 22 | adantr 481 |
. . . . . 6
|
24 | 9, 17, 18, 21, 23 | mpt2curryvald 7396 |
. . . . 5
curry coe1 coe1 |
25 | | fveq2 6191 |
. . . . . . . . 9
coe1 coe1 |
26 | 25 | mpt2eq3dv 6721 |
. . . . . . . 8
coe1
coe1 |
27 | 26 | csbeq2dv 3992 |
. . . . . . 7
coe1
coe1 |
28 | | eqcom 2629 |
. . . . . . . . 9
|
29 | | eqcom 2629 |
. . . . . . . . 9
coe1
coe1
coe1
coe1 |
30 | 6, 28, 29 | 3imtr3i 280 |
. . . . . . . 8
coe1
coe1 |
31 | 30 | cbvcsbv 3539 |
. . . . . . 7
coe1
coe1 |
32 | 27, 31 | syl6eq 2672 |
. . . . . 6
coe1
coe1 |
33 | 32 | cbvmptv 4750 |
. . . . 5
coe1 coe1 |
34 | 24, 33 | syl6eq 2672 |
. . . 4
curry coe1 coe1 |
35 | | dmeq 5324 |
. . . . . . . . . . 11
|
36 | 35 | dmeqd 5326 |
. . . . . . . . . 10
|
37 | | oveq 6656 |
. . . . . . . . . . . 12
|
38 | 37 | fveq2d 6195 |
. . . . . . . . . . 11
coe1 coe1 |
39 | 38 | fveq1d 6193 |
. . . . . . . . . 10
coe1 coe1 |
40 | 36, 36, 39 | mpt2eq123dv 6717 |
. . . . . . . . 9
coe1 coe1 |
41 | 40 | adantl 482 |
. . . . . . . 8
coe1 coe1 |
42 | 22, 41 | csbied 3560 |
. . . . . . 7
coe1
coe1 |
43 | | pmatcollpw.c |
. . . . . . . . . . . . 13
Mat |
44 | | eqid 2622 |
. . . . . . . . . . . . 13
|
45 | | pmatcollpw.b |
. . . . . . . . . . . . 13
|
46 | 43, 44, 45 | matbas2i 20228 |
. . . . . . . . . . . 12
|
47 | | elmapi 7879 |
. . . . . . . . . . . 12
|
48 | | fdm 6051 |
. . . . . . . . . . . . . 14
|
49 | 48 | dmeqd 5326 |
. . . . . . . . . . . . 13
|
50 | | dmxpid 5345 |
. . . . . . . . . . . . 13
|
51 | 49, 50 | syl6req 2673 |
. . . . . . . . . . . 12
|
52 | 46, 47, 51 | 3syl 18 |
. . . . . . . . . . 11
|
53 | 52 | 3ad2ant3 1084 |
. . . . . . . . . 10
|
54 | 53 | adantr 481 |
. . . . . . . . 9
|
55 | | simpr 477 |
. . . . . . . . . . . 12
|
56 | 55 | oveqd 6667 |
. . . . . . . . . . 11
|
57 | 56 | fveq2d 6195 |
. . . . . . . . . 10
coe1 coe1 |
58 | 57 | fveq1d 6193 |
. . . . . . . . 9
coe1 coe1 |
59 | 54, 54, 58 | mpt2eq123dv 6717 |
. . . . . . . 8
coe1 coe1 |
60 | 22, 59 | csbied 3560 |
. . . . . . 7
coe1 coe1 |
61 | 42, 60 | eqtr4d 2659 |
. . . . . 6
coe1 coe1 |
62 | 61 | adantr 481 |
. . . . 5
coe1 coe1 |
63 | 62 | mpteq2dv 4745 |
. . . 4
coe1
coe1 |
64 | 34, 63 | eqtrd 2656 |
. . 3
curry coe1
coe1 |
65 | | oveq 6656 |
. . . . . . . . . . . 12
|
66 | 65 | adantl 482 |
. . . . . . . . . . 11
|
67 | 66 | fveq2d 6195 |
. . . . . . . . . 10
coe1 coe1 |
68 | 67 | fveq1d 6193 |
. . . . . . . . 9
coe1 coe1 |
69 | 68 | mpt2eq3dv 6721 |
. . . . . . . 8
coe1
coe1 |
70 | 22, 69 | csbied 3560 |
. . . . . . 7
coe1 coe1 |
71 | 70 | ad2antrr 762 |
. . . . . 6
coe1 coe1 |
72 | | pmatcollpw3.a |
. . . . . . 7
Mat |
73 | | eqid 2622 |
. . . . . . 7
|
74 | | pmatcollpw3.d |
. . . . . . 7
|
75 | | simpll1 1100 |
. . . . . . 7
|
76 | | simpll2 1101 |
. . . . . . 7
|
77 | | simp2 1062 |
. . . . . . . . 9
|
78 | | simp3 1063 |
. . . . . . . . 9
|
79 | 23 | adantr 481 |
. . . . . . . . . 10
|
80 | 79 | 3ad2ant1 1082 |
. . . . . . . . 9
|
81 | 43, 44, 45, 77, 78, 80 | matecld 20232 |
. . . . . . . 8
|
82 | | ssel 3597 |
. . . . . . . . . . 11
|
83 | 82 | ad2antrl 764 |
. . . . . . . . . 10
|
84 | 83 | imp 445 |
. . . . . . . . 9
|
85 | 84 | 3ad2ant1 1082 |
. . . . . . . 8
|
86 | | eqid 2622 |
. . . . . . . . 9
coe1 coe1 |
87 | | pmatcollpw.p |
. . . . . . . . 9
Poly1 |
88 | 86, 44, 87, 73 | coe1fvalcl 19582 |
. . . . . . . 8
coe1 |
89 | 81, 85, 88 | syl2anc 693 |
. . . . . . 7
coe1 |
90 | 72, 73, 74, 75, 76, 89 | matbas2d 20229 |
. . . . . 6
coe1 |
91 | 71, 90 | eqeltrd 2701 |
. . . . 5
coe1 |
92 | | eqid 2622 |
. . . . 5
coe1
coe1 |
93 | 91, 92 | fmptd 6385 |
. . . 4
coe1 |
94 | | fvex 6201 |
. . . . . . 7
|
95 | 74, 94 | eqeltri 2697 |
. . . . . 6
|
96 | 95 | a1i 11 |
. . . . 5
|
97 | 20 | adantr 481 |
. . . . 5
|
98 | | elmapg 7870 |
. . . . 5
coe1
coe1 |
99 | 96, 97, 98 | syl2an 494 |
. . . 4
coe1
coe1 |
100 | 93, 99 | mpbird 247 |
. . 3
coe1 |
101 | 64, 100 | eqeltrd 2701 |
. 2
curry coe1 |
102 | | fveq1 6190 |
. . . . . . . . . . 11
curry
coe1
curry coe1 |
103 | 102 | adantl 482 |
. . . . . . . . . 10
curry coe1 curry coe1 |
104 | 103 | adantr 481 |
. . . . . . . . 9
curry
coe1
curry
coe1 |
105 | | eqid 2622 |
. . . . . . . . . . . 12
coe1
coe1 |
106 | | dmexg 7097 |
. . . . . . . . . . . . . . . . 17
|
107 | | dmexg 7097 |
. . . . . . . . . . . . . . . . 17
|
108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . 16
|
109 | 108, 108 | jca 554 |
. . . . . . . . . . . . . . 15
|
110 | 109 | ad2antrl 764 |
. . . . . . . . . . . . . 14
|
111 | | mpt2exga 7246 |
. . . . . . . . . . . . . 14
coe1 |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . 13
coe1 |
113 | 112 | ralrimivva 2971 |
. . . . . . . . . . . 12
coe1 |
114 | 21 | adantr 481 |
. . . . . . . . . . . 12
|
115 | 23 | adantr 481 |
. . . . . . . . . . . 12
|
116 | | simpr 477 |
. . . . . . . . . . . 12
|
117 | 105, 113,
114, 115, 116 | fvmpt2curryd 7397 |
. . . . . . . . . . 11
curry coe1 coe1 |
118 | | df-decpmat 20568 |
. . . . . . . . . . . . . 14
decompPMat
coe1 |
119 | 118 | reseq1i 5392 |
. . . . . . . . . . . . 13
decompPMat
coe1 |
120 | | ssv 3625 |
. . . . . . . . . . . . . . . . 17
|
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
122 | | simpl 473 |
. . . . . . . . . . . . . . . 16
|
123 | 121, 122 | anim12i 590 |
. . . . . . . . . . . . . . 15
|
124 | 123 | adantr 481 |
. . . . . . . . . . . . . 14
|
125 | | resmpt2 6758 |
. . . . . . . . . . . . . 14
coe1
coe1 |
126 | 124, 125 | syl 17 |
. . . . . . . . . . . . 13
coe1
coe1 |
127 | 119, 126 | syl5req 2669 |
. . . . . . . . . . . 12
coe1 decompPMat |
128 | 127 | oveqd 6667 |
. . . . . . . . . . 11
coe1 decompPMat
|
129 | 117, 128 | eqtrd 2656 |
. . . . . . . . . 10
curry coe1 decompPMat
|
130 | 129 | adantlr 751 |
. . . . . . . . 9
curry
coe1
curry
coe1 decompPMat |
131 | 104, 130 | eqtrd 2656 |
. . . . . . . 8
curry
coe1
decompPMat |
132 | 131 | fveq2d 6195 |
. . . . . . 7
curry
coe1
decompPMat |
133 | 22 | ad2antrr 762 |
. . . . . . . . 9
curry coe1 |
134 | | ovres 6800 |
. . . . . . . . 9
decompPMat decompPMat |
135 | 133, 134 | sylan 488 |
. . . . . . . 8
curry
coe1
decompPMat decompPMat |
136 | 135 | fveq2d 6195 |
. . . . . . 7
curry
coe1
decompPMat
decompPMat |
137 | 132, 136 | eqtrd 2656 |
. . . . . 6
curry
coe1
decompPMat |
138 | 137 | oveq2d 6666 |
. . . . 5
curry
coe1
decompPMat |
139 | 138 | mpteq2dva 4744 |
. . . 4
curry coe1 decompPMat |
140 | 139 | oveq2d 6666 |
. . 3
curry coe1 g
g
decompPMat |
141 | 140 | eqeq2d 2632 |
. 2
curry coe1 g
g decompPMat |
142 | 101, 141 | rspcedv 3313 |
1
g decompPMat
g |