Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . . 7
Mat Mat |
2 | | eqid 2622 |
. . . . . . 7
Mat Mat |
3 | 1, 2 | matrcl 20218 |
. . . . . 6
Mat
|
4 | 3 | simpld 475 |
. . . . 5
Mat |
5 | 4 | ad3antlr 767 |
. . . 4
Field
Mat curry LIndF freeLMod
|
6 | | isfld 18756 |
. . . . . . 7
Field
|
7 | 6 | simplbi 476 |
. . . . . 6
Field |
8 | 7 | anim1i 592 |
. . . . 5
Field
Mat
Mat |
9 | 4 | ad2antrl 764 |
. . . . . . . . . . . 12
Mat |
10 | | simpr 477 |
. . . . . . . . . . . . . . 15
Mat
Mat |
11 | | xpfi 8231 |
. . . . . . . . . . . . . . . . . . . . 21
|
12 | 11 | anidms 677 |
. . . . . . . . . . . . . . . . . . . 20
|
13 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
freeLMod
freeLMod |
14 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
|
15 | 13, 14 | frlmfibas 20105 |
. . . . . . . . . . . . . . . . . . . 20
freeLMod |
16 | 12, 15 | sylan2 491 |
. . . . . . . . . . . . . . . . . . 19
freeLMod |
17 | 1, 13 | matbas 20219 |
. . . . . . . . . . . . . . . . . . . 20
freeLMod Mat |
18 | 17 | ancoms 469 |
. . . . . . . . . . . . . . . . . . 19
freeLMod Mat |
19 | 16, 18 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
Mat |
20 | 19 | eleq2d 2687 |
. . . . . . . . . . . . . . . . 17
Mat |
21 | 4, 20 | sylan2 491 |
. . . . . . . . . . . . . . . 16
Mat
Mat |
22 | | fvex 6201 |
. . . . . . . . . . . . . . . . . 18
|
23 | 4, 4, 11 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
Mat |
24 | | elmapg 7870 |
. . . . . . . . . . . . . . . . . 18
|
25 | 22, 23, 24 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
Mat
|
26 | 25 | adantl 482 |
. . . . . . . . . . . . . . . 16
Mat
|
27 | 21, 26 | bitr3d 270 |
. . . . . . . . . . . . . . 15
Mat
Mat |
28 | 10, 27 | mpbid 222 |
. . . . . . . . . . . . . 14
Mat
|
29 | 28 | adantrr 753 |
. . . . . . . . . . . . 13
Mat |
30 | | eldifsn 4317 |
. . . . . . . . . . . . . . . 16
|
31 | 30 | biimpri 218 |
. . . . . . . . . . . . . . 15
|
32 | 4, 31 | sylan 488 |
. . . . . . . . . . . . . 14
Mat
|
33 | 32 | adantl 482 |
. . . . . . . . . . . . 13
Mat |
34 | | curf 33387 |
. . . . . . . . . . . . . 14
curry |
35 | 22, 34 | mp3an3 1413 |
. . . . . . . . . . . . 13
curry
|
36 | 29, 33, 35 | syl2anc 693 |
. . . . . . . . . . . 12
Mat curry |
37 | 9, 36 | jca 554 |
. . . . . . . . . . 11
Mat curry |
38 | 37 | ex 450 |
. . . . . . . . . 10
Mat curry |
39 | 38 | imdistani 726 |
. . . . . . . . 9
Mat
curry |
40 | 39 | anassrs 680 |
. . . . . . . 8
Mat
curry |
41 | | anass 681 |
. . . . . . . 8
curry
curry
|
42 | 40, 41 | sylibr 224 |
. . . . . . 7
Mat
curry |
43 | | drngring 18754 |
. . . . . . . . . . . . 13
|
44 | | eqid 2622 |
. . . . . . . . . . . . . 14
unitVec unitVec |
45 | | eqid 2622 |
. . . . . . . . . . . . . 14
freeLMod freeLMod |
46 | | eqid 2622 |
. . . . . . . . . . . . . 14
freeLMod
freeLMod
|
47 | 44, 45, 46 | uvcff 20130 |
. . . . . . . . . . . . 13
unitVec freeLMod |
48 | 43, 47 | sylan 488 |
. . . . . . . . . . . 12
unitVec freeLMod |
49 | 48 | ffvelrnda 6359 |
. . . . . . . . . . 11
unitVec freeLMod
|
50 | 49 | ad4ant14 1293 |
. . . . . . . . . 10
curry curry LIndF freeLMod
unitVec freeLMod |
51 | | ffn 6045 |
. . . . . . . . . . . . . . . 16
curry curry |
52 | | fnima 6010 |
. . . . . . . . . . . . . . . 16
curry
curry curry |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . 15
curry curry curry |
54 | 53 | adantl 482 |
. . . . . . . . . . . . . 14
curry curry curry
|
55 | 54 | fveq2d 6195 |
. . . . . . . . . . . . 13
curry freeLMod curry freeLMod curry |
56 | 55 | adantr 481 |
. . . . . . . . . . . 12
curry
curry LIndF freeLMod freeLMod curry freeLMod curry |
57 | | simplll 798 |
. . . . . . . . . . . . . 14
curry
curry LIndF freeLMod
|
58 | | simpllr 799 |
. . . . . . . . . . . . . 14
curry
curry LIndF freeLMod
|
59 | 45 | frlmlmod 20093 |
. . . . . . . . . . . . . . . . 17
freeLMod |
60 | 43, 59 | sylan 488 |
. . . . . . . . . . . . . . . 16
freeLMod |
61 | 60 | adantr 481 |
. . . . . . . . . . . . . . 15
curry freeLMod
|
62 | | lindfrn 20160 |
. . . . . . . . . . . . . . 15
freeLMod
curry LIndF freeLMod curry LIndS
freeLMod |
63 | 61, 62 | sylan 488 |
. . . . . . . . . . . . . 14
curry
curry LIndF freeLMod curry LIndS
freeLMod |
64 | 45 | frlmsca 20097 |
. . . . . . . . . . . . . . . . . . . . . 22
Scalar freeLMod |
65 | | drngnzr 19262 |
. . . . . . . . . . . . . . . . . . . . . . 23
NzRing |
66 | 65 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
NzRing |
67 | 64, 66 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . . 21
Scalar freeLMod
NzRing |
68 | 60, 67 | jca 554 |
. . . . . . . . . . . . . . . . . . . 20
freeLMod
Scalar freeLMod NzRing |
69 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
Scalar
freeLMod Scalar freeLMod |
70 | 46, 69 | lindff1 20159 |
. . . . . . . . . . . . . . . . . . . . 21
freeLMod
Scalar freeLMod NzRing curry LIndF freeLMod
curry curry freeLMod |
71 | 70 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . 20
freeLMod
Scalar freeLMod
NzRing curry LIndF freeLMod curry curry
freeLMod
|
72 | 68, 71 | sylan 488 |
. . . . . . . . . . . . . . . . . . 19
curry LIndF freeLMod
curry curry freeLMod |
73 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . 19
curry curry |
74 | | f1eq2 6097 |
. . . . . . . . . . . . . . . . . . . 20
curry
curry curry freeLMod
curry freeLMod |
75 | 74 | biimpac 503 |
. . . . . . . . . . . . . . . . . . 19
curry curry freeLMod curry curry freeLMod
|
76 | 72, 73, 75 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
curry
LIndF freeLMod curry curry freeLMod |
77 | 76 | an32s 846 |
. . . . . . . . . . . . . . . . 17
curry
curry LIndF freeLMod curry freeLMod
|
78 | | f1f1orn 6148 |
. . . . . . . . . . . . . . . . 17
curry freeLMod
curry curry |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . 16
curry
curry LIndF freeLMod curry curry |
80 | | f1oeng 7974 |
. . . . . . . . . . . . . . . 16
curry curry curry |
81 | 58, 79, 80 | syl2anc 693 |
. . . . . . . . . . . . . . 15
curry
curry LIndF freeLMod
curry |
82 | 81 | ensymd 8007 |
. . . . . . . . . . . . . 14
curry
curry LIndF freeLMod curry |
83 | | lindsenlbs 33404 |
. . . . . . . . . . . . . 14
curry LIndS freeLMod
curry
curry LBasis freeLMod |
84 | 57, 58, 63, 82, 83 | syl31anc 1329 |
. . . . . . . . . . . . 13
curry
curry LIndF freeLMod curry LBasis
freeLMod |
85 | | eqid 2622 |
. . . . . . . . . . . . . 14
LBasis
freeLMod LBasis freeLMod |
86 | | eqid 2622 |
. . . . . . . . . . . . . 14
freeLMod
freeLMod
|
87 | 46, 85, 86 | lbssp 19079 |
. . . . . . . . . . . . 13
curry
LBasis freeLMod freeLMod curry freeLMod |
88 | 84, 87 | syl 17 |
. . . . . . . . . . . 12
curry
curry LIndF freeLMod freeLMod curry freeLMod |
89 | 56, 88 | eqtrd 2656 |
. . . . . . . . . . 11
curry
curry LIndF freeLMod freeLMod curry freeLMod
|
90 | 89 | adantr 481 |
. . . . . . . . . 10
curry curry LIndF freeLMod
freeLMod curry freeLMod
|
91 | 50, 90 | eleqtrrd 2704 |
. . . . . . . . 9
curry curry LIndF freeLMod
unitVec freeLMod curry |
92 | | eqid 2622 |
. . . . . . . . . . . . 13
Scalar freeLMod Scalar freeLMod
|
93 | | eqid 2622 |
. . . . . . . . . . . . 13
Scalar freeLMod Scalar freeLMod
|
94 | | eqid 2622 |
. . . . . . . . . . . . 13
freeLMod freeLMod |
95 | 45, 14 | frlmfibas 20105 |
. . . . . . . . . . . . . . 15
freeLMod |
96 | 95 | feq3d 6032 |
. . . . . . . . . . . . . 14
curry
curry freeLMod |
97 | 96 | biimpa 501 |
. . . . . . . . . . . . 13
curry curry freeLMod
|
98 | 59 | adantr 481 |
. . . . . . . . . . . . 13
curry freeLMod
|
99 | | simplr 792 |
. . . . . . . . . . . . 13
curry
|
100 | 86, 46, 92, 69, 93, 94, 97, 98, 99 | elfilspd 20142 |
. . . . . . . . . . . 12
curry unitVec freeLMod curry
Scalar freeLMod
unitVec freeLMod g freeLMod curry |
101 | 45 | frlmsca 20097 |
. . . . . . . . . . . . . . . 16
Scalar freeLMod |
102 | 101 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
Scalar freeLMod
|
103 | 102 | oveq1d 6665 |
. . . . . . . . . . . . . 14
Scalar freeLMod
|
104 | 103 | adantr 481 |
. . . . . . . . . . . . 13
curry
Scalar freeLMod |
105 | | elmapi 7879 |
. . . . . . . . . . . . . . 15
|
106 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . 20
|
107 | 106 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
curry
|
108 | 51 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
curry
curry |
109 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . 19
curry
|
110 | | inidm 3822 |
. . . . . . . . . . . . . . . . . . 19
|
111 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . 19
curry
|
112 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . 19
curry
curry curry |
113 | 107, 108,
109, 109, 110, 111, 112 | offval 6904 |
. . . . . . . . . . . . . . . . . 18
curry
freeLMod curry freeLMod curry |
114 | | simp-4r 807 |
. . . . . . . . . . . . . . . . . . . . 21
curry
|
115 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . . 22
|
116 | 115 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . 21
curry
|
117 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . . . 23
curry curry
|
118 | 117 | ad4ant24 1298 |
. . . . . . . . . . . . . . . . . . . . . 22
curry
curry |
119 | 95 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
curry
freeLMod |
120 | 118, 119 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . 21
curry
curry freeLMod
|
121 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
|
122 | 45, 46, 14, 114, 116, 120, 94, 121 | frlmvscafval 20109 |
. . . . . . . . . . . . . . . . . . . 20
curry
freeLMod curry curry |
123 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . 22
|
124 | | fnconstg 6093 |
. . . . . . . . . . . . . . . . . . . . . 22
|
125 | 123, 124 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . 21
curry
|
126 | | elmapfn 7880 |
. . . . . . . . . . . . . . . . . . . . . . 23
curry
curry |
127 | 117, 126 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
curry curry |
128 | 127 | ad4ant24 1298 |
. . . . . . . . . . . . . . . . . . . . 21
curry
curry |
129 | 123 | fvconst2 6469 |
. . . . . . . . . . . . . . . . . . . . . 22
|
130 | 129 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
curry
|
131 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . 21
curry
curry curry |
132 | 125, 128,
114, 114, 110, 130, 131 | offval 6904 |
. . . . . . . . . . . . . . . . . . . 20
curry
curry curry |
133 | 122, 132 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
curry
freeLMod curry curry |
134 | 133 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . . 18
curry
freeLMod curry curry |
135 | 113, 134 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
curry
freeLMod curry curry |
136 | 135 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
curry
freeLMod
g freeLMod curry freeLMod
g curry |
137 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
freeLMod freeLMod |
138 | | simplll 798 |
. . . . . . . . . . . . . . . . 17
curry
|
139 | | simp-5l 808 |
. . . . . . . . . . . . . . . . . . . 20
curry
|
140 | 115 | ad4ant23 1297 |
. . . . . . . . . . . . . . . . . . . 20
curry
|
141 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . 21
curry
curry |
142 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . . . . 23
curry
curry |
143 | 117, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
curry curry |
144 | 143 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . 21
curry
curry |
145 | 141, 144 | sylanl1 682 |
. . . . . . . . . . . . . . . . . . . 20
curry
curry |
146 | 14, 121 | ringcl 18561 |
. . . . . . . . . . . . . . . . . . . 20
curry
curry |
147 | 139, 140,
145, 146 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
curry
curry |
148 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
curry curry |
149 | 147, 148 | fmptd 6385 |
. . . . . . . . . . . . . . . . . 18
curry
curry |
150 | | elmapg 7870 |
. . . . . . . . . . . . . . . . . . . . . 22
curry
curry |
151 | 22, 150 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . 21
curry
curry |
152 | 151 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
curry
curry |
153 | 95 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . 20
curry
curry freeLMod |
154 | 152, 153 | bitr3d 270 |
. . . . . . . . . . . . . . . . . . 19
curry curry freeLMod |
155 | 154 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
curry
curry curry freeLMod |
156 | 149, 155 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
curry
curry freeLMod |
157 | | mptexg 6484 |
. . . . . . . . . . . . . . . . . . . . 21
curry |
158 | 157 | ralrimivw 2967 |
. . . . . . . . . . . . . . . . . . . 20
curry |
159 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
curry curry |
160 | 159 | fnmpt 6020 |
. . . . . . . . . . . . . . . . . . . 20
curry curry |
161 | 158, 160 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
curry |
162 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
|
163 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . 19
freeLMod |
164 | 161, 162,
163 | fndmfifsupp 8288 |
. . . . . . . . . . . . . . . . . 18
curry finSupp
freeLMod |
165 | 164 | ad3antlr 767 |
. . . . . . . . . . . . . . . . 17
curry
curry finSupp
freeLMod |
166 | 45, 46, 137, 109, 109, 138, 156, 165 | frlmgsum 20111 |
. . . . . . . . . . . . . . . 16
curry
freeLMod
g curry g curry |
167 | 136, 166 | eqtr2d 2657 |
. . . . . . . . . . . . . . 15
curry
g curry freeLMod g freeLMod curry |
168 | 105, 167 | sylan2 491 |
. . . . . . . . . . . . . 14
curry
g curry freeLMod g freeLMod curry |
169 | 168 | eqeq2d 2632 |
. . . . . . . . . . . . 13
curry
unitVec
g curry unitVec freeLMod g freeLMod curry |
170 | 104, 169 | rexeqbidva 3155 |
. . . . . . . . . . . 12
curry
unitVec g curry Scalar freeLMod
unitVec freeLMod g freeLMod curry |
171 | 100, 170 | bitr4d 271 |
. . . . . . . . . . 11
curry unitVec freeLMod curry
unitVec g curry |
172 | 43, 171 | sylanl1 682 |
. . . . . . . . . 10
curry unitVec freeLMod curry
unitVec g curry |
173 | 172 | ad2antrr 762 |
. . . . . . . . 9
curry curry LIndF freeLMod
unitVec freeLMod curry
unitVec g curry |
174 | 91, 173 | mpbid 222 |
. . . . . . . 8
curry curry LIndF freeLMod
unitVec g curry |
175 | 174 | ralrimiva 2966 |
. . . . . . 7
curry
curry LIndF freeLMod
unitVec g curry |
176 | 42, 175 | sylan 488 |
. . . . . 6
Mat curry LIndF freeLMod
unitVec g curry |
177 | 10, 21 | mpbird 247 |
. . . . . . . . 9
Mat
|
178 | | elmapfn 7880 |
. . . . . . . . 9
|
179 | 177, 178 | syl 17 |
. . . . . . . 8
Mat
|
180 | 4 | adantl 482 |
. . . . . . . 8
Mat
|
181 | | an32 839 |
. . . . . . . . . . . . . . . . . . 19
|
182 | | df-3an 1039 |
. . . . . . . . . . . . . . . . . . 19
|
183 | 181, 182 | bitr4i 267 |
. . . . . . . . . . . . . . . . . 18
|
184 | | curfv 33389 |
. . . . . . . . . . . . . . . . . 18
curry |
185 | 183, 184 | sylanb 489 |
. . . . . . . . . . . . . . . . 17
curry |
186 | 185 | an32s 846 |
. . . . . . . . . . . . . . . 16
curry |
187 | 186 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
curry |
188 | 187 | mpteq2dva 4744 |
. . . . . . . . . . . . . 14
curry |
189 | 188 | an32s 846 |
. . . . . . . . . . . . 13
curry |
190 | 189 | oveq2d 6666 |
. . . . . . . . . . . 12
g curry g |
191 | 190 | mpteq2dva 4744 |
. . . . . . . . . . 11
g curry g |
192 | 191 | eqeq2d 2632 |
. . . . . . . . . 10
unitVec g curry unitVec g |
193 | 192 | rexbidv 3052 |
. . . . . . . . 9
unitVec g curry
unitVec g |
194 | 193 | ralbidv 2986 |
. . . . . . . 8
unitVec g curry
unitVec g |
195 | 179, 180,
194 | syl2anc 693 |
. . . . . . 7
Mat
unitVec g curry
unitVec g |
196 | 195 | ad2antrr 762 |
. . . . . 6
Mat curry LIndF freeLMod
unitVec g curry
unitVec g |
197 | 176, 196 | mpbid 222 |
. . . . 5
Mat curry LIndF freeLMod
unitVec g |
198 | 8, 197 | sylanl1 682 |
. . . 4
Field
Mat curry LIndF freeLMod
unitVec g |
199 | | fveq1 6190 |
. . . . . . . . . . 11
|
200 | | vex 3203 |
. . . . . . . . . . . 12
|
201 | | vex 3203 |
. . . . . . . . . . . 12
|
202 | | uncov 33390 |
. . . . . . . . . . . 12
uncurry |
203 | 200, 201,
202 | mp2an 708 |
. . . . . . . . . . 11
uncurry |
204 | 199, 203 | syl6eqr 2674 |
. . . . . . . . . 10
uncurry |
205 | 204 | oveq1d 6665 |
. . . . . . . . 9
uncurry |
206 | 205 | mpteq2dv 4745 |
. . . . . . . 8
uncurry |
207 | 206 | oveq2d 6666 |
. . . . . . 7
g g uncurry |
208 | 207 | mpteq2dv 4745 |
. . . . . 6
g g uncurry |
209 | 208 | eqeq2d 2632 |
. . . . 5
unitVec g
unitVec g uncurry |
210 | 209 | ac6sfi 8204 |
. . . 4
unitVec g
unitVec g uncurry |
211 | 5, 198, 210 | syl2anc 693 |
. . 3
Field
Mat curry LIndF freeLMod
unitVec g uncurry |
212 | | uncf 33388 |
. . . . . . 7
uncurry |
213 | 13, 14 | frlmfibas 20105 |
. . . . . . . . . . . . . . . 16
Field
freeLMod |
214 | 12, 213 | sylan2 491 |
. . . . . . . . . . . . . . 15
Field
freeLMod |
215 | 1, 13 | matbas 20219 |
. . . . . . . . . . . . . . . 16
Field freeLMod Mat |
216 | 215 | ancoms 469 |
. . . . . . . . . . . . . . 15
Field
freeLMod Mat |
217 | 214, 216 | eqtrd 2656 |
. . . . . . . . . . . . . 14
Field
Mat |
218 | 4, 217 | sylan2 491 |
. . . . . . . . . . . . 13
Field
Mat
Mat |
219 | 218 | eleq2d 2687 |
. . . . . . . . . . . 12
Field
Mat
uncurry
uncurry Mat |
220 | | elmapg 7870 |
. . . . . . . . . . . . . 14
uncurry
uncurry |
221 | 22, 23, 220 | sylancr 695 |
. . . . . . . . . . . . 13
Mat uncurry
uncurry |
222 | 221 | adantl 482 |
. . . . . . . . . . . 12
Field
Mat
uncurry
uncurry |
223 | 219, 222 | bitr3d 270 |
. . . . . . . . . . 11
Field
Mat
uncurry Mat uncurry |
224 | 223 | biimpar 502 |
. . . . . . . . . 10
Field Mat
uncurry uncurry Mat |
225 | 224 | adantr 481 |
. . . . . . . . 9
Field
Mat uncurry unitVec
g uncurry
uncurry Mat |
226 | | nfv 1843 |
. . . . . . . . . . . . . 14
Field
Mat uncurry |
227 | | nfmpt1 4747 |
. . . . . . . . . . . . . . 15
g uncurry |
228 | 227 | nfeq2 2780 |
. . . . . . . . . . . . . 14
unitVec g uncurry |
229 | | fveq1 6190 |
. . . . . . . . . . . . . . . . 17
unitVec
g uncurry unitVec g uncurry |
230 | 7, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
Field |
231 | 230, 4 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . 20
Field
Mat
|
232 | 231 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
Field Mat
uncurry
|
233 | | equcom 1945 |
. . . . . . . . . . . . . . . . . . . . 21
|
234 | | ifbi 4107 |
. . . . . . . . . . . . . . . . . . . . 21
|
235 | 233, 234 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
|
236 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
|
237 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
|
238 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . . 21
|
239 | | simplll 798 |
. . . . . . . . . . . . . . . . . . . . 21
|
240 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . 21
|
241 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
|
242 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
Mat Mat |
243 | 1, 236, 237, 238, 239, 240, 241, 242 | mat1ov 20254 |
. . . . . . . . . . . . . . . . . . . 20
Mat
|
244 | | df-3an 1039 |
. . . . . . . . . . . . . . . . . . . . 21
|
245 | 44, 236, 237 | uvcvval 20125 |
. . . . . . . . . . . . . . . . . . . . 21
unitVec
|
246 | 244, 245 | sylanbr 490 |
. . . . . . . . . . . . . . . . . . . 20
unitVec |
247 | 235, 243,
246 | 3eqtr4a 2682 |
. . . . . . . . . . . . . . . . . . 19
Mat
unitVec |
248 | 232, 247 | sylanl1 682 |
. . . . . . . . . . . . . . . . . 18
Field
Mat uncurry Mat
unitVec |
249 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . 21
g uncurry |
250 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
g uncurry g uncurry |
251 | 250 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . . . . 21
g uncurry g uncurry g uncurry |
252 | 249, 251 | mpan2 707 |
. . . . . . . . . . . . . . . . . . . 20
g uncurry g uncurry |
253 | 252 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
Field
Mat uncurry g uncurry g uncurry |
254 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
maMul maMul |
255 | | simp-4l 806 |
. . . . . . . . . . . . . . . . . . . 20
Field
Mat uncurry Field |
256 | 4 | ad4antlr 769 |
. . . . . . . . . . . . . . . . . . . 20
Field
Mat uncurry |
257 | 221 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . 21
Mat
uncurry uncurry
|
258 | 257 | ad5ant23 1304 |
. . . . . . . . . . . . . . . . . . . 20
Field
Mat uncurry uncurry
|
259 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
Field
Mat
Mat |
260 | 259, 218 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . . . . . 21
Field
Mat
|
261 | 260 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . 20
Field
Mat uncurry
|
262 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . 20
Field
Mat uncurry |
263 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
Field
Mat uncurry |
264 | 254, 14, 121, 255, 256, 256, 256, 258, 261, 262, 263 | mamufv 20193 |
. . . . . . . . . . . . . . . . . . 19
Field
Mat uncurry uncurry
maMul g uncurry |
265 | 1, 254 | matmulr 20244 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Field maMul Mat |
266 | 265 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . 23
Field
maMul Mat |
267 | 266 | oveqd 6667 |
. . . . . . . . . . . . . . . . . . . . . 22
Field
uncurry maMul uncurry Mat
|
268 | 267 | oveqd 6667 |
. . . . . . . . . . . . . . . . . . . . 21
Field
uncurry
maMul uncurry Mat |
269 | 4, 268 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . 20
Field
Mat
uncurry maMul uncurry Mat
|
270 | 269 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . 19
Field
Mat uncurry uncurry
maMul uncurry Mat |
271 | 253, 264,
270 | 3eqtr2rd 2663 |
. . . . . . . . . . . . . . . . . 18
Field
Mat uncurry uncurry
Mat g uncurry |
272 | 248, 271 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . 17
Field
Mat uncurry Mat uncurry Mat
unitVec g uncurry |
273 | 229, 272 | syl5ibr 236 |
. . . . . . . . . . . . . . . 16
Field
Mat uncurry unitVec g uncurry Mat
uncurry Mat |
274 | 273 | ex 450 |
. . . . . . . . . . . . . . 15
Field
Mat uncurry
unitVec g uncurry Mat uncurry Mat |
275 | 274 | com23 86 |
. . . . . . . . . . . . . 14
Field
Mat uncurry
unitVec g uncurry
Mat uncurry Mat |
276 | 226, 228,
275 | ralrimd 2959 |
. . . . . . . . . . . . 13
Field
Mat uncurry
unitVec g uncurry Mat uncurry Mat
|
277 | 276 | ralimdva 2962 |
. . . . . . . . . . . 12
Field Mat
uncurry
unitVec g uncurry
Mat uncurry Mat |
278 | 1, 2, 242 | mat1bas 20255 |
. . . . . . . . . . . . . . . . 17
Mat Mat |
279 | 13, 14 | frlmfibas 20105 |
. . . . . . . . . . . . . . . . . . 19
freeLMod |
280 | 12, 279 | sylan2 491 |
. . . . . . . . . . . . . . . . . 18
freeLMod |
281 | 1, 13 | matbas 20219 |
. . . . . . . . . . . . . . . . . . 19
freeLMod Mat |
282 | 281 | ancoms 469 |
. . . . . . . . . . . . . . . . . 18
freeLMod Mat |
283 | 280, 282 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
Mat |
284 | 278, 283 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . 16
Mat
|
285 | | elmapfn 7880 |
. . . . . . . . . . . . . . . 16
Mat
Mat |
286 | 284, 285 | syl 17 |
. . . . . . . . . . . . . . 15
Mat |
287 | 230, 4, 286 | syl2an 494 |
. . . . . . . . . . . . . 14
Field
Mat
Mat |
288 | 287 | adantr 481 |
. . . . . . . . . . . . 13
Field Mat
uncurry Mat |
289 | 1 | matring 20249 |
. . . . . . . . . . . . . . . . . 18
Mat |
290 | 4, 230, 289 | syl2anr 495 |
. . . . . . . . . . . . . . . . 17
Field
Mat
Mat |
291 | 290 | adantr 481 |
. . . . . . . . . . . . . . . 16
Field Mat
uncurry Mat |
292 | | simplr 792 |
. . . . . . . . . . . . . . . 16
Field Mat
uncurry Mat |
293 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
Mat Mat |
294 | 2, 293 | ringcl 18561 |
. . . . . . . . . . . . . . . 16
Mat
uncurry Mat Mat uncurry
Mat Mat |
295 | 291, 224,
292, 294 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
Field Mat
uncurry uncurry Mat Mat |
296 | 218 | adantr 481 |
. . . . . . . . . . . . . . 15
Field Mat
uncurry Mat |
297 | 295, 296 | eleqtrrd 2704 |
. . . . . . . . . . . . . 14
Field Mat
uncurry uncurry Mat
|
298 | | elmapfn 7880 |
. . . . . . . . . . . . . 14
uncurry Mat
uncurry Mat
|
299 | 297, 298 | syl 17 |
. . . . . . . . . . . . 13
Field Mat
uncurry uncurry Mat |
300 | | eqfnov2 6767 |
. . . . . . . . . . . . 13
Mat uncurry Mat
Mat uncurry Mat
Mat uncurry Mat |
301 | 288, 299,
300 | syl2anc 693 |
. . . . . . . . . . . 12
Field Mat
uncurry Mat uncurry Mat
Mat uncurry Mat
|
302 | 277, 301 | sylibrd 249 |
. . . . . . . . . . 11
Field Mat
uncurry
unitVec g uncurry Mat uncurry Mat
|
303 | 302 | imp 445 |
. . . . . . . . . 10
Field
Mat uncurry unitVec
g uncurry
Mat uncurry Mat |
304 | 303 | eqcomd 2628 |
. . . . . . . . 9
Field
Mat uncurry unitVec
g uncurry
uncurry Mat Mat |
305 | | oveq1 6657 |
. . . . . . . . . . 11
uncurry Mat
uncurry Mat |
306 | 305 | eqeq1d 2624 |
. . . . . . . . . 10
uncurry Mat Mat
uncurry Mat Mat
|
307 | 306 | rspcev 3309 |
. . . . . . . . 9
uncurry Mat uncurry Mat Mat Mat Mat
Mat |
308 | 225, 304,
307 | syl2anc 693 |
. . . . . . . 8
Field
Mat uncurry unitVec
g uncurry
Mat Mat Mat
|
309 | 308 | expl 648 |
. . . . . . 7
Field
Mat
uncurry
unitVec
g uncurry
Mat Mat Mat
|
310 | 212, 309 | sylani 686 |
. . . . . 6
Field
Mat
unitVec
g uncurry
Mat Mat Mat
|
311 | 310 | exlimdv 1861 |
. . . . 5
Field
Mat
unitVec g uncurry
Mat Mat Mat
|
312 | 311 | imp 445 |
. . . 4
Field Mat
unitVec g uncurry Mat Mat
Mat |
313 | 312 | adantlr 751 |
. . 3
Field
Mat
unitVec g uncurry Mat Mat Mat
|
314 | 211, 313 | syldan 487 |
. 2
Field
Mat curry LIndF freeLMod
Mat Mat Mat |
315 | 6 | simprbi 480 |
. . . 4
Field |
316 | | eqid 2622 |
. . . . . . . . . 10
maDet maDet |
317 | 316, 1, 2, 14 | mdetcl 20402 |
. . . . . . . . 9
Mat
maDet |
318 | 316, 1, 2, 14 | mdetcl 20402 |
. . . . . . . . 9
Mat
maDet |
319 | | eqid 2622 |
. . . . . . . . . 10
r r |
320 | 14, 319, 121 | dvdsrmul 18648 |
. . . . . . . . 9
maDet
maDet maDet r maDet maDet |
321 | 317, 318,
320 | syl2an 494 |
. . . . . . . 8
Mat
Mat maDet
r maDet maDet |
322 | 321 | anandis 873 |
. . . . . . 7
Mat Mat maDet
r maDet maDet |
323 | 322 | anassrs 680 |
. . . . . 6
Mat Mat
maDet r maDet maDet |
324 | 323 | adantrr 753 |
. . . . 5
Mat Mat Mat Mat
maDet r maDet maDet |
325 | | fveq2 6191 |
. . . . . . . . 9
Mat
Mat maDet Mat
maDet Mat |
326 | 1, 2, 316, 121, 293 | mdetmul 20429 |
. . . . . . . . . . . 12
Mat Mat maDet Mat
maDet maDet |
327 | 326 | 3expa 1265 |
. . . . . . . . . . 11
Mat Mat
maDet Mat
maDet maDet |
328 | 327 | an32s 846 |
. . . . . . . . . 10
Mat Mat
maDet Mat
maDet maDet |
329 | 316, 1, 242, 236 | mdet1 20407 |
. . . . . . . . . . . 12
maDet
Mat |
330 | 4, 329 | sylan2 491 |
. . . . . . . . . . 11
Mat
maDet Mat |
331 | 330 | adantr 481 |
. . . . . . . . . 10
Mat Mat
maDet Mat |
332 | 328, 331 | eqeq12d 2637 |
. . . . . . . . 9
Mat Mat
maDet
Mat maDet Mat maDet maDet |
333 | 325, 332 | syl5ib 234 |
. . . . . . . 8
Mat Mat
Mat
Mat maDet maDet |
334 | 333 | impr 649 |
. . . . . . 7
Mat Mat Mat Mat
maDet
maDet |
335 | 334 | breq2d 4665 |
. . . . . 6
Mat Mat Mat Mat
maDet
r maDet maDet maDet r |
336 | | eqid 2622 |
. . . . . . . 8
Unit Unit |
337 | 336, 236,
319 | crngunit 18662 |
. . . . . . 7
maDet
Unit
maDet r |
338 | 337 | ad2antrr 762 |
. . . . . 6
Mat Mat Mat Mat
maDet
Unit
maDet r |
339 | 335, 338 | bitr4d 271 |
. . . . 5
Mat Mat Mat Mat
maDet
r maDet maDet maDet Unit |
340 | 324, 339 | mpbid 222 |
. . . 4
Mat Mat Mat Mat
maDet Unit |
341 | 315, 340 | sylanl1 682 |
. . 3
Field Mat Mat Mat Mat maDet Unit |
342 | 341 | ad4ant14 1293 |
. 2
Field
Mat curry LIndF freeLMod
Mat Mat Mat maDet Unit |
343 | 314, 342 | rexlimddv 3035 |
1
Field
Mat curry LIndF freeLMod maDet Unit |