Step | Hyp | Ref
| Expression |
1 | | pmatcollpw1.p |
. . 3
โข ๐ = (Poly1โ๐
) |
2 | | pmatcollpw1.c |
. . 3
โข ๐ถ = (๐ Mat ๐) |
3 | | pmatcollpw1.b |
. . 3
โข ๐ต = (Baseโ๐ถ) |
4 | | pmatcollpw1.m |
. . 3
โข ร = (
ยท๐ โ๐) |
5 | | pmatcollpw1.e |
. . 3
โข โ =
(.gโ(mulGrpโ๐)) |
6 | | pmatcollpw1.x |
. . 3
โข ๐ = (var1โ๐
) |
7 | 1, 2, 3, 4, 5, 6 | pmatcollpw1 22499 |
. 2
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ ๐ = (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐(๐ decompPMat ๐)๐) ร (๐ โ ๐)))))) |
8 | | eqid 2731 |
. . 3
โข
(0gโ๐ถ) = (0gโ๐ถ) |
9 | | simp1 1135 |
. . 3
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ ๐ โ Fin) |
10 | | nn0ex 12483 |
. . . 4
โข
โ0 โ V |
11 | 10 | a1i 11 |
. . 3
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ โ0 โ
V) |
12 | 1 | ply1ring 21991 |
. . . 4
โข (๐
โ Ring โ ๐ โ Ring) |
13 | 12 | 3ad2ant2 1133 |
. . 3
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ ๐ โ Ring) |
14 | | eqid 2731 |
. . . 4
โข
(Baseโ๐) =
(Baseโ๐) |
15 | 9 | adantr 480 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โ ๐ โ Fin) |
16 | 13 | adantr 480 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โ ๐ โ Ring) |
17 | | simp1l2 1266 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ ๐
โ Ring) |
18 | | eqid 2731 |
. . . . . 6
โข (๐ Mat ๐
) = (๐ Mat ๐
) |
19 | | eqid 2731 |
. . . . . 6
โข
(Baseโ๐
) =
(Baseโ๐
) |
20 | | eqid 2731 |
. . . . . 6
โข
(Baseโ(๐ Mat
๐
)) = (Baseโ(๐ Mat ๐
)) |
21 | | simp2 1136 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ โ ๐) |
22 | | simp3 1137 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ โ ๐) |
23 | | simp2 1136 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ ๐
โ Ring) |
24 | 23 | adantr 480 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โ ๐
โ Ring) |
25 | | simp3 1137 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
26 | 25 | adantr 480 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โ ๐ โ ๐ต) |
27 | | simpr 484 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โ ๐ โ
โ0) |
28 | 24, 26, 27 | 3jca 1127 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โ (๐
โ Ring โง ๐ โ ๐ต โง ๐ โ
โ0)) |
29 | 28 | 3ad2ant1 1132 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐
โ Ring โง ๐ โ ๐ต โง ๐ โ
โ0)) |
30 | 1, 2, 3, 18, 20 | decpmatcl 22490 |
. . . . . . 7
โข ((๐
โ Ring โง ๐ โ ๐ต โง ๐ โ โ0) โ (๐ decompPMat ๐) โ (Baseโ(๐ Mat ๐
))) |
31 | 29, 30 | syl 17 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ decompPMat ๐) โ (Baseโ(๐ Mat ๐
))) |
32 | 18, 19, 20, 21, 22, 31 | matecld 22149 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐(๐ decompPMat ๐)๐) โ (Baseโ๐
)) |
33 | | simp1r 1197 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ โ โ0) |
34 | | eqid 2731 |
. . . . . 6
โข
(mulGrpโ๐) =
(mulGrpโ๐) |
35 | 19, 1, 6, 4, 34, 5,
14 | ply1tmcl 22015 |
. . . . 5
โข ((๐
โ Ring โง (๐(๐ decompPMat ๐)๐) โ (Baseโ๐
) โง ๐ โ โ0) โ ((๐(๐ decompPMat ๐)๐) ร (๐ โ ๐)) โ (Baseโ๐)) |
36 | 17, 32, 33, 35 | syl3anc 1370 |
. . . 4
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ ((๐(๐ decompPMat ๐)๐) ร (๐ โ ๐)) โ (Baseโ๐)) |
37 | 2, 14, 3, 15, 16, 36 | matbas2d 22146 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โ (๐ โ ๐, ๐ โ ๐ โฆ ((๐(๐ decompPMat ๐)๐) ร (๐ โ ๐))) โ ๐ต) |
38 | 1, 2, 3, 4, 5, 6 | pmatcollpw2lem 22500 |
. . 3
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ (๐ โ โ0 โฆ (๐ โ ๐, ๐ โ ๐ โฆ ((๐(๐ decompPMat ๐)๐) ร (๐ โ ๐)))) finSupp (0gโ๐ถ)) |
39 | 2, 3, 8, 9, 11, 13, 37, 38 | matgsum 22160 |
. 2
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ (๐ถ ฮฃg (๐ โ โ0
โฆ (๐ โ ๐, ๐ โ ๐ โฆ ((๐(๐ decompPMat ๐)๐) ร (๐ โ ๐))))) = (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ โ0
โฆ ((๐(๐ decompPMat ๐)๐) ร (๐ โ ๐)))))) |
40 | 7, 39 | eqtr4d 2774 |
1
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ ๐ = (๐ถ ฮฃg (๐ โ โ0
โฆ (๐ โ ๐, ๐ โ ๐ โฆ ((๐(๐ decompPMat ๐)๐) ร (๐ โ ๐)))))) |