Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ โ Fin) |
2 | | simplr 768 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐
โ Ring) |
3 | | pm2mpmhm.p |
. . . . . . . 8
โข ๐ = (Poly1โ๐
) |
4 | | pm2mpmhm.c |
. . . . . . . 8
โข ๐ถ = (๐ Mat ๐) |
5 | 3, 4 | pmatring 22057 |
. . . . . . 7
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ถ โ Ring) |
6 | 5 | adantr 482 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ถ โ Ring) |
7 | | simpl 484 |
. . . . . . 7
โข ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ ๐ฅ โ ๐ต) |
8 | 7 | adantl 483 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ฅ โ ๐ต) |
9 | | simpr 486 |
. . . . . . 7
โข ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ ๐ฆ โ ๐ต) |
10 | 9 | adantl 483 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ฆ โ ๐ต) |
11 | | pm2mpmhm.b |
. . . . . . 7
โข ๐ต = (Baseโ๐ถ) |
12 | | eqid 2733 |
. . . . . . 7
โข
(.rโ๐ถ) = (.rโ๐ถ) |
13 | 11, 12 | ringcl 19986 |
. . . . . 6
โข ((๐ถ โ Ring โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ(.rโ๐ถ)๐ฆ) โ ๐ต) |
14 | 6, 8, 10, 13 | syl3anc 1372 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ(.rโ๐ถ)๐ฆ) โ ๐ต) |
15 | | eqid 2733 |
. . . . . 6
โข (
ยท๐ โ๐) = ( ยท๐
โ๐) |
16 | | eqid 2733 |
. . . . . 6
โข
(.gโ(mulGrpโ๐)) =
(.gโ(mulGrpโ๐)) |
17 | | eqid 2733 |
. . . . . 6
โข
(var1โ๐ด) = (var1โ๐ด) |
18 | | pm2mpmhm.a |
. . . . . 6
โข ๐ด = (๐ Mat ๐
) |
19 | | pm2mpmhm.q |
. . . . . 6
โข ๐ = (Poly1โ๐ด) |
20 | | pm2mpmhm.t |
. . . . . 6
โข ๐ = (๐ pMatToMatPoly ๐
) |
21 | 3, 4, 11, 15, 16, 17, 18, 19, 20 | pm2mpfval 22161 |
. . . . 5
โข ((๐ โ Fin โง ๐
โ Ring โง (๐ฅ(.rโ๐ถ)๐ฆ) โ ๐ต) โ (๐โ(๐ฅ(.rโ๐ถ)๐ฆ)) = (๐ ฮฃg (๐ โ โ0
โฆ (((๐ฅ(.rโ๐ถ)๐ฆ) decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))) |
22 | 1, 2, 14, 21 | syl3anc 1372 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐โ(๐ฅ(.rโ๐ถ)๐ฆ)) = (๐ ฮฃg (๐ โ โ0
โฆ (((๐ฅ(.rโ๐ถ)๐ฆ) decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))) |
23 | 3, 4, 11, 18 | decpmatmul 22137 |
. . . . . . . 8
โข ((๐
โ Ring โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง ๐ โ โ0) โ ((๐ฅ(.rโ๐ถ)๐ฆ) decompPMat ๐) = (๐ด ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))) |
24 | 23 | ad4ant234 1176 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ((๐ฅ(.rโ๐ถ)๐ฆ) decompPMat ๐) = (๐ด ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))) |
25 | 24 | oveq1d 7373 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (((๐ฅ(.rโ๐ถ)๐ฆ) decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))) = ((๐ด ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))) |
26 | 25 | mpteq2dva 5206 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ โ0 โฆ (((๐ฅ(.rโ๐ถ)๐ฆ) decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))) = (๐ โ โ0 โฆ ((๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) |
27 | 26 | oveq2d 7374 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ ฮฃg (๐ โ โ0
โฆ (((๐ฅ(.rโ๐ถ)๐ฆ) decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐ด
ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))) |
28 | | eqid 2733 |
. . . . . . . 8
โข
(Baseโ๐) =
(Baseโ๐) |
29 | 18 | matring 21808 |
. . . . . . . . 9
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ด โ Ring) |
30 | 29 | ad2antrr 725 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ๐ด โ Ring) |
31 | | eqid 2733 |
. . . . . . . 8
โข
(Baseโ๐ด) =
(Baseโ๐ด) |
32 | | eqid 2733 |
. . . . . . . 8
โข
(0gโ๐ด) = (0gโ๐ด) |
33 | | ringcmn 20008 |
. . . . . . . . . . . 12
โข (๐ด โ Ring โ ๐ด โ CMnd) |
34 | 29, 33 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ด โ CMnd) |
35 | 34 | ad3antrrr 729 |
. . . . . . . . . 10
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ โ0)
โ ๐ด โ
CMnd) |
36 | | fzfid 13884 |
. . . . . . . . . 10
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ โ0)
โ (0...๐) โ
Fin) |
37 | 30 | ad2antrr 725 |
. . . . . . . . . . . 12
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ โ0)
โง ๐ง โ (0...๐)) โ ๐ด โ Ring) |
38 | | simp-5r 785 |
. . . . . . . . . . . . 13
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ โ0)
โง ๐ง โ (0...๐)) โ ๐
โ Ring) |
39 | 8 | ad3antrrr 729 |
. . . . . . . . . . . . 13
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ โ0)
โง ๐ง โ (0...๐)) โ ๐ฅ โ ๐ต) |
40 | | elfznn0 13540 |
. . . . . . . . . . . . . 14
โข (๐ง โ (0...๐) โ ๐ง โ โ0) |
41 | 40 | adantl 483 |
. . . . . . . . . . . . 13
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ โ0)
โง ๐ง โ (0...๐)) โ ๐ง โ โ0) |
42 | 3, 4, 11, 18, 31 | decpmatcl 22132 |
. . . . . . . . . . . . 13
โข ((๐
โ Ring โง ๐ฅ โ ๐ต โง ๐ง โ โ0) โ (๐ฅ decompPMat ๐ง) โ (Baseโ๐ด)) |
43 | 38, 39, 41, 42 | syl3anc 1372 |
. . . . . . . . . . . 12
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ โ0)
โง ๐ง โ (0...๐)) โ (๐ฅ decompPMat ๐ง) โ (Baseโ๐ด)) |
44 | 10 | ad3antrrr 729 |
. . . . . . . . . . . . 13
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ โ0)
โง ๐ง โ (0...๐)) โ ๐ฆ โ ๐ต) |
45 | | fznn0sub 13479 |
. . . . . . . . . . . . . 14
โข (๐ง โ (0...๐) โ (๐ โ ๐ง) โ
โ0) |
46 | 45 | adantl 483 |
. . . . . . . . . . . . 13
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ โ0)
โง ๐ง โ (0...๐)) โ (๐ โ ๐ง) โ
โ0) |
47 | 3, 4, 11, 18, 31 | decpmatcl 22132 |
. . . . . . . . . . . . 13
โข ((๐
โ Ring โง ๐ฆ โ ๐ต โง (๐ โ ๐ง) โ โ0) โ (๐ฆ decompPMat (๐ โ ๐ง)) โ (Baseโ๐ด)) |
48 | 38, 44, 46, 47 | syl3anc 1372 |
. . . . . . . . . . . 12
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ โ0)
โง ๐ง โ (0...๐)) โ (๐ฆ decompPMat (๐ โ ๐ง)) โ (Baseโ๐ด)) |
49 | | eqid 2733 |
. . . . . . . . . . . . 13
โข
(.rโ๐ด) = (.rโ๐ด) |
50 | 31, 49 | ringcl 19986 |
. . . . . . . . . . . 12
โข ((๐ด โ Ring โง (๐ฅ decompPMat ๐ง) โ (Baseโ๐ด) โง (๐ฆ decompPMat (๐ โ ๐ง)) โ (Baseโ๐ด)) โ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))) โ (Baseโ๐ด)) |
51 | 37, 43, 48, 50 | syl3anc 1372 |
. . . . . . . . . . 11
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ โ0)
โง ๐ง โ (0...๐)) โ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))) โ (Baseโ๐ด)) |
52 | 51 | ralrimiva 3140 |
. . . . . . . . . 10
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ โ0)
โ โ๐ง โ
(0...๐)((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))) โ (Baseโ๐ด)) |
53 | 31, 35, 36, 52 | gsummptcl 19749 |
. . . . . . . . 9
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ โ0)
โ (๐ด
ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))))) โ (Baseโ๐ด)) |
54 | 53 | ralrimiva 3140 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ
โ๐ โ
โ0 (๐ด
ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))))) โ (Baseโ๐ด)) |
55 | 3, 4, 11, 18, 49, 32 | decpmatmulsumfsupp 22138 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ โ0 โฆ (๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))) finSupp (0gโ๐ด)) |
56 | 55 | adantr 482 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ โ0
โฆ (๐ด
ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))) finSupp (0gโ๐ด)) |
57 | | simpr 486 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ๐ โ
โ0) |
58 | 19, 28, 17, 16, 30, 31, 15, 32, 54, 56, 57 | gsummoncoe1 21691 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ
((coe1โ(๐
ฮฃg (๐ โ โ0 โฆ ((๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐) = โฆ๐ / ๐โฆ(๐ด ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))) |
59 | | csbov2g 7404 |
. . . . . . . . 9
โข (๐ โ โ0
โ โฆ๐ /
๐โฆ(๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))))) = (๐ด ฮฃg
โฆ๐ / ๐โฆ(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))) |
60 | | id 22 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ ๐ โ
โ0) |
61 | | oveq2 7366 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (0...๐) = (0...๐)) |
62 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (๐ โ ๐ง) = (๐ โ ๐ง)) |
63 | 62 | oveq2d 7374 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ (๐ฆ decompPMat (๐ โ ๐ง)) = (๐ฆ decompPMat (๐ โ ๐ง))) |
64 | 63 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))) = ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))) |
65 | 61, 64 | mpteq12dv 5197 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))) = (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))))) |
66 | 65 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ = ๐) โ (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))) = (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))))) |
67 | 60, 66 | csbied 3894 |
. . . . . . . . . 10
โข (๐ โ โ0
โ โฆ๐ /
๐โฆ(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))) = (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))))) |
68 | 67 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ โ โ0
โ (๐ด
ฮฃg โฆ๐ / ๐โฆ(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))))) = (๐ด ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))) |
69 | 59, 68 | eqtrd 2773 |
. . . . . . . 8
โข (๐ โ โ0
โ โฆ๐ /
๐โฆ(๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))))) = (๐ด ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))) |
70 | 69 | adantl 483 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ
โฆ๐ / ๐โฆ(๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))))) = (๐ด ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))) |
71 | | eqidd 2734 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ โ0
โฆ (๐ด
ฮฃg (๐ โ (0...๐) โฆ (((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐)))))) = (๐ โ โ0 โฆ (๐ด ฮฃg
(๐ โ (0...๐) โฆ
(((coe1โ(๐
ฮฃg (๐ โ โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐))))))) |
72 | | oveq2 7366 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (0...๐) = (0...๐)) |
73 | | fvoveq1 7381 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฆ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐)) = ((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฆ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐))) |
74 | 73 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐))) = (((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐)))) |
75 | 72, 74 | mpteq12dv 5197 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ โ (0...๐) โฆ (((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐)))) = (๐ โ (0...๐) โฆ (((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐))))) |
76 | 75 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ด ฮฃg (๐ โ (0...๐) โฆ (((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐))))) = (๐ด ฮฃg (๐ โ (0...๐) โฆ (((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐)))))) |
77 | 76 | adantl 483 |
. . . . . . . . 9
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ = ๐) โ (๐ด ฮฃg (๐ โ (0...๐) โฆ (((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐))))) = (๐ด ฮฃg (๐ โ (0...๐) โฆ (((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐)))))) |
78 | | ovexd 7393 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ด ฮฃg
(๐ โ (0...๐) โฆ
(((coe1โ(๐
ฮฃg (๐ โ โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐))))) โ V) |
79 | 71, 77, 57, 78 | fvmptd 6956 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ((๐ โ โ0
โฆ (๐ด
ฮฃg (๐ โ (0...๐) โฆ (((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐))))))โ๐) = (๐ด ฮฃg (๐ โ (0...๐) โฆ (((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐)))))) |
80 | | eqid 2733 |
. . . . . . . . . 10
โข
(0gโ๐) = (0gโ๐) |
81 | 19 | ply1ring 21635 |
. . . . . . . . . . . . 13
โข (๐ด โ Ring โ ๐ โ Ring) |
82 | 29, 81 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ โ Ring) |
83 | | ringcmn 20008 |
. . . . . . . . . . . 12
โข (๐ โ Ring โ ๐ โ CMnd) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ โ CMnd) |
85 | 84 | ad2antrr 725 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ๐ โ CMnd) |
86 | | nn0ex 12424 |
. . . . . . . . . . 11
โข
โ0 โ V |
87 | 86 | a1i 11 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ
โ0 โ V) |
88 | 7 | anim2i 618 |
. . . . . . . . . . . . . 14
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐ โ Fin โง ๐
โ Ring) โง ๐ฅ โ ๐ต)) |
89 | | df-3an 1090 |
. . . . . . . . . . . . . 14
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ฅ โ ๐ต) โ ((๐ โ Fin โง ๐
โ Ring) โง ๐ฅ โ ๐ต)) |
90 | 88, 89 | sylibr 233 |
. . . . . . . . . . . . 13
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ Fin โง ๐
โ Ring โง ๐ฅ โ ๐ต)) |
91 | 90 | adantr 482 |
. . . . . . . . . . . 12
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ Fin โง ๐
โ Ring โง ๐ฅ โ ๐ต)) |
92 | 3, 4, 11, 15, 16, 17, 18, 19, 28 | pm2mpghmlem1 22178 |
. . . . . . . . . . . 12
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ฅ โ ๐ต) โง ๐ โ โ0) โ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))) โ (Baseโ๐)) |
93 | 91, 92 | sylan 581 |
. . . . . . . . . . 11
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ โ0)
โ ((๐ฅ decompPMat ๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))) โ (Baseโ๐)) |
94 | 93 | fmpttd 7064 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ โ0
โฆ ((๐ฅ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))):โ0โถ(Baseโ๐)) |
95 | 3, 4, 11, 15, 16, 17, 18, 19 | pm2mpghmlem2 22177 |
. . . . . . . . . . 11
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ฅ โ ๐ต) โ (๐ โ โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))) finSupp
(0gโ๐)) |
96 | 91, 95 | syl 17 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ โ0
โฆ ((๐ฅ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))) finSupp
(0gโ๐)) |
97 | 28, 80, 85, 87, 94, 96 | gsumcl 19697 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) โ (Baseโ๐)) |
98 | 9 | anim2i 618 |
. . . . . . . . . . . . . 14
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐ โ Fin โง ๐
โ Ring) โง ๐ฆ โ ๐ต)) |
99 | | df-3an 1090 |
. . . . . . . . . . . . . 14
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ฆ โ ๐ต) โ ((๐ โ Fin โง ๐
โ Ring) โง ๐ฆ โ ๐ต)) |
100 | 98, 99 | sylibr 233 |
. . . . . . . . . . . . 13
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ Fin โง ๐
โ Ring โง ๐ฆ โ ๐ต)) |
101 | 100 | adantr 482 |
. . . . . . . . . . . 12
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ Fin โง ๐
โ Ring โง ๐ฆ โ ๐ต)) |
102 | 3, 4, 11, 15, 16, 17, 18, 19, 28 | pm2mpghmlem1 22178 |
. . . . . . . . . . . 12
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ฆ โ ๐ต) โง ๐ โ โ0) โ ((๐ฆ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))) โ (Baseโ๐)) |
103 | 101, 102 | sylan 581 |
. . . . . . . . . . 11
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ โ0)
โ ((๐ฆ decompPMat ๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))) โ (Baseโ๐)) |
104 | 103 | fmpttd 7064 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))):โ0โถ(Baseโ๐)) |
105 | 1, 2, 10 | 3jca 1129 |
. . . . . . . . . . . 12
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ Fin โง ๐
โ Ring โง ๐ฆ โ ๐ต)) |
106 | 105 | adantr 482 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ Fin โง ๐
โ Ring โง ๐ฆ โ ๐ต)) |
107 | 3, 4, 11, 15, 16, 17, 18, 19 | pm2mpghmlem2 22177 |
. . . . . . . . . . 11
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ฆ โ ๐ต) โ (๐ โ โ0 โฆ ((๐ฆ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))) finSupp
(0gโ๐)) |
108 | 106, 107 | syl 17 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))) finSupp
(0gโ๐)) |
109 | 28, 80, 85, 87, 104, 108 | gsumcl 19697 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฆ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) โ (Baseโ๐)) |
110 | | eqid 2733 |
. . . . . . . . . . 11
โข
(.rโ๐) = (.rโ๐) |
111 | 19, 110, 49, 28 | coe1mul 21657 |
. . . . . . . . . 10
โข ((๐ด โ Ring โง (๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) โ (Baseโ๐) โง (๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) โ (Baseโ๐)) โ
(coe1โ((๐
ฮฃg (๐ โ โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))) = (๐ โ โ0 โฆ (๐ด ฮฃg
(๐ โ (0...๐) โฆ
(((coe1โ(๐
ฮฃg (๐ โ โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐))))))) |
112 | 111 | fveq1d 6845 |
. . . . . . . . 9
โข ((๐ด โ Ring โง (๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) โ (Baseโ๐) โง (๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) โ (Baseโ๐)) โ
((coe1โ((๐
ฮฃg (๐ โ โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))))โ๐) = ((๐ โ โ0 โฆ (๐ด ฮฃg
(๐ โ (0...๐) โฆ
(((coe1โ(๐
ฮฃg (๐ โ โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐))))))โ๐)) |
113 | 30, 97, 109, 112 | syl3anc 1372 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ
((coe1โ((๐
ฮฃg (๐ โ โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))))โ๐) = ((๐ โ โ0 โฆ (๐ด ฮฃg
(๐ โ (0...๐) โฆ
(((coe1โ(๐
ฮฃg (๐ โ โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐))))))โ๐)) |
114 | | oveq2 7366 |
. . . . . . . . . . . 12
โข (๐ง = ๐ โ (๐ฅ decompPMat ๐ง) = (๐ฅ decompPMat ๐)) |
115 | | oveq2 7366 |
. . . . . . . . . . . . 13
โข (๐ง = ๐ โ (๐ โ ๐ง) = (๐ โ ๐)) |
116 | 115 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ง = ๐ โ (๐ฆ decompPMat (๐ โ ๐ง)) = (๐ฆ decompPMat (๐ โ ๐))) |
117 | 114, 116 | oveq12d 7376 |
. . . . . . . . . . 11
โข (๐ง = ๐ โ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))) = ((๐ฅ decompPMat ๐)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐)))) |
118 | 117 | cbvmptv 5219 |
. . . . . . . . . 10
โข (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))) = (๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐)))) |
119 | 29 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ๐ด โ Ring) |
120 | | simp-5r 785 |
. . . . . . . . . . . . . . . 16
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โง ๐ โ โ0) โ ๐
โ Ring) |
121 | 8 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โง ๐ โ โ0) โ ๐ฅ โ ๐ต) |
122 | | simpr 486 |
. . . . . . . . . . . . . . . 16
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โง ๐ โ โ0) โ ๐ โ
โ0) |
123 | 3, 4, 11, 18, 31 | decpmatcl 22132 |
. . . . . . . . . . . . . . . 16
โข ((๐
โ Ring โง ๐ฅ โ ๐ต โง ๐ โ โ0) โ (๐ฅ decompPMat ๐) โ (Baseโ๐ด)) |
124 | 120, 121,
122, 123 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โง ๐ โ โ0) โ (๐ฅ decompPMat ๐) โ (Baseโ๐ด)) |
125 | 124 | ralrimiva 3140 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ โ๐ โ โ0 (๐ฅ decompPMat ๐) โ (Baseโ๐ด)) |
126 | 2, 8 | jca 513 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐
โ Ring โง ๐ฅ โ ๐ต)) |
127 | 126 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐
โ Ring โง ๐ฅ โ ๐ต)) |
128 | 3, 4, 11, 18, 32 | decpmatfsupp 22134 |
. . . . . . . . . . . . . . 15
โข ((๐
โ Ring โง ๐ฅ โ ๐ต) โ (๐ โ โ0 โฆ (๐ฅ decompPMat ๐)) finSupp (0gโ๐ด)) |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐ โ โ0 โฆ (๐ฅ decompPMat ๐)) finSupp (0gโ๐ด)) |
130 | | elfznn0 13540 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0...๐) โ ๐ โ โ0) |
131 | 130 | adantl 483 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ๐ โ โ0) |
132 | 19, 28, 17, 16, 119, 31, 15, 32, 125, 129, 131 | gsummoncoe1 21691 |
. . . . . . . . . . . . 13
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐) = โฆ๐ / ๐โฆ(๐ฅ decompPMat ๐)) |
133 | | csbov2g 7404 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0...๐) โ โฆ๐ / ๐โฆ(๐ฅ decompPMat ๐) = (๐ฅ decompPMat โฆ๐ / ๐โฆ๐)) |
134 | | csbvarg 4392 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (0...๐) โ โฆ๐ / ๐โฆ๐ = ๐) |
135 | 134 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0...๐) โ (๐ฅ decompPMat โฆ๐ / ๐โฆ๐) = (๐ฅ decompPMat ๐)) |
136 | 133, 135 | eqtrd 2773 |
. . . . . . . . . . . . . 14
โข (๐ โ (0...๐) โ โฆ๐ / ๐โฆ(๐ฅ decompPMat ๐) = (๐ฅ decompPMat ๐)) |
137 | 136 | adantl 483 |
. . . . . . . . . . . . 13
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ โฆ๐ / ๐โฆ(๐ฅ decompPMat ๐) = (๐ฅ decompPMat ๐)) |
138 | 132, 137 | eqtr2d 2774 |
. . . . . . . . . . . 12
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐ฅ decompPMat ๐) = ((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)) |
139 | 10 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โง ๐ โ โ0) โ ๐ฆ โ ๐ต) |
140 | 3, 4, 11, 18, 31 | decpmatcl 22132 |
. . . . . . . . . . . . . . . 16
โข ((๐
โ Ring โง ๐ฆ โ ๐ต โง ๐ โ โ0) โ (๐ฆ decompPMat ๐) โ (Baseโ๐ด)) |
141 | 120, 139,
122, 140 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โง ๐ โ โ0) โ (๐ฆ decompPMat ๐) โ (Baseโ๐ด)) |
142 | 141 | ralrimiva 3140 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ โ๐ โ โ0 (๐ฆ decompPMat ๐) โ (Baseโ๐ด)) |
143 | 2, 10 | jca 513 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐
โ Ring โง ๐ฆ โ ๐ต)) |
144 | 143 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐
โ Ring โง ๐ฆ โ ๐ต)) |
145 | 3, 4, 11, 18, 32 | decpmatfsupp 22134 |
. . . . . . . . . . . . . . 15
โข ((๐
โ Ring โง ๐ฆ โ ๐ต) โ (๐ โ โ0 โฆ (๐ฆ decompPMat ๐)) finSupp (0gโ๐ด)) |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐ โ โ0 โฆ (๐ฆ decompPMat ๐)) finSupp (0gโ๐ด)) |
147 | | fznn0sub 13479 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0...๐) โ (๐ โ ๐) โ
โ0) |
148 | 147 | adantl 483 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐ โ ๐) โ
โ0) |
149 | 19, 28, 17, 16, 119, 31, 15, 32, 142, 146, 148 | gsummoncoe1 21691 |
. . . . . . . . . . . . 13
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฆ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐)) = โฆ(๐ โ ๐) / ๐โฆ(๐ฆ decompPMat ๐)) |
150 | | ovex 7391 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐) โ V |
151 | | csbov2g 7404 |
. . . . . . . . . . . . . 14
โข ((๐ โ ๐) โ V โ โฆ(๐ โ ๐) / ๐โฆ(๐ฆ decompPMat ๐) = (๐ฆ decompPMat โฆ(๐ โ ๐) / ๐โฆ๐)) |
152 | 150, 151 | mp1i 13 |
. . . . . . . . . . . . 13
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ โฆ(๐ โ ๐) / ๐โฆ(๐ฆ decompPMat ๐) = (๐ฆ decompPMat โฆ(๐ โ ๐) / ๐โฆ๐)) |
153 | | csbvarg 4392 |
. . . . . . . . . . . . . . 15
โข ((๐ โ ๐) โ V โ โฆ(๐ โ ๐) / ๐โฆ๐ = (๐ โ ๐)) |
154 | 150, 153 | mp1i 13 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ โฆ(๐ โ ๐) / ๐โฆ๐ = (๐ โ ๐)) |
155 | 154 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐ฆ decompPMat โฆ(๐ โ ๐) / ๐โฆ๐) = (๐ฆ decompPMat (๐ โ ๐))) |
156 | 149, 152,
155 | 3eqtrrd 2778 |
. . . . . . . . . . . 12
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐ฆ decompPMat (๐ โ ๐)) = ((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฆ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐))) |
157 | 138, 156 | oveq12d 7376 |
. . . . . . . . . . 11
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ((๐ฅ decompPMat ๐)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐))) = (((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐)))) |
158 | 157 | mpteq2dva 5206 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ (0...๐) โฆ ((๐ฅ decompPMat ๐)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐)))) = (๐ โ (0...๐) โฆ (((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐))))) |
159 | 118, 158 | eqtrid 2785 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))) = (๐ โ (0...๐) โฆ (((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐))))) |
160 | 159 | oveq2d 7374 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))))) = (๐ด ฮฃg (๐ โ (0...๐) โฆ (((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐)(.rโ๐ด)((coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ(๐ โ ๐)))))) |
161 | 79, 113, 160 | 3eqtr4rd 2784 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))))) = ((coe1โ((๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))))โ๐)) |
162 | 58, 70, 161 | 3eqtrd 2777 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ
((coe1โ(๐
ฮฃg (๐ โ โ0 โฆ ((๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐) = ((coe1โ((๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))))โ๐)) |
163 | 162 | ralrimiva 3140 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ โ๐ โ โ0
((coe1โ(๐
ฮฃg (๐ โ โ0 โฆ ((๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐) = ((coe1โ((๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))))โ๐)) |
164 | 29 | adantr 482 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ด โ Ring) |
165 | 84 | adantr 482 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ โ CMnd) |
166 | 86 | a1i 11 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ โ0 โ
V) |
167 | 19 | ply1lmod 21639 |
. . . . . . . . . . 11
โข (๐ด โ Ring โ ๐ โ LMod) |
168 | 29, 167 | syl 17 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ โ LMod) |
169 | 168 | ad2antrr 725 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ๐ โ LMod) |
170 | 34 | ad2antrr 725 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ๐ด โ CMnd) |
171 | | fzfid 13884 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ
(0...๐) โ
Fin) |
172 | 29 | ad3antrrr 729 |
. . . . . . . . . . . . 13
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ง โ (0...๐)) โ ๐ด โ Ring) |
173 | | simp-4r 783 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ง โ (0...๐)) โ ๐
โ Ring) |
174 | | simplrl 776 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ๐ฅ โ ๐ต) |
175 | 174 | adantr 482 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ง โ (0...๐)) โ ๐ฅ โ ๐ต) |
176 | 40 | adantl 483 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ง โ (0...๐)) โ ๐ง โ โ0) |
177 | 173, 175,
176, 42 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ง โ (0...๐)) โ (๐ฅ decompPMat ๐ง) โ (Baseโ๐ด)) |
178 | | simplrr 777 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ๐ฆ โ ๐ต) |
179 | 178 | adantr 482 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ง โ (0...๐)) โ ๐ฆ โ ๐ต) |
180 | 45 | adantl 483 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ง โ (0...๐)) โ (๐ โ ๐ง) โ
โ0) |
181 | 173, 179,
180, 47 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ง โ (0...๐)) โ (๐ฆ decompPMat (๐ โ ๐ง)) โ (Baseโ๐ด)) |
182 | 172, 177,
181, 50 | syl3anc 1372 |
. . . . . . . . . . . 12
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โง ๐ง โ (0...๐)) โ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))) โ (Baseโ๐ด)) |
183 | 182 | ralrimiva 3140 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ
โ๐ง โ (0...๐)((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))) โ (Baseโ๐ด)) |
184 | 31, 170, 171, 183 | gsummptcl 19749 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))))) โ (Baseโ๐ด)) |
185 | 29 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ๐ด โ Ring) |
186 | 19 | ply1sca 21640 |
. . . . . . . . . . . . 13
โข (๐ด โ Ring โ ๐ด = (Scalarโ๐)) |
187 | 185, 186 | syl 17 |
. . . . . . . . . . . 12
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ๐ด = (Scalarโ๐)) |
188 | 187 | eqcomd 2739 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ
(Scalarโ๐) = ๐ด) |
189 | 188 | fveq2d 6847 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ
(Baseโ(Scalarโ๐)) = (Baseโ๐ด)) |
190 | 184, 189 | eleqtrrd 2837 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))))) โ (Baseโ(Scalarโ๐))) |
191 | | eqid 2733 |
. . . . . . . . . . 11
โข
(mulGrpโ๐) =
(mulGrpโ๐) |
192 | 19, 17, 191, 16, 28 | ply1moncl 21658 |
. . . . . . . . . 10
โข ((๐ด โ Ring โง ๐ โ โ0)
โ (๐(.gโ(mulGrpโ๐))(var1โ๐ด)) โ (Baseโ๐)) |
193 | 185, 192 | sylancom 589 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ (๐(.gโ(mulGrpโ๐))(var1โ๐ด)) โ (Baseโ๐)) |
194 | | eqid 2733 |
. . . . . . . . . 10
โข
(Scalarโ๐) =
(Scalarโ๐) |
195 | | eqid 2733 |
. . . . . . . . . 10
โข
(Baseโ(Scalarโ๐)) = (Baseโ(Scalarโ๐)) |
196 | 28, 194, 15, 195 | lmodvscl 20354 |
. . . . . . . . 9
โข ((๐ โ LMod โง (๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง))))) โ (Baseโ(Scalarโ๐)) โง (๐(.gโ(mulGrpโ๐))(var1โ๐ด)) โ (Baseโ๐)) โ ((๐ด ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))) โ (Baseโ๐)) |
197 | 169, 190,
193, 196 | syl3anc 1372 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ((๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))) โ (Baseโ๐)) |
198 | 197 | fmpttd 7064 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ โ0 โฆ ((๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))):โ0โถ(Baseโ๐)) |
199 | 3, 4, 11, 15, 16, 17, 18, 19, 28, 20 | pm2mpmhmlem1 22183 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ โ0 โฆ ((๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))) finSupp
(0gโ๐)) |
200 | 28, 80, 165, 166, 198, 199 | gsumcl 19697 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ ฮฃg (๐ โ โ0
โฆ ((๐ด
ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) โ (Baseโ๐)) |
201 | 82 | adantr 482 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ๐ โ Ring) |
202 | 90, 92 | sylan 581 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))) โ (Baseโ๐)) |
203 | 202 | fmpttd 7064 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))):โ0โถ(Baseโ๐)) |
204 | 90, 95 | syl 17 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))) finSupp
(0gโ๐)) |
205 | 28, 80, 165, 166, 203, 204 | gsumcl 19697 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ ฮฃg (๐ โ โ0
โฆ ((๐ฅ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) โ (Baseโ๐)) |
206 | 100, 102 | sylan 581 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โง ๐ โ โ0) โ ((๐ฆ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))) โ (Baseโ๐)) |
207 | 206 | fmpttd 7064 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ โ0 โฆ ((๐ฆ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))):โ0โถ(Baseโ๐)) |
208 | 1, 2, 10, 107 | syl3anc 1372 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ โ โ0 โฆ ((๐ฆ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))) finSupp
(0gโ๐)) |
209 | 28, 80, 165, 166, 207, 208 | gsumcl 19697 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) โ (Baseโ๐)) |
210 | 28, 110 | ringcl 19986 |
. . . . . . 7
โข ((๐ โ Ring โง (๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) โ (Baseโ๐) โง (๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) โ (Baseโ๐)) โ ((๐ ฮฃg (๐ โ โ0
โฆ ((๐ฅ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))) โ (Baseโ๐)) |
211 | 201, 205,
209, 210 | syl3anc 1372 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐ ฮฃg (๐ โ โ0
โฆ ((๐ฅ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))) โ (Baseโ๐)) |
212 | | eqid 2733 |
. . . . . . 7
โข
(coe1โ(๐ ฮฃg (๐ โ โ0
โฆ ((๐ด
ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))) =
(coe1โ(๐
ฮฃg (๐ โ โ0 โฆ ((๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))) |
213 | | eqid 2733 |
. . . . . . 7
โข
(coe1โ((๐ ฮฃg (๐ โ โ0
โฆ ((๐ฅ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))) =
(coe1โ((๐
ฮฃg (๐ โ โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))) |
214 | 19, 28, 212, 213 | ply1coe1eq 21685 |
. . . . . 6
โข ((๐ด โ Ring โง (๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ด ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) โ (Baseโ๐) โง ((๐ ฮฃg (๐ โ โ0
โฆ ((๐ฅ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))) โ (Baseโ๐)) โ (โ๐ โ โ0
((coe1โ(๐
ฮฃg (๐ โ โ0 โฆ ((๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐) = ((coe1โ((๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))))โ๐) โ (๐ ฮฃg (๐ โ โ0
โฆ ((๐ด
ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) = ((๐ ฮฃg (๐ โ โ0
โฆ ((๐ฅ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))))) |
215 | 164, 200,
211, 214 | syl3anc 1372 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (โ๐ โ โ0
((coe1โ(๐
ฮฃg (๐ โ โ0 โฆ ((๐ด ฮฃg
(๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))โ๐) = ((coe1โ((๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ฅ decompPMat ๐)( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))))โ๐) โ (๐ ฮฃg (๐ โ โ0
โฆ ((๐ด
ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) = ((๐ ฮฃg (๐ โ โ0
โฆ ((๐ฅ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))))) |
216 | 163, 215 | mpbid 231 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ ฮฃg (๐ โ โ0
โฆ ((๐ด
ฮฃg (๐ง โ (0...๐) โฆ ((๐ฅ decompPMat ๐ง)(.rโ๐ด)(๐ฆ decompPMat (๐ โ ๐ง)))))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))) = ((๐ ฮฃg (๐ โ โ0
โฆ ((๐ฅ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))) |
217 | 22, 27, 216 | 3eqtrd 2777 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐โ(๐ฅ(.rโ๐ถ)๐ฆ)) = ((๐ ฮฃg (๐ โ โ0
โฆ ((๐ฅ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))) |
218 | 3, 4, 11, 15, 16, 17, 18, 19, 20 | pm2mpfval 22161 |
. . . . 5
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ฅ โ ๐ต) โ (๐โ๐ฅ) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐ฅ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))) |
219 | 1, 2, 8, 218 | syl3anc 1372 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐โ๐ฅ) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐ฅ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))) |
220 | 3, 4, 11, 15, 16, 17, 18, 19, 20 | pm2mpfval 22161 |
. . . . 5
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ฆ โ ๐ต) โ (๐โ๐ฆ) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))) |
221 | 1, 2, 10, 220 | syl3anc 1372 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐โ๐ฆ) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))) |
222 | 219, 221 | oveq12d 7376 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ ((๐โ๐ฅ)(.rโ๐)(๐โ๐ฆ)) = ((๐ ฮฃg (๐ โ โ0
โฆ ((๐ฅ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด)))))(.rโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ฆ decompPMat
๐)(
ยท๐ โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐ด))))))) |
223 | 217, 222 | eqtr4d 2776 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐โ(๐ฅ(.rโ๐ถ)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐)(๐โ๐ฆ))) |
224 | 223 | ralrimivva 3194 |
1
โข ((๐ โ Fin โง ๐
โ Ring) โ
โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (๐โ(๐ฅ(.rโ๐ถ)๐ฆ)) = ((๐โ๐ฅ)(.rโ๐)(๐โ๐ฆ))) |