Metamath Proof Explorer


Theorem matunitlindflem1

Description: One direction of matunitlindf . (Contributed by Brendan Leahy, 2-Jun-2021)

Ref Expression
Assertion matunitlindflem1 R Field M : I × I Base R I Fin ¬ curry M LIndF R freeLMod I I maDet R M = 0 R

Proof

Step Hyp Ref Expression
1 isfld R Field R DivRing R CRing
2 1 simplbi R Field R DivRing
3 drngring R DivRing R Ring
4 2 3 syl R Field R Ring
5 eqid R freeLMod I = R freeLMod I
6 5 frlmlmod R Ring I Fin R freeLMod I LMod
7 6 adantlr R Ring M : I × I Base R I Fin R freeLMod I LMod
8 simpr R Ring M : I × I Base R I Fin I Fin
9 eldifi I Fin I Fin
10 eqid Base R = Base R
11 5 10 frlmfibas R Ring I Fin Base R I = Base R freeLMod I
12 9 11 sylan2 R Ring I Fin Base R I = Base R freeLMod I
13 fvex Base R V
14 curf M : I × I Base R I Fin Base R V curry M : I Base R I
15 13 14 mp3an3 M : I × I Base R I Fin curry M : I Base R I
16 feq3 Base R I = Base R freeLMod I curry M : I Base R I curry M : I Base R freeLMod I
17 16 biimpa Base R I = Base R freeLMod I curry M : I Base R I curry M : I Base R freeLMod I
18 12 15 17 syl2an R Ring I Fin M : I × I Base R I Fin curry M : I Base R freeLMod I
19 18 anandirs R Ring M : I × I Base R I Fin curry M : I Base R freeLMod I
20 eqid Base R freeLMod I = Base R freeLMod I
21 eqid Scalar R freeLMod I = Scalar R freeLMod I
22 eqid R freeLMod I = R freeLMod I
23 eqid 0 R freeLMod I = 0 R freeLMod I
24 eqid 0 Scalar R freeLMod I = 0 Scalar R freeLMod I
25 eqid Base Scalar R freeLMod I freeLMod I = Base Scalar R freeLMod I freeLMod I
26 20 21 22 23 24 25 islindf4 R freeLMod I LMod I Fin curry M : I Base R freeLMod I curry M LIndF R freeLMod I f Base Scalar R freeLMod I freeLMod I R freeLMod I f R freeLMod I f curry M = 0 R freeLMod I f = I × 0 Scalar R freeLMod I
27 7 8 19 26 syl3anc R Ring M : I × I Base R I Fin curry M LIndF R freeLMod I f Base Scalar R freeLMod I freeLMod I R freeLMod I f R freeLMod I f curry M = 0 R freeLMod I f = I × 0 Scalar R freeLMod I
28 5 frlmsca R Ring I Fin R = Scalar R freeLMod I
29 28 fvoveq1d R Ring I Fin Base R freeLMod I = Base Scalar R freeLMod I freeLMod I
30 12 29 eqtrd R Ring I Fin Base R I = Base Scalar R freeLMod I freeLMod I
31 30 adantlr R Ring M : I × I Base R I Fin Base R I = Base Scalar R freeLMod I freeLMod I
32 elmapi f Base R I f : I Base R
33 ffn f : I Base R f Fn I
34 33 adantl R Ring M : I × I Base R I Fin f : I Base R f Fn I
35 19 ffnd R Ring M : I × I Base R I Fin curry M Fn I
36 35 adantr R Ring M : I × I Base R I Fin f : I Base R curry M Fn I
37 simplr R Ring M : I × I Base R I Fin f : I Base R I Fin
38 inidm I I = I
39 eqidd R Ring M : I × I Base R I Fin f : I Base R n I f n = f n
40 eqidd R Ring M : I × I Base R I Fin f : I Base R n I curry M n = curry M n
41 34 36 37 37 38 39 40 offval R Ring M : I × I Base R I Fin f : I Base R f R freeLMod I f curry M = n I f n R freeLMod I curry M n
42 simpllr R Ring M : I × I Base R I Fin f : I Base R n I I Fin
43 ffvelrn f : I Base R n I f n Base R
44 43 adantll R Ring M : I × I Base R I Fin f : I Base R n I f n Base R
45 19 ffvelrnda R Ring M : I × I Base R I Fin n I curry M n Base R freeLMod I
46 45 adantlr R Ring M : I × I Base R I Fin f : I Base R n I curry M n Base R freeLMod I
47 eqid R = R
48 5 20 10 42 44 46 22 47 frlmvscafval R Ring M : I × I Base R I Fin f : I Base R n I f n R freeLMod I curry M n = I × f n R f curry M n
49 fvex f n V
50 fnconstg f n V I × f n Fn I
51 49 50 mp1i R Ring M : I × I Base R I Fin f : I Base R n I I × f n Fn I
52 15 ffvelrnda M : I × I Base R I Fin n I curry M n Base R I
53 elmapfn curry M n Base R I curry M n Fn I
54 52 53 syl M : I × I Base R I Fin n I curry M n Fn I
55 54 adantlll R Ring M : I × I Base R I Fin n I curry M n Fn I
56 55 adantlr R Ring M : I × I Base R I Fin f : I Base R n I curry M n Fn I
57 49 fvconst2 k I I × f n k = f n
58 57 adantl R Ring M : I × I Base R I Fin f : I Base R n I k I I × f n k = f n
59 ffn M : I × I Base R M Fn I × I
60 59 anim2i I Fin M : I × I Base R I Fin M Fn I × I
61 60 ancoms M : I × I Base R I Fin I Fin M Fn I × I
62 61 ad4ant23 R Ring M : I × I Base R I Fin f : I Base R I Fin M Fn I × I
63 curfv M Fn I × I n I k I I Fin curry M n k = n M k
64 63 3exp1 M Fn I × I n I k I I Fin curry M n k = n M k
65 64 com4r I Fin M Fn I × I n I k I curry M n k = n M k
66 65 imp41 I Fin M Fn I × I n I k I curry M n k = n M k
67 62 66 sylanl1 R Ring M : I × I Base R I Fin f : I Base R n I k I curry M n k = n M k
68 51 56 42 42 38 58 67 offval R Ring M : I × I Base R I Fin f : I Base R n I I × f n R f curry M n = k I f n R n M k
69 48 68 eqtrd R Ring M : I × I Base R I Fin f : I Base R n I f n R freeLMod I curry M n = k I f n R n M k
70 69 mpteq2dva R Ring M : I × I Base R I Fin f : I Base R n I f n R freeLMod I curry M n = n I k I f n R n M k
71 41 70 eqtrd R Ring M : I × I Base R I Fin f : I Base R f R freeLMod I f curry M = n I k I f n R n M k
72 71 oveq2d R Ring M : I × I Base R I Fin f : I Base R R freeLMod I f R freeLMod I f curry M = R freeLMod I n I k I f n R n M k
73 simplll R Ring M : I × I Base R I Fin f : I Base R R Ring
74 simp-4l R Ring M : I × I Base R f : I Base R n I k I R Ring
75 43 ad4ant23 R Ring M : I × I Base R f : I Base R n I k I f n Base R
76 fovrn M : I × I Base R n I k I n M k Base R
77 76 ad5ant245 R Ring M : I × I Base R f : I Base R n I k I n M k Base R
78 10 47 ringcl R Ring f n Base R n M k Base R f n R n M k Base R
79 74 75 77 78 syl3anc R Ring M : I × I Base R f : I Base R n I k I f n R n M k Base R
80 79 fmpttd R Ring M : I × I Base R f : I Base R n I k I f n R n M k : I Base R
81 80 adantllr R Ring M : I × I Base R I Fin f : I Base R n I k I f n R n M k : I Base R
82 elmapg Base R V I Fin k I f n R n M k Base R I k I f n R n M k : I Base R
83 13 82 mpan I Fin k I f n R n M k Base R I k I f n R n M k : I Base R
84 83 adantl R Ring I Fin k I f n R n M k Base R I k I f n R n M k : I Base R
85 12 eleq2d R Ring I Fin k I f n R n M k Base R I k I f n R n M k Base R freeLMod I
86 84 85 bitr3d R Ring I Fin k I f n R n M k : I Base R k I f n R n M k Base R freeLMod I
87 86 ad5ant13 R Ring M : I × I Base R I Fin f : I Base R n I k I f n R n M k : I Base R k I f n R n M k Base R freeLMod I
88 81 87 mpbid R Ring M : I × I Base R I Fin f : I Base R n I k I f n R n M k Base R freeLMod I
89 mptexg I Fin k I f n R n M k V
90 89 ralrimivw I Fin n I k I f n R n M k V
91 eqid n I k I f n R n M k = n I k I f n R n M k
92 91 fnmpt n I k I f n R n M k V n I k I f n R n M k Fn I
93 90 92 syl I Fin n I k I f n R n M k Fn I
94 fvexd I Fin 0 R freeLMod I V
95 93 9 94 fndmfifsupp I Fin finSupp 0 R freeLMod I n I k I f n R n M k
96 95 ad2antlr R Ring M : I × I Base R I Fin f : I Base R finSupp 0 R freeLMod I n I k I f n R n M k
97 5 20 23 37 37 73 88 96 frlmgsum R Ring M : I × I Base R I Fin f : I Base R R freeLMod I n I k I f n R n M k = k I R n I f n R n M k
98 72 97 eqtr2d R Ring M : I × I Base R I Fin f : I Base R k I R n I f n R n M k = R freeLMod I f R freeLMod I f curry M
99 32 98 sylan2 R Ring M : I × I Base R I Fin f Base R I k I R n I f n R n M k = R freeLMod I f R freeLMod I f curry M
100 eqid 0 R = 0 R
101 5 100 frlm0 R Ring I Fin I × 0 R = 0 R freeLMod I
102 101 ad4ant13 R Ring M : I × I Base R I Fin f Base R I I × 0 R = 0 R freeLMod I
103 99 102 eqeq12d R Ring M : I × I Base R I Fin f Base R I k I R n I f n R n M k = I × 0 R R freeLMod I f R freeLMod I f curry M = 0 R freeLMod I
104 28 fveq2d R Ring I Fin 0 R = 0 Scalar R freeLMod I
105 104 sneqd R Ring I Fin 0 R = 0 Scalar R freeLMod I
106 105 xpeq2d R Ring I Fin I × 0 R = I × 0 Scalar R freeLMod I
107 106 eqeq2d R Ring I Fin f = I × 0 R f = I × 0 Scalar R freeLMod I
108 107 ad4ant13 R Ring M : I × I Base R I Fin f Base R I f = I × 0 R f = I × 0 Scalar R freeLMod I
109 103 108 imbi12d R Ring M : I × I Base R I Fin f Base R I k I R n I f n R n M k = I × 0 R f = I × 0 R R freeLMod I f R freeLMod I f curry M = 0 R freeLMod I f = I × 0 Scalar R freeLMod I
110 31 109 raleqbidva R Ring M : I × I Base R I Fin f Base R I k I R n I f n R n M k = I × 0 R f = I × 0 R f Base Scalar R freeLMod I freeLMod I R freeLMod I f R freeLMod I f curry M = 0 R freeLMod I f = I × 0 Scalar R freeLMod I
111 27 110 bitr4d R Ring M : I × I Base R I Fin curry M LIndF R freeLMod I f Base R I k I R n I f n R n M k = I × 0 R f = I × 0 R
112 111 notbid R Ring M : I × I Base R I Fin ¬ curry M LIndF R freeLMod I ¬ f Base R I k I R n I f n R n M k = I × 0 R f = I × 0 R
113 rexanali f Base R I k I R n I f n R n M k = I × 0 R ¬ f = I × 0 R ¬ f Base R I k I R n I f n R n M k = I × 0 R f = I × 0 R
114 112 113 bitr4di R Ring M : I × I Base R I Fin ¬ curry M LIndF R freeLMod I f Base R I k I R n I f n R n M k = I × 0 R ¬ f = I × 0 R
115 4 114 sylanl1 R Field M : I × I Base R I Fin ¬ curry M LIndF R freeLMod I f Base R I k I R n I f n R n M k = I × 0 R ¬ f = I × 0 R
116 fconstfv f : I 0 R f Fn I i I f i = 0 R
117 fvex 0 R V
118 117 fconst2 f : I 0 R f = I × 0 R
119 116 118 sylbb1 f Fn I i I f i = 0 R f = I × 0 R
120 119 ex f Fn I i I f i = 0 R f = I × 0 R
121 120 con3d f Fn I ¬ f = I × 0 R ¬ i I f i = 0 R
122 df-ne f i 0 R ¬ f i = 0 R
123 122 rexbii i I f i 0 R i I ¬ f i = 0 R
124 rexnal i I ¬ f i = 0 R ¬ i I f i = 0 R
125 123 124 bitri i I f i 0 R ¬ i I f i = 0 R
126 121 125 syl6ibr f Fn I ¬ f = I × 0 R i I f i 0 R
127 33 126 syl f : I Base R ¬ f = I × 0 R i I f i 0 R
128 127 adantl R Field M : I × I Base R I Fin f : I Base R ¬ f = I × 0 R i I f i 0 R
129 neldifsn ¬ i I i
130 difss I i I
131 diffi I Fin I i Fin
132 131 ad4antlr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i I i I i I I i Fin
133 eleq2 y = i y i
134 133 notbid y = ¬ i y ¬ i
135 sseq1 y = y I I
136 134 135 anbi12d y = ¬ i y y I ¬ i I
137 136 anbi2d y = R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i y y I R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i I
138 mpteq1 y = n y inv r R f i R f n R n M k = n inv r R f i R f n R n M k
139 mpt0 n inv r R f i R f n R n M k =
140 138 139 eqtrdi y = n y inv r R f i R f n R n M k =
141 140 oveq2d y = R n y inv r R f i R f n R n M k = R
142 100 gsum0 R = 0 R
143 141 142 eqtrdi y = R n y inv r R f i R f n R n M k = 0 R
144 143 oveq1d y = R n y inv r R f i R f n R n M k + R i M k = 0 R + R i M k
145 144 ifeq1d y = if j = i R n y inv r R f i R f n R n M k + R i M k j M k = if j = i 0 R + R i M k j M k
146 145 mpoeq3dv y = j I , k I if j = i R n y inv r R f i R f n R n M k + R i M k j M k = j I , k I if j = i 0 R + R i M k j M k
147 146 fveq2d y = I maDet R j I , k I if j = i R n y inv r R f i R f n R n M k + R i M k j M k = I maDet R j I , k I if j = i 0 R + R i M k j M k
148 147 eqeq2d y = I maDet R M = I maDet R j I , k I if j = i R n y inv r R f i R f n R n M k + R i M k j M k I maDet R M = I maDet R j I , k I if j = i 0 R + R i M k j M k
149 137 148 imbi12d y = R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i y y I I maDet R M = I maDet R j I , k I if j = i R n y inv r R f i R f n R n M k + R i M k j M k R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i I I maDet R M = I maDet R j I , k I if j = i 0 R + R i M k j M k
150 elequ2 y = x i y i x
151 150 notbid y = x ¬ i y ¬ i x
152 sseq1 y = x y I x I
153 151 152 anbi12d y = x ¬ i y y I ¬ i x x I
154 153 anbi2d y = x R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i y y I R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x x I
155 mpteq1 y = x n y inv r R f i R f n R n M k = n x inv r R f i R f n R n M k
156 155 oveq2d y = x R n y inv r R f i R f n R n M k = R n x inv r R f i R f n R n M k
157 156 oveq1d y = x R n y inv r R f i R f n R n M k + R i M k = R n x inv r R f i R f n R n M k + R i M k
158 157 ifeq1d y = x if j = i R n y inv r R f i R f n R n M k + R i M k j M k = if j = i R n x inv r R f i R f n R n M k + R i M k j M k
159 158 mpoeq3dv y = x j I , k I if j = i R n y inv r R f i R f n R n M k + R i M k j M k = j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k j M k
160 159 fveq2d y = x I maDet R j I , k I if j = i R n y inv r R f i R f n R n M k + R i M k j M k = I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k j M k
161 160 eqeq2d y = x I maDet R M = I maDet R j I , k I if j = i R n y inv r R f i R f n R n M k + R i M k j M k I maDet R M = I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k j M k
162 154 161 imbi12d y = x R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i y y I I maDet R M = I maDet R j I , k I if j = i R n y inv r R f i R f n R n M k + R i M k j M k R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x x I I maDet R M = I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k j M k
163 eleq2 y = x z i y i x z
164 163 notbid y = x z ¬ i y ¬ i x z
165 sseq1 y = x z y I x z I
166 164 165 anbi12d y = x z ¬ i y y I ¬ i x z x z I
167 166 anbi2d y = x z R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i y y I R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x z x z I
168 mpteq1 y = x z n y inv r R f i R f n R n M k = n x z inv r R f i R f n R n M k
169 168 oveq2d y = x z R n y inv r R f i R f n R n M k = R n x z inv r R f i R f n R n M k
170 169 oveq1d y = x z R n y inv r R f i R f n R n M k + R i M k = R n x z inv r R f i R f n R n M k + R i M k
171 170 ifeq1d y = x z if j = i R n y inv r R f i R f n R n M k + R i M k j M k = if j = i R n x z inv r R f i R f n R n M k + R i M k j M k
172 171 mpoeq3dv y = x z j I , k I if j = i R n y inv r R f i R f n R n M k + R i M k j M k = j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k j M k
173 172 fveq2d y = x z I maDet R j I , k I if j = i R n y inv r R f i R f n R n M k + R i M k j M k = I maDet R j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k j M k
174 173 eqeq2d y = x z I maDet R M = I maDet R j I , k I if j = i R n y inv r R f i R f n R n M k + R i M k j M k I maDet R M = I maDet R j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k j M k
175 167 174 imbi12d y = x z R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i y y I I maDet R M = I maDet R j I , k I if j = i R n y inv r R f i R f n R n M k + R i M k j M k R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x z x z I I maDet R M = I maDet R j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k j M k
176 eleq2 y = I i i y i I i
177 176 notbid y = I i ¬ i y ¬ i I i
178 sseq1 y = I i y I I i I
179 177 178 anbi12d y = I i ¬ i y y I ¬ i I i I i I
180 179 anbi2d y = I i R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i y y I R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i I i I i I
181 mpteq1 y = I i n y inv r R f i R f n R n M k = n I i inv r R f i R f n R n M k
182 181 oveq2d y = I i R n y inv r R f i R f n R n M k = R n I i inv r R f i R f n R n M k
183 182 oveq1d y = I i R n y inv r R f i R f n R n M k + R i M k = R n I i inv r R f i R f n R n M k + R i M k
184 183 ifeq1d y = I i if j = i R n y inv r R f i R f n R n M k + R i M k j M k = if j = i R n I i inv r R f i R f n R n M k + R i M k j M k
185 184 mpoeq3dv y = I i j I , k I if j = i R n y inv r R f i R f n R n M k + R i M k j M k = j I , k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k
186 185 fveq2d y = I i I maDet R j I , k I if j = i R n y inv r R f i R f n R n M k + R i M k j M k = I maDet R j I , k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k
187 186 eqeq2d y = I i I maDet R M = I maDet R j I , k I if j = i R n y inv r R f i R f n R n M k + R i M k j M k I maDet R M = I maDet R j I , k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k
188 180 187 imbi12d y = I i R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i y y I I maDet R M = I maDet R j I , k I if j = i R n y inv r R f i R f n R n M k + R i M k j M k R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i I i I i I I maDet R M = I maDet R j I , k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k
189 fnov M Fn I × I M = j I , k I j M k
190 59 189 sylib M : I × I Base R M = j I , k I j M k
191 190 adantl R Field M : I × I Base R M = j I , k I j M k
192 ringgrp R Ring R Grp
193 4 192 syl R Field R Grp
194 oveq1 i = j i M k = j M k
195 194 equcoms j = i i M k = j M k
196 195 oveq2d j = i 0 R + R i M k = 0 R + R j M k
197 simp1l R Grp M : I × I Base R j I k I R Grp
198 fovrn M : I × I Base R j I k I j M k Base R
199 198 3adant1l R Grp M : I × I Base R j I k I j M k Base R
200 eqid + R = + R
201 10 200 100 grplid R Grp j M k Base R 0 R + R j M k = j M k
202 197 199 201 syl2anc R Grp M : I × I Base R j I k I 0 R + R j M k = j M k
203 196 202 sylan9eqr R Grp M : I × I Base R j I k I j = i 0 R + R i M k = j M k
204 eqidd R Grp M : I × I Base R j I k I ¬ j = i j M k = j M k
205 203 204 ifeqda R Grp M : I × I Base R j I k I if j = i 0 R + R i M k j M k = j M k
206 205 mpoeq3dva R Grp M : I × I Base R j I , k I if j = i 0 R + R i M k j M k = j I , k I j M k
207 193 206 sylan R Field M : I × I Base R j I , k I if j = i 0 R + R i M k j M k = j I , k I j M k
208 191 207 eqtr4d R Field M : I × I Base R M = j I , k I if j = i 0 R + R i M k j M k
209 208 fveq2d R Field M : I × I Base R I maDet R M = I maDet R j I , k I if j = i 0 R + R i M k j M k
210 209 ad4antr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i I I maDet R M = I maDet R j I , k I if j = i 0 R + R i M k j M k
211 elun1 i x i x z
212 211 con3i ¬ i x z ¬ i x
213 ssun1 x x z
214 sstr x x z x z I x I
215 213 214 mpan x z I x I
216 212 215 anim12i ¬ i x z x z I ¬ i x x I
217 216 anim2i R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x z x z I R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x x I
218 217 adantr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x z x z I ¬ z x R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x x I
219 velsn i z i = z
220 elun2 i z i x z
221 219 220 sylbir i = z i x z
222 221 necon3bi ¬ i x z i z
223 222 anim1i ¬ i x z x z I i z x z I
224 ringcmn R Ring R CMnd
225 4 224 syl R Field R CMnd
226 225 ad7antr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x k I R CMnd
227 simplr R Field M : I × I Base R I Fin f : I Base R I Fin
228 215 adantl i z x z I x I
229 ssfi I Fin x I x Fin
230 227 228 229 syl2an R Field M : I × I Base R I Fin f : I Base R i z x z I x Fin
231 230 ad5ant13 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x k I x Fin
232 215 sselda x z I n x n I
233 232 adantll i z x z I n x n I
234 233 ad4ant24 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I k I n x n I
235 4 ad6antr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I n I R Ring
236 2 ad2antrr R Field M : I × I Base R I Fin R DivRing
237 ffvelrn f : I Base R i I f i Base R
238 237 anim2i R DivRing f : I Base R i I R DivRing f i Base R
239 238 anassrs R DivRing f : I Base R i I R DivRing f i Base R
240 eqid inv r R = inv r R
241 10 100 240 drnginvrcl R DivRing f i Base R f i 0 R inv r R f i Base R
242 241 3expa R DivRing f i Base R f i 0 R inv r R f i Base R
243 239 242 sylan R DivRing f : I Base R i I f i 0 R inv r R f i Base R
244 243 anasss R DivRing f : I Base R i I f i 0 R inv r R f i Base R
245 236 244 sylanl1 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R inv r R f i Base R
246 245 ad2antrr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I n I inv r R f i Base R
247 43 ad5ant25 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I n I f n Base R
248 simp-4r R Field M : I × I Base R I Fin f : I Base R i I f i 0 R M : I × I Base R
249 76 3expa M : I × I Base R n I k I n M k Base R
250 249 an32s M : I × I Base R k I n I n M k Base R
251 248 250 sylanl1 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I n I n M k Base R
252 235 247 251 78 syl3anc R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I n I f n R n M k Base R
253 10 47 ringcl R Ring inv r R f i Base R f n R n M k Base R inv r R f i R f n R n M k Base R
254 235 246 252 253 syl3anc R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I n I inv r R f i R f n R n M k Base R
255 254 adantllr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I k I n I inv r R f i R f n R n M k Base R
256 234 255 syldan R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I k I n x inv r R f i R f n R n M k Base R
257 256 adantllr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x k I n x inv r R f i R f n R n M k Base R
258 vex z V
259 258 a1i R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x k I z V
260 simplr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x k I ¬ z x
261 ssun2 z x z
262 sstr z x z x z I z I
263 261 262 mpan x z I z I
264 258 snss z I z I
265 263 264 sylibr x z I z I
266 265 adantl i z x z I z I
267 4 ad6antr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R z I k I R Ring
268 4 ad5antr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R z I R Ring
269 245 adantr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R z I inv r R f i Base R
270 ffvelrn f : I Base R z I f z Base R
271 270 ad4ant24 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R z I f z Base R
272 10 47 ringcl R Ring inv r R f i Base R f z Base R inv r R f i R f z Base R
273 268 269 271 272 syl3anc R Field M : I × I Base R I Fin f : I Base R i I f i 0 R z I inv r R f i R f z Base R
274 273 adantr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R z I k I inv r R f i R f z Base R
275 fovrn M : I × I Base R z I k I z M k Base R
276 275 3expa M : I × I Base R z I k I z M k Base R
277 248 276 sylanl1 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R z I k I z M k Base R
278 10 47 ringcl R Ring inv r R f i R f z Base R z M k Base R inv r R f i R f z R z M k Base R
279 267 274 277 278 syl3anc R Field M : I × I Base R I Fin f : I Base R i I f i 0 R z I k I inv r R f i R f z R z M k Base R
280 266 279 sylanl2 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I k I inv r R f i R f z R z M k Base R
281 280 adantlr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x k I inv r R f i R f z R z M k Base R
282 fveq2 n = z f n = f z
283 oveq1 n = z n M k = z M k
284 282 283 oveq12d n = z f n R n M k = f z R z M k
285 284 oveq2d n = z inv r R f i R f n R n M k = inv r R f i R f z R z M k
286 245 ad2antrr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R z I k I inv r R f i Base R
287 270 ad5ant24 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R z I k I f z Base R
288 10 47 ringass R Ring inv r R f i Base R f z Base R z M k Base R inv r R f i R f z R z M k = inv r R f i R f z R z M k
289 267 286 287 277 288 syl13anc R Field M : I × I Base R I Fin f : I Base R i I f i 0 R z I k I inv r R f i R f z R z M k = inv r R f i R f z R z M k
290 289 eqcomd R Field M : I × I Base R I Fin f : I Base R i I f i 0 R z I k I inv r R f i R f z R z M k = inv r R f i R f z R z M k
291 266 290 sylanl2 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I k I inv r R f i R f z R z M k = inv r R f i R f z R z M k
292 285 291 sylan9eqr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I k I n = z inv r R f i R f n R n M k = inv r R f i R f z R z M k
293 292 adantllr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x k I n = z inv r R f i R f n R n M k = inv r R f i R f z R z M k
294 10 200 226 231 257 259 260 281 293 gsumunsnd R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x k I R n x z inv r R f i R f n R n M k = R n x inv r R f i R f n R n M k + R inv r R f i R f z R z M k
295 294 oveq1d R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x k I R n x z inv r R f i R f n R n M k + R i M k = R n x inv r R f i R f n R n M k + R inv r R f i R f z R z M k + R i M k
296 ringabl R Ring R Abel
297 4 296 syl R Field R Abel
298 297 ad6antr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R x z I k I R Abel
299 225 ad6antr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R x I k I R CMnd
300 vex x V
301 300 a1i R Field M : I × I Base R I Fin f : I Base R i I f i 0 R x I k I x V
302 ssel2 x I n x n I
303 302 254 sylan2 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I x I n x inv r R f i R f n R n M k Base R
304 303 anassrs R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I x I n x inv r R f i R f n R n M k Base R
305 304 fmpttd R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I x I n x inv r R f i R f n R n M k : x Base R
306 305 an32s R Field M : I × I Base R I Fin f : I Base R i I f i 0 R x I k I n x inv r R f i R f n R n M k : x Base R
307 ovex inv r R f i R f n R n M k V
308 eqid n x inv r R f i R f n R n M k = n x inv r R f i R f n R n M k
309 307 308 fnmpti n x inv r R f i R f n R n M k Fn x
310 309 a1i I Fin x I n x inv r R f i R f n R n M k Fn x
311 fvexd I Fin x I 0 R V
312 310 229 311 fndmfifsupp I Fin x I finSupp 0 R n x inv r R f i R f n R n M k
313 312 adantll R Field M : I × I Base R I Fin x I finSupp 0 R n x inv r R f i R f n R n M k
314 313 ad5ant14 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R x I k I finSupp 0 R n x inv r R f i R f n R n M k
315 10 100 299 301 306 314 gsumcl R Field M : I × I Base R I Fin f : I Base R i I f i 0 R x I k I R n x inv r R f i R f n R n M k Base R
316 215 315 sylanl2 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R x z I k I R n x inv r R f i R f n R n M k Base R
317 265 279 sylanl2 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R x z I k I inv r R f i R f z R z M k Base R
318 simpllr R Field M : I × I Base R I Fin f : I Base R M : I × I Base R
319 simpl i I f i 0 R i I
320 318 319 anim12i R Field M : I × I Base R I Fin f : I Base R i I f i 0 R M : I × I Base R i I
321 320 adantr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R x z I M : I × I Base R i I
322 fovrn M : I × I Base R i I k I i M k Base R
323 322 3expa M : I × I Base R i I k I i M k Base R
324 321 323 sylan R Field M : I × I Base R I Fin f : I Base R i I f i 0 R x z I k I i M k Base R
325 10 200 298 316 317 324 abl32 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R x z I k I R n x inv r R f i R f n R n M k + R inv r R f i R f z R z M k + R i M k = R n x inv r R f i R f n R n M k + R i M k + R inv r R f i R f z R z M k
326 325 adantlrl R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I k I R n x inv r R f i R f n R n M k + R inv r R f i R f z R z M k + R i M k = R n x inv r R f i R f n R n M k + R i M k + R inv r R f i R f z R z M k
327 326 adantlr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x k I R n x inv r R f i R f n R n M k + R inv r R f i R f z R z M k + R i M k = R n x inv r R f i R f n R n M k + R i M k + R inv r R f i R f z R z M k
328 295 327 eqtrd R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x k I R n x z inv r R f i R f n R n M k + R i M k = R n x inv r R f i R f n R n M k + R i M k + R inv r R f i R f z R z M k
329 328 ifeq1d R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x k I if j = i R n x z inv r R f i R f n R n M k + R i M k if j = z z M k j M k = if j = i R n x inv r R f i R f n R n M k + R i M k + R inv r R f i R f z R z M k if j = z z M k j M k
330 329 3adant2 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x j I k I if j = i R n x z inv r R f i R f n R n M k + R i M k if j = z z M k j M k = if j = i R n x inv r R f i R f n R n M k + R i M k + R inv r R f i R f z R z M k if j = z z M k j M k
331 330 mpoeq3dva R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k if j = z z M k j M k = j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k + R inv r R f i R f z R z M k if j = z z M k j M k
332 331 fveq2d R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x I maDet R j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k if j = z z M k j M k = I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k + R inv r R f i R f z R z M k if j = z z M k j M k
333 eqid I maDet R = I maDet R
334 1 simprbi R Field R CRing
335 334 ad5antr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I R CRing
336 simp-4r R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I I Fin
337 193 ad6antr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R x I k I R Grp
338 320 adantr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R x I M : I × I Base R i I
339 338 323 sylan R Field M : I × I Base R I Fin f : I Base R i I f i 0 R x I k I i M k Base R
340 10 200 grpcl R Grp R n x inv r R f i R f n R n M k Base R i M k Base R R n x inv r R f i R f n R n M k + R i M k Base R
341 337 315 339 340 syl3anc R Field M : I × I Base R I Fin f : I Base R i I f i 0 R x I k I R n x inv r R f i R f n R n M k + R i M k Base R
342 228 341 sylanl2 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I k I R n x inv r R f i R f n R n M k + R i M k Base R
343 248 266 anim12i R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I M : I × I Base R z I
344 343 276 sylan R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I k I z M k Base R
345 simp-5r R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I M : I × I Base R
346 345 198 syl3an1 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I j I k I j M k Base R
347 266 273 sylan2 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I inv r R f i R f z Base R
348 simplrl R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I i I
349 265 ad2antll R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I z I
350 simprl R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I i z
351 333 10 200 47 335 336 342 344 346 347 348 349 350 mdetero R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k + R inv r R f i R f z R z M k if j = z z M k j M k = I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k if j = z z M k j M k
352 351 adantr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k + R inv r R f i R f z R z M k if j = z z M k j M k = I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k if j = z z M k j M k
353 332 352 eqtrd R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x I maDet R j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k if j = z z M k j M k = I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k if j = z z M k j M k
354 iftrue j = z if j = z z M k j M k = z M k
355 oveq1 j = z j M k = z M k
356 354 355 eqtr4d j = z if j = z z M k j M k = j M k
357 iffalse ¬ j = z if j = z z M k j M k = j M k
358 356 357 pm2.61i if j = z z M k j M k = j M k
359 ifeq2 if j = z z M k j M k = j M k if j = i R n x z inv r R f i R f n R n M k + R i M k if j = z z M k j M k = if j = i R n x z inv r R f i R f n R n M k + R i M k j M k
360 358 359 mp1i j I k I if j = i R n x z inv r R f i R f n R n M k + R i M k if j = z z M k j M k = if j = i R n x z inv r R f i R f n R n M k + R i M k j M k
361 360 mpoeq3ia j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k if j = z z M k j M k = j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k j M k
362 361 fveq2i I maDet R j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k if j = z z M k j M k = I maDet R j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k j M k
363 ifeq2 if j = z z M k j M k = j M k if j = i R n x inv r R f i R f n R n M k + R i M k if j = z z M k j M k = if j = i R n x inv r R f i R f n R n M k + R i M k j M k
364 358 363 mp1i j I k I if j = i R n x inv r R f i R f n R n M k + R i M k if j = z z M k j M k = if j = i R n x inv r R f i R f n R n M k + R i M k j M k
365 364 mpoeq3ia j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k if j = z z M k j M k = j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k j M k
366 365 fveq2i I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k if j = z z M k j M k = I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k j M k
367 353 362 366 3eqtr3g R Field M : I × I Base R I Fin f : I Base R i I f i 0 R i z x z I ¬ z x I maDet R j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k j M k = I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k j M k
368 223 367 sylanl2 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x z x z I ¬ z x I maDet R j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k j M k = I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k j M k
369 368 eqeq2d R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x z x z I ¬ z x I maDet R M = I maDet R j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k j M k I maDet R M = I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k j M k
370 369 biimprd R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x z x z I ¬ z x I maDet R M = I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k j M k I maDet R M = I maDet R j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k j M k
371 218 370 embantd R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x z x z I ¬ z x R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x x I I maDet R M = I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k j M k I maDet R M = I maDet R j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k j M k
372 371 expcom ¬ z x R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x z x z I R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x x I I maDet R M = I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k j M k I maDet R M = I maDet R j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k j M k
373 372 com23 ¬ z x R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x x I I maDet R M = I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k j M k R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x z x z I I maDet R M = I maDet R j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k j M k
374 373 adantl x Fin ¬ z x R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x x I I maDet R M = I maDet R j I , k I if j = i R n x inv r R f i R f n R n M k + R i M k j M k R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i x z x z I I maDet R M = I maDet R j I , k I if j = i R n x z inv r R f i R f n R n M k + R i M k j M k
375 149 162 175 188 210 374 findcard2s I i Fin R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i I i I i I I maDet R M = I maDet R j I , k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k
376 132 375 mpcom R Field M : I × I Base R I Fin f : I Base R i I f i 0 R ¬ i I i I i I I maDet R M = I maDet R j I , k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k
377 129 130 376 mpanr12 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R I maDet R M = I maDet R j I , k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k
378 377 adantlr R Field M : I × I Base R I Fin f : I Base R k I R n I f n R n M k = I × 0 R i I f i 0 R I maDet R M = I maDet R j I , k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k
379 eqid I = I
380 fconstmpt I × 0 R = k I 0 R
381 380 eqeq2i k I R n I f n R n M k = I × 0 R k I R n I f n R n M k = k I 0 R
382 ovex R n I f n R n M k V
383 382 rgenw k I R n I f n R n M k V
384 mpteqb k I R n I f n R n M k V k I R n I f n R n M k = k I 0 R k I R n I f n R n M k = 0 R
385 383 384 ax-mp k I R n I f n R n M k = k I 0 R k I R n I f n R n M k = 0 R
386 381 385 bitri k I R n I f n R n M k = I × 0 R k I R n I f n R n M k = 0 R
387 225 ad5antr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R CMnd
388 simp-4r R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I I Fin
389 eqid n I inv r R f i R f n R n M k = n I inv r R f i R f n R n M k
390 307 389 fnmpti n I inv r R f i R f n R n M k Fn I
391 390 a1i I Fin n I inv r R f i R f n R n M k Fn I
392 id I Fin I Fin
393 fvexd I Fin 0 R V
394 391 392 393 fndmfifsupp I Fin finSupp 0 R n I inv r R f i R f n R n M k
395 394 ad4antlr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I finSupp 0 R n I inv r R f i R f n R n M k
396 simplrl R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I i I
397 320 323 sylan R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I i M k Base R
398 fveq2 n = i f n = f i
399 oveq1 n = i n M k = i M k
400 398 399 oveq12d n = i f n R n M k = f i R i M k
401 400 oveq2d n = i inv r R f i R f n R n M k = inv r R f i R f i R i M k
402 simpll R Field M : I × I Base R I Fin R Field
403 2 237 anim12i R Field f : I Base R i I R DivRing f i Base R
404 403 anassrs R Field f : I Base R i I R DivRing f i Base R
405 eqid 1 R = 1 R
406 10 100 47 405 240 drnginvrl R DivRing f i Base R f i 0 R inv r R f i R f i = 1 R
407 406 3expa R DivRing f i Base R f i 0 R inv r R f i R f i = 1 R
408 404 407 sylan R Field f : I Base R i I f i 0 R inv r R f i R f i = 1 R
409 408 anasss R Field f : I Base R i I f i 0 R inv r R f i R f i = 1 R
410 409 oveq1d R Field f : I Base R i I f i 0 R inv r R f i R f i R i M k = 1 R R i M k
411 402 410 sylanl1 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R inv r R f i R f i R i M k = 1 R R i M k
412 411 adantr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I inv r R f i R f i R i M k = 1 R R i M k
413 4 ad5antr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R Ring
414 245 adantr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I inv r R f i Base R
415 237 ad2ant2lr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R f i Base R
416 415 adantr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I f i Base R
417 10 47 ringass R Ring inv r R f i Base R f i Base R i M k Base R inv r R f i R f i R i M k = inv r R f i R f i R i M k
418 413 414 416 397 417 syl13anc R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I inv r R f i R f i R i M k = inv r R f i R f i R i M k
419 4 adantr R Field M : I × I Base R R Ring
420 419 3ad2ant1 R Field M : I × I Base R i I k I R Ring
421 322 3adant1l R Field M : I × I Base R i I k I i M k Base R
422 10 47 405 ringlidm R Ring i M k Base R 1 R R i M k = i M k
423 420 421 422 syl2anc R Field M : I × I Base R i I k I 1 R R i M k = i M k
424 423 ad5ant145 R Field M : I × I Base R I Fin f : I Base R i I k I 1 R R i M k = i M k
425 424 adantlrr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I 1 R R i M k = i M k
426 412 418 425 3eqtr3d R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I inv r R f i R f i R i M k = i M k
427 401 426 sylan9eqr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I n = i inv r R f i R f n R n M k = i M k
428 10 200 387 388 395 254 396 397 427 gsumdifsnd R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R n I inv r R f i R f n R n M k = R n I i inv r R f i R f n R n M k + R i M k
429 ovex f n R n M k V
430 eqid n I f n R n M k = n I f n R n M k
431 429 430 fnmpti n I f n R n M k Fn I
432 431 a1i I Fin n I f n R n M k Fn I
433 432 392 393 fndmfifsupp I Fin finSupp 0 R n I f n R n M k
434 433 ad4antlr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I finSupp 0 R n I f n R n M k
435 10 100 200 47 413 388 414 252 434 gsummulc2 R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R n I inv r R f i R f n R n M k = inv r R f i R R n I f n R n M k
436 428 435 eqtr3d R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R n I i inv r R f i R f n R n M k + R i M k = inv r R f i R R n I f n R n M k
437 436 adantr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R n I f n R n M k = 0 R R n I i inv r R f i R f n R n M k + R i M k = inv r R f i R R n I f n R n M k
438 oveq2 R n I f n R n M k = 0 R inv r R f i R R n I f n R n M k = inv r R f i R 0 R
439 438 adantl R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R n I f n R n M k = 0 R inv r R f i R R n I f n R n M k = inv r R f i R 0 R
440 4 ad4antr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R R Ring
441 10 47 100 ringrz R Ring inv r R f i Base R inv r R f i R 0 R = 0 R
442 440 245 441 syl2anc R Field M : I × I Base R I Fin f : I Base R i I f i 0 R inv r R f i R 0 R = 0 R
443 442 ad2antrr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R n I f n R n M k = 0 R inv r R f i R 0 R = 0 R
444 437 439 443 3eqtrd R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R n I f n R n M k = 0 R R n I i inv r R f i R f n R n M k + R i M k = 0 R
445 444 ifeq1d R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R n I f n R n M k = 0 R if j = i R n I i inv r R f i R f n R n M k + R i M k j M k = if j = i 0 R j M k
446 445 ex R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R n I f n R n M k = 0 R if j = i R n I i inv r R f i R f n R n M k + R i M k j M k = if j = i 0 R j M k
447 446 ralimdva R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R n I f n R n M k = 0 R k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k = if j = i 0 R j M k
448 447 imp R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R n I f n R n M k = 0 R k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k = if j = i 0 R j M k
449 386 448 sylan2b R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R n I f n R n M k = I × 0 R k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k = if j = i 0 R j M k
450 449 379 jctil R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R n I f n R n M k = I × 0 R I = I k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k = if j = i 0 R j M k
451 450 ralrimivw R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R n I f n R n M k = I × 0 R j I I = I k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k = if j = i 0 R j M k
452 mpoeq123 I = I j I I = I k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k = if j = i 0 R j M k j I , k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k = j I , k I if j = i 0 R j M k
453 379 451 452 sylancr R Field M : I × I Base R I Fin f : I Base R i I f i 0 R k I R n I f n R n M k = I × 0 R j I , k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k = j I , k I if j = i 0 R j M k
454 453 an32s R Field M : I × I Base R I Fin f : I Base R k I R n I f n R n M k = I × 0 R i I f i 0 R j I , k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k = j I , k I if j = i 0 R j M k
455 454 fveq2d R Field M : I × I Base R I Fin f : I Base R k I R n I f n R n M k = I × 0 R i I f i 0 R I maDet R j I , k I if j = i R n I i inv r R f i R f n R n M k + R i M k j M k = I maDet R j I , k I if j = i 0 R j M k
456 334 ad3antrrr R Field M : I × I Base R I Fin i I f i 0 R R CRing
457 simplr R Field M : I × I Base R I Fin i I f i 0 R I Fin
458 simpllr R Field M : I × I Base R I Fin i I f i 0 R M : I × I Base R
459 458 198 syl3an1 R Field M : I × I Base R I Fin i I f i 0 R j I k I j M k Base R
460 simprl R Field M : I × I Base R I Fin i I f i 0 R i I
461 333 10 100 456 457 459 460 mdetr0 R Field M : I × I Base R I Fin i I f i 0 R I maDet R j I , k I if j = i 0 R j M k = 0 R
462 461 ad4ant14 R Field M : I × I Base R I Fin f : I Base R k I R n I f n R n M k = I × 0 R i I f i 0 R I maDet R j I , k I if j = i 0 R j M k = 0 R
463 378 455 462 3eqtrd R Field M : I × I Base R I Fin f : I Base R k I R n I f n R n M k = I × 0 R i I f i 0 R I maDet R M = 0 R
464 463 rexlimdvaa R Field M : I × I Base R I Fin f : I Base R k I R n I f n R n M k = I × 0 R i I f i 0 R I maDet R M = 0 R
465 464 expimpd R Field M : I × I Base R I Fin f : I Base R k I R n I f n R n M k = I × 0 R i I f i 0 R I maDet R M = 0 R
466 128 465 sylan2d R Field M : I × I Base R I Fin f : I Base R k I R n I f n R n M k = I × 0 R ¬ f = I × 0 R I maDet R M = 0 R
467 32 466 sylan2 R Field M : I × I Base R I Fin f Base R I k I R n I f n R n M k = I × 0 R ¬ f = I × 0 R I maDet R M = 0 R
468 467 rexlimdva R Field M : I × I Base R I Fin f Base R I k I R n I f n R n M k = I × 0 R ¬ f = I × 0 R I maDet R M = 0 R
469 9 468 sylan2 R Field M : I × I Base R I Fin f Base R I k I R n I f n R n M k = I × 0 R ¬ f = I × 0 R I maDet R M = 0 R
470 115 469 sylbid R Field M : I × I Base R I Fin ¬ curry M LIndF R freeLMod I I maDet R M = 0 R