Step | Hyp | Ref
| Expression |
1 | | crngring 20068 |
. . . 4
β’ (π
β CRing β π
β Ring) |
2 | 1 | 3ad2ant2 1135 |
. . 3
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π
β Ring) |
3 | | simp3 1139 |
. . 3
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π β π΅) |
4 | | pmatcollpw.p |
. . . 4
β’ π = (Poly1βπ
) |
5 | | pmatcollpw.c |
. . . 4
β’ πΆ = (π Mat π) |
6 | | pmatcollpw.b |
. . . 4
β’ π΅ = (BaseβπΆ) |
7 | | eqid 2733 |
. . . 4
β’ (π Mat π
) = (π Mat π
) |
8 | | eqid 2733 |
. . . 4
β’
(0gβ(π Mat π
)) = (0gβ(π Mat π
)) |
9 | 4, 5, 6, 7, 8 | decpmataa0 22270 |
. . 3
β’ ((π
β Ring β§ π β π΅) β βπ β β0 βπ β β0
(π < π β (π decompPMat π) = (0gβ(π Mat π
)))) |
10 | 2, 3, 9 | syl2anc 585 |
. 2
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β βπ β β0 βπ β β0
(π < π β (π decompPMat π) = (0gβ(π Mat π
)))) |
11 | | pmatcollpw.m |
. . . . . . 7
β’ β = (
Β·π βπΆ) |
12 | | pmatcollpw.e |
. . . . . . 7
β’ β =
(.gβ(mulGrpβπ)) |
13 | | pmatcollpw.x |
. . . . . . 7
β’ π = (var1βπ
) |
14 | | pmatcollpw.t |
. . . . . . 7
β’ π = (π matToPolyMat π
) |
15 | 4, 5, 6, 11, 12, 13, 14 | pmatcollpw 22283 |
. . . . . 6
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π = (πΆ Ξ£g (π β β0
β¦ ((π β π) β (πβ(π decompPMat π)))))) |
16 | 15 | ad2antrr 725 |
. . . . 5
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§
βπ β
β0 (π <
π β (π decompPMat π) = (0gβ(π Mat π
)))) β π = (πΆ Ξ£g (π β β0
β¦ ((π β π) β (πβ(π decompPMat π)))))) |
17 | | eqid 2733 |
. . . . . 6
β’
(0gβπΆ) = (0gβπΆ) |
18 | | simp1 1137 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π β Fin) |
19 | 4, 5 | pmatring 22194 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring) β πΆ β Ring) |
20 | 18, 2, 19 | syl2anc 585 |
. . . . . . . 8
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β πΆ β Ring) |
21 | | ringcmn 20099 |
. . . . . . . 8
β’ (πΆ β Ring β πΆ β CMnd) |
22 | 20, 21 | syl 17 |
. . . . . . 7
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β πΆ β CMnd) |
23 | 22 | ad2antrr 725 |
. . . . . 6
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§
βπ β
β0 (π <
π β (π decompPMat π) = (0gβ(π Mat π
)))) β πΆ β CMnd) |
24 | 18 | adantr 482 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β π β Fin) |
25 | 2 | adantr 482 |
. . . . . . . . . 10
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β π
β Ring) |
26 | 4 | ply1ring 21770 |
. . . . . . . . . 10
β’ (π
β Ring β π β Ring) |
27 | 25, 26 | syl 17 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β π β Ring) |
28 | 2 | anim1i 616 |
. . . . . . . . . 10
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β (π
β Ring β§ π β
β0)) |
29 | | eqid 2733 |
. . . . . . . . . . 11
β’
(mulGrpβπ) =
(mulGrpβπ) |
30 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
31 | 4, 13, 29, 12, 30 | ply1moncl 21793 |
. . . . . . . . . 10
β’ ((π
β Ring β§ π β β0)
β (π β π) β (Baseβπ)) |
32 | 28, 31 | syl 17 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β (π β π) β (Baseβπ)) |
33 | | simpl2 1193 |
. . . . . . . . . . 11
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β π
β CRing) |
34 | 3 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β π β π΅) |
35 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β π β
β0) |
36 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(Baseβ(π Mat
π
)) = (Baseβ(π Mat π
)) |
37 | 4, 5, 6, 7, 36 | decpmatcl 22269 |
. . . . . . . . . . 11
β’ ((π
β CRing β§ π β π΅ β§ π β β0) β (π decompPMat π) β (Baseβ(π Mat π
))) |
38 | 33, 34, 35, 37 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β (π decompPMat π) β (Baseβ(π Mat π
))) |
39 | 14, 7, 36, 4, 5, 6 | mat2pmatbas0 22229 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β Ring β§ (π decompPMat π) β (Baseβ(π Mat π
))) β (πβ(π decompPMat π)) β π΅) |
40 | 24, 25, 38, 39 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β (πβ(π decompPMat π)) β π΅) |
41 | 30, 5, 6, 11 | matvscl 21933 |
. . . . . . . . 9
β’ (((π β Fin β§ π β Ring) β§ ((π β π) β (Baseβπ) β§ (πβ(π decompPMat π)) β π΅)) β ((π β π) β (πβ(π decompPMat π))) β π΅) |
42 | 24, 27, 32, 40, 41 | syl22anc 838 |
. . . . . . . 8
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β ((π β π) β (πβ(π decompPMat π))) β π΅) |
43 | 42 | ralrimiva 3147 |
. . . . . . 7
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β βπ β β0 ((π β π) β (πβ(π decompPMat π))) β π΅) |
44 | 43 | ad2antrr 725 |
. . . . . 6
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§
βπ β
β0 (π <
π β (π decompPMat π) = (0gβ(π Mat π
)))) β βπ β β0 ((π β π) β (πβ(π decompPMat π))) β π΅) |
45 | | simplr 768 |
. . . . . 6
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§
βπ β
β0 (π <
π β (π decompPMat π) = (0gβ(π Mat π
)))) β π β β0) |
46 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ ((π decompPMat π) = (0gβ(π Mat π
)) β (πβ(π decompPMat π)) = (πβ(0gβ(π Mat π
)))) |
47 | 2, 18 | jca 513 |
. . . . . . . . . . . . . . 15
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (π
β Ring β§ π β Fin)) |
48 | 47 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§ π β β0)
β (π
β Ring β§
π β
Fin)) |
49 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(0gβ(π Mat π)) = (0gβ(π Mat π)) |
50 | 14, 4, 8, 49 | 0mat2pmat 22238 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§ π β Fin) β (πβ(0gβ(π Mat π
))) = (0gβ(π Mat π))) |
51 | 48, 50 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§ π β β0)
β (πβ(0gβ(π Mat π
))) = (0gβ(π Mat π))) |
52 | 46, 51 | sylan9eqr 2795 |
. . . . . . . . . . . 12
β’
(((((π β Fin
β§ π
β CRing β§
π β π΅) β§ π β β0) β§ π β β0)
β§ (π decompPMat π) = (0gβ(π Mat π
))) β (πβ(π decompPMat π)) = (0gβ(π Mat π))) |
53 | 52 | oveq2d 7425 |
. . . . . . . . . . 11
β’
(((((π β Fin
β§ π
β CRing β§
π β π΅) β§ π β β0) β§ π β β0)
β§ (π decompPMat π) = (0gβ(π Mat π
))) β ((π β π) β (πβ(π decompPMat π))) = ((π β π) β
(0gβ(π Mat
π)))) |
54 | 4, 5 | pmatlmod 22195 |
. . . . . . . . . . . . . . 15
β’ ((π β Fin β§ π
β Ring) β πΆ β LMod) |
55 | 18, 2, 54 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β πΆ β LMod) |
56 | 55 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§ π β β0)
β πΆ β
LMod) |
57 | 28 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§ π β β0)
β (π
β Ring β§
π β
β0)) |
58 | 57, 31 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§ π β β0)
β (π β π) β (Baseβπ)) |
59 | 4 | ply1crng 21722 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π
β CRing β π β CRing) |
60 | 59 | anim2i 618 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Fin β§ π
β CRing) β (π β Fin β§ π β CRing)) |
61 | 60 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (π β Fin β§ π β CRing)) |
62 | 5 | matsca2 21922 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Fin β§ π β CRing) β π = (ScalarβπΆ)) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π = (ScalarβπΆ)) |
64 | 63 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (ScalarβπΆ) = π) |
65 | 64 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§ π β β0)
β (ScalarβπΆ) =
π) |
66 | 65 | fveq2d 6896 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§ π β β0)
β (Baseβ(ScalarβπΆ)) = (Baseβπ)) |
67 | 58, 66 | eleqtrrd 2837 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§ π β β0)
β (π β π) β
(Baseβ(ScalarβπΆ))) |
68 | 5 | eqcomi 2742 |
. . . . . . . . . . . . . . . 16
β’ (π Mat π) = πΆ |
69 | 68 | fveq2i 6895 |
. . . . . . . . . . . . . . 15
β’
(0gβ(π Mat π)) = (0gβπΆ) |
70 | 69 | oveq2i 7420 |
. . . . . . . . . . . . . 14
β’ ((π β π) β
(0gβ(π Mat
π))) = ((π β π) β
(0gβπΆ)) |
71 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(ScalarβπΆ) =
(ScalarβπΆ) |
72 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(Baseβ(ScalarβπΆ)) = (Baseβ(ScalarβπΆ)) |
73 | 71, 11, 72, 17 | lmodvs0 20506 |
. . . . . . . . . . . . . 14
β’ ((πΆ β LMod β§ (π β π) β (Baseβ(ScalarβπΆ))) β ((π β π) β
(0gβπΆ)) =
(0gβπΆ)) |
74 | 70, 73 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’ ((πΆ β LMod β§ (π β π) β (Baseβ(ScalarβπΆ))) β ((π β π) β
(0gβ(π Mat
π))) =
(0gβπΆ)) |
75 | 56, 67, 74 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§ π β β0)
β ((π β π) β
(0gβ(π Mat
π))) =
(0gβπΆ)) |
76 | 75 | adantr 482 |
. . . . . . . . . . 11
β’
(((((π β Fin
β§ π
β CRing β§
π β π΅) β§ π β β0) β§ π β β0)
β§ (π decompPMat π) = (0gβ(π Mat π
))) β ((π β π) β
(0gβ(π Mat
π))) =
(0gβπΆ)) |
77 | 53, 76 | eqtrd 2773 |
. . . . . . . . . 10
β’
(((((π β Fin
β§ π
β CRing β§
π β π΅) β§ π β β0) β§ π β β0)
β§ (π decompPMat π) = (0gβ(π Mat π
))) β ((π β π) β (πβ(π decompPMat π))) = (0gβπΆ)) |
78 | 77 | ex 414 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§ π β β0)
β ((π decompPMat π) = (0gβ(π Mat π
)) β ((π β π) β (πβ(π decompPMat π))) = (0gβπΆ))) |
79 | 78 | imim2d 57 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§ π β β0)
β ((π < π β (π decompPMat π) = (0gβ(π Mat π
))) β (π < π β ((π β π) β (πβ(π decompPMat π))) = (0gβπΆ)))) |
80 | 79 | ralimdva 3168 |
. . . . . . 7
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β
(βπ β
β0 (π <
π β (π decompPMat π) = (0gβ(π Mat π
))) β βπ β β0 (π < π β ((π β π) β (πβ(π decompPMat π))) = (0gβπΆ)))) |
81 | 80 | imp 408 |
. . . . . 6
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§
βπ β
β0 (π <
π β (π decompPMat π) = (0gβ(π Mat π
)))) β βπ β β0 (π < π β ((π β π) β (πβ(π decompPMat π))) = (0gβπΆ))) |
82 | 6, 17, 23, 44, 45, 81 | gsummptnn0fz 19854 |
. . . . 5
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§
βπ β
β0 (π <
π β (π decompPMat π) = (0gβ(π Mat π
)))) β (πΆ Ξ£g (π β β0
β¦ ((π β π) β (πβ(π decompPMat π))))) = (πΆ Ξ£g (π β (0...π ) β¦ ((π β π) β (πβ(π decompPMat π)))))) |
83 | 16, 82 | eqtrd 2773 |
. . . 4
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β§
βπ β
β0 (π <
π β (π decompPMat π) = (0gβ(π Mat π
)))) β π = (πΆ Ξ£g (π β (0...π ) β¦ ((π β π) β (πβ(π decompPMat π)))))) |
84 | 83 | ex 414 |
. . 3
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β0) β
(βπ β
β0 (π <
π β (π decompPMat π) = (0gβ(π Mat π
))) β π = (πΆ Ξ£g (π β (0...π ) β¦ ((π β π) β (πβ(π decompPMat π))))))) |
85 | 84 | reximdva 3169 |
. 2
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (βπ β β0 βπ β β0
(π < π β (π decompPMat π) = (0gβ(π Mat π
))) β βπ β β0 π = (πΆ Ξ£g (π β (0...π ) β¦ ((π β π) β (πβ(π decompPMat π))))))) |
86 | 10, 85 | mpd 15 |
1
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β βπ β β0 π = (πΆ Ξ£g (π β (0...π ) β¦ ((π β π) β (πβ(π decompPMat π)))))) |