Step | Hyp | Ref
| Expression |
1 | | fvexd 6906 |
. 2
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (0gβπ) β V) |
2 | | ovexd 7449 |
. 2
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β ((π΄ Ξ£g
(π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π))))) β (π β π)) β V) |
3 | | oveq2 7422 |
. . . . 5
β’ (π = π β (0...π) = (0...π)) |
4 | | oveq1 7421 |
. . . . . . 7
β’ (π = π β (π β π) = (π β π)) |
5 | 4 | oveq2d 7430 |
. . . . . 6
β’ (π = π β (π¦ decompPMat (π β π)) = (π¦ decompPMat (π β π))) |
6 | 5 | oveq2d 7430 |
. . . . 5
β’ (π = π β ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π))) = ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π)))) |
7 | 3, 6 | mpteq12dv 5233 |
. . . 4
β’ (π = π β (π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π)))) = (π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π))))) |
8 | 7 | oveq2d 7430 |
. . 3
β’ (π = π β (π΄ Ξ£g (π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π))))) = (π΄ Ξ£g (π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π)))))) |
9 | | oveq1 7421 |
. . 3
β’ (π = π β (π β π) = (π β π)) |
10 | 8, 9 | oveq12d 7432 |
. 2
β’ (π = π β ((π΄ Ξ£g (π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π))))) β (π β π)) = ((π΄ Ξ£g (π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π))))) β (π β π))) |
11 | | simpll 766 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β π β Fin) |
12 | | simplr 768 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β π
β Ring) |
13 | | pm2mpfo.p |
. . . . . . . . . 10
β’ π = (Poly1βπ
) |
14 | | pm2mpfo.c |
. . . . . . . . . 10
β’ πΆ = (π Mat π) |
15 | 13, 14 | pmatring 22581 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring) β πΆ β Ring) |
16 | 15 | anim1i 614 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΆ β Ring β§ (π₯ β π΅ β§ π¦ β π΅))) |
17 | | 3anass 1093 |
. . . . . . . 8
β’ ((πΆ β Ring β§ π₯ β π΅ β§ π¦ β π΅) β (πΆ β Ring β§ (π₯ β π΅ β§ π¦ β π΅))) |
18 | 16, 17 | sylibr 233 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΆ β Ring β§ π₯ β π΅ β§ π¦ β π΅)) |
19 | | pm2mpfo.b |
. . . . . . . 8
β’ π΅ = (BaseβπΆ) |
20 | | eqid 2727 |
. . . . . . . 8
β’
(.rβπΆ) = (.rβπΆ) |
21 | 19, 20 | ringcl 20181 |
. . . . . . 7
β’ ((πΆ β Ring β§ π₯ β π΅ β§ π¦ β π΅) β (π₯(.rβπΆ)π¦) β π΅) |
22 | 18, 21 | syl 17 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΆ)π¦) β π΅) |
23 | | eqid 2727 |
. . . . . . 7
β’
(0gβπ
) = (0gβπ
) |
24 | 13, 14, 19, 23 | pmatcoe1fsupp 22590 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ (π₯(.rβπΆ)π¦) β π΅) β βπ β β0 βπ β β0
(π < π β βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
))) |
25 | 11, 12, 22, 24 | syl3anc 1369 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β βπ β β0 βπ β β0
(π < π β βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
))) |
26 | | fvoveq1 7437 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (coe1β(π(π₯(.rβπΆ)π¦)π)) = (coe1β(π(π₯(.rβπΆ)π¦)π))) |
27 | 26 | fveq1d 6893 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ)) |
28 | 27 | eqeq1d 2729 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
) β ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
))) |
29 | | oveq2 7422 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (π(π₯(.rβπΆ)π¦)π) = (π(π₯(.rβπΆ)π¦)π)) |
30 | 29 | fveq2d 6895 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (coe1β(π(π₯(.rβπΆ)π¦)π)) = (coe1β(π(π₯(.rβπΆ)π¦)π))) |
31 | 30 | fveq1d 6893 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ)) |
32 | 31 | eqeq1d 2729 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
) β ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
))) |
33 | 28, 32 | rspc2va 3619 |
. . . . . . . . . . . . . . . 16
β’ (((π β π β§ π β π) β§ βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
)) β ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
)) |
34 | 33 | expcom 413 |
. . . . . . . . . . . . . . 15
β’
(βπ β
π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
) β ((π β π β§ π β π) β ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
))) |
35 | 34 | adantl 481 |
. . . . . . . . . . . . . 14
β’
(((((π β Fin
β§ π
β Ring) β§
(π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β§
βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
)) β ((π β π β§ π β π) β ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
))) |
36 | 35 | 3impib 1114 |
. . . . . . . . . . . . 13
β’
((((((π β Fin
β§ π
β Ring) β§
(π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β§
βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
)) β§ π β π β§ π β π) β ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
)) |
37 | 36 | mpoeq3dva 7491 |
. . . . . . . . . . . 12
β’
(((((π β Fin
β§ π
β Ring) β§
(π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β§
βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
)) β (π β π, π β π β¦ ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ)) = (π β π, π β π β¦ (0gβπ
))) |
38 | | pm2mpfo.a |
. . . . . . . . . . . . . 14
β’ π΄ = (π Mat π
) |
39 | 38, 23 | mat0op 22308 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π
β Ring) β
(0gβπ΄) =
(π β π, π β π β¦ (0gβπ
))) |
40 | 39 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’
(((((π β Fin
β§ π
β Ring) β§
(π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β§
βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
)) β (0gβπ΄) = (π β π, π β π β¦ (0gβπ
))) |
41 | 38 | matring 22332 |
. . . . . . . . . . . . . . 15
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
42 | | pm2mpfo.q |
. . . . . . . . . . . . . . . 16
β’ π = (Poly1βπ΄) |
43 | 42 | ply1sca 22158 |
. . . . . . . . . . . . . . 15
β’ (π΄ β Ring β π΄ = (Scalarβπ)) |
44 | 41, 43 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β Fin β§ π
β Ring) β π΄ = (Scalarβπ)) |
45 | 44 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’
(((((π β Fin
β§ π
β Ring) β§
(π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β§
βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
)) β π΄ = (Scalarβπ)) |
46 | 45 | fveq2d 6895 |
. . . . . . . . . . . 12
β’
(((((π β Fin
β§ π
β Ring) β§
(π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β§
βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
)) β (0gβπ΄) =
(0gβ(Scalarβπ))) |
47 | 37, 40, 46 | 3eqtr2d 2773 |
. . . . . . . . . . 11
β’
(((((π β Fin
β§ π
β Ring) β§
(π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β§
βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
)) β (π β π, π β π β¦ ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ)) = (0gβ(Scalarβπ))) |
48 | 47 | oveq1d 7429 |
. . . . . . . . . 10
β’
(((((π β Fin
β§ π
β Ring) β§
(π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β§
βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
)) β ((π β π, π β π β¦ ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ)) β (π β π)) =
((0gβ(Scalarβπ)) β (π β π))) |
49 | 42 | ply1lmod 22157 |
. . . . . . . . . . . . . 14
β’ (π΄ β Ring β π β LMod) |
50 | 41, 49 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π
β Ring) β π β LMod) |
51 | 50 | adantr 480 |
. . . . . . . . . . . 12
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β π β LMod) |
52 | 41 | adantr 480 |
. . . . . . . . . . . . 13
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β π΄ β Ring) |
53 | | pm2mpfo.x |
. . . . . . . . . . . . . 14
β’ π = (var1βπ΄) |
54 | | eqid 2727 |
. . . . . . . . . . . . . 14
β’
(mulGrpβπ) =
(mulGrpβπ) |
55 | | pm2mpfo.e |
. . . . . . . . . . . . . 14
β’ β =
(.gβ(mulGrpβπ)) |
56 | | pm2mpfo.l |
. . . . . . . . . . . . . 14
β’ πΏ = (Baseβπ) |
57 | 42, 53, 54, 55, 56 | ply1moncl 22177 |
. . . . . . . . . . . . 13
β’ ((π΄ β Ring β§ π β β0)
β (π β π) β πΏ) |
58 | 52, 57 | sylan 579 |
. . . . . . . . . . . 12
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β (π β π) β πΏ) |
59 | | eqid 2727 |
. . . . . . . . . . . . 13
β’
(Scalarβπ) =
(Scalarβπ) |
60 | | pm2mpfo.m |
. . . . . . . . . . . . 13
β’ β = (
Β·π βπ) |
61 | | eqid 2727 |
. . . . . . . . . . . . 13
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
62 | | eqid 2727 |
. . . . . . . . . . . . 13
β’
(0gβπ) = (0gβπ) |
63 | 56, 59, 60, 61, 62 | lmod0vs 20767 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ (π β π) β πΏ) β
((0gβ(Scalarβπ)) β (π β π)) = (0gβπ)) |
64 | 51, 58, 63 | syl2an2r 684 |
. . . . . . . . . . 11
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β
((0gβ(Scalarβπ)) β (π β π)) = (0gβπ)) |
65 | 64 | adantr 480 |
. . . . . . . . . 10
β’
(((((π β Fin
β§ π
β Ring) β§
(π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β§
βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
)) β
((0gβ(Scalarβπ)) β (π β π)) = (0gβπ)) |
66 | 48, 65 | eqtrd 2767 |
. . . . . . . . 9
β’
(((((π β Fin
β§ π
β Ring) β§
(π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β§
βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
)) β ((π β π, π β π β¦ ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ)) β (π β π)) = (0gβπ)) |
67 | 66 | ex 412 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β
(βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
) β ((π β π, π β π β¦ ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ)) β (π β π)) = (0gβπ))) |
68 | 67 | imim2d 57 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β ((π < π β βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
)) β (π < π β ((π β π, π β π β¦ ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ)) β (π β π)) = (0gβπ)))) |
69 | 68 | ralimdva 3162 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (βπ β β0 (π < π β βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
)) β βπ β β0 (π < π β ((π β π, π β π β¦ ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ)) β (π β π)) = (0gβπ)))) |
70 | 69 | reximdv 3165 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (βπ β β0 βπ β β0
(π < π β βπ β π βπ β π ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ) = (0gβπ
)) β βπ β β0 βπ β β0
(π < π β ((π β π, π β π β¦ ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ)) β (π β π)) = (0gβπ)))) |
71 | 25, 70 | mpd 15 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β βπ β β0 βπ β β0
(π < π β ((π β π, π β π β¦ ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ)) β (π β π)) = (0gβπ))) |
72 | 14, 19 | decpmatval 22654 |
. . . . . . . . . 10
β’ (((π₯(.rβπΆ)π¦) β π΅ β§ π β β0) β ((π₯(.rβπΆ)π¦) decompPMat π) = (π β π, π β π β¦ ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ))) |
73 | 22, 72 | sylan 579 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β ((π₯(.rβπΆ)π¦) decompPMat π) = (π β π, π β π β¦ ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ))) |
74 | 73 | oveq1d 7429 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β (((π₯(.rβπΆ)π¦) decompPMat π) β (π β π)) = ((π β π, π β π β¦ ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ)) β (π β π))) |
75 | 74 | eqeq1d 2729 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β ((((π₯(.rβπΆ)π¦) decompPMat π) β (π β π)) = (0gβπ) β ((π β π, π β π β¦ ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ)) β (π β π)) = (0gβπ))) |
76 | 75 | imbi2d 340 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β ((π < π β (((π₯(.rβπΆ)π¦) decompPMat π) β (π β π)) = (0gβπ)) β (π < π β ((π β π, π β π β¦ ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ)) β (π β π)) = (0gβπ)))) |
77 | 76 | ralbidva 3170 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (βπ β β0 (π < π β (((π₯(.rβπΆ)π¦) decompPMat π) β (π β π)) = (0gβπ)) β βπ β β0 (π < π β ((π β π, π β π β¦ ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ)) β (π β π)) = (0gβπ)))) |
78 | 77 | rexbidv 3173 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (βπ β β0 βπ β β0
(π < π β (((π₯(.rβπΆ)π¦) decompPMat π) β (π β π)) = (0gβπ)) β βπ β β0 βπ β β0
(π < π β ((π β π, π β π β¦ ((coe1β(π(π₯(.rβπΆ)π¦)π))βπ)) β (π β π)) = (0gβπ)))) |
79 | 71, 78 | mpbird 257 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β βπ β β0 βπ β β0
(π < π β (((π₯(.rβπΆ)π¦) decompPMat π) β (π β π)) = (0gβπ))) |
80 | 13, 14, 19, 38 | decpmatmul 22661 |
. . . . . . . . . 10
β’ ((π
β Ring β§ (π₯ β π΅ β§ π¦ β π΅) β§ π β β0) β ((π₯(.rβπΆ)π¦) decompPMat π) = (π΄ Ξ£g (π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π)))))) |
81 | 80 | ad4ant234 1173 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β ((π₯(.rβπΆ)π¦) decompPMat π) = (π΄ Ξ£g (π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π)))))) |
82 | 81 | eqcomd 2733 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β (π΄ Ξ£g
(π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π))))) = ((π₯(.rβπΆ)π¦) decompPMat π)) |
83 | 82 | oveq1d 7429 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β ((π΄ Ξ£g
(π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π))))) β (π β π)) = (((π₯(.rβπΆ)π¦) decompPMat π) β (π β π))) |
84 | 83 | eqeq1d 2729 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β (((π΄ Ξ£g
(π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π))))) β (π β π)) = (0gβπ) β (((π₯(.rβπΆ)π¦) decompPMat π) β (π β π)) = (0gβπ))) |
85 | 84 | imbi2d 340 |
. . . . 5
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β β0) β ((π < π β ((π΄ Ξ£g (π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π))))) β (π β π)) = (0gβπ)) β (π < π β (((π₯(.rβπΆ)π¦) decompPMat π) β (π β π)) = (0gβπ)))) |
86 | 85 | ralbidva 3170 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (βπ β β0 (π < π β ((π΄ Ξ£g (π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π))))) β (π β π)) = (0gβπ)) β βπ β β0 (π < π β (((π₯(.rβπΆ)π¦) decompPMat π) β (π β π)) = (0gβπ)))) |
87 | 86 | rexbidv 3173 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (βπ β β0 βπ β β0
(π < π β ((π΄ Ξ£g (π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π))))) β (π β π)) = (0gβπ)) β βπ β β0 βπ β β0
(π < π β (((π₯(.rβπΆ)π¦) decompPMat π) β (π β π)) = (0gβπ)))) |
88 | 79, 87 | mpbird 257 |
. 2
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β βπ β β0 βπ β β0
(π < π β ((π΄ Ξ£g (π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π))))) β (π β π)) = (0gβπ))) |
89 | 1, 2, 10, 88 | mptnn0fsuppd 13987 |
1
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β β0 β¦ ((π΄ Ξ£g
(π β (0...π) β¦ ((π₯ decompPMat π)(.rβπ΄)(π¦ decompPMat (π β π))))) β (π β π))) finSupp (0gβπ)) |