Step | Hyp | Ref
| Expression |
1 | | m2cpm.t |
. . . . . . . . 9
β’ π = (π matToPolyMat π
) |
2 | | m2cpm.a |
. . . . . . . . 9
β’ π΄ = (π Mat π
) |
3 | | m2cpm.b |
. . . . . . . . 9
β’ π΅ = (Baseβπ΄) |
4 | | eqid 2733 |
. . . . . . . . 9
β’
(Poly1βπ
) = (Poly1βπ
) |
5 | | eqid 2733 |
. . . . . . . . 9
β’
(algScβ(Poly1βπ
)) =
(algScβ(Poly1βπ
)) |
6 | 1, 2, 3, 4, 5 | mat2pmatvalel 22090 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β (π(πβπ)π) =
((algScβ(Poly1βπ
))β(πππ))) |
7 | 6 | adantr 482 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β§ π β β) β (π(πβπ)π) =
((algScβ(Poly1βπ
))β(πππ))) |
8 | 7 | fveq2d 6847 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β§ π β β) β
(coe1β(π(πβπ)π)) =
(coe1β((algScβ(Poly1βπ
))β(πππ)))) |
9 | 8 | fveq1d 6845 |
. . . . 5
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β§ π β β) β
((coe1β(π(πβπ)π))βπ) =
((coe1β((algScβ(Poly1βπ
))β(πππ)))βπ)) |
10 | | simpl2 1193 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β π
β Ring) |
11 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβπ
) =
(Baseβπ
) |
12 | | simprl 770 |
. . . . . . . . . 10
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β π β π) |
13 | | simprr 772 |
. . . . . . . . . 10
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β π β π) |
14 | | simpl3 1194 |
. . . . . . . . . 10
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β π β π΅) |
15 | 2, 11, 3, 12, 13, 14 | matecld 21791 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β (πππ) β (Baseβπ
)) |
16 | 10, 15 | jca 513 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β (π
β Ring β§ (πππ) β (Baseβπ
))) |
17 | 16 | adantr 482 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β§ π β β) β (π
β Ring β§ (πππ) β (Baseβπ
))) |
18 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπ
) = (0gβπ
) |
19 | 4, 5, 11, 18 | coe1scl 21674 |
. . . . . . 7
β’ ((π
β Ring β§ (πππ) β (Baseβπ
)) β
(coe1β((algScβ(Poly1βπ
))β(πππ))) = (π β β0 β¦ if(π = 0, (πππ), (0gβπ
)))) |
20 | 17, 19 | syl 17 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β§ π β β) β
(coe1β((algScβ(Poly1βπ
))β(πππ))) = (π β β0 β¦ if(π = 0, (πππ), (0gβπ
)))) |
21 | | eqeq1 2737 |
. . . . . . . 8
β’ (π = π β (π = 0 β π = 0)) |
22 | 21 | ifbid 4510 |
. . . . . . 7
β’ (π = π β if(π = 0, (πππ), (0gβπ
)) = if(π = 0, (πππ), (0gβπ
))) |
23 | 22 | adantl 483 |
. . . . . 6
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β π β§ π β π)) β§ π β β) β§ π = π) β if(π = 0, (πππ), (0gβπ
)) = if(π = 0, (πππ), (0gβπ
))) |
24 | | nnnn0 12425 |
. . . . . . 7
β’ (π β β β π β
β0) |
25 | 24 | adantl 483 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β§ π β β) β π β β0) |
26 | | ovex 7391 |
. . . . . . . 8
β’ (πππ) β V |
27 | | fvex 6856 |
. . . . . . . 8
β’
(0gβπ
) β V |
28 | 26, 27 | ifex 4537 |
. . . . . . 7
β’ if(π = 0, (πππ), (0gβπ
)) β V |
29 | 28 | a1i 11 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β§ π β β) β if(π = 0, (πππ), (0gβπ
)) β V) |
30 | 20, 23, 25, 29 | fvmptd 6956 |
. . . . 5
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β§ π β β) β
((coe1β((algScβ(Poly1βπ
))β(πππ)))βπ) = if(π = 0, (πππ), (0gβπ
))) |
31 | | nnne0 12192 |
. . . . . . . 8
β’ (π β β β π β 0) |
32 | 31 | neneqd 2945 |
. . . . . . 7
β’ (π β β β Β¬
π = 0) |
33 | 32 | adantl 483 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β§ π β β) β Β¬ π = 0) |
34 | 33 | iffalsed 4498 |
. . . . 5
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β§ π β β) β if(π = 0, (πππ), (0gβπ
)) = (0gβπ
)) |
35 | 9, 30, 34 | 3eqtrd 2777 |
. . . 4
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β§ π β β) β
((coe1β(π(πβπ)π))βπ) = (0gβπ
)) |
36 | 35 | ralrimiva 3140 |
. . 3
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β π β§ π β π)) β βπ β β
((coe1β(π(πβπ)π))βπ) = (0gβπ
)) |
37 | 36 | ralrimivva 3194 |
. 2
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β βπ β π βπ β π βπ β β
((coe1β(π(πβπ)π))βπ) = (0gβπ
)) |
38 | | eqid 2733 |
. . . 4
β’ (π Mat
(Poly1βπ
))
= (π Mat
(Poly1βπ
)) |
39 | 1, 2, 3, 4, 38 | mat2pmatbas 22091 |
. . 3
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (πβπ) β (Baseβ(π Mat (Poly1βπ
)))) |
40 | | m2cpm.s |
. . . 4
β’ π = (π ConstPolyMat π
) |
41 | | eqid 2733 |
. . . 4
β’
(Baseβ(π Mat
(Poly1βπ
))) = (Baseβ(π Mat (Poly1βπ
))) |
42 | 40, 4, 38, 41 | cpmatel 22076 |
. . 3
β’ ((π β Fin β§ π
β Ring β§ (πβπ) β (Baseβ(π Mat (Poly1βπ
)))) β ((πβπ) β π β βπ β π βπ β π βπ β β
((coe1β(π(πβπ)π))βπ) = (0gβπ
))) |
43 | 39, 42 | syld3an3 1410 |
. 2
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β ((πβπ) β π β βπ β π βπ β π βπ β β
((coe1β(π(πβπ)π))βπ) = (0gβπ
))) |
44 | 37, 43 | mpbird 257 |
1
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (πβπ) β π) |