Step | Hyp | Ref
| Expression |
1 | | eqidd 2727 |
. . . . 5
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π₯ β π, π¦ β π β¦ (π
Ξ£g (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦))))))) = (π₯ β π, π¦ β π β¦ (π
Ξ£g (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)))))))) |
2 | | oveq1 7412 |
. . . . . . . . . . 11
β’ (π₯ = π β (π₯(π decompPMat π)π‘) = (π(π decompPMat π)π‘)) |
3 | | oveq2 7413 |
. . . . . . . . . . 11
β’ (π¦ = π β (π‘(π decompPMat (πΎ β π))π¦) = (π‘(π decompPMat (πΎ β π))π)) |
4 | 2, 3 | oveqan12d 7424 |
. . . . . . . . . 10
β’ ((π₯ = π β§ π¦ = π) β ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)) = ((π(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π))) |
5 | 4 | mpteq2dv 5243 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = π) β (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦))) = (π‘ β π β¦ ((π(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π)))) |
6 | 5 | oveq2d 7421 |
. . . . . . . 8
β’ ((π₯ = π β§ π¦ = π) β (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)))) = (π
Ξ£g (π‘ β π β¦ ((π(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π))))) |
7 | 6 | mpteq2dv 5243 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = π) β (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦))))) = (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π)))))) |
8 | 7 | oveq2d 7421 |
. . . . . 6
β’ ((π₯ = π β§ π¦ = π) β (π
Ξ£g (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)))))) = (π
Ξ£g (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π))))))) |
9 | 8 | adantl 481 |
. . . . 5
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ (π₯ = π β§ π¦ = π)) β (π
Ξ£g (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)))))) = (π
Ξ£g (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π))))))) |
10 | | simprl 768 |
. . . . 5
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β π β π) |
11 | | simprr 770 |
. . . . 5
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β π β π) |
12 | | ovexd 7440 |
. . . . 5
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π
Ξ£g (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π)))))) β V) |
13 | 1, 9, 10, 11, 12 | ovmpod 7556 |
. . . 4
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π(π₯ β π, π¦ β π β¦ (π
Ξ£g (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)))))))π) = (π
Ξ£g (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π))))))) |
14 | | decpmatmul.c |
. . . . . . . . . . . . . . . . . . . 20
β’ πΆ = (π Mat π) |
15 | | decpmatmul.b |
. . . . . . . . . . . . . . . . . . . 20
β’ π΅ = (BaseβπΆ) |
16 | 14, 15 | matrcl 22267 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΅ β (π β Fin β§ π β V)) |
17 | 16 | simpld 494 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΅ β π β Fin) |
18 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π΅ β§ π β π΅) β π β Fin) |
19 | 18 | anim2i 616 |
. . . . . . . . . . . . . . . 16
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅)) β (π
β Ring β§ π β Fin)) |
20 | 19 | ancomd 461 |
. . . . . . . . . . . . . . 15
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅)) β (π β Fin β§ π
β Ring)) |
21 | 20 | 3adant3 1129 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β (π β Fin β§ π
β Ring)) |
22 | | decpmatmul.a |
. . . . . . . . . . . . . . 15
β’ π΄ = (π Mat π
) |
23 | | eqid 2726 |
. . . . . . . . . . . . . . 15
β’ (π
maMul β¨π, π, πβ©) = (π
maMul β¨π, π, πβ©) |
24 | 22, 23 | matmulr 22295 |
. . . . . . . . . . . . . 14
β’ ((π β Fin β§ π
β Ring) β (π
maMul β¨π, π, πβ©) = (.rβπ΄)) |
25 | 21, 24 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β (π
maMul β¨π, π, πβ©) = (.rβπ΄)) |
26 | 25 | adantr 480 |
. . . . . . . . . . . 12
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π
maMul β¨π, π, πβ©) = (.rβπ΄)) |
27 | 26 | adantr 480 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β (π
maMul β¨π, π, πβ©) = (.rβπ΄)) |
28 | 27 | eqcomd 2732 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β (.rβπ΄) = (π
maMul β¨π, π, πβ©)) |
29 | 28 | oveqd 7422 |
. . . . . . . . 9
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π))) = ((π decompPMat π)(π
maMul β¨π, π, πβ©)(π decompPMat (πΎ β π)))) |
30 | | eqid 2726 |
. . . . . . . . . 10
β’
(Baseβπ
) =
(Baseβπ
) |
31 | | eqid 2726 |
. . . . . . . . . 10
β’
(.rβπ
) = (.rβπ
) |
32 | | simp1 1133 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β π
β Ring) |
33 | 32 | adantr 480 |
. . . . . . . . . . 11
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β π
β Ring) |
34 | 33 | adantr 480 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β π
β Ring) |
35 | 21 | simpld 494 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β π β Fin) |
36 | 35 | adantr 480 |
. . . . . . . . . . 11
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β π β Fin) |
37 | 36 | adantr 480 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β π β Fin) |
38 | | simpl2l 1223 |
. . . . . . . . . . . . . 14
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β π β π΅) |
39 | 38 | adantr 480 |
. . . . . . . . . . . . 13
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β π β π΅) |
40 | | elfznn0 13600 |
. . . . . . . . . . . . . 14
β’ (π β (0...πΎ) β π β β0) |
41 | 40 | adantl 481 |
. . . . . . . . . . . . 13
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β π β β0) |
42 | 34, 39, 41 | 3jca 1125 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β (π
β Ring β§ π β π΅ β§ π β
β0)) |
43 | | decpmatmul.p |
. . . . . . . . . . . . 13
β’ π = (Poly1βπ
) |
44 | | eqid 2726 |
. . . . . . . . . . . . 13
β’
(Baseβπ΄) =
(Baseβπ΄) |
45 | 43, 14, 15, 22, 44 | decpmatcl 22624 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ π β π΅ β§ π β β0) β (π decompPMat π) β (Baseβπ΄)) |
46 | 42, 45 | syl 17 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β (π decompPMat π) β (Baseβπ΄)) |
47 | 22, 30, 44 | matbas2i 22279 |
. . . . . . . . . . 11
β’ ((π decompPMat π) β (Baseβπ΄) β (π decompPMat π) β ((Baseβπ
) βm (π Γ π))) |
48 | 46, 47 | syl 17 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β (π decompPMat π) β ((Baseβπ
) βm (π Γ π))) |
49 | | simpl2r 1224 |
. . . . . . . . . . . . . 14
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β π β π΅) |
50 | 49 | adantr 480 |
. . . . . . . . . . . . 13
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β π β π΅) |
51 | | fznn0sub 13539 |
. . . . . . . . . . . . . 14
β’ (π β (0...πΎ) β (πΎ β π) β
β0) |
52 | 51 | adantl 481 |
. . . . . . . . . . . . 13
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β (πΎ β π) β
β0) |
53 | 34, 50, 52 | 3jca 1125 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β (π
β Ring β§ π β π΅ β§ (πΎ β π) β
β0)) |
54 | 43, 14, 15, 22, 44 | decpmatcl 22624 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ π β π΅ β§ (πΎ β π) β β0) β (π decompPMat (πΎ β π)) β (Baseβπ΄)) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β (π decompPMat (πΎ β π)) β (Baseβπ΄)) |
56 | 22, 30, 44 | matbas2i 22279 |
. . . . . . . . . . 11
β’ ((π decompPMat (πΎ β π)) β (Baseβπ΄) β (π decompPMat (πΎ β π)) β ((Baseβπ
) βm (π Γ π))) |
57 | 55, 56 | syl 17 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β (π decompPMat (πΎ β π)) β ((Baseβπ
) βm (π Γ π))) |
58 | 23, 30, 31, 34, 37, 37, 37, 48, 57 | mamuval 22243 |
. . . . . . . . 9
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β ((π decompPMat π)(π
maMul β¨π, π, πβ©)(π decompPMat (πΎ β π))) = (π₯ β π, π¦ β π β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)))))) |
59 | 29, 58 | eqtrd 2766 |
. . . . . . . 8
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π))) = (π₯ β π, π¦ β π β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)))))) |
60 | 59 | mpteq2dva 5241 |
. . . . . . 7
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π β (0...πΎ) β¦ ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π)))) = (π β (0...πΎ) β¦ (π₯ β π, π¦ β π β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦))))))) |
61 | 60 | oveq2d 7421 |
. . . . . 6
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π΄ Ξ£g (π β (0...πΎ) β¦ ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π))))) = (π΄ Ξ£g (π β (0...πΎ) β¦ (π₯ β π, π¦ β π β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)))))))) |
62 | | eqid 2726 |
. . . . . . 7
β’
(0gβπ΄) = (0gβπ΄) |
63 | | ovexd 7440 |
. . . . . . 7
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (0...πΎ) β V) |
64 | | ringcmn 20181 |
. . . . . . . . . . . . 13
β’ (π
β Ring β π
β CMnd) |
65 | 32, 64 | syl 17 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β π
β CMnd) |
66 | 65 | adantr 480 |
. . . . . . . . . . 11
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β π
β CMnd) |
67 | 66 | adantr 480 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β π
β CMnd) |
68 | 67 | 3ad2ant1 1130 |
. . . . . . . . 9
β’
(((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β π
β CMnd) |
69 | 37 | 3ad2ant1 1130 |
. . . . . . . . 9
β’
(((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β π β Fin) |
70 | 34 | 3ad2ant1 1130 |
. . . . . . . . . . . 12
β’
(((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β π
β Ring) |
71 | 70 | adantr 480 |
. . . . . . . . . . 11
β’
((((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β§ π‘ β π) β π
β Ring) |
72 | | simpl2 1189 |
. . . . . . . . . . . 12
β’
((((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β§ π‘ β π) β π₯ β π) |
73 | | simpr 484 |
. . . . . . . . . . . 12
β’
((((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β§ π‘ β π) β π‘ β π) |
74 | 42 | 3ad2ant1 1130 |
. . . . . . . . . . . . . 14
β’
(((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β (π
β Ring β§ π β π΅ β§ π β
β0)) |
75 | 74 | adantr 480 |
. . . . . . . . . . . . 13
β’
((((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β§ π‘ β π) β (π
β Ring β§ π β π΅ β§ π β
β0)) |
76 | 75, 45 | syl 17 |
. . . . . . . . . . . 12
β’
((((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β§ π‘ β π) β (π decompPMat π) β (Baseβπ΄)) |
77 | 22, 30, 44, 72, 73, 76 | matecld 22283 |
. . . . . . . . . . 11
β’
((((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β§ π‘ β π) β (π₯(π decompPMat π)π‘) β (Baseβπ
)) |
78 | | simpl3 1190 |
. . . . . . . . . . . 12
β’
((((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β§ π‘ β π) β π¦ β π) |
79 | 55 | 3ad2ant1 1130 |
. . . . . . . . . . . . 13
β’
(((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β (π decompPMat (πΎ β π)) β (Baseβπ΄)) |
80 | 79 | adantr 480 |
. . . . . . . . . . . 12
β’
((((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β§ π‘ β π) β (π decompPMat (πΎ β π)) β (Baseβπ΄)) |
81 | 22, 30, 44, 73, 78, 80 | matecld 22283 |
. . . . . . . . . . 11
β’
((((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β§ π‘ β π) β (π‘(π decompPMat (πΎ β π))π¦) β (Baseβπ
)) |
82 | 30, 31 | ringcl 20155 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ (π₯(π decompPMat π)π‘) β (Baseβπ
) β§ (π‘(π decompPMat (πΎ β π))π¦) β (Baseβπ
)) β ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)) β (Baseβπ
)) |
83 | 71, 77, 81, 82 | syl3anc 1368 |
. . . . . . . . . 10
β’
((((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β§ π‘ β π) β ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)) β (Baseβπ
)) |
84 | 83 | ralrimiva 3140 |
. . . . . . . . 9
β’
(((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β βπ‘ β π ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)) β (Baseβπ
)) |
85 | 30, 68, 69, 84 | gsummptcl 19887 |
. . . . . . . 8
β’
(((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π₯ β π β§ π¦ β π) β (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)))) β (Baseβπ
)) |
86 | 22, 30, 44, 37, 34, 85 | matbas2d 22280 |
. . . . . . 7
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β (π₯ β π, π¦ β π β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦))))) β (Baseβπ΄)) |
87 | | eqid 2726 |
. . . . . . . 8
β’ (π β (0...πΎ) β¦ (π₯ β π, π¦ β π β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)))))) = (π β (0...πΎ) β¦ (π₯ β π, π¦ β π β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)))))) |
88 | | fzfid 13944 |
. . . . . . . 8
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (0...πΎ) β Fin) |
89 | | simpl 482 |
. . . . . . . . . . . . . . 15
β’ ((π β Fin β§ π β V) β π β Fin) |
90 | 89, 89 | jca 511 |
. . . . . . . . . . . . . 14
β’ ((π β Fin β§ π β V) β (π β Fin β§ π β Fin)) |
91 | 16, 90 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π΅ β (π β Fin β§ π β Fin)) |
92 | 91 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π β π΅ β§ π β π΅) β (π β Fin β§ π β Fin)) |
93 | 92 | 3ad2ant2 1131 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β (π β Fin β§ π β Fin)) |
94 | 93 | adantr 480 |
. . . . . . . . . 10
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π β Fin β§ π β Fin)) |
95 | 94 | adantr 480 |
. . . . . . . . 9
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β (π β Fin β§ π β Fin)) |
96 | | mpoexga 8063 |
. . . . . . . . 9
β’ ((π β Fin β§ π β Fin) β (π₯ β π, π¦ β π β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦))))) β V) |
97 | 95, 96 | syl 17 |
. . . . . . . 8
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β (π₯ β π, π¦ β π β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦))))) β V) |
98 | | fvexd 6900 |
. . . . . . . 8
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (0gβπ΄) β V) |
99 | 87, 88, 97, 98 | fsuppmptdm 9376 |
. . . . . . 7
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π β (0...πΎ) β¦ (π₯ β π, π¦ β π β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)))))) finSupp (0gβπ΄)) |
100 | 22, 44, 62, 36, 63, 33, 86, 99 | matgsum 22294 |
. . . . . 6
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π΄ Ξ£g (π β (0...πΎ) β¦ (π₯ β π, π¦ β π β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦))))))) = (π₯ β π, π¦ β π β¦ (π
Ξ£g (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)))))))) |
101 | 61, 100 | eqtrd 2766 |
. . . . 5
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π΄ Ξ£g (π β (0...πΎ) β¦ ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π))))) = (π₯ β π, π¦ β π β¦ (π
Ξ£g (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)))))))) |
102 | 101 | oveqd 7422 |
. . . 4
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π(π΄ Ξ£g (π β (0...πΎ) β¦ ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π)))))π) = (π(π₯ β π, π¦ β π β¦ (π
Ξ£g (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π₯(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π¦)))))))π)) |
103 | | simpl2 1189 |
. . . . . 6
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π β π΅ β§ π β π΅)) |
104 | | simpl3 1190 |
. . . . . 6
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β πΎ β
β0) |
105 | 43, 14, 15 | decpmatmullem 22628 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π β π΅ β§ π β π΅) β§ (π β π β§ π β π β§ πΎ β β0)) β (π((π(.rβπΆ)π) decompPMat πΎ)π) = (π
Ξ£g (π‘ β π β¦ (π
Ξ£g (π β (0...πΎ) β¦ (((coe1β(πππ‘))βπ)(.rβπ
)((coe1β(π‘ππ))β(πΎ β π)))))))) |
106 | 36, 33, 103, 10, 11, 104, 105 | syl213anc 1386 |
. . . . 5
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π((π(.rβπΆ)π) decompPMat πΎ)π) = (π
Ξ£g (π‘ β π β¦ (π
Ξ£g (π β (0...πΎ) β¦ (((coe1β(πππ‘))βπ)(.rβπ
)((coe1β(π‘ππ))β(πΎ β π)))))))) |
107 | | simpll1 1209 |
. . . . . . 7
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ (π‘ β π β§ π β (0...πΎ))) β π
β Ring) |
108 | | simplrl 774 |
. . . . . . . . 9
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ (π‘ β π β§ π β (0...πΎ))) β π β π) |
109 | | simprl 768 |
. . . . . . . . 9
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ (π‘ β π β§ π β (0...πΎ))) β π‘ β π) |
110 | 15 | eleq2i 2819 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β π β (BaseβπΆ)) |
111 | 110 | biimpi 215 |
. . . . . . . . . . . . 13
β’ (π β π΅ β π β (BaseβπΆ)) |
112 | 111 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π β π΅ β§ π β π΅) β π β (BaseβπΆ)) |
113 | 112 | 3ad2ant2 1131 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β π β (BaseβπΆ)) |
114 | 113 | adantr 480 |
. . . . . . . . . 10
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β π β (BaseβπΆ)) |
115 | 114 | adantr 480 |
. . . . . . . . 9
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ (π‘ β π β§ π β (0...πΎ))) β π β (BaseβπΆ)) |
116 | | eqid 2726 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
117 | 14, 116 | matecl 22282 |
. . . . . . . . 9
β’ ((π β π β§ π‘ β π β§ π β (BaseβπΆ)) β (πππ‘) β (Baseβπ)) |
118 | 108, 109,
115, 117 | syl3anc 1368 |
. . . . . . . 8
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ (π‘ β π β§ π β (0...πΎ))) β (πππ‘) β (Baseβπ)) |
119 | 40 | ad2antll 726 |
. . . . . . . 8
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ (π‘ β π β§ π β (0...πΎ))) β π β β0) |
120 | | eqid 2726 |
. . . . . . . . 9
β’
(coe1β(πππ‘)) = (coe1β(πππ‘)) |
121 | 120, 116,
43, 30 | coe1fvalcl 22086 |
. . . . . . . 8
β’ (((πππ‘) β (Baseβπ) β§ π β β0) β
((coe1β(πππ‘))βπ) β (Baseβπ
)) |
122 | 118, 119,
121 | syl2anc 583 |
. . . . . . 7
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ (π‘ β π β§ π β (0...πΎ))) β ((coe1β(πππ‘))βπ) β (Baseβπ
)) |
123 | | simplrr 775 |
. . . . . . . . 9
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ (π‘ β π β§ π β (0...πΎ))) β π β π) |
124 | 49 | adantr 480 |
. . . . . . . . 9
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ (π‘ β π β§ π β (0...πΎ))) β π β π΅) |
125 | 14, 116, 15, 109, 123, 124 | matecld 22283 |
. . . . . . . 8
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ (π‘ β π β§ π β (0...πΎ))) β (π‘ππ) β (Baseβπ)) |
126 | 51 | ad2antll 726 |
. . . . . . . 8
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ (π‘ β π β§ π β (0...πΎ))) β (πΎ β π) β
β0) |
127 | | eqid 2726 |
. . . . . . . . 9
β’
(coe1β(π‘ππ)) = (coe1β(π‘ππ)) |
128 | 127, 116,
43, 30 | coe1fvalcl 22086 |
. . . . . . . 8
β’ (((π‘ππ) β (Baseβπ) β§ (πΎ β π) β β0) β
((coe1β(π‘ππ))β(πΎ β π)) β (Baseβπ
)) |
129 | 125, 126,
128 | syl2anc 583 |
. . . . . . 7
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ (π‘ β π β§ π β (0...πΎ))) β ((coe1β(π‘ππ))β(πΎ β π)) β (Baseβπ
)) |
130 | 30, 31 | ringcl 20155 |
. . . . . . 7
β’ ((π
β Ring β§
((coe1β(πππ‘))βπ) β (Baseβπ
) β§ ((coe1β(π‘ππ))β(πΎ β π)) β (Baseβπ
)) β (((coe1β(πππ‘))βπ)(.rβπ
)((coe1β(π‘ππ))β(πΎ β π))) β (Baseβπ
)) |
131 | 107, 122,
129, 130 | syl3anc 1368 |
. . . . . 6
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ (π‘ β π β§ π β (0...πΎ))) β (((coe1β(πππ‘))βπ)(.rβπ
)((coe1β(π‘ππ))β(πΎ β π))) β (Baseβπ
)) |
132 | 30, 66, 36, 88, 131 | gsumcom3fi 19899 |
. . . . 5
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π
Ξ£g (π‘ β π β¦ (π
Ξ£g (π β (0...πΎ) β¦ (((coe1β(πππ‘))βπ)(.rβπ
)((coe1β(π‘ππ))β(πΎ β π))))))) = (π
Ξ£g (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ (((coe1β(πππ‘))βπ)(.rβπ
)((coe1β(π‘ππ))β(πΎ β π)))))))) |
133 | 10 | adantr 480 |
. . . . . . . . . . . . 13
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β π β π) |
134 | 133 | anim1i 614 |
. . . . . . . . . . . 12
β’
(((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π‘ β π) β (π β π β§ π‘ β π)) |
135 | 43, 14, 15 | decpmate 22623 |
. . . . . . . . . . . 12
β’ (((π
β Ring β§ π β π΅ β§ π β β0) β§ (π β π β§ π‘ β π)) β (π(π decompPMat π)π‘) = ((coe1β(πππ‘))βπ)) |
136 | 42, 134, 135 | syl2an2r 682 |
. . . . . . . . . . 11
β’
(((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π‘ β π) β (π(π decompPMat π)π‘) = ((coe1β(πππ‘))βπ)) |
137 | | simplrr 775 |
. . . . . . . . . . . . 13
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β π β π) |
138 | 137 | anim1ci 615 |
. . . . . . . . . . . 12
β’
(((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π‘ β π) β (π‘ β π β§ π β π)) |
139 | 43, 14, 15 | decpmate 22623 |
. . . . . . . . . . . 12
β’ (((π
β Ring β§ π β π΅ β§ (πΎ β π) β β0) β§ (π‘ β π β§ π β π)) β (π‘(π decompPMat (πΎ β π))π) = ((coe1β(π‘ππ))β(πΎ β π))) |
140 | 53, 138, 139 | syl2an2r 682 |
. . . . . . . . . . 11
β’
(((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π‘ β π) β (π‘(π decompPMat (πΎ β π))π) = ((coe1β(π‘ππ))β(πΎ β π))) |
141 | 136, 140 | oveq12d 7423 |
. . . . . . . . . 10
β’
(((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π‘ β π) β ((π(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π)) = (((coe1β(πππ‘))βπ)(.rβπ
)((coe1β(π‘ππ))β(πΎ β π)))) |
142 | 141 | eqcomd 2732 |
. . . . . . . . 9
β’
(((((π
β Ring
β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β§ π‘ β π) β (((coe1β(πππ‘))βπ)(.rβπ
)((coe1β(π‘ππ))β(πΎ β π))) = ((π(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π))) |
143 | 142 | mpteq2dva 5241 |
. . . . . . . 8
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β (π‘ β π β¦ (((coe1β(πππ‘))βπ)(.rβπ
)((coe1β(π‘ππ))β(πΎ β π)))) = (π‘ β π β¦ ((π(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π)))) |
144 | 143 | oveq2d 7421 |
. . . . . . 7
β’ ((((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β§ π β (0...πΎ)) β (π
Ξ£g (π‘ β π β¦ (((coe1β(πππ‘))βπ)(.rβπ
)((coe1β(π‘ππ))β(πΎ β π))))) = (π
Ξ£g (π‘ β π β¦ ((π(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π))))) |
145 | 144 | mpteq2dva 5241 |
. . . . . 6
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ (((coe1β(πππ‘))βπ)(.rβπ
)((coe1β(π‘ππ))β(πΎ β π)))))) = (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π)))))) |
146 | 145 | oveq2d 7421 |
. . . . 5
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π
Ξ£g (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ (((coe1β(πππ‘))βπ)(.rβπ
)((coe1β(π‘ππ))β(πΎ β π))))))) = (π
Ξ£g (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π))))))) |
147 | 106, 132,
146 | 3eqtrd 2770 |
. . . 4
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π((π(.rβπΆ)π) decompPMat πΎ)π) = (π
Ξ£g (π β (0...πΎ) β¦ (π
Ξ£g (π‘ β π β¦ ((π(π decompPMat π)π‘)(.rβπ
)(π‘(π decompPMat (πΎ β π))π))))))) |
148 | 13, 102, 147 | 3eqtr4rd 2777 |
. . 3
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ (π β π β§ π β π)) β (π((π(.rβπΆ)π) decompPMat πΎ)π) = (π(π΄ Ξ£g (π β (0...πΎ) β¦ ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π)))))π)) |
149 | 148 | ralrimivva 3194 |
. 2
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β
βπ β π βπ β π (π((π(.rβπΆ)π) decompPMat πΎ)π) = (π(π΄ Ξ£g (π β (0...πΎ) β¦ ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π)))))π)) |
150 | 43, 14 | pmatring 22549 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β πΆ β Ring) |
151 | 20, 150 | syl 17 |
. . . . . 6
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅)) β πΆ β Ring) |
152 | | simprl 768 |
. . . . . 6
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅)) β π β π΅) |
153 | | simprr 770 |
. . . . . 6
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅)) β π β π΅) |
154 | | eqid 2726 |
. . . . . . 7
β’
(.rβπΆ) = (.rβπΆ) |
155 | 15, 154 | ringcl 20155 |
. . . . . 6
β’ ((πΆ β Ring β§ π β π΅ β§ π β π΅) β (π(.rβπΆ)π) β π΅) |
156 | 151, 152,
153, 155 | syl3anc 1368 |
. . . . 5
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅)) β (π(.rβπΆ)π) β π΅) |
157 | 156 | 3adant3 1129 |
. . . 4
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β (π(.rβπΆ)π) β π΅) |
158 | 43, 14, 15, 22, 44 | decpmatcl 22624 |
. . . 4
β’ ((π
β Ring β§ (π(.rβπΆ)π) β π΅ β§ πΎ β β0) β ((π(.rβπΆ)π) decompPMat πΎ) β (Baseβπ΄)) |
159 | 157, 158 | syld3an2 1408 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β ((π(.rβπΆ)π) decompPMat πΎ) β (Baseβπ΄)) |
160 | 22 | matring 22300 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
161 | 21, 160 | syl 17 |
. . . . 5
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β π΄ β Ring) |
162 | | ringcmn 20181 |
. . . . 5
β’ (π΄ β Ring β π΄ β CMnd) |
163 | 161, 162 | syl 17 |
. . . 4
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β π΄ β CMnd) |
164 | | fzfid 13944 |
. . . 4
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β
(0...πΎ) β
Fin) |
165 | 161 | adantr 480 |
. . . . . 6
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ π β (0...πΎ)) β π΄ β Ring) |
166 | 32 | adantr 480 |
. . . . . . . 8
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ π β (0...πΎ)) β π
β Ring) |
167 | | simpl2l 1223 |
. . . . . . . 8
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ π β (0...πΎ)) β π β π΅) |
168 | 40 | adantl 481 |
. . . . . . . 8
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ π β (0...πΎ)) β π β β0) |
169 | 166, 167,
168 | 3jca 1125 |
. . . . . . 7
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ π β (0...πΎ)) β (π
β Ring β§ π β π΅ β§ π β
β0)) |
170 | 169, 45 | syl 17 |
. . . . . 6
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ π β (0...πΎ)) β (π decompPMat π) β (Baseβπ΄)) |
171 | | simpl2r 1224 |
. . . . . . . 8
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ π β (0...πΎ)) β π β π΅) |
172 | 51 | adantl 481 |
. . . . . . . 8
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ π β (0...πΎ)) β (πΎ β π) β
β0) |
173 | 166, 171,
172 | 3jca 1125 |
. . . . . . 7
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ π β (0...πΎ)) β (π
β Ring β§ π β π΅ β§ (πΎ β π) β
β0)) |
174 | 173, 54 | syl 17 |
. . . . . 6
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ π β (0...πΎ)) β (π decompPMat (πΎ β π)) β (Baseβπ΄)) |
175 | | eqid 2726 |
. . . . . . 7
β’
(.rβπ΄) = (.rβπ΄) |
176 | 44, 175 | ringcl 20155 |
. . . . . 6
β’ ((π΄ β Ring β§ (π decompPMat π) β (Baseβπ΄) β§ (π decompPMat (πΎ β π)) β (Baseβπ΄)) β ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π))) β (Baseβπ΄)) |
177 | 165, 170,
174, 176 | syl3anc 1368 |
. . . . 5
β’ (((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β§ π β (0...πΎ)) β ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π))) β (Baseβπ΄)) |
178 | 177 | ralrimiva 3140 |
. . . 4
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β
βπ β (0...πΎ)((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π))) β (Baseβπ΄)) |
179 | 44, 163, 164, 178 | gsummptcl 19887 |
. . 3
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β (π΄ Ξ£g
(π β (0...πΎ) β¦ ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π))))) β (Baseβπ΄)) |
180 | 22, 44 | eqmat 22281 |
. . 3
β’ ((((π(.rβπΆ)π) decompPMat πΎ) β (Baseβπ΄) β§ (π΄ Ξ£g (π β (0...πΎ) β¦ ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π))))) β (Baseβπ΄)) β (((π(.rβπΆ)π) decompPMat πΎ) = (π΄ Ξ£g (π β (0...πΎ) β¦ ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π))))) β βπ β π βπ β π (π((π(.rβπΆ)π) decompPMat πΎ)π) = (π(π΄ Ξ£g (π β (0...πΎ) β¦ ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π)))))π))) |
181 | 159, 179,
180 | syl2anc 583 |
. 2
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β (((π(.rβπΆ)π) decompPMat πΎ) = (π΄ Ξ£g (π β (0...πΎ) β¦ ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π))))) β βπ β π βπ β π (π((π(.rβπΆ)π) decompPMat πΎ)π) = (π(π΄ Ξ£g (π β (0...πΎ) β¦ ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π)))))π))) |
182 | 149, 181 | mpbird 257 |
1
β’ ((π
β Ring β§ (π β π΅ β§ π β π΅) β§ πΎ β β0) β ((π(.rβπΆ)π) decompPMat πΎ) = (π΄ Ξ£g (π β (0...πΎ) β¦ ((π decompPMat π)(.rβπ΄)(π decompPMat (πΎ β π)))))) |