Step | Hyp | Ref
| Expression |
1 | | decpmatmulsumfsupp.0 |
. . . 4
โข 0 =
(0gโ๐ด) |
2 | 1 | fvexi 6857 |
. . 3
โข 0 โ
V |
3 | 2 | a1i 11 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ 0 โ V) |
4 | | ovexd 7393 |
. 2
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ด ฮฃg
(๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐))))) โ V) |
5 | | oveq2 7366 |
. . . 4
โข (๐ = ๐ โ (0...๐) = (0...๐)) |
6 | | oveq1 7365 |
. . . . . 6
โข (๐ = ๐ โ (๐ โ ๐) = (๐ โ ๐)) |
7 | 6 | oveq2d 7374 |
. . . . 5
โข (๐ = ๐ โ (๐ฆ decompPMat (๐ โ ๐)) = (๐ฆ decompPMat (๐ โ ๐))) |
8 | 7 | oveq2d 7374 |
. . . 4
โข (๐ = ๐ โ ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐))) = ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐)))) |
9 | 5, 8 | mpteq12dv 5197 |
. . 3
โข (๐ = ๐ โ (๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐)))) = (๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐))))) |
10 | 9 | oveq2d 7374 |
. 2
โข (๐ = ๐ โ (๐ด ฮฃg (๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐))))) = (๐ด ฮฃg (๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐)))))) |
11 | | simpll 766 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ โ Fin) |
12 | | simplr 768 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐
โ Ring) |
13 | | decpmatmul.p |
. . . . . . . . 9
โข ๐ = (Poly1โ๐
) |
14 | | decpmatmul.c |
. . . . . . . . 9
โข ๐ถ = (๐ Mat ๐) |
15 | 13, 14 | pmatring 22057 |
. . . . . . . 8
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ถ โ Ring) |
16 | 15 | anim1i 616 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ถ โ Ring โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต))) |
17 | | 3anass 1096 |
. . . . . . 7
โข ((๐ถ โ Ring โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ถ โ Ring โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต))) |
18 | 16, 17 | sylibr 233 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ถ โ Ring โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) |
19 | | decpmatmul.b |
. . . . . . 7
โข ๐ต = (Baseโ๐ถ) |
20 | | eqid 2733 |
. . . . . . 7
โข
(.rโ๐ถ) = (.rโ๐ถ) |
21 | 19, 20 | ringcl 19986 |
. . . . . 6
โข ((๐ถ โ Ring โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ(.rโ๐ถ)๐ฆ) โ ๐ต) |
22 | 18, 21 | syl 17 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ(.rโ๐ถ)๐ฆ) โ ๐ต) |
23 | | eqid 2733 |
. . . . . 6
โข
(0gโ๐
) = (0gโ๐
) |
24 | 13, 14, 19, 23 | pmatcoe1fsupp 22066 |
. . . . 5
โข ((๐ โ Fin โง ๐
โ Ring โง (๐ฅ(.rโ๐ถ)๐ฆ) โ ๐ต) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ โ๐ โ ๐ โ๐ โ ๐ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
))) |
25 | 11, 12, 22, 24 | syl3anc 1372 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ โ๐ โ ๐ โ๐ โ ๐ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
))) |
26 | | fvoveq1 7381 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐)) = (coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))) |
27 | 26 | fveq1d 6845 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐)) |
28 | 27 | eqeq1d 2735 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ (((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
) โ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
))) |
29 | | oveq2 7366 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ (๐(๐ฅ(.rโ๐ถ)๐ฆ)๐) = (๐(๐ฅ(.rโ๐ถ)๐ฆ)๐)) |
30 | 29 | fveq2d 6847 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐)) = (coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))) |
31 | 30 | fveq1d 6845 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐)) |
32 | 31 | eqeq1d 2735 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ (((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
) โ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
))) |
33 | 28, 32 | rspc2va 3590 |
. . . . . . . . . . . . 13
โข (((๐ โ ๐ โง ๐ โ ๐) โง โ๐ โ ๐ โ๐ โ ๐ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
)) โ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
)) |
34 | 33 | expcom 415 |
. . . . . . . . . . . 12
โข
(โ๐ โ
๐ โ๐ โ ๐ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
) โ ((๐ โ ๐ โง ๐ โ ๐) โ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
))) |
35 | 34 | adantl 483 |
. . . . . . . . . . 11
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง
โ๐ โ ๐ โ๐ โ ๐ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
)) โ ((๐ โ ๐ โง ๐ โ ๐) โ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
))) |
36 | 35 | 3impib 1117 |
. . . . . . . . . 10
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง
โ๐ โ ๐ โ๐ โ ๐ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
)) โง ๐ โ ๐ โง ๐ โ ๐) โ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
)) |
37 | 36 | mpoeq3dva 7435 |
. . . . . . . . 9
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง
โ๐ โ ๐ โ๐ โ ๐ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
)) โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐)) = (๐ โ ๐, ๐ โ ๐ โฆ (0gโ๐
))) |
38 | | decpmatmul.a |
. . . . . . . . . . . 12
โข ๐ด = (๐ Mat ๐
) |
39 | 38, 23 | mat0op 21784 |
. . . . . . . . . . 11
โข ((๐ โ Fin โง ๐
โ Ring) โ
(0gโ๐ด) =
(๐ โ ๐, ๐ โ ๐ โฆ (0gโ๐
))) |
40 | 1, 39 | eqtrid 2785 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ Ring) โ 0 = (๐ โ ๐, ๐ โ ๐ โฆ (0gโ๐
))) |
41 | 40 | ad3antrrr 729 |
. . . . . . . . 9
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง
โ๐ โ ๐ โ๐ โ ๐ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
)) โ 0 = (๐ โ ๐, ๐ โ ๐ โฆ (0gโ๐
))) |
42 | 37, 41 | eqtr4d 2776 |
. . . . . . . 8
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง
โ๐ โ ๐ โ๐ โ ๐ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
)) โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐)) = 0 ) |
43 | 42 | ex 414 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ
(โ๐ โ ๐ โ๐ โ ๐ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
) โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐)) = 0 )) |
44 | 43 | imim2d 57 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ((๐ < ๐ โ โ๐ โ ๐ โ๐ โ ๐ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
)) โ (๐ < ๐ โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐)) = 0 ))) |
45 | 44 | ralimdva 3161 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (โ๐ โ โ0 (๐ < ๐ โ โ๐ โ ๐ โ๐ โ ๐ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
)) โ โ๐ โ โ0 (๐ < ๐ โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐)) = 0 ))) |
46 | 45 | reximdv 3164 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ โ๐ โ ๐ โ๐ โ ๐ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐) = (0gโ๐
)) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐)) = 0 ))) |
47 | 25, 46 | mpd 15 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐)) = 0 )) |
48 | | decpmatmulsumfsupp.m |
. . . . . . . . . . . 12
โข ยท =
(.rโ๐ด) |
49 | 48 | oveqi 7371 |
. . . . . . . . . . 11
โข ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐))) = ((๐ฅ decompPMat ๐)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐))) |
50 | 49 | a1i 11 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐))) = ((๐ฅ decompPMat ๐)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐)))) |
51 | 50 | mpteq2dv 5208 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐)))) = (๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐))))) |
52 | 51 | oveq2d 7374 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ด ฮฃg
(๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐))))) = (๐ด ฮฃg (๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐)))))) |
53 | 13, 14, 19, 38 | decpmatmul 22137 |
. . . . . . . . 9
โข ((๐
โ Ring โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง ๐ โ โ0) โ ((๐ฅ(.rโ๐ถ)๐ฆ) decompPMat ๐) = (๐ด ฮฃg (๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐)))))) |
54 | 53 | ad4ant234 1176 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ((๐ฅ(.rโ๐ถ)๐ฆ) decompPMat ๐) = (๐ด ฮฃg (๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐)))))) |
55 | 14, 19 | decpmatval 22130 |
. . . . . . . . 9
โข (((๐ฅ(.rโ๐ถ)๐ฆ) โ ๐ต โง ๐ โ โ0) โ ((๐ฅ(.rโ๐ถ)๐ฆ) decompPMat ๐) = (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐))) |
56 | 22, 55 | sylan 581 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ((๐ฅ(.rโ๐ถ)๐ฆ) decompPMat ๐) = (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐))) |
57 | 52, 54, 56 | 3eqtr2d 2779 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ด ฮฃg
(๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐))))) = (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐))) |
58 | 57 | eqeq1d 2735 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ((๐ด ฮฃg
(๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐))))) = 0 โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐)) = 0 )) |
59 | 58 | imbi2d 341 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ((๐ < ๐ โ (๐ด ฮฃg (๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐))))) = 0 ) โ (๐ < ๐ โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐)) = 0 ))) |
60 | 59 | ralbidva 3169 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (โ๐ โ โ0 (๐ < ๐ โ (๐ด ฮฃg (๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐))))) = 0 ) โ โ๐ โ โ0
(๐ < ๐ โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐)) = 0 ))) |
61 | 60 | rexbidv 3172 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐ด ฮฃg (๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐))))) = 0 ) โ โ๐ โ โ0
โ๐ โ
โ0 (๐ <
๐ โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐ฅ(.rโ๐ถ)๐ฆ)๐))โ๐)) = 0 ))) |
62 | 47, 61 | mpbird 257 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ โ๐ โ โ0 โ๐ โ โ0
(๐ < ๐ โ (๐ด ฮฃg (๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐))))) = 0 )) |
63 | 3, 4, 10, 62 | mptnn0fsuppd 13909 |
1
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ โ0 โฆ (๐ด ฮฃg
(๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐) ยท (๐ฆ decompPMat (๐ โ ๐)))))) finSupp 0 ) |