Step | Hyp | Ref
| Expression |
1 | | eqid 2731 |
. . 3
β’
(0gβπ
) = (0gβπ
) |
2 | | coe1sclmul.k |
. . 3
β’ πΎ = (Baseβπ
) |
3 | | coe1sclmul.p |
. . 3
β’ π = (Poly1βπ
) |
4 | | eqid 2731 |
. . 3
β’
(var1βπ
) = (var1βπ
) |
5 | | eqid 2731 |
. . 3
β’ (
Β·π βπ) = ( Β·π
βπ) |
6 | | eqid 2731 |
. . 3
β’
(mulGrpβπ) =
(mulGrpβπ) |
7 | | eqid 2731 |
. . 3
β’
(.gβ(mulGrpβπ)) =
(.gβ(mulGrpβπ)) |
8 | | coe1sclmul.b |
. . 3
β’ π΅ = (Baseβπ) |
9 | | coe1sclmul.t |
. . 3
β’ β =
(.rβπ) |
10 | | coe1sclmul.u |
. . 3
β’ Β· =
(.rβπ
) |
11 | | simp3 1137 |
. . 3
β’ ((π
β Ring β§ π β πΎ β§ π β π΅) β π β π΅) |
12 | | simp1 1135 |
. . 3
β’ ((π
β Ring β§ π β πΎ β§ π β π΅) β π
β Ring) |
13 | | simp2 1136 |
. . 3
β’ ((π
β Ring β§ π β πΎ β§ π β π΅) β π β πΎ) |
14 | | 0nn0 12492 |
. . . 4
β’ 0 β
β0 |
15 | 14 | a1i 11 |
. . 3
β’ ((π
β Ring β§ π β πΎ β§ π β π΅) β 0 β
β0) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 15 | coe1tmmul 22020 |
. 2
β’ ((π
β Ring β§ π β πΎ β§ π β π΅) β (coe1β((π(
Β·π βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) β π)) = (π₯ β β0 β¦ if(0 β€
π₯, (π Β·
((coe1βπ)β(π₯ β 0))), (0gβπ
)))) |
17 | | coe1sclmul.a |
. . . . 5
β’ π΄ = (algScβπ) |
18 | 2, 3, 4, 5, 6, 7, 17 | ply1scltm 22024 |
. . . 4
β’ ((π
β Ring β§ π β πΎ) β (π΄βπ) = (π( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
)))) |
19 | 18 | 3adant3 1131 |
. . 3
β’ ((π
β Ring β§ π β πΎ β§ π β π΅) β (π΄βπ) = (π( Β·π
βπ)(0(.gβ(mulGrpβπ))(var1βπ
)))) |
20 | 19 | fvoveq1d 7434 |
. 2
β’ ((π
β Ring β§ π β πΎ β§ π β π΅) β (coe1β((π΄βπ) β π)) = (coe1β((π(
Β·π βπ)(0(.gβ(mulGrpβπ))(var1βπ
))) β π))) |
21 | | nn0ex 12483 |
. . . . 5
β’
β0 β V |
22 | 21 | a1i 11 |
. . . 4
β’ ((π
β Ring β§ π β πΎ β§ π β π΅) β β0 β
V) |
23 | | simpl2 1191 |
. . . 4
β’ (((π
β Ring β§ π β πΎ β§ π β π΅) β§ π₯ β β0) β π β πΎ) |
24 | | fvexd 6907 |
. . . 4
β’ (((π
β Ring β§ π β πΎ β§ π β π΅) β§ π₯ β β0) β
((coe1βπ)βπ₯) β V) |
25 | | fconstmpt 5739 |
. . . . 5
β’
(β0 Γ {π}) = (π₯ β β0 β¦ π) |
26 | 25 | a1i 11 |
. . . 4
β’ ((π
β Ring β§ π β πΎ β§ π β π΅) β (β0 Γ {π}) = (π₯ β β0 β¦ π)) |
27 | | eqid 2731 |
. . . . . . 7
β’
(coe1βπ) = (coe1βπ) |
28 | 27, 8, 3, 2 | coe1f 21955 |
. . . . . 6
β’ (π β π΅ β (coe1βπ):β0βΆπΎ) |
29 | 28 | 3ad2ant3 1134 |
. . . . 5
β’ ((π
β Ring β§ π β πΎ β§ π β π΅) β (coe1βπ):β0βΆπΎ) |
30 | 29 | feqmptd 6961 |
. . . 4
β’ ((π
β Ring β§ π β πΎ β§ π β π΅) β (coe1βπ) = (π₯ β β0 β¦
((coe1βπ)βπ₯))) |
31 | 22, 23, 24, 26, 30 | offval2 7693 |
. . 3
β’ ((π
β Ring β§ π β πΎ β§ π β π΅) β ((β0 Γ
{π}) βf
Β·
(coe1βπ))
= (π₯ β
β0 β¦ (π Β·
((coe1βπ)βπ₯)))) |
32 | | nn0ge0 12502 |
. . . . . 6
β’ (π₯ β β0
β 0 β€ π₯) |
33 | 32 | iftrued 4537 |
. . . . 5
β’ (π₯ β β0
β if(0 β€ π₯, (π Β·
((coe1βπ)β(π₯ β 0))), (0gβπ
)) = (π Β·
((coe1βπ)β(π₯ β 0)))) |
34 | | nn0cn 12487 |
. . . . . . . 8
β’ (π₯ β β0
β π₯ β
β) |
35 | 34 | subid1d 11565 |
. . . . . . 7
β’ (π₯ β β0
β (π₯ β 0) =
π₯) |
36 | 35 | fveq2d 6896 |
. . . . . 6
β’ (π₯ β β0
β ((coe1βπ)β(π₯ β 0)) = ((coe1βπ)βπ₯)) |
37 | 36 | oveq2d 7428 |
. . . . 5
β’ (π₯ β β0
β (π Β·
((coe1βπ)β(π₯ β 0))) = (π Β·
((coe1βπ)βπ₯))) |
38 | 33, 37 | eqtrd 2771 |
. . . 4
β’ (π₯ β β0
β if(0 β€ π₯, (π Β·
((coe1βπ)β(π₯ β 0))), (0gβπ
)) = (π Β·
((coe1βπ)βπ₯))) |
39 | 38 | mpteq2ia 5252 |
. . 3
β’ (π₯ β β0
β¦ if(0 β€ π₯, (π Β·
((coe1βπ)β(π₯ β 0))), (0gβπ
))) = (π₯ β β0 β¦ (π Β·
((coe1βπ)βπ₯))) |
40 | 31, 39 | eqtr4di 2789 |
. 2
β’ ((π
β Ring β§ π β πΎ β§ π β π΅) β ((β0 Γ
{π}) βf
Β·
(coe1βπ))
= (π₯ β
β0 β¦ if(0 β€ π₯, (π Β·
((coe1βπ)β(π₯ β 0))), (0gβπ
)))) |
41 | 16, 20, 40 | 3eqtr4d 2781 |
1
β’ ((π
β Ring β§ π β πΎ β§ π β π΅) β (coe1β((π΄βπ) β π)) = ((β0 Γ {π}) βf Β·
(coe1βπ))) |