Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ
) =
(Baseβπ
) |
2 | | eqid 2733 |
. . . . . . . . . . 11
β’
(1rβπ
) = (1rβπ
) |
3 | 1, 2 | ringidcl 19997 |
. . . . . . . . . 10
β’ (π
β Ring β
(1rβπ
)
β (Baseβπ
)) |
4 | 3 | ancli 550 |
. . . . . . . . 9
β’ (π
β Ring β (π
β Ring β§
(1rβπ
)
β (Baseβπ
))) |
5 | 4 | adantl 483 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring) β (π
β Ring β§
(1rβπ
)
β (Baseβπ
))) |
6 | 5 | ad2antrl 727 |
. . . . . . 7
β’ ((π = π β§ ((π β Fin β§ π
β Ring) β§ (π β π β§ π β π))) β (π
β Ring β§
(1rβπ
)
β (Baseβπ
))) |
7 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπ
) = (0gβπ
) |
8 | | cpmatsrngpmat.p |
. . . . . . . 8
β’ π = (Poly1βπ
) |
9 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
10 | | eqid 2733 |
. . . . . . . 8
β’
(algScβπ) =
(algScβπ) |
11 | 1, 7, 8, 9, 10 | cply1coe0 21693 |
. . . . . . 7
β’ ((π
β Ring β§
(1rβπ
)
β (Baseβπ
))
β βπ β
β ((coe1β((algScβπ)β(1rβπ
)))βπ) = (0gβπ
)) |
12 | 6, 11 | syl 17 |
. . . . . 6
β’ ((π = π β§ ((π β Fin β§ π
β Ring) β§ (π β π β§ π β π))) β βπ β β
((coe1β((algScβπ)β(1rβπ
)))βπ) = (0gβπ
)) |
13 | | iftrue 4496 |
. . . . . . . . . . 11
β’ (π = π β if(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))) = ((algScβπ)β(1rβπ
))) |
14 | 13 | fveq2d 6850 |
. . . . . . . . . 10
β’ (π = π β (coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
)))) =
(coe1β((algScβπ)β(1rβπ
)))) |
15 | 14 | fveq1d 6848 |
. . . . . . . . 9
β’ (π = π β ((coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))))βπ) =
((coe1β((algScβπ)β(1rβπ
)))βπ)) |
16 | 15 | eqeq1d 2735 |
. . . . . . . 8
β’ (π = π β (((coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))))βπ) = (0gβπ
) β
((coe1β((algScβπ)β(1rβπ
)))βπ) = (0gβπ
))) |
17 | 16 | ralbidv 3171 |
. . . . . . 7
β’ (π = π β (βπ β β
((coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))))βπ) = (0gβπ
) β βπ β β
((coe1β((algScβπ)β(1rβπ
)))βπ) = (0gβπ
))) |
18 | 17 | adantr 482 |
. . . . . 6
β’ ((π = π β§ ((π β Fin β§ π
β Ring) β§ (π β π β§ π β π))) β (βπ β β
((coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))))βπ) = (0gβπ
) β βπ β β
((coe1β((algScβπ)β(1rβπ
)))βπ) = (0gβπ
))) |
19 | 12, 18 | mpbird 257 |
. . . . 5
β’ ((π = π β§ ((π β Fin β§ π
β Ring) β§ (π β π β§ π β π))) β βπ β β
((coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))))βπ) = (0gβπ
)) |
20 | 1, 7 | ring0cl 19998 |
. . . . . . . . . 10
β’ (π
β Ring β
(0gβπ
)
β (Baseβπ
)) |
21 | 20 | ancli 550 |
. . . . . . . . 9
β’ (π
β Ring β (π
β Ring β§
(0gβπ
)
β (Baseβπ
))) |
22 | 21 | adantl 483 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring) β (π
β Ring β§
(0gβπ
)
β (Baseβπ
))) |
23 | 1, 7, 8, 9, 10 | cply1coe0 21693 |
. . . . . . . 8
β’ ((π
β Ring β§
(0gβπ
)
β (Baseβπ
))
β βπ β
β ((coe1β((algScβπ)β(0gβπ
)))βπ) = (0gβπ
)) |
24 | 22, 23 | syl 17 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β
βπ β β
((coe1β((algScβπ)β(0gβπ
)))βπ) = (0gβπ
)) |
25 | 24 | ad2antrl 727 |
. . . . . 6
β’ ((Β¬
π = π β§ ((π β Fin β§ π
β Ring) β§ (π β π β§ π β π))) β βπ β β
((coe1β((algScβπ)β(0gβπ
)))βπ) = (0gβπ
)) |
26 | | iffalse 4499 |
. . . . . . . . . . 11
β’ (Β¬
π = π β if(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))) = ((algScβπ)β(0gβπ
))) |
27 | 26 | adantr 482 |
. . . . . . . . . 10
β’ ((Β¬
π = π β§ ((π β Fin β§ π
β Ring) β§ (π β π β§ π β π))) β if(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))) = ((algScβπ)β(0gβπ
))) |
28 | 27 | fveq2d 6850 |
. . . . . . . . 9
β’ ((Β¬
π = π β§ ((π β Fin β§ π
β Ring) β§ (π β π β§ π β π))) β (coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
)))) =
(coe1β((algScβπ)β(0gβπ
)))) |
29 | 28 | fveq1d 6848 |
. . . . . . . 8
β’ ((Β¬
π = π β§ ((π β Fin β§ π
β Ring) β§ (π β π β§ π β π))) β ((coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))))βπ) =
((coe1β((algScβπ)β(0gβπ
)))βπ)) |
30 | 29 | eqeq1d 2735 |
. . . . . . 7
β’ ((Β¬
π = π β§ ((π β Fin β§ π
β Ring) β§ (π β π β§ π β π))) β (((coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))))βπ) = (0gβπ
) β
((coe1β((algScβπ)β(0gβπ
)))βπ) = (0gβπ
))) |
31 | 30 | ralbidv 3171 |
. . . . . 6
β’ ((Β¬
π = π β§ ((π β Fin β§ π
β Ring) β§ (π β π β§ π β π))) β (βπ β β
((coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))))βπ) = (0gβπ
) β βπ β β
((coe1β((algScβπ)β(0gβπ
)))βπ) = (0gβπ
))) |
32 | 25, 31 | mpbird 257 |
. . . . 5
β’ ((Β¬
π = π β§ ((π β Fin β§ π
β Ring) β§ (π β π β§ π β π))) β βπ β β
((coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))))βπ) = (0gβπ
)) |
33 | 19, 32 | pm2.61ian 811 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β βπ β β
((coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))))βπ) = (0gβπ
)) |
34 | 33 | ralrimivva 3194 |
. . 3
β’ ((π β Fin β§ π
β Ring) β
βπ β π βπ β π βπ β β
((coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))))βπ) = (0gβπ
)) |
35 | | cpmatsrngpmat.c |
. . . . . . . . 9
β’ πΆ = (π Mat π) |
36 | | simpll 766 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β π β Fin) |
37 | | simplr 768 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β π
β Ring) |
38 | | simprl 770 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β π β π) |
39 | | simprr 772 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β π β π) |
40 | | eqid 2733 |
. . . . . . . . 9
β’
(1rβπΆ) = (1rβπΆ) |
41 | 8, 35, 10, 7, 2, 36, 37, 38, 39, 40 | pmat1ovscd 22072 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β (π(1rβπΆ)π) = if(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
)))) |
42 | 41 | fveq2d 6850 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β (coe1β(π(1rβπΆ)π)) = (coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))))) |
43 | 42 | fveq1d 6848 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β ((coe1β(π(1rβπΆ)π))βπ) = ((coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))))βπ)) |
44 | 43 | eqeq1d 2735 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β (((coe1β(π(1rβπΆ)π))βπ) = (0gβπ
) β ((coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))))βπ) = (0gβπ
))) |
45 | 44 | ralbidv 3171 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π β π β§ π β π)) β (βπ β β
((coe1β(π(1rβπΆ)π))βπ) = (0gβπ
) β βπ β β
((coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))))βπ) = (0gβπ
))) |
46 | 45 | 2ralbidva 3207 |
. . 3
β’ ((π β Fin β§ π
β Ring) β
(βπ β π βπ β π βπ β β
((coe1β(π(1rβπΆ)π))βπ) = (0gβπ
) β βπ β π βπ β π βπ β β
((coe1βif(π = π, ((algScβπ)β(1rβπ
)), ((algScβπ)β(0gβπ
))))βπ) = (0gβπ
))) |
47 | 34, 46 | mpbird 257 |
. 2
β’ ((π β Fin β§ π
β Ring) β
βπ β π βπ β π βπ β β
((coe1β(π(1rβπΆ)π))βπ) = (0gβπ
)) |
48 | 8, 35 | pmatring 22064 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β πΆ β Ring) |
49 | | eqid 2733 |
. . . . 5
β’
(BaseβπΆ) =
(BaseβπΆ) |
50 | 49, 40 | ringidcl 19997 |
. . . 4
β’ (πΆ β Ring β
(1rβπΆ)
β (BaseβπΆ)) |
51 | 48, 50 | syl 17 |
. . 3
β’ ((π β Fin β§ π
β Ring) β
(1rβπΆ)
β (BaseβπΆ)) |
52 | | cpmatsrngpmat.s |
. . . 4
β’ π = (π ConstPolyMat π
) |
53 | 52, 8, 35, 49 | cpmatel 22083 |
. . 3
β’ ((π β Fin β§ π
β Ring β§
(1rβπΆ)
β (BaseβπΆ))
β ((1rβπΆ) β π β βπ β π βπ β π βπ β β
((coe1β(π(1rβπΆ)π))βπ) = (0gβπ
))) |
54 | 51, 53 | mpd3an3 1463 |
. 2
β’ ((π β Fin β§ π
β Ring) β
((1rβπΆ)
β π β
βπ β π βπ β π βπ β β
((coe1β(π(1rβπΆ)π))βπ) = (0gβπ
))) |
55 | 47, 54 | mpbird 257 |
1
β’ ((π β Fin β§ π
β Ring) β
(1rβπΆ)
β π) |