Step | Hyp | Ref
| Expression |
1 | | pmatcollpwscmat.m2 |
. . . . . . . 8
β’ π = (π β 1 ) |
2 | 1 | oveqi 7371 |
. . . . . . 7
β’ (πππ) = (π(π β 1 )π) |
3 | | pmatcollpwscmat.p |
. . . . . . . . . . . 12
β’ π = (Poly1βπ
) |
4 | 3 | ply1ring 21635 |
. . . . . . . . . . 11
β’ (π
β Ring β π β Ring) |
5 | 4 | anim2i 618 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β Ring) β (π β Fin β§ π β Ring)) |
6 | | simpr 486 |
. . . . . . . . . 10
β’ ((πΏ β β0
β§ π β πΈ) β π β πΈ) |
7 | 5, 6 | anim12i 614 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β ((π β Fin β§ π β Ring) β§ π β πΈ)) |
8 | | df-3an 1090 |
. . . . . . . . 9
β’ ((π β Fin β§ π β Ring β§ π β πΈ) β ((π β Fin β§ π β Ring) β§ π β πΈ)) |
9 | 7, 8 | sylibr 233 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β (π β Fin β§ π β Ring β§ π β πΈ)) |
10 | | pmatcollpwscmat.c |
. . . . . . . . 9
β’ πΆ = (π Mat π) |
11 | | pmatcollpwscmat.e2 |
. . . . . . . . 9
β’ πΈ = (Baseβπ) |
12 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβπ) = (0gβπ) |
13 | | pmatcollpwscmat.1 |
. . . . . . . . 9
β’ 1 =
(1rβπΆ) |
14 | | pmatcollpwscmat.m1 |
. . . . . . . . 9
β’ β = (
Β·π βπΆ) |
15 | 10, 11, 12, 13, 14 | scmatscmide 21872 |
. . . . . . . 8
β’ (((π β Fin β§ π β Ring β§ π β πΈ) β§ (π β π β§ π β π)) β (π(π β 1 )π) = if(π = π, π, (0gβπ))) |
16 | 9, 15 | sylan 581 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β§ (π β π β§ π β π)) β (π(π β 1 )π) = if(π = π, π, (0gβπ))) |
17 | 2, 16 | eqtrid 2785 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β§ (π β π β§ π β π)) β (πππ) = if(π = π, π, (0gβπ))) |
18 | 17 | fveq2d 6847 |
. . . . 5
β’ ((((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β§ (π β π β§ π β π)) β (coe1β(πππ)) = (coe1βif(π = π, π, (0gβπ)))) |
19 | 18 | fveq1d 6845 |
. . . 4
β’ ((((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β§ (π β π β§ π β π)) β ((coe1β(πππ))βπΏ) = ((coe1βif(π = π, π, (0gβπ)))βπΏ)) |
20 | | fvif 6859 |
. . . . . 6
β’
(coe1βif(π = π, π, (0gβπ))) = if(π = π, (coe1βπ),
(coe1β(0gβπ))) |
21 | 20 | fveq1i 6844 |
. . . . 5
β’
((coe1βif(π = π, π, (0gβπ)))βπΏ) = (if(π = π, (coe1βπ),
(coe1β(0gβπ)))βπΏ) |
22 | | iffv 6860 |
. . . . 5
β’ (if(π = π, (coe1βπ),
(coe1β(0gβπ)))βπΏ) = if(π = π, ((coe1βπ)βπΏ),
((coe1β(0gβπ))βπΏ)) |
23 | 21, 22 | eqtri 2761 |
. . . 4
β’
((coe1βif(π = π, π, (0gβπ)))βπΏ) = if(π = π, ((coe1βπ)βπΏ),
((coe1β(0gβπ))βπΏ)) |
24 | 19, 23 | eqtrdi 2789 |
. . 3
β’ ((((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β§ (π β π β§ π β π)) β ((coe1β(πππ))βπΏ) = if(π = π, ((coe1βπ)βπΏ),
((coe1β(0gβπ))βπΏ))) |
25 | 24 | oveq1d 7373 |
. 2
β’ ((((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β§ (π β π β§ π β π)) β (((coe1β(πππ))βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) = (if(π = π, ((coe1βπ)βπΏ),
((coe1β(0gβπ))βπΏ))( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
)))) |
26 | | ovif 7455 |
. . 3
β’ (if(π = π, ((coe1βπ)βπΏ),
((coe1β(0gβπ))βπΏ))( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) = if(π = π, (((coe1βπ)βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))),
(((coe1β(0gβπ))βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
)))) |
27 | | eqid 2733 |
. . . . . . . . . . 11
β’
(0gβπ
) = (0gβπ
) |
28 | 3, 12, 27 | coe1z 21650 |
. . . . . . . . . 10
β’ (π
β Ring β
(coe1β(0gβπ)) = (β0 Γ
{(0gβπ
)})) |
29 | 28 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β
(coe1β(0gβπ)) = (β0 Γ
{(0gβπ
)})) |
30 | 29 | fveq1d 6845 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β
((coe1β(0gβπ))βπΏ) = ((β0 Γ
{(0gβπ
)})βπΏ)) |
31 | | fvexd 6858 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β Ring) β
(0gβπ
)
β V) |
32 | | simpl 484 |
. . . . . . . . . 10
β’ ((πΏ β β0
β§ π β πΈ) β πΏ β
β0) |
33 | 31, 32 | anim12i 614 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β
((0gβπ
)
β V β§ πΏ β
β0)) |
34 | | fvconst2g 7152 |
. . . . . . . . 9
β’
(((0gβπ
) β V β§ πΏ β β0) β
((β0 Γ {(0gβπ
)})βπΏ) = (0gβπ
)) |
35 | 33, 34 | syl 17 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β ((β0
Γ {(0gβπ
)})βπΏ) = (0gβπ
)) |
36 | 30, 35 | eqtrd 2773 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β
((coe1β(0gβπ))βπΏ) = (0gβπ
)) |
37 | 36 | oveq1d 7373 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β
(((coe1β(0gβπ))βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) =
((0gβπ
)(
Β·π βπ)(0(.gβ(mulGrpβπ))(var1βπ
)))) |
38 | 3 | ply1lmod 21639 |
. . . . . . . . 9
β’ (π
β Ring β π β LMod) |
39 | 38 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β π β LMod) |
40 | | eqid 2733 |
. . . . . . . . . . 11
β’
(mulGrpβπ) =
(mulGrpβπ) |
41 | 40, 11 | mgpbas 19907 |
. . . . . . . . . 10
β’ πΈ =
(Baseβ(mulGrpβπ)) |
42 | | eqid 2733 |
. . . . . . . . . 10
β’
(.gβ(mulGrpβπ)) =
(.gβ(mulGrpβπ)) |
43 | 40 | ringmgp 19975 |
. . . . . . . . . . 11
β’ (π β Ring β
(mulGrpβπ) β
Mnd) |
44 | 4, 43 | syl 17 |
. . . . . . . . . 10
β’ (π
β Ring β
(mulGrpβπ) β
Mnd) |
45 | | 0nn0 12433 |
. . . . . . . . . . 11
β’ 0 β
β0 |
46 | 45 | a1i 11 |
. . . . . . . . . 10
β’ (π
β Ring β 0 β
β0) |
47 | | eqid 2733 |
. . . . . . . . . . 11
β’
(var1βπ
) = (var1βπ
) |
48 | 47, 3, 11 | vr1cl 21604 |
. . . . . . . . . 10
β’ (π
β Ring β
(var1βπ
)
β πΈ) |
49 | 41, 42, 44, 46, 48 | mulgnn0cld 18902 |
. . . . . . . . 9
β’ (π
β Ring β
(0(.gβ(mulGrpβπ))(var1βπ
)) β πΈ) |
50 | 49 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β
(0(.gβ(mulGrpβπ))(var1βπ
)) β πΈ) |
51 | | eqid 2733 |
. . . . . . . . 9
β’
(Scalarβπ) =
(Scalarβπ) |
52 | | eqid 2733 |
. . . . . . . . 9
β’ (
Β·π βπ) = ( Β·π
βπ) |
53 | | eqid 2733 |
. . . . . . . . 9
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
54 | 11, 51, 52, 53, 12 | lmod0vs 20370 |
. . . . . . . 8
β’ ((π β LMod β§
(0(.gβ(mulGrpβπ))(var1βπ
)) β πΈ) β
((0gβ(Scalarβπ))( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) = (0gβπ)) |
55 | 39, 50, 54 | syl2anc 585 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β
((0gβ(Scalarβπ))( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) = (0gβπ)) |
56 | 3 | ply1sca 21640 |
. . . . . . . . . . . 12
β’ (π
β Ring β π
= (Scalarβπ)) |
57 | 56 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β Ring) β π
= (Scalarβπ)) |
58 | 57 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β Ring) β
(0gβπ
) =
(0gβ(Scalarβπ))) |
59 | 58 | oveq1d 7373 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring) β
((0gβπ
)(
Β·π βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) =
((0gβ(Scalarβπ))( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
)))) |
60 | 59 | eqeq1d 2735 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring) β
(((0gβπ
)(
Β·π βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) = (0gβπ) β
((0gβ(Scalarβπ))( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) = (0gβπ))) |
61 | 60 | adantr 482 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β
(((0gβπ
)(
Β·π βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) = (0gβπ) β
((0gβ(Scalarβπ))( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) = (0gβπ))) |
62 | 55, 61 | mpbird 257 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β
((0gβπ
)(
Β·π βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) = (0gβπ)) |
63 | 37, 62 | eqtrd 2773 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β
(((coe1β(0gβπ))βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) = (0gβπ)) |
64 | 63 | ifeq2d 4507 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β if(π = π, (((coe1βπ)βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))),
(((coe1β(0gβπ))βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
)))) = if(π = π, (((coe1βπ)βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))), (0gβπ))) |
65 | 64 | adantr 482 |
. . 3
β’ ((((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β§ (π β π β§ π β π)) β if(π = π, (((coe1βπ)βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))),
(((coe1β(0gβπ))βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
)))) = if(π = π, (((coe1βπ)βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))), (0gβπ))) |
66 | 26, 65 | eqtrid 2785 |
. 2
β’ ((((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β§ (π β π β§ π β π)) β (if(π = π, ((coe1βπ)βπΏ),
((coe1β(0gβπ))βπΏ))( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) = if(π = π, (((coe1βπ)βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))), (0gβπ))) |
67 | | simpr 486 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β (πΏ β β0 β§ π β πΈ)) |
68 | 67 | ancomd 463 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β (π β πΈ β§ πΏ β
β0)) |
69 | | eqid 2733 |
. . . . . . . . 9
β’
(coe1βπ) = (coe1βπ) |
70 | | pmatcollpwscmat.k |
. . . . . . . . 9
β’ πΎ = (Baseβπ
) |
71 | 69, 11, 3, 70 | coe1fvalcl 21599 |
. . . . . . . 8
β’ ((π β πΈ β§ πΏ β β0) β
((coe1βπ)βπΏ) β πΎ) |
72 | 68, 71 | syl 17 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β
((coe1βπ)βπΏ) β πΎ) |
73 | 56 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ (π
β Ring β
(Scalarβπ) = π
) |
74 | 73 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β Ring) β
(Scalarβπ) = π
) |
75 | 74 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β Ring) β
(Baseβ(Scalarβπ)) = (Baseβπ
)) |
76 | 75, 70 | eqtr4di 2791 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring) β
(Baseβ(Scalarβπ)) = πΎ) |
77 | 76 | eleq2d 2820 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring) β
(((coe1βπ)βπΏ) β (Baseβ(Scalarβπ)) β
((coe1βπ)βπΏ) β πΎ)) |
78 | 77 | adantr 482 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β
(((coe1βπ)βπΏ) β (Baseβ(Scalarβπ)) β
((coe1βπ)βπΏ) β πΎ)) |
79 | 72, 78 | mpbird 257 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β
((coe1βπ)βπΏ) β (Baseβ(Scalarβπ))) |
80 | | pmatcollpwscmat.u |
. . . . . . 7
β’ π = (algScβπ) |
81 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
82 | | eqid 2733 |
. . . . . . 7
β’
(1rβπ) = (1rβπ) |
83 | 80, 51, 81, 52, 82 | asclval 21299 |
. . . . . 6
β’
(((coe1βπ)βπΏ) β (Baseβ(Scalarβπ)) β (πβ((coe1βπ)βπΏ)) = (((coe1βπ)βπΏ)( Β·π
βπ)(1rβπ))) |
84 | 79, 83 | syl 17 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β (πβ((coe1βπ)βπΏ)) = (((coe1βπ)βπΏ)( Β·π
βπ)(1rβπ))) |
85 | 3, 47, 40, 42 | ply1idvr1 21680 |
. . . . . . . 8
β’ (π
β Ring β
(0(.gβ(mulGrpβπ))(var1βπ
)) = (1rβπ)) |
86 | 85 | eqcomd 2739 |
. . . . . . 7
β’ (π
β Ring β
(1rβπ) =
(0(.gβ(mulGrpβπ))(var1βπ
))) |
87 | 86 | ad2antlr 726 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β
(1rβπ) =
(0(.gβ(mulGrpβπ))(var1βπ
))) |
88 | 87 | oveq2d 7374 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β
(((coe1βπ)βπΏ)( Β·π
βπ)(1rβπ)) = (((coe1βπ)βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
)))) |
89 | 84, 88 | eqtr2d 2774 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β
(((coe1βπ)βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) = (πβ((coe1βπ)βπΏ))) |
90 | 89 | ifeq1d 4506 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β if(π = π, (((coe1βπ)βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))), (0gβπ)) = if(π = π, (πβ((coe1βπ)βπΏ)), (0gβπ))) |
91 | 90 | adantr 482 |
. 2
β’ ((((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β§ (π β π β§ π β π)) β if(π = π, (((coe1βπ)βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))), (0gβπ)) = if(π = π, (πβ((coe1βπ)βπΏ)), (0gβπ))) |
92 | 25, 66, 91 | 3eqtrd 2777 |
1
β’ ((((π β Fin β§ π
β Ring) β§ (πΏ β β0
β§ π β πΈ)) β§ (π β π β§ π β π)) β (((coe1β(πππ))βπΏ)( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) = if(π = π, (πβ((coe1βπ)βπΏ)), (0gβπ))) |