Step | Hyp | Ref
| Expression |
1 | | oveq2 7369 |
. . 3
β’ ((π½βπΌ) = (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ))))) β (πΌ Γ (π½βπΌ)) = (πΌ Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ))))))) |
2 | | cpmadugsum.i |
. . . . . 6
β’ πΌ = ((π Β· 1 ) β (πβπ)) |
3 | 2 | a1i 11 |
. . . . 5
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β πΌ = ((π Β· 1 ) β (πβπ))) |
4 | 3 | oveq1d 7376 |
. . . 4
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β (πΌ Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) = (((π Β· 1 ) β (πβπ)) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ))))))) |
5 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
6 | | cpmadugsum.r |
. . . . 5
β’ Γ =
(.rβπ) |
7 | | cpmadugsum.s |
. . . . 5
β’ β =
(-gβπ) |
8 | | crngring 19984 |
. . . . . . . . 9
β’ (π
β CRing β π
β Ring) |
9 | 8 | anim2i 618 |
. . . . . . . 8
β’ ((π β Fin β§ π
β CRing) β (π β Fin β§ π
β Ring)) |
10 | 9 | 3adant3 1133 |
. . . . . . 7
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (π β Fin β§ π
β Ring)) |
11 | 10 | ad2antrr 725 |
. . . . . 6
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β (π β Fin β§ π
β Ring)) |
12 | | cpmadugsum.p |
. . . . . . 7
β’ π = (Poly1βπ
) |
13 | | cpmadugsum.y |
. . . . . . 7
β’ π = (π Mat π) |
14 | 12, 13 | pmatring 22064 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β π β Ring) |
15 | 11, 14 | syl 17 |
. . . . 5
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β π β Ring) |
16 | 12, 13 | pmatlmod 22065 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring) β π β LMod) |
17 | 8, 16 | sylan2 594 |
. . . . . . . 8
β’ ((π β Fin β§ π
β CRing) β π β LMod) |
18 | 8 | adantl 483 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β CRing) β π
β Ring) |
19 | | cpmadugsum.x |
. . . . . . . . . . 11
β’ π = (var1βπ
) |
20 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
21 | 19, 12, 20 | vr1cl 21611 |
. . . . . . . . . 10
β’ (π
β Ring β π β (Baseβπ)) |
22 | 18, 21 | syl 17 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β CRing) β π β (Baseβπ)) |
23 | 12 | ply1crng 21592 |
. . . . . . . . . . 11
β’ (π
β CRing β π β CRing) |
24 | 13 | matsca2 21792 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π β CRing) β π = (Scalarβπ)) |
25 | 23, 24 | sylan2 594 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β CRing) β π = (Scalarβπ)) |
26 | 25 | fveq2d 6850 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β CRing) β
(Baseβπ) =
(Baseβ(Scalarβπ))) |
27 | 22, 26 | eleqtrd 2836 |
. . . . . . . 8
β’ ((π β Fin β§ π
β CRing) β π β
(Baseβ(Scalarβπ))) |
28 | 8, 14 | sylan2 594 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β CRing) β π β Ring) |
29 | | cpmadugsum.1 |
. . . . . . . . . 10
β’ 1 =
(1rβπ) |
30 | 5, 29 | ringidcl 19997 |
. . . . . . . . 9
β’ (π β Ring β 1 β
(Baseβπ)) |
31 | 28, 30 | syl 17 |
. . . . . . . 8
β’ ((π β Fin β§ π
β CRing) β 1 β
(Baseβπ)) |
32 | | eqid 2733 |
. . . . . . . . 9
β’
(Scalarβπ) =
(Scalarβπ) |
33 | | cpmadugsum.m |
. . . . . . . . 9
β’ Β· = (
Β·π βπ) |
34 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
35 | 5, 32, 33, 34 | lmodvscl 20383 |
. . . . . . . 8
β’ ((π β LMod β§ π β
(Baseβ(Scalarβπ)) β§ 1 β (Baseβπ)) β (π Β· 1 ) β (Baseβπ)) |
36 | 17, 27, 31, 35 | syl3anc 1372 |
. . . . . . 7
β’ ((π β Fin β§ π
β CRing) β (π Β· 1 ) β (Baseβπ)) |
37 | 36 | 3adant3 1133 |
. . . . . 6
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (π Β· 1 ) β (Baseβπ)) |
38 | 37 | ad2antrr 725 |
. . . . 5
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β (π Β· 1 ) β (Baseβπ)) |
39 | | cpmadugsum.t |
. . . . . . . 8
β’ π = (π matToPolyMat π
) |
40 | | cpmadugsum.a |
. . . . . . . 8
β’ π΄ = (π Mat π
) |
41 | | cpmadugsum.b |
. . . . . . . 8
β’ π΅ = (Baseβπ΄) |
42 | 39, 40, 41, 12, 13 | mat2pmatbas 22098 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (πβπ) β (Baseβπ)) |
43 | 8, 42 | syl3an2 1165 |
. . . . . 6
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (πβπ) β (Baseβπ)) |
44 | 43 | ad2antrr 725 |
. . . . 5
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β (πβπ) β (Baseβπ)) |
45 | | ringcmn 20011 |
. . . . . . . . 9
β’ (π β Ring β π β CMnd) |
46 | 28, 45 | syl 17 |
. . . . . . . 8
β’ ((π β Fin β§ π
β CRing) β π β CMnd) |
47 | 46 | 3adant3 1133 |
. . . . . . 7
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π β CMnd) |
48 | 47 | ad2antrr 725 |
. . . . . 6
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β π β CMnd) |
49 | | fzfid 13887 |
. . . . . 6
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β (0...π ) β Fin) |
50 | 10 | ad3antrrr 729 |
. . . . . . . 8
β’
(((((π β Fin
β§ π
β CRing β§
π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β§ π β (0...π )) β (π β Fin β§ π
β Ring)) |
51 | | elmapi 8793 |
. . . . . . . . . . 11
β’ (π β (π΅ βm (0...π )) β π:(0...π )βΆπ΅) |
52 | | ffvelcdm 7036 |
. . . . . . . . . . . 12
β’ ((π:(0...π )βΆπ΅ β§ π β (0...π )) β (πβπ) β π΅) |
53 | 52 | ex 414 |
. . . . . . . . . . 11
β’ (π:(0...π )βΆπ΅ β (π β (0...π ) β (πβπ) β π΅)) |
54 | 51, 53 | syl 17 |
. . . . . . . . . 10
β’ (π β (π΅ βm (0...π )) β (π β (0...π ) β (πβπ) β π΅)) |
55 | 54 | adantl 483 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β (π β (0...π ) β (πβπ) β π΅)) |
56 | 55 | imp 408 |
. . . . . . . 8
β’
(((((π β Fin
β§ π
β CRing β§
π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β§ π β (0...π )) β (πβπ) β π΅) |
57 | | elfznn0 13543 |
. . . . . . . . 9
β’ (π β (0...π ) β π β β0) |
58 | 57 | adantl 483 |
. . . . . . . 8
β’
(((((π β Fin
β§ π
β CRing β§
π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β§ π β (0...π )) β π β β0) |
59 | | cpmadugsum.e |
. . . . . . . . 9
β’ β =
(.gβ(mulGrpβπ)) |
60 | 40, 41, 39, 12, 13, 5, 33, 59, 19 | mat2pmatscmxcl 22112 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ ((πβπ) β π΅ β§ π β β0)) β ((π β π) Β· (πβ(πβπ))) β (Baseβπ)) |
61 | 50, 56, 58, 60 | syl12anc 836 |
. . . . . . 7
β’
(((((π β Fin
β§ π
β CRing β§
π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β§ π β (0...π )) β ((π β π) Β· (πβ(πβπ))) β (Baseβπ)) |
62 | 61 | ralrimiva 3140 |
. . . . . 6
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β βπ β (0...π )((π β π) Β· (πβ(πβπ))) β (Baseβπ)) |
63 | 5, 48, 49, 62 | gsummptcl 19752 |
. . . . 5
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ))))) β (Baseβπ)) |
64 | 5, 6, 7, 15, 38, 44, 63 | ringsubdir 20032 |
. . . 4
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β (((π Β· 1 ) β (πβπ)) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) = (((π Β· 1 ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) β ((πβπ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))))) |
65 | | oveq1 7368 |
. . . . . . . . . 10
β’ (π = π β (π β π) = (π β π)) |
66 | | 2fveq3 6851 |
. . . . . . . . . 10
β’ (π = π β (πβ(πβπ)) = (πβ(πβπ))) |
67 | 65, 66 | oveq12d 7379 |
. . . . . . . . 9
β’ (π = π β ((π β π) Β· (πβ(πβπ))) = ((π β π) Β· (πβ(πβπ)))) |
68 | 67 | cbvmptv 5222 |
. . . . . . . 8
β’ (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))) = (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))) |
69 | 68 | oveq2i 7372 |
. . . . . . 7
β’ (π Ξ£g
(π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ))))) = (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ))))) |
70 | 69 | oveq2i 7372 |
. . . . . 6
β’ ((π Β· 1 ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) = ((π Β· 1 ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) |
71 | 69 | oveq2i 7372 |
. . . . . 6
β’ ((πβπ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) = ((πβπ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) |
72 | 70, 71 | oveq12i 7373 |
. . . . 5
β’ (((π Β· 1 ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) β ((πβπ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ))))))) = (((π Β· 1 ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) β ((πβπ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ))))))) |
73 | | cpmadugsum.g |
. . . . . . 7
β’ + =
(+gβπ) |
74 | 40, 41, 12, 13, 39, 19, 59, 33, 6, 29, 73, 7 | cpmadugsumlemF 22248 |
. . . . . 6
β’ (((π β Fin β§ π
β CRing β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (((π Β· 1 ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) β ((πβπ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ))))))) = ((π Ξ£g (π β (1...π ) β¦ ((π β π) Β· ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ))))))) + ((((π + 1) β π) Β· (πβ(πβπ ))) β ((πβπ) Γ (πβ(πβ0)))))) |
75 | 74 | anassrs 469 |
. . . . 5
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β (((π Β· 1 ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) β ((πβπ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ))))))) = ((π Ξ£g (π β (1...π ) β¦ ((π β π) Β· ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ))))))) + ((((π + 1) β π) Β· (πβ(πβπ ))) β ((πβπ) Γ (πβ(πβ0)))))) |
76 | 72, 75 | eqtrid 2785 |
. . . 4
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β (((π Β· 1 ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) β ((πβπ) Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ))))))) = ((π Ξ£g (π β (1...π ) β¦ ((π β π) Β· ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ))))))) + ((((π + 1) β π) Β· (πβ(πβπ ))) β ((πβπ) Γ (πβ(πβ0)))))) |
77 | 4, 64, 76 | 3eqtrd 2777 |
. . 3
β’ ((((π β Fin β§ π
β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β (πΌ Γ (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) = ((π Ξ£g (π β (1...π ) β¦ ((π β π) Β· ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ))))))) + ((((π + 1) β π) Β· (πβ(πβπ ))) β ((πβπ) Γ (πβ(πβ0)))))) |
78 | 1, 77 | sylan9eqr 2795 |
. 2
β’
(((((π β Fin
β§ π
β CRing β§
π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β§ (π½βπΌ) = (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) β (πΌ Γ (π½βπΌ)) = ((π Ξ£g (π β (1...π ) β¦ ((π β π) Β· ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ))))))) + ((((π + 1) β π) Β· (πβ(πβπ ))) β ((πβπ) Γ (πβ(πβ0)))))) |
79 | | cpmadugsum.j |
. . . . . . 7
β’ π½ = (π maAdju π) |
80 | 13, 79, 5 | maduf 22013 |
. . . . . 6
β’ (π β CRing β π½:(Baseβπ)βΆ(Baseβπ)) |
81 | 23, 80 | syl 17 |
. . . . 5
β’ (π
β CRing β π½:(Baseβπ)βΆ(Baseβπ)) |
82 | 81 | 3ad2ant2 1135 |
. . . 4
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β π½:(Baseβπ)βΆ(Baseβπ)) |
83 | 40, 41, 12, 13, 19, 39, 7, 33, 29, 2 | chmatcl 22200 |
. . . . 5
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β πΌ β (Baseβπ)) |
84 | 8, 83 | syl3an2 1165 |
. . . 4
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β πΌ β (Baseβπ)) |
85 | 82, 84 | ffvelcdmd 7040 |
. . 3
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β (π½βπΌ) β (Baseβπ)) |
86 | 12, 13, 5, 33, 59, 19, 39, 40, 41 | pmatcollpw3fi1 22160 |
. . 3
β’ ((π β Fin β§ π
β CRing β§ (π½βπΌ) β (Baseβπ)) β βπ β β βπ β (π΅ βm (0...π ))(π½βπΌ) = (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) |
87 | 85, 86 | syld3an3 1410 |
. 2
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β βπ β β βπ β (π΅ βm (0...π ))(π½βπΌ) = (π Ξ£g (π β (0...π ) β¦ ((π β π) Β· (πβ(πβπ)))))) |
88 | 78, 87 | reximddv2 3203 |
1
β’ ((π β Fin β§ π
β CRing β§ π β π΅) β βπ β β βπ β (π΅ βm (0...π ))(πΌ Γ (π½βπΌ)) = ((π Ξ£g (π β (1...π ) β¦ ((π β π) Β· ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ))))))) + ((((π + 1) β π) Β· (πβ(πβπ ))) β ((πβπ) Γ (πβ(πβ0)))))) |