Step | Hyp | Ref
| Expression |
1 | | dmatid.a |
. . . . . 6
β’ π΄ = (π Mat π
) |
2 | | eqid 2730 |
. . . . . 6
β’ (π
maMul β¨π, π, πβ©) = (π
maMul β¨π, π, πβ©) |
3 | 1, 2 | matmulr 22160 |
. . . . 5
β’ ((π β Fin β§ π
β Ring) β (π
maMul β¨π, π, πβ©) = (.rβπ΄)) |
4 | 3 | adantr 479 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β (π
maMul β¨π, π, πβ©) = (.rβπ΄)) |
5 | 4 | eqcomd 2736 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β (.rβπ΄) = (π
maMul β¨π, π, πβ©)) |
6 | 5 | oveqd 7428 |
. 2
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β (π(.rβπ΄)π) = (π(π
maMul β¨π, π, πβ©)π)) |
7 | | eqid 2730 |
. . 3
β’
(Baseβπ
) =
(Baseβπ
) |
8 | | eqid 2730 |
. . 3
β’
(.rβπ
) = (.rβπ
) |
9 | | simplr 765 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β π
β Ring) |
10 | | simpll 763 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β π β Fin) |
11 | | dmatid.b |
. . . . . . 7
β’ π΅ = (Baseβπ΄) |
12 | | dmatid.0 |
. . . . . . 7
β’ 0 =
(0gβπ
) |
13 | | dmatid.d |
. . . . . . 7
β’ π· = (π DMat π
) |
14 | 1, 11, 12, 13 | dmatmat 22216 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β (π β π· β π β π΅)) |
15 | 14 | imp 405 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ π β π·) β π β π΅) |
16 | 1, 7, 11 | matbas2i 22144 |
. . . . 5
β’ (π β π΅ β π β ((Baseβπ
) βm (π Γ π))) |
17 | 15, 16 | syl 17 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ π β π·) β π β ((Baseβπ
) βm (π Γ π))) |
18 | 17 | adantrr 713 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β π β ((Baseβπ
) βm (π Γ π))) |
19 | 1, 11, 12, 13 | dmatmat 22216 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β (π β π· β π β π΅)) |
20 | 19 | imp 405 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ π β π·) β π β π΅) |
21 | 1, 7, 11 | matbas2i 22144 |
. . . . 5
β’ (π β π΅ β π β ((Baseβπ
) βm (π Γ π))) |
22 | 20, 21 | syl 17 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ π β π·) β π β ((Baseβπ
) βm (π Γ π))) |
23 | 22 | adantrl 712 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β π β ((Baseβπ
) βm (π Γ π))) |
24 | 2, 7, 8, 9, 10, 10, 10, 18, 23 | mamuval 22108 |
. 2
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β (π(π
maMul β¨π, π, πβ©)π) = (π₯ β π, π¦ β π β¦ (π
Ξ£g (π β π β¦ ((π₯ππ)(.rβπ
)(πππ¦)))))) |
25 | | eqid 2730 |
. . . . . . 7
β’
(+gβπ
) = (+gβπ
) |
26 | | ringcmn 20170 |
. . . . . . . . . 10
β’ (π
β Ring β π
β CMnd) |
27 | 26 | ad2antlr 723 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β π
β CMnd) |
28 | 27 | 3ad2ant1 1131 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β π
β CMnd) |
29 | 28 | adantl 480 |
. . . . . . 7
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β π
β CMnd) |
30 | 10 | 3ad2ant1 1131 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β π β Fin) |
31 | 30 | adantl 480 |
. . . . . . 7
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β π β Fin) |
32 | | eqid 2730 |
. . . . . . . 8
β’ (π β π β¦ ((π₯ππ)(.rβπ
)(πππ¦))) = (π β π β¦ ((π₯ππ)(.rβπ
)(πππ¦))) |
33 | | ovexd 7446 |
. . . . . . . 8
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β ((π₯ππ)(.rβπ
)(πππ¦)) β V) |
34 | | fvexd 6905 |
. . . . . . . 8
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β (0gβπ
) β V) |
35 | 32, 31, 33, 34 | fsuppmptdm 9376 |
. . . . . . 7
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β (π β π β¦ ((π₯ππ)(.rβπ
)(πππ¦))) finSupp (0gβπ
)) |
36 | 9 | 3ad2ant1 1131 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β π
β Ring) |
37 | 36 | ad2antlr 723 |
. . . . . . . 8
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β π
β Ring) |
38 | | simp2 1135 |
. . . . . . . . . 10
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β π₯ β π) |
39 | 38 | ad2antlr 723 |
. . . . . . . . 9
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β π₯ β π) |
40 | | simpr 483 |
. . . . . . . . 9
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β π β π) |
41 | | eqid 2730 |
. . . . . . . . . . . . . 14
β’
(Baseβπ΄) =
(Baseβπ΄) |
42 | 1, 41, 12, 13 | dmatmat 22216 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π
β Ring) β (π β π· β π β (Baseβπ΄))) |
43 | 42 | imp 405 |
. . . . . . . . . . . 12
β’ (((π β Fin β§ π
β Ring) β§ π β π·) β π β (Baseβπ΄)) |
44 | 43 | adantrr 713 |
. . . . . . . . . . 11
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β π β (Baseβπ΄)) |
45 | 44 | 3ad2ant1 1131 |
. . . . . . . . . 10
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β π β (Baseβπ΄)) |
46 | 45 | ad2antlr 723 |
. . . . . . . . 9
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β π β (Baseβπ΄)) |
47 | 1, 7 | matecl 22147 |
. . . . . . . . 9
β’ ((π₯ β π β§ π β π β§ π β (Baseβπ΄)) β (π₯ππ) β (Baseβπ
)) |
48 | 39, 40, 46, 47 | syl3anc 1369 |
. . . . . . . 8
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β (π₯ππ) β (Baseβπ
)) |
49 | | simplr3 1215 |
. . . . . . . . 9
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β π¦ β π) |
50 | 1, 41, 12, 13 | dmatmat 22216 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π
β Ring) β (π β π· β π β (Baseβπ΄))) |
51 | 50 | imp 405 |
. . . . . . . . . . . 12
β’ (((π β Fin β§ π
β Ring) β§ π β π·) β π β (Baseβπ΄)) |
52 | 51 | adantrl 712 |
. . . . . . . . . . 11
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β π β (Baseβπ΄)) |
53 | 52 | 3ad2ant1 1131 |
. . . . . . . . . 10
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β π β (Baseβπ΄)) |
54 | 53 | ad2antlr 723 |
. . . . . . . . 9
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β π β (Baseβπ΄)) |
55 | 1, 7 | matecl 22147 |
. . . . . . . . 9
β’ ((π β π β§ π¦ β π β§ π β (Baseβπ΄)) β (πππ¦) β (Baseβπ
)) |
56 | 40, 49, 54, 55 | syl3anc 1369 |
. . . . . . . 8
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β (πππ¦) β (Baseβπ
)) |
57 | 7, 8 | ringcl 20144 |
. . . . . . . 8
β’ ((π
β Ring β§ (π₯ππ) β (Baseβπ
) β§ (πππ¦) β (Baseβπ
)) β ((π₯ππ)(.rβπ
)(πππ¦)) β (Baseβπ
)) |
58 | 37, 48, 56, 57 | syl3anc 1369 |
. . . . . . 7
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β ((π₯ππ)(.rβπ
)(πππ¦)) β (Baseβπ
)) |
59 | 38 | adantl 480 |
. . . . . . 7
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β π₯ β π) |
60 | | simp3 1136 |
. . . . . . . . . 10
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β π¦ β π) |
61 | 15 | adantrr 713 |
. . . . . . . . . . . 12
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β π β π΅) |
62 | 61, 11 | eleqtrdi 2841 |
. . . . . . . . . . 11
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β π β (Baseβπ΄)) |
63 | 62 | 3ad2ant1 1131 |
. . . . . . . . . 10
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β π β (Baseβπ΄)) |
64 | 1, 7 | matecl 22147 |
. . . . . . . . . 10
β’ ((π₯ β π β§ π¦ β π β§ π β (Baseβπ΄)) β (π₯ππ¦) β (Baseβπ
)) |
65 | 38, 60, 63, 64 | syl3anc 1369 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β (π₯ππ¦) β (Baseβπ
)) |
66 | 50 | a1d 25 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ π
β Ring) β (π β π· β (π β π· β π β (Baseβπ΄)))) |
67 | 66 | imp32 417 |
. . . . . . . . . . 11
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β π β (Baseβπ΄)) |
68 | 67 | 3ad2ant1 1131 |
. . . . . . . . . 10
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β π β (Baseβπ΄)) |
69 | 1, 7 | matecl 22147 |
. . . . . . . . . 10
β’ ((π₯ β π β§ π¦ β π β§ π β (Baseβπ΄)) β (π₯ππ¦) β (Baseβπ
)) |
70 | 38, 60, 68, 69 | syl3anc 1369 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β (π₯ππ¦) β (Baseβπ
)) |
71 | 7, 8 | ringcl 20144 |
. . . . . . . . 9
β’ ((π
β Ring β§ (π₯ππ¦) β (Baseβπ
) β§ (π₯ππ¦) β (Baseβπ
)) β ((π₯ππ¦)(.rβπ
)(π₯ππ¦)) β (Baseβπ
)) |
72 | 36, 65, 70, 71 | syl3anc 1369 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β ((π₯ππ¦)(.rβπ
)(π₯ππ¦)) β (Baseβπ
)) |
73 | 72 | adantl 480 |
. . . . . . 7
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β ((π₯ππ¦)(.rβπ
)(π₯ππ¦)) β (Baseβπ
)) |
74 | | eqtr 2753 |
. . . . . . . . . . 11
β’ ((π = π₯ β§ π₯ = π¦) β π = π¦) |
75 | 74 | ancoms 457 |
. . . . . . . . . 10
β’ ((π₯ = π¦ β§ π = π₯) β π = π¦) |
76 | 75 | oveq2d 7427 |
. . . . . . . . 9
β’ ((π₯ = π¦ β§ π = π₯) β (π₯ππ) = (π₯ππ¦)) |
77 | 76 | adantlr 711 |
. . . . . . . 8
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π = π₯) β (π₯ππ) = (π₯ππ¦)) |
78 | | oveq1 7418 |
. . . . . . . . 9
β’ (π = π₯ β (πππ¦) = (π₯ππ¦)) |
79 | 78 | adantl 480 |
. . . . . . . 8
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π = π₯) β (πππ¦) = (π₯ππ¦)) |
80 | 77, 79 | oveq12d 7429 |
. . . . . . 7
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π = π₯) β ((π₯ππ)(.rβπ
)(πππ¦)) = ((π₯ππ¦)(.rβπ
)(π₯ππ¦))) |
81 | 7, 25, 29, 31, 35, 58, 59, 73, 80 | gsumdifsnd 19870 |
. . . . . 6
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β (π
Ξ£g (π β π β¦ ((π₯ππ)(.rβπ
)(πππ¦)))) = ((π
Ξ£g (π β (π β {π₯}) β¦ ((π₯ππ)(.rβπ
)(πππ¦))))(+gβπ
)((π₯ππ¦)(.rβπ
)(π₯ππ¦)))) |
82 | | simprl 767 |
. . . . . . . . . . . . . . . 16
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β π β π·) |
83 | 10, 9, 82 | 3jca 1126 |
. . . . . . . . . . . . . . 15
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β (π β Fin β§ π
β Ring β§ π β π·)) |
84 | 83 | 3ad2ant1 1131 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β (π β Fin β§ π
β Ring β§ π β π·)) |
85 | 84 | ad2antlr 723 |
. . . . . . . . . . . . 13
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β (π β {π₯})) β (π β Fin β§ π
β Ring β§ π β π·)) |
86 | 38 | ad2antlr 723 |
. . . . . . . . . . . . 13
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β (π β {π₯})) β π₯ β π) |
87 | | eldifi 4125 |
. . . . . . . . . . . . . 14
β’ (π β (π β {π₯}) β π β π) |
88 | 87 | adantl 480 |
. . . . . . . . . . . . 13
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β (π β {π₯})) β π β π) |
89 | | eldifsni 4792 |
. . . . . . . . . . . . . . 15
β’ (π β (π β {π₯}) β π β π₯) |
90 | 89 | necomd 2994 |
. . . . . . . . . . . . . 14
β’ (π β (π β {π₯}) β π₯ β π) |
91 | 90 | adantl 480 |
. . . . . . . . . . . . 13
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β (π β {π₯})) β π₯ β π) |
92 | 1, 11, 12, 13 | dmatelnd 22218 |
. . . . . . . . . . . . 13
β’ (((π β Fin β§ π
β Ring β§ π β π·) β§ (π₯ β π β§ π β π β§ π₯ β π)) β (π₯ππ) = 0 ) |
93 | 85, 86, 88, 91, 92 | syl13anc 1370 |
. . . . . . . . . . . 12
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β (π β {π₯})) β (π₯ππ) = 0 ) |
94 | 93 | oveq1d 7426 |
. . . . . . . . . . 11
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β (π β {π₯})) β ((π₯ππ)(.rβπ
)(πππ¦)) = ( 0 (.rβπ
)(πππ¦))) |
95 | 36 | ad2antlr 723 |
. . . . . . . . . . . 12
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β (π β {π₯})) β π
β Ring) |
96 | | simplr3 1215 |
. . . . . . . . . . . . 13
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β (π β {π₯})) β π¦ β π) |
97 | 53 | ad2antlr 723 |
. . . . . . . . . . . . 13
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β (π β {π₯})) β π β (Baseβπ΄)) |
98 | 88, 96, 97, 55 | syl3anc 1369 |
. . . . . . . . . . . 12
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β (π β {π₯})) β (πππ¦) β (Baseβπ
)) |
99 | 7, 8, 12 | ringlz 20181 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ (πππ¦) β (Baseβπ
)) β ( 0 (.rβπ
)(πππ¦)) = 0 ) |
100 | 95, 98, 99 | syl2anc 582 |
. . . . . . . . . . 11
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β (π β {π₯})) β ( 0 (.rβπ
)(πππ¦)) = 0 ) |
101 | 94, 100 | eqtrd 2770 |
. . . . . . . . . 10
β’ (((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β (π β {π₯})) β ((π₯ππ)(.rβπ
)(πππ¦)) = 0 ) |
102 | 101 | mpteq2dva 5247 |
. . . . . . . . 9
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β (π β (π β {π₯}) β¦ ((π₯ππ)(.rβπ
)(πππ¦))) = (π β (π β {π₯}) β¦ 0 )) |
103 | 102 | oveq2d 7427 |
. . . . . . . 8
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β (π
Ξ£g (π β (π β {π₯}) β¦ ((π₯ππ)(.rβπ
)(πππ¦)))) = (π
Ξ£g (π β (π β {π₯}) β¦ 0 ))) |
104 | | diffi 9181 |
. . . . . . . . . . . . 13
β’ (π β Fin β (π β {π₯}) β Fin) |
105 | | ringmnd 20137 |
. . . . . . . . . . . . 13
β’ (π
β Ring β π
β Mnd) |
106 | 104, 105 | anim12ci 612 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ π
β Ring) β (π
β Mnd β§ (π β {π₯}) β Fin)) |
107 | 106 | adantr 479 |
. . . . . . . . . . 11
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β (π
β Mnd β§ (π β {π₯}) β Fin)) |
108 | 107 | 3ad2ant1 1131 |
. . . . . . . . . 10
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β (π
β Mnd β§ (π β {π₯}) β Fin)) |
109 | 108 | adantl 480 |
. . . . . . . . 9
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β (π
β Mnd β§ (π β {π₯}) β Fin)) |
110 | 12 | gsumz 18753 |
. . . . . . . . 9
β’ ((π
β Mnd β§ (π β {π₯}) β Fin) β (π
Ξ£g (π β (π β {π₯}) β¦ 0 )) = 0 ) |
111 | 109, 110 | syl 17 |
. . . . . . . 8
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β (π
Ξ£g (π β (π β {π₯}) β¦ 0 )) = 0 ) |
112 | 103, 111 | eqtrd 2770 |
. . . . . . 7
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β (π
Ξ£g (π β (π β {π₯}) β¦ ((π₯ππ)(.rβπ
)(πππ¦)))) = 0 ) |
113 | 112 | oveq1d 7426 |
. . . . . 6
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β ((π
Ξ£g (π β (π β {π₯}) β¦ ((π₯ππ)(.rβπ
)(πππ¦))))(+gβπ
)((π₯ππ¦)(.rβπ
)(π₯ππ¦))) = ( 0 (+gβπ
)((π₯ππ¦)(.rβπ
)(π₯ππ¦)))) |
114 | 105 | ad2antlr 723 |
. . . . . . . . . 10
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β π
β Mnd) |
115 | 114 | 3ad2ant1 1131 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β π
β Mnd) |
116 | 38, 60, 53, 69 | syl3anc 1369 |
. . . . . . . . . 10
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β (π₯ππ¦) β (Baseβπ
)) |
117 | 36, 65, 116, 71 | syl3anc 1369 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β ((π₯ππ¦)(.rβπ
)(π₯ππ¦)) β (Baseβπ
)) |
118 | 115, 117 | jca 510 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β (π
β Mnd β§ ((π₯ππ¦)(.rβπ
)(π₯ππ¦)) β (Baseβπ
))) |
119 | 118 | adantl 480 |
. . . . . . 7
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β (π
β Mnd β§ ((π₯ππ¦)(.rβπ
)(π₯ππ¦)) β (Baseβπ
))) |
120 | 7, 25, 12 | mndlid 18679 |
. . . . . . 7
β’ ((π
β Mnd β§ ((π₯ππ¦)(.rβπ
)(π₯ππ¦)) β (Baseβπ
)) β ( 0 (+gβπ
)((π₯ππ¦)(.rβπ
)(π₯ππ¦))) = ((π₯ππ¦)(.rβπ
)(π₯ππ¦))) |
121 | 119, 120 | syl 17 |
. . . . . 6
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β ( 0 (+gβπ
)((π₯ππ¦)(.rβπ
)(π₯ππ¦))) = ((π₯ππ¦)(.rβπ
)(π₯ππ¦))) |
122 | 81, 113, 121 | 3eqtrd 2774 |
. . . . 5
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β (π
Ξ£g (π β π β¦ ((π₯ππ)(.rβπ
)(πππ¦)))) = ((π₯ππ¦)(.rβπ
)(π₯ππ¦))) |
123 | | iftrue 4533 |
. . . . . 6
β’ (π₯ = π¦ β if(π₯ = π¦, ((π₯ππ¦)(.rβπ
)(π₯ππ¦)), 0 ) = ((π₯ππ¦)(.rβπ
)(π₯ππ¦))) |
124 | 123 | adantr 479 |
. . . . 5
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β if(π₯ = π¦, ((π₯ππ¦)(.rβπ
)(π₯ππ¦)), 0 ) = ((π₯ππ¦)(.rβπ
)(π₯ππ¦))) |
125 | 122, 124 | eqtr4d 2773 |
. . . 4
β’ ((π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β (π
Ξ£g (π β π β¦ ((π₯ππ)(.rβπ
)(πππ¦)))) = if(π₯ = π¦, ((π₯ππ¦)(.rβπ
)(π₯ππ¦)), 0 )) |
126 | | simprr 769 |
. . . . . . . . . . . . . . 15
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β π β π·) |
127 | 10, 9, 126 | 3jca 1126 |
. . . . . . . . . . . . . 14
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β (π β Fin β§ π
β Ring β§ π β π·)) |
128 | 127 | 3ad2ant1 1131 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β (π β Fin β§ π
β Ring β§ π β π·)) |
129 | 128 | ad2antlr 723 |
. . . . . . . . . . . 12
β’ (((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β (π β Fin β§ π
β Ring β§ π β π·)) |
130 | 129 | adantl 480 |
. . . . . . . . . . 11
β’ ((π₯ = π β§ ((Β¬ π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π)) β (π β Fin β§ π
β Ring β§ π β π·)) |
131 | | simprr 769 |
. . . . . . . . . . 11
β’ ((π₯ = π β§ ((Β¬ π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π)) β π β π) |
132 | | simplr3 1215 |
. . . . . . . . . . . 12
β’ (((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β π¦ β π) |
133 | 132 | adantl 480 |
. . . . . . . . . . 11
β’ ((π₯ = π β§ ((Β¬ π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π)) β π¦ β π) |
134 | | df-ne 2939 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π¦ β Β¬ π₯ = π¦) |
135 | | neeq1 3001 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (π₯ β π¦ β π β π¦)) |
136 | 135 | biimpcd 248 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π¦ β (π₯ = π β π β π¦)) |
137 | 134, 136 | sylbir 234 |
. . . . . . . . . . . . . 14
β’ (Β¬
π₯ = π¦ β (π₯ = π β π β π¦)) |
138 | 137 | adantr 479 |
. . . . . . . . . . . . 13
β’ ((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β (π₯ = π β π β π¦)) |
139 | 138 | adantr 479 |
. . . . . . . . . . . 12
β’ (((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β (π₯ = π β π β π¦)) |
140 | 139 | impcom 406 |
. . . . . . . . . . 11
β’ ((π₯ = π β§ ((Β¬ π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π)) β π β π¦) |
141 | 1, 11, 12, 13 | dmatelnd 22218 |
. . . . . . . . . . 11
β’ (((π β Fin β§ π
β Ring β§ π β π·) β§ (π β π β§ π¦ β π β§ π β π¦)) β (πππ¦) = 0 ) |
142 | 130, 131,
133, 140, 141 | syl13anc 1370 |
. . . . . . . . . 10
β’ ((π₯ = π β§ ((Β¬ π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π)) β (πππ¦) = 0 ) |
143 | 142 | oveq2d 7427 |
. . . . . . . . 9
β’ ((π₯ = π β§ ((Β¬ π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π)) β ((π₯ππ)(.rβπ
)(πππ¦)) = ((π₯ππ)(.rβπ
) 0 )) |
144 | 36 | ad2antlr 723 |
. . . . . . . . . . 11
β’ (((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β π
β Ring) |
145 | 38 | ad2antlr 723 |
. . . . . . . . . . . 12
β’ (((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β π₯ β π) |
146 | | simpr 483 |
. . . . . . . . . . . 12
β’ (((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β π β π) |
147 | 63 | ad2antlr 723 |
. . . . . . . . . . . 12
β’ (((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β π β (Baseβπ΄)) |
148 | 145, 146,
147, 47 | syl3anc 1369 |
. . . . . . . . . . 11
β’ (((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β (π₯ππ) β (Baseβπ
)) |
149 | 7, 8, 12 | ringrz 20182 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ (π₯ππ) β (Baseβπ
)) β ((π₯ππ)(.rβπ
) 0 ) = 0 ) |
150 | 144, 148,
149 | syl2anc 582 |
. . . . . . . . . 10
β’ (((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β ((π₯ππ)(.rβπ
) 0 ) = 0 ) |
151 | 150 | adantl 480 |
. . . . . . . . 9
β’ ((π₯ = π β§ ((Β¬ π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π)) β ((π₯ππ)(.rβπ
) 0 ) = 0 ) |
152 | 143, 151 | eqtrd 2770 |
. . . . . . . 8
β’ ((π₯ = π β§ ((Β¬ π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π)) β ((π₯ππ)(.rβπ
)(πππ¦)) = 0 ) |
153 | 84 | ad2antlr 723 |
. . . . . . . . . . . 12
β’ (((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β (π β Fin β§ π
β Ring β§ π β π·)) |
154 | 153 | adantl 480 |
. . . . . . . . . . 11
β’ ((Β¬
π₯ = π β§ ((Β¬ π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π)) β (π β Fin β§ π
β Ring β§ π β π·)) |
155 | 145 | adantl 480 |
. . . . . . . . . . 11
β’ ((Β¬
π₯ = π β§ ((Β¬ π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π)) β π₯ β π) |
156 | | simprr 769 |
. . . . . . . . . . 11
β’ ((Β¬
π₯ = π β§ ((Β¬ π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π)) β π β π) |
157 | | neqne 2946 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ = π β π₯ β π) |
158 | 157 | adantr 479 |
. . . . . . . . . . 11
β’ ((Β¬
π₯ = π β§ ((Β¬ π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π)) β π₯ β π) |
159 | 154, 155,
156, 158, 92 | syl13anc 1370 |
. . . . . . . . . 10
β’ ((Β¬
π₯ = π β§ ((Β¬ π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π)) β (π₯ππ) = 0 ) |
160 | 159 | oveq1d 7426 |
. . . . . . . . 9
β’ ((Β¬
π₯ = π β§ ((Β¬ π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π)) β ((π₯ππ)(.rβπ
)(πππ¦)) = ( 0 (.rβπ
)(πππ¦))) |
161 | 68 | ad2antlr 723 |
. . . . . . . . . . . 12
β’ (((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β π β (Baseβπ΄)) |
162 | 146, 132,
161, 55 | syl3anc 1369 |
. . . . . . . . . . 11
β’ (((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β (πππ¦) β (Baseβπ
)) |
163 | 144, 162,
99 | syl2anc 582 |
. . . . . . . . . 10
β’ (((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β ( 0 (.rβπ
)(πππ¦)) = 0 ) |
164 | 163 | adantl 480 |
. . . . . . . . 9
β’ ((Β¬
π₯ = π β§ ((Β¬ π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π)) β ( 0 (.rβπ
)(πππ¦)) = 0 ) |
165 | 160, 164 | eqtrd 2770 |
. . . . . . . 8
β’ ((Β¬
π₯ = π β§ ((Β¬ π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π)) β ((π₯ππ)(.rβπ
)(πππ¦)) = 0 ) |
166 | 152, 165 | pm2.61ian 808 |
. . . . . . 7
β’ (((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β§ π β π) β ((π₯ππ)(.rβπ
)(πππ¦)) = 0 ) |
167 | 166 | mpteq2dva 5247 |
. . . . . 6
β’ ((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β (π β π β¦ ((π₯ππ)(.rβπ
)(πππ¦))) = (π β π β¦ 0 )) |
168 | 167 | oveq2d 7427 |
. . . . 5
β’ ((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β (π
Ξ£g (π β π β¦ ((π₯ππ)(.rβπ
)(πππ¦)))) = (π
Ξ£g (π β π β¦ 0 ))) |
169 | 105 | anim2i 615 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β Ring) β (π β Fin β§ π
β Mnd)) |
170 | 169 | ancomd 460 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring) β (π
β Mnd β§ π β Fin)) |
171 | 12 | gsumz 18753 |
. . . . . . . . 9
β’ ((π
β Mnd β§ π β Fin) β (π
Ξ£g
(π β π β¦ 0 )) = 0 ) |
172 | 170, 171 | syl 17 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring) β (π
Ξ£g
(π β π β¦ 0 )) = 0 ) |
173 | 172 | adantr 479 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β (π
Ξ£g (π β π β¦ 0 )) = 0 ) |
174 | 173 | 3ad2ant1 1131 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β (π
Ξ£g (π β π β¦ 0 )) = 0 ) |
175 | 174 | adantl 480 |
. . . . 5
β’ ((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β (π
Ξ£g (π β π β¦ 0 )) = 0 ) |
176 | | iffalse 4536 |
. . . . . . 7
β’ (Β¬
π₯ = π¦ β if(π₯ = π¦, ((π₯ππ¦)(.rβπ
)(π₯ππ¦)), 0 ) = 0 ) |
177 | 176 | eqcomd 2736 |
. . . . . 6
β’ (Β¬
π₯ = π¦ β 0 = if(π₯ = π¦, ((π₯ππ¦)(.rβπ
)(π₯ππ¦)), 0 )) |
178 | 177 | adantr 479 |
. . . . 5
β’ ((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β 0 = if(π₯ = π¦, ((π₯ππ¦)(.rβπ
)(π₯ππ¦)), 0 )) |
179 | 168, 175,
178 | 3eqtrd 2774 |
. . . 4
β’ ((Β¬
π₯ = π¦ β§ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π)) β (π
Ξ£g (π β π β¦ ((π₯ππ)(.rβπ
)(πππ¦)))) = if(π₯ = π¦, ((π₯ππ¦)(.rβπ
)(π₯ππ¦)), 0 )) |
180 | 125, 179 | pm2.61ian 808 |
. . 3
β’ ((((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β§ π₯ β π β§ π¦ β π) β (π
Ξ£g (π β π β¦ ((π₯ππ)(.rβπ
)(πππ¦)))) = if(π₯ = π¦, ((π₯ππ¦)(.rβπ
)(π₯ππ¦)), 0 )) |
181 | 180 | mpoeq3dva 7488 |
. 2
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β (π₯ β π, π¦ β π β¦ (π
Ξ£g (π β π β¦ ((π₯ππ)(.rβπ
)(πππ¦))))) = (π₯ β π, π¦ β π β¦ if(π₯ = π¦, ((π₯ππ¦)(.rβπ
)(π₯ππ¦)), 0 ))) |
182 | 6, 24, 181 | 3eqtrd 2774 |
1
β’ (((π β Fin β§ π
β Ring) β§ (π β π· β§ π β π·)) β (π(.rβπ΄)π) = (π₯ β π, π¦ β π β¦ if(π₯ = π¦, ((π₯ππ¦)(.rβπ
)(π₯ππ¦)), 0 ))) |