Step | Hyp | Ref
| Expression |
1 | | m2cpminvid2lem.s |
. . . . . . . 8
β’ π = (π ConstPolyMat π
) |
2 | | m2cpminvid2lem.p |
. . . . . . . 8
β’ π = (Poly1βπ
) |
3 | | eqid 2733 |
. . . . . . . 8
β’ (π Mat π) = (π Mat π) |
4 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβ(π Mat
π)) = (Baseβ(π Mat π)) |
5 | 1, 2, 3, 4 | cpmatelimp 22077 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β (π β π β (π β (Baseβ(π Mat π)) β§ βπ β π βπ β π βπ β β
((coe1β(πππ))βπ) = (0gβπ
)))) |
6 | 5 | 3impia 1118 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ π β π) β (π β (Baseβ(π Mat π)) β§ βπ β π βπ β π βπ β β
((coe1β(πππ))βπ) = (0gβπ
))) |
7 | 6 | simprd 497 |
. . . . 5
β’ ((π β Fin β§ π
β Ring β§ π β π) β βπ β π βπ β π βπ β β
((coe1β(πππ))βπ) = (0gβπ
)) |
8 | 7 | adantr 482 |
. . . 4
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β βπ β π βπ β π βπ β β
((coe1β(πππ))βπ) = (0gβπ
)) |
9 | | fvoveq1 7381 |
. . . . . . . . . 10
β’ (π = π₯ β (coe1β(πππ)) = (coe1β(π₯ππ))) |
10 | 9 | fveq1d 6845 |
. . . . . . . . 9
β’ (π = π₯ β ((coe1β(πππ))βπ) = ((coe1β(π₯ππ))βπ)) |
11 | 10 | eqeq1d 2735 |
. . . . . . . 8
β’ (π = π₯ β (((coe1β(πππ))βπ) = (0gβπ
) β ((coe1β(π₯ππ))βπ) = (0gβπ
))) |
12 | 11 | ralbidv 3171 |
. . . . . . 7
β’ (π = π₯ β (βπ β β
((coe1β(πππ))βπ) = (0gβπ
) β βπ β β
((coe1β(π₯ππ))βπ) = (0gβπ
))) |
13 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π = π¦ β (π₯ππ) = (π₯ππ¦)) |
14 | 13 | fveq2d 6847 |
. . . . . . . . . 10
β’ (π = π¦ β (coe1β(π₯ππ)) = (coe1β(π₯ππ¦))) |
15 | 14 | fveq1d 6845 |
. . . . . . . . 9
β’ (π = π¦ β ((coe1β(π₯ππ))βπ) = ((coe1β(π₯ππ¦))βπ)) |
16 | 15 | eqeq1d 2735 |
. . . . . . . 8
β’ (π = π¦ β (((coe1β(π₯ππ))βπ) = (0gβπ
) β ((coe1β(π₯ππ¦))βπ) = (0gβπ
))) |
17 | 16 | ralbidv 3171 |
. . . . . . 7
β’ (π = π¦ β (βπ β β
((coe1β(π₯ππ))βπ) = (0gβπ
) β βπ β β
((coe1β(π₯ππ¦))βπ) = (0gβπ
))) |
18 | 12, 17 | rspc2v 3589 |
. . . . . 6
β’ ((π₯ β π β§ π¦ β π) β (βπ β π βπ β π βπ β β
((coe1β(πππ))βπ) = (0gβπ
) β βπ β β
((coe1β(π₯ππ¦))βπ) = (0gβπ
))) |
19 | 18 | adantl 483 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β (βπ β π βπ β π βπ β β
((coe1β(πππ))βπ) = (0gβπ
) β βπ β β
((coe1β(π₯ππ¦))βπ) = (0gβπ
))) |
20 | | fveqeq2 6852 |
. . . . . . 7
β’ (π = π β (((coe1β(π₯ππ¦))βπ) = (0gβπ
) β ((coe1β(π₯ππ¦))βπ) = (0gβπ
))) |
21 | 20 | cbvralvw 3224 |
. . . . . 6
β’
(βπ β
β ((coe1β(π₯ππ¦))βπ) = (0gβπ
) β βπ β β
((coe1β(π₯ππ¦))βπ) = (0gβπ
)) |
22 | | simpl2 1193 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β π
β Ring) |
23 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
(Baseβπ) =
(Baseβπ) |
24 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β π₯ β π) |
25 | | simprr 772 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β π¦ β π) |
26 | 1, 2, 3, 4 | cpmatpmat 22075 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β Fin β§ π
β Ring β§ π β π) β π β (Baseβ(π Mat π))) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β π β (Baseβ(π Mat π))) |
28 | 3, 23, 4, 24, 25, 27 | matecld 21791 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦) β (Baseβπ)) |
29 | | 0nn0 12433 |
. . . . . . . . . . . . . . . . . 18
β’ 0 β
β0 |
30 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
(coe1β(π₯ππ¦)) = (coe1β(π₯ππ¦)) |
31 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
(Baseβπ
) =
(Baseβπ
) |
32 | 30, 23, 2, 31 | coe1fvalcl 21599 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ππ¦) β (Baseβπ) β§ 0 β β0) β
((coe1β(π₯ππ¦))β0) β (Baseβπ
)) |
33 | 28, 29, 32 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β ((coe1β(π₯ππ¦))β0) β (Baseβπ
)) |
34 | 22, 33 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β (π
β Ring β§
((coe1β(π₯ππ¦))β0) β (Baseβπ
))) |
35 | 34 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β§ π β β) β (π
β Ring β§
((coe1β(π₯ππ¦))β0) β (Baseβπ
))) |
36 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(algScβπ) =
(algScβπ) |
37 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(0gβπ
) = (0gβπ
) |
38 | 2, 36, 31, 37 | coe1scl 21674 |
. . . . . . . . . . . . . . 15
β’ ((π
β Ring β§
((coe1β(π₯ππ¦))β0) β (Baseβπ
)) β
(coe1β((algScβπ)β((coe1β(π₯ππ¦))β0))) = (π β β0 β¦ if(π = 0,
((coe1β(π₯ππ¦))β0), (0gβπ
)))) |
39 | 35, 38 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β§ π β β) β
(coe1β((algScβπ)β((coe1β(π₯ππ¦))β0))) = (π β β0 β¦ if(π = 0,
((coe1β(π₯ππ¦))β0), (0gβπ
)))) |
40 | 39 | fveq1d 6845 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β§ π β β) β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((π β β0 β¦ if(π = 0,
((coe1β(π₯ππ¦))β0), (0gβπ
)))βπ)) |
41 | | eqidd 2734 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β§ π β β) β (π β β0 β¦ if(π = 0,
((coe1β(π₯ππ¦))β0), (0gβπ
))) = (π β β0 β¦ if(π = 0,
((coe1β(π₯ππ¦))β0), (0gβπ
)))) |
42 | | eqeq1 2737 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π = 0 β π = 0)) |
43 | 42 | ifbid 4510 |
. . . . . . . . . . . . . . 15
β’ (π = π β if(π = 0, ((coe1β(π₯ππ¦))β0), (0gβπ
)) = if(π = 0, ((coe1β(π₯ππ¦))β0), (0gβπ
))) |
44 | 43 | adantl 483 |
. . . . . . . . . . . . . 14
β’
(((((π β Fin
β§ π
β Ring β§
π β π) β§ (π₯ β π β§ π¦ β π)) β§ π β β) β§ π = π) β if(π = 0, ((coe1β(π₯ππ¦))β0), (0gβπ
)) = if(π = 0, ((coe1β(π₯ππ¦))β0), (0gβπ
))) |
45 | | nnnn0 12425 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β0) |
46 | 45 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β§ π β β) β π β β0) |
47 | | fvex 6856 |
. . . . . . . . . . . . . . . 16
β’
((coe1β(π₯ππ¦))β0) β V |
48 | | fvex 6856 |
. . . . . . . . . . . . . . . 16
β’
(0gβπ
) β V |
49 | 47, 48 | ifex 4537 |
. . . . . . . . . . . . . . 15
β’ if(π = 0,
((coe1β(π₯ππ¦))β0), (0gβπ
)) β V |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β§ π β β) β if(π = 0, ((coe1β(π₯ππ¦))β0), (0gβπ
)) β V) |
51 | 41, 44, 46, 50 | fvmptd 6956 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β§ π β β) β ((π β β0 β¦ if(π = 0,
((coe1β(π₯ππ¦))β0), (0gβπ
)))βπ) = if(π = 0, ((coe1β(π₯ππ¦))β0), (0gβπ
))) |
52 | | nnne0 12192 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β 0) |
53 | 52 | neneqd 2945 |
. . . . . . . . . . . . . . 15
β’ (π β β β Β¬
π = 0) |
54 | 53 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β§ π β β) β Β¬ π = 0) |
55 | 54 | iffalsed 4498 |
. . . . . . . . . . . . 13
β’ ((((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β§ π β β) β if(π = 0, ((coe1β(π₯ππ¦))β0), (0gβπ
)) = (0gβπ
)) |
56 | 40, 51, 55 | 3eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β§ π β β) β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = (0gβπ
)) |
57 | | eqcom 2740 |
. . . . . . . . . . . . 13
β’
(((coe1β(π₯ππ¦))βπ) = (0gβπ
) β (0gβπ
) =
((coe1β(π₯ππ¦))βπ)) |
58 | 57 | biimpi 215 |
. . . . . . . . . . . 12
β’
(((coe1β(π₯ππ¦))βπ) = (0gβπ
) β (0gβπ
) =
((coe1β(π₯ππ¦))βπ)) |
59 | 56, 58 | sylan9eq 2793 |
. . . . . . . . . . 11
β’
(((((π β Fin
β§ π
β Ring β§
π β π) β§ (π₯ β π β§ π¦ β π)) β§ π β β) β§
((coe1β(π₯ππ¦))βπ) = (0gβπ
)) β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ)) |
60 | 59 | ex 414 |
. . . . . . . . . 10
β’ ((((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β§ π β β) β
(((coe1β(π₯ππ¦))βπ) = (0gβπ
) β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ))) |
61 | 60 | ralimdva 3161 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β (βπ β β
((coe1β(π₯ππ¦))βπ) = (0gβπ
) β βπ β β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ))) |
62 | 61 | imp 408 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β§ βπ β β
((coe1β(π₯ππ¦))βπ) = (0gβπ
)) β βπ β β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ)) |
63 | 34 | adantr 482 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β§ βπ β β
((coe1β(π₯ππ¦))βπ) = (0gβπ
)) β (π
β Ring β§
((coe1β(π₯ππ¦))β0) β (Baseβπ
))) |
64 | 2, 36, 31 | ply1sclid 21675 |
. . . . . . . . . 10
β’ ((π
β Ring β§
((coe1β(π₯ππ¦))β0) β (Baseβπ
)) β
((coe1β(π₯ππ¦))β0) =
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))β0)) |
65 | 64 | eqcomd 2739 |
. . . . . . . . 9
β’ ((π
β Ring β§
((coe1β(π₯ππ¦))β0) β (Baseβπ
)) β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))β0) =
((coe1β(π₯ππ¦))β0)) |
66 | 63, 65 | syl 17 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β§ βπ β β
((coe1β(π₯ππ¦))βπ) = (0gβπ
)) β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))β0) =
((coe1β(π₯ππ¦))β0)) |
67 | 62, 66 | jca 513 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β§ βπ β β
((coe1β(π₯ππ¦))βπ) = (0gβπ
)) β (βπ β β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ) β§
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))β0) =
((coe1β(π₯ππ¦))β0))) |
68 | 67 | ex 414 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β (βπ β β
((coe1β(π₯ππ¦))βπ) = (0gβπ
) β (βπ β β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ) β§
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))β0) =
((coe1β(π₯ππ¦))β0)))) |
69 | 21, 68 | biimtrid 241 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β (βπ β β
((coe1β(π₯ππ¦))βπ) = (0gβπ
) β (βπ β β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ) β§
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))β0) =
((coe1β(π₯ππ¦))β0)))) |
70 | 19, 69 | syld 47 |
. . . 4
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β (βπ β π βπ β π βπ β β
((coe1β(πππ))βπ) = (0gβπ
) β (βπ β β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ) β§
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))β0) =
((coe1β(π₯ππ¦))β0)))) |
71 | 8, 70 | mpd 15 |
. . 3
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β (βπ β β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ) β§
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))β0) =
((coe1β(π₯ππ¦))β0))) |
72 | | c0ex 11154 |
. . . 4
β’ 0 β
V |
73 | | fveq2 6843 |
. . . . . 6
β’ (π = 0 β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) =
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))β0)) |
74 | | fveq2 6843 |
. . . . . 6
β’ (π = 0 β
((coe1β(π₯ππ¦))βπ) = ((coe1β(π₯ππ¦))β0)) |
75 | 73, 74 | eqeq12d 2749 |
. . . . 5
β’ (π = 0 β
(((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ) β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))β0) =
((coe1β(π₯ππ¦))β0))) |
76 | 75 | ralunsn 4852 |
. . . 4
β’ (0 β
V β (βπ β
(β βͺ {0})((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ) β (βπ β β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ) β§
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))β0) =
((coe1β(π₯ππ¦))β0)))) |
77 | 72, 76 | mp1i 13 |
. . 3
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β (βπ β (β βͺ
{0})((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ) β (βπ β β
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ) β§
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))β0) =
((coe1β(π₯ππ¦))β0)))) |
78 | 71, 77 | mpbird 257 |
. 2
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β βπ β (β βͺ
{0})((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ)) |
79 | | df-n0 12419 |
. . 3
β’
β0 = (β βͺ {0}) |
80 | 79 | raleqi 3310 |
. 2
β’
(βπ β
β0 ((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ) β βπ β (β βͺ
{0})((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ)) |
81 | 78, 80 | sylibr 233 |
1
β’ (((π β Fin β§ π
β Ring β§ π β π) β§ (π₯ β π β§ π¦ β π)) β βπ β β0
((coe1β((algScβπ)β((coe1β(π₯ππ¦))β0)))βπ) = ((coe1β(π₯ππ¦))βπ)) |