Step | Hyp | Ref
| Expression |
1 | | monmat2matmon.b |
. . 3
β’ π΅ = (BaseβπΆ) |
2 | | eqid 2733 |
. . 3
β’
(0gβπΆ) = (0gβπΆ) |
3 | | crngring 19981 |
. . . . . 6
β’ (π
β CRing β π
β Ring) |
4 | 3 | anim2i 618 |
. . . . 5
β’ ((π β Fin β§ π
β CRing) β (π β Fin β§ π
β Ring)) |
5 | | monmat2matmon.p |
. . . . . 6
β’ π = (Poly1βπ
) |
6 | | monmat2matmon.c |
. . . . . 6
β’ πΆ = (π Mat π) |
7 | 5, 6 | pmatring 22057 |
. . . . 5
β’ ((π β Fin β§ π
β Ring) β πΆ β Ring) |
8 | | ringcmn 20008 |
. . . . 5
β’ (πΆ β Ring β πΆ β CMnd) |
9 | 4, 7, 8 | 3syl 18 |
. . . 4
β’ ((π β Fin β§ π
β CRing) β πΆ β CMnd) |
10 | 9 | adantr 482 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β πΆ β
CMnd) |
11 | | monmat2matmon.a |
. . . . . . 7
β’ π΄ = (π Mat π
) |
12 | 11 | matring 21808 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
13 | 3, 12 | sylan2 594 |
. . . . 5
β’ ((π β Fin β§ π
β CRing) β π΄ β Ring) |
14 | | monmat2matmon.q |
. . . . . 6
β’ π = (Poly1βπ΄) |
15 | 14 | ply1ring 21635 |
. . . . 5
β’ (π΄ β Ring β π β Ring) |
16 | | ringmnd 19979 |
. . . . 5
β’ (π β Ring β π β Mnd) |
17 | 13, 15, 16 | 3syl 18 |
. . . 4
β’ ((π β Fin β§ π
β CRing) β π β Mnd) |
18 | 17 | adantr 482 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β π β
Mnd) |
19 | | nn0ex 12424 |
. . . 4
β’
β0 β V |
20 | 19 | a1i 11 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β β0 β V) |
21 | | monmat2matmon.m1 |
. . . . . . 7
β’ β = (
Β·π βπ) |
22 | | monmat2matmon.e1 |
. . . . . . 7
β’ β =
(.gβ(mulGrpβπ)) |
23 | | monmat2matmon.x |
. . . . . . 7
β’ π = (var1βπ΄) |
24 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
25 | | monmat2matmon.i |
. . . . . . 7
β’ πΌ = (π pMatToMatPoly π
) |
26 | 5, 6, 1, 21, 22, 23, 11, 14, 24, 25 | pm2mpghm 22181 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β πΌ β (πΆ GrpHom π)) |
27 | 3, 26 | sylan2 594 |
. . . . 5
β’ ((π β Fin β§ π
β CRing) β πΌ β (πΆ GrpHom π)) |
28 | 27 | adantr 482 |
. . . 4
β’ (((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β πΌ β (πΆ GrpHom π)) |
29 | | ghmmhm 19023 |
. . . 4
β’ (πΌ β (πΆ GrpHom π) β πΌ β (πΆ MndHom π)) |
30 | 28, 29 | syl 17 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β πΌ β (πΆ MndHom π)) |
31 | 4 | adantr 482 |
. . . . 5
β’ (((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β (π β Fin β§
π
β
Ring)) |
32 | 31 | adantr 482 |
. . . 4
β’ ((((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β§ π β
β0) β (π β Fin β§ π
β Ring)) |
33 | | elmapi 8790 |
. . . . . . 7
β’ (π β (πΎ βm β0)
β π:β0βΆπΎ) |
34 | 33 | adantr 482 |
. . . . . 6
β’ ((π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄))
β π:β0βΆπΎ) |
35 | 34 | adantl 483 |
. . . . 5
β’ (((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β π:β0βΆπΎ) |
36 | 35 | ffvelcdmda 7036 |
. . . 4
β’ ((((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β§ π β
β0) β (πβπ) β πΎ) |
37 | | simpr 486 |
. . . 4
β’ ((((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β§ π β
β0) β π β β0) |
38 | | monmat2matmon.k |
. . . . 5
β’ πΎ = (Baseβπ΄) |
39 | | monmat2matmon.t |
. . . . 5
β’ π = (π matToPolyMat π
) |
40 | | monmat2matmon.m2 |
. . . . 5
β’ Β· = (
Β·π βπΆ) |
41 | | monmat2matmon.e2 |
. . . . 5
β’ πΈ =
(.gβ(mulGrpβπ)) |
42 | | monmat2matmon.y |
. . . . 5
β’ π = (var1βπ
) |
43 | 11, 38, 39, 5, 6, 1,
40, 41, 42 | mat2pmatscmxcl 22105 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ ((πβπ) β πΎ β§ π β β0)) β ((ππΈπ) Β· (πβ(πβπ))) β π΅) |
44 | 32, 36, 37, 43 | syl12anc 836 |
. . 3
β’ ((((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β§ π β
β0) β ((ππΈπ) Β· (πβ(πβπ))) β π΅) |
45 | | fvexd 6858 |
. . . 4
β’ (((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β (0gβπΆ) β V) |
46 | | ovexd 7393 |
. . . 4
β’ ((((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β§ π β
β0) β ((ππΈπ) Β· (πβ(πβπ))) β V) |
47 | | simpr 486 |
. . . . . . 7
β’ (((π β Fin β§ π
β CRing) β§ π β (πΎ βm β0))
β π β (πΎ βm
β0)) |
48 | | fvex 6856 |
. . . . . . 7
β’
(0gβπ΄) β V |
49 | | fsuppmapnn0ub 13906 |
. . . . . . 7
β’ ((π β (πΎ βm β0)
β§ (0gβπ΄) β V) β (π finSupp (0gβπ΄) β βπ¦ β β0
βπ₯ β
β0 (π¦ <
π₯ β (πβπ₯) = (0gβπ΄)))) |
50 | 47, 48, 49 | sylancl 587 |
. . . . . 6
β’ (((π β Fin β§ π
β CRing) β§ π β (πΎ βm β0))
β (π finSupp
(0gβπ΄)
β βπ¦ β
β0 βπ₯ β β0 (π¦ < π₯ β (πβπ₯) = (0gβπ΄)))) |
51 | | csbov12g 7402 |
. . . . . . . . . . . . . 14
β’ (π₯ β β0
β β¦π₯ /
πβ¦((ππΈπ) Β· (πβ(πβπ))) = (β¦π₯ / πβ¦(ππΈπ) Β·
β¦π₯ / πβ¦(πβ(πβπ)))) |
52 | | csbov1g 7403 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β0
β β¦π₯ /
πβ¦(ππΈπ) = (β¦π₯ / πβ¦ππΈπ)) |
53 | | csbvarg 4392 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β0
β β¦π₯ /
πβ¦π = π₯) |
54 | 53 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β0
β (β¦π₯ /
πβ¦ππΈπ) = (π₯πΈπ)) |
55 | 52, 54 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β0
β β¦π₯ /
πβ¦(ππΈπ) = (π₯πΈπ)) |
56 | | csbfv2g 6892 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β0
β β¦π₯ /
πβ¦(πβ(πβπ)) = (πββ¦π₯ / πβ¦(πβπ))) |
57 | | csbfv2g 6892 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β0
β β¦π₯ /
πβ¦(πβπ) = (πββ¦π₯ / πβ¦π)) |
58 | 53 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β0
β (πββ¦π₯ / πβ¦π) = (πβπ₯)) |
59 | 57, 58 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β0
β β¦π₯ /
πβ¦(πβπ) = (πβπ₯)) |
60 | 59 | fveq2d 6847 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β0
β (πββ¦π₯ / πβ¦(πβπ)) = (πβ(πβπ₯))) |
61 | 56, 60 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β0
β β¦π₯ /
πβ¦(πβ(πβπ)) = (πβ(πβπ₯))) |
62 | 55, 61 | oveq12d 7376 |
. . . . . . . . . . . . . 14
β’ (π₯ β β0
β (β¦π₯ /
πβ¦(ππΈπ) Β·
β¦π₯ / πβ¦(πβ(πβπ))) = ((π₯πΈπ) Β· (πβ(πβπ₯)))) |
63 | 51, 62 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (π₯ β β0
β β¦π₯ /
πβ¦((ππΈπ) Β· (πβ(πβπ))) = ((π₯πΈπ) Β· (πβ(πβπ₯)))) |
64 | 63 | adantl 483 |
. . . . . . . . . . . 12
β’
(((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β
β¦π₯ / πβ¦((ππΈπ) Β· (πβ(πβπ))) = ((π₯πΈπ) Β· (πβ(πβπ₯)))) |
65 | 64 | adantr 482 |
. . . . . . . . . . 11
β’
((((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β§ (πβπ₯) = (0gβπ΄)) β β¦π₯ / πβ¦((ππΈπ) Β· (πβ(πβπ))) = ((π₯πΈπ) Β· (πβ(πβπ₯)))) |
66 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ ((πβπ₯) = (0gβπ΄) β (πβ(πβπ₯)) = (πβ(0gβπ΄))) |
67 | 66 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ ((πβπ₯) = (0gβπ΄) β ((π₯πΈπ) Β· (πβ(πβπ₯))) = ((π₯πΈπ) Β· (πβ(0gβπ΄)))) |
68 | 39, 11, 38, 5, 6, 1 | mat2pmatghm 22095 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Fin β§ π
β Ring) β π β (π΄ GrpHom πΆ)) |
69 | 3, 68 | sylan2 594 |
. . . . . . . . . . . . . . . 16
β’ ((π β Fin β§ π
β CRing) β π β (π΄ GrpHom πΆ)) |
70 | 69 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’
(((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β π β (π΄ GrpHom πΆ)) |
71 | | ghmmhm 19023 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄ GrpHom πΆ) β π β (π΄ MndHom πΆ)) |
72 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(0gβπ΄) = (0gβπ΄) |
73 | 72, 2 | mhm0 18615 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄ MndHom πΆ) β (πβ(0gβπ΄)) = (0gβπΆ)) |
74 | 70, 71, 73 | 3syl 18 |
. . . . . . . . . . . . . 14
β’
(((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β (πβ(0gβπ΄)) = (0gβπΆ)) |
75 | 74 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’
(((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β ((π₯πΈπ) Β· (πβ(0gβπ΄))) = ((π₯πΈπ) Β·
(0gβπΆ))) |
76 | 5 | ply1ring 21635 |
. . . . . . . . . . . . . . . . 17
β’ (π
β Ring β π β Ring) |
77 | 3, 76 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π
β CRing β π β Ring) |
78 | 6 | matlmod 21794 |
. . . . . . . . . . . . . . . 16
β’ ((π β Fin β§ π β Ring) β πΆ β LMod) |
79 | 77, 78 | sylan2 594 |
. . . . . . . . . . . . . . 15
β’ ((π β Fin β§ π
β CRing) β πΆ β LMod) |
80 | 79 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’
(((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β πΆ β LMod) |
81 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(mulGrpβπ) =
(mulGrpβπ) |
82 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(Baseβπ) =
(Baseβπ) |
83 | 81, 82 | mgpbas 19907 |
. . . . . . . . . . . . . . . 16
β’
(Baseβπ) =
(Baseβ(mulGrpβπ)) |
84 | 77 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Fin β§ π
β CRing) β π β Ring) |
85 | 81 | ringmgp 19975 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Ring β
(mulGrpβπ) β
Mnd) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Fin β§ π
β CRing) β
(mulGrpβπ) β
Mnd) |
87 | 86 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’
(((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β
(mulGrpβπ) β
Mnd) |
88 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
(((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β π₯ β
β0) |
89 | 3 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Fin β§ π
β CRing) β π
β Ring) |
90 | 42, 5, 82 | vr1cl 21604 |
. . . . . . . . . . . . . . . . . 18
β’ (π
β Ring β π β (Baseβπ)) |
91 | 89, 90 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Fin β§ π
β CRing) β π β (Baseβπ)) |
92 | 91 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’
(((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β π β (Baseβπ)) |
93 | 83, 41, 87, 88, 92 | mulgnn0cld 18902 |
. . . . . . . . . . . . . . 15
β’
(((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β (π₯πΈπ) β (Baseβπ)) |
94 | 5 | ply1crng 21585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π
β CRing β π β CRing) |
95 | 6 | matsca2 21785 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Fin β§ π β CRing) β π = (ScalarβπΆ)) |
96 | 94, 95 | sylan2 594 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Fin β§ π
β CRing) β π = (ScalarβπΆ)) |
97 | 96 | eqcomd 2739 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Fin β§ π
β CRing) β
(ScalarβπΆ) = π) |
98 | 97 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’
(((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β
(ScalarβπΆ) = π) |
99 | 98 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’
(((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β
(Baseβ(ScalarβπΆ)) = (Baseβπ)) |
100 | 93, 99 | eleqtrrd 2837 |
. . . . . . . . . . . . . 14
β’
(((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β (π₯πΈπ) β (Baseβ(ScalarβπΆ))) |
101 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(ScalarβπΆ) =
(ScalarβπΆ) |
102 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(Baseβ(ScalarβπΆ)) = (Baseβ(ScalarβπΆ)) |
103 | 101, 40, 102, 2 | lmodvs0 20371 |
. . . . . . . . . . . . . 14
β’ ((πΆ β LMod β§ (π₯πΈπ) β (Baseβ(ScalarβπΆ))) β ((π₯πΈπ) Β·
(0gβπΆ)) =
(0gβπΆ)) |
104 | 80, 100, 103 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
(((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β ((π₯πΈπ) Β·
(0gβπΆ)) =
(0gβπΆ)) |
105 | 75, 104 | eqtrd 2773 |
. . . . . . . . . . . 12
β’
(((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β ((π₯πΈπ) Β· (πβ(0gβπ΄))) = (0gβπΆ)) |
106 | 67, 105 | sylan9eqr 2795 |
. . . . . . . . . . 11
β’
((((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β§ (πβπ₯) = (0gβπ΄)) β ((π₯πΈπ) Β· (πβ(πβπ₯))) = (0gβπΆ)) |
107 | 65, 106 | eqtrd 2773 |
. . . . . . . . . 10
β’
((((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β§ (πβπ₯) = (0gβπ΄)) β β¦π₯ / πβ¦((ππΈπ) Β· (πβ(πβπ))) = (0gβπΆ)) |
108 | 107 | ex 414 |
. . . . . . . . 9
β’
(((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β ((πβπ₯) = (0gβπ΄) β β¦π₯ / πβ¦((ππΈπ) Β· (πβ(πβπ))) = (0gβπΆ))) |
109 | 108 | imim2d 57 |
. . . . . . . 8
β’
(((((π β Fin
β§ π
β CRing) β§
π β (πΎ βm β0))
β§ π¦ β
β0) β§ π₯ β β0) β ((π¦ < π₯ β (πβπ₯) = (0gβπ΄)) β (π¦ < π₯ β β¦π₯ / πβ¦((ππΈπ) Β· (πβ(πβπ))) = (0gβπΆ)))) |
110 | 109 | ralimdva 3161 |
. . . . . . 7
β’ ((((π β Fin β§ π
β CRing) β§ π β (πΎ βm β0))
β§ π¦ β
β0) β (βπ₯ β β0 (π¦ < π₯ β (πβπ₯) = (0gβπ΄)) β βπ₯ β β0 (π¦ < π₯ β β¦π₯ / πβ¦((ππΈπ) Β· (πβ(πβπ))) = (0gβπΆ)))) |
111 | 110 | reximdva 3162 |
. . . . . 6
β’ (((π β Fin β§ π
β CRing) β§ π β (πΎ βm β0))
β (βπ¦ β
β0 βπ₯ β β0 (π¦ < π₯ β (πβπ₯) = (0gβπ΄)) β βπ¦ β β0 βπ₯ β β0
(π¦ < π₯ β β¦π₯ / πβ¦((ππΈπ) Β· (πβ(πβπ))) = (0gβπΆ)))) |
112 | 50, 111 | syld 47 |
. . . . 5
β’ (((π β Fin β§ π
β CRing) β§ π β (πΎ βm β0))
β (π finSupp
(0gβπ΄)
β βπ¦ β
β0 βπ₯ β β0 (π¦ < π₯ β β¦π₯ / πβ¦((ππΈπ) Β· (πβ(πβπ))) = (0gβπΆ)))) |
113 | 112 | impr 456 |
. . . 4
β’ (((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β βπ¦ β
β0 βπ₯ β β0 (π¦ < π₯ β β¦π₯ / πβ¦((ππΈπ) Β· (πβ(πβπ))) = (0gβπΆ))) |
114 | 45, 46, 113 | mptnn0fsupp 13908 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β (π β
β0 β¦ ((ππΈπ) Β· (πβ(πβπ)))) finSupp (0gβπΆ)) |
115 | 1, 2, 10, 18, 20, 30, 44, 114 | gsummptmhm 19722 |
. 2
β’ (((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β (π
Ξ£g (π β β0 β¦ (πΌβ((ππΈπ) Β· (πβ(πβπ)))))) = (πΌβ(πΆ Ξ£g (π β β0
β¦ ((ππΈπ) Β· (πβ(πβπ))))))) |
116 | | simpll 766 |
. . . . 5
β’ ((((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β§ π β
β0) β (π β Fin β§ π
β CRing)) |
117 | 5, 6, 1, 21, 22, 23, 11, 38, 14, 25, 41, 42, 40, 39 | monmat2matmon 22189 |
. . . . 5
β’ (((π β Fin β§ π
β CRing) β§ ((πβπ) β πΎ β§ π β β0)) β (πΌβ((ππΈπ) Β· (πβ(πβπ)))) = ((πβπ) β (π β π))) |
118 | 116, 36, 37, 117 | syl12anc 836 |
. . . 4
β’ ((((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β§ π β
β0) β (πΌβ((ππΈπ) Β· (πβ(πβπ)))) = ((πβπ) β (π β π))) |
119 | 118 | mpteq2dva 5206 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β (π β
β0 β¦ (πΌβ((ππΈπ) Β· (πβ(πβπ))))) = (π β β0 β¦ ((πβπ) β (π β π)))) |
120 | 119 | oveq2d 7374 |
. 2
β’ (((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β (π
Ξ£g (π β β0 β¦ (πΌβ((ππΈπ) Β· (πβ(πβπ)))))) = (π Ξ£g (π β β0
β¦ ((πβπ) β (π β π))))) |
121 | 115, 120 | eqtr3d 2775 |
1
β’ (((π β Fin β§ π
β CRing) β§ (π β (πΎ βm β0)
β§ π finSupp
(0gβπ΄)))
β (πΌβ(πΆ Ξ£g
(π β
β0 β¦ ((ππΈπ) Β· (πβ(πβπ)))))) = (π Ξ£g (π β β0
β¦ ((πβπ) β (π β π))))) |