Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
2 | | ply1fermltlchr.l |
. . 3
β’ + =
(+gβπ) |
3 | | ply1fermltlchr.t |
. . . 4
β’ β =
(.gβπ) |
4 | | ply1fermltlchr.n |
. . . . 5
β’ π = (mulGrpβπ) |
5 | 4 | fveq2i 6849 |
. . . 4
β’
(.gβπ) = (.gβ(mulGrpβπ)) |
6 | 3, 5 | eqtri 2761 |
. . 3
β’ β =
(.gβ(mulGrpβπ)) |
7 | | eqid 2733 |
. . 3
β’
(chrβπ) =
(chrβπ) |
8 | | ply1fermltlchr.f |
. . . 4
β’ (π β πΉ β CRing) |
9 | | ply1fermltlchr.w |
. . . . 5
β’ π = (Poly1βπΉ) |
10 | 9 | ply1crng 21592 |
. . . 4
β’ (πΉ β CRing β π β CRing) |
11 | 8, 10 | syl 17 |
. . 3
β’ (π β π β CRing) |
12 | 9 | ply1chr 32338 |
. . . . . 6
β’ (πΉ β CRing β
(chrβπ) =
(chrβπΉ)) |
13 | 8, 12 | syl 17 |
. . . . 5
β’ (π β (chrβπ) = (chrβπΉ)) |
14 | | ply1fermltlchr.p |
. . . . 5
β’ π = (chrβπΉ) |
15 | 13, 14 | eqtr4di 2791 |
. . . 4
β’ (π β (chrβπ) = π) |
16 | | ply1fermltlchr.1 |
. . . 4
β’ (π β π β β) |
17 | 15, 16 | eqeltrd 2834 |
. . 3
β’ (π β (chrβπ) β
β) |
18 | 8 | crngringd 19985 |
. . . 4
β’ (π β πΉ β Ring) |
19 | | ply1fermltlchr.x |
. . . . 5
β’ π = (var1βπΉ) |
20 | 19, 9, 1 | vr1cl 21611 |
. . . 4
β’ (πΉ β Ring β π β (Baseβπ)) |
21 | 18, 20 | syl 17 |
. . 3
β’ (π β π β (Baseβπ)) |
22 | | ply1fermltlchr.a |
. . . 4
β’ π΄ = (πΆβ((β€RHomβπΉ)βπΈ)) |
23 | | eqid 2733 |
. . . . . . . 8
β’
(β€RHomβπΉ) = (β€RHomβπΉ) |
24 | 23 | zrhrhm 20935 |
. . . . . . 7
β’ (πΉ β Ring β
(β€RHomβπΉ)
β (β€ring RingHom πΉ)) |
25 | | zringbas 20898 |
. . . . . . . 8
β’ β€ =
(Baseββ€ring) |
26 | | eqid 2733 |
. . . . . . . 8
β’
(BaseβπΉ) =
(BaseβπΉ) |
27 | 25, 26 | rhmf 20168 |
. . . . . . 7
β’
((β€RHomβπΉ) β (β€ring RingHom
πΉ) β
(β€RHomβπΉ):β€βΆ(BaseβπΉ)) |
28 | 18, 24, 27 | 3syl 18 |
. . . . . 6
β’ (π β (β€RHomβπΉ):β€βΆ(BaseβπΉ)) |
29 | | ply1fermltlchr.2 |
. . . . . 6
β’ (π β πΈ β β€) |
30 | 28, 29 | ffvelcdmd 7040 |
. . . . 5
β’ (π β ((β€RHomβπΉ)βπΈ) β (BaseβπΉ)) |
31 | | ply1fermltlchr.c |
. . . . . 6
β’ πΆ = (algScβπ) |
32 | 9, 31, 26, 1 | ply1sclcl 21680 |
. . . . 5
β’ ((πΉ β Ring β§
((β€RHomβπΉ)βπΈ) β (BaseβπΉ)) β (πΆβ((β€RHomβπΉ)βπΈ)) β (Baseβπ)) |
33 | 18, 30, 32 | syl2anc 585 |
. . . 4
β’ (π β (πΆβ((β€RHomβπΉ)βπΈ)) β (Baseβπ)) |
34 | 22, 33 | eqeltrid 2838 |
. . 3
β’ (π β π΄ β (Baseβπ)) |
35 | 1, 2, 6, 7, 11, 17, 21, 34 | freshmansdream 32123 |
. 2
β’ (π β ((chrβπ) β (π + π΄)) = (((chrβπ) β π) + ((chrβπ) β π΄))) |
36 | 15 | oveq1d 7376 |
. 2
β’ (π β ((chrβπ) β (π + π΄)) = (π β (π + π΄))) |
37 | 15 | oveq1d 7376 |
. . 3
β’ (π β ((chrβπ) β π) = (π β π)) |
38 | 15 | oveq1d 7376 |
. . . 4
β’ (π β ((chrβπ) β π΄) = (π β π΄)) |
39 | 9 | ply1assa 21593 |
. . . . . . . . 9
β’ (πΉ β CRing β π β AssAlg) |
40 | | eqid 2733 |
. . . . . . . . . 10
β’
(Scalarβπ) =
(Scalarβπ) |
41 | 31, 40 | asclrhm 21316 |
. . . . . . . . 9
β’ (π β AssAlg β πΆ β ((Scalarβπ) RingHom π)) |
42 | 8, 39, 41 | 3syl 18 |
. . . . . . . 8
β’ (π β πΆ β ((Scalarβπ) RingHom π)) |
43 | 8 | crnggrpd 19986 |
. . . . . . . . . 10
β’ (π β πΉ β Grp) |
44 | 9 | ply1sca 21647 |
. . . . . . . . . 10
β’ (πΉ β Grp β πΉ = (Scalarβπ)) |
45 | 43, 44 | syl 17 |
. . . . . . . . 9
β’ (π β πΉ = (Scalarβπ)) |
46 | 45 | oveq1d 7376 |
. . . . . . . 8
β’ (π β (πΉ RingHom π) = ((Scalarβπ) RingHom π)) |
47 | 42, 46 | eleqtrrd 2837 |
. . . . . . 7
β’ (π β πΆ β (πΉ RingHom π)) |
48 | | eqid 2733 |
. . . . . . . 8
β’
(mulGrpβπΉ) =
(mulGrpβπΉ) |
49 | 48, 4 | rhmmhm 20163 |
. . . . . . 7
β’ (πΆ β (πΉ RingHom π) β πΆ β ((mulGrpβπΉ) MndHom π)) |
50 | 47, 49 | syl 17 |
. . . . . 6
β’ (π β πΆ β ((mulGrpβπΉ) MndHom π)) |
51 | | prmnn 16558 |
. . . . . . 7
β’ (π β β β π β
β) |
52 | | nnnn0 12428 |
. . . . . . 7
β’ (π β β β π β
β0) |
53 | 16, 51, 52 | 3syl 18 |
. . . . . 6
β’ (π β π β
β0) |
54 | 48, 26 | mgpbas 19910 |
. . . . . . 7
β’
(BaseβπΉ) =
(Baseβ(mulGrpβπΉ)) |
55 | | eqid 2733 |
. . . . . . 7
β’
(.gβ(mulGrpβπΉ)) =
(.gβ(mulGrpβπΉ)) |
56 | 54, 55, 3 | mhmmulg 18925 |
. . . . . 6
β’ ((πΆ β ((mulGrpβπΉ) MndHom π) β§ π β β0 β§
((β€RHomβπΉ)βπΈ) β (BaseβπΉ)) β (πΆβ(π(.gβ(mulGrpβπΉ))((β€RHomβπΉ)βπΈ))) = (π β (πΆβ((β€RHomβπΉ)βπΈ)))) |
57 | 50, 53, 30, 56 | syl3anc 1372 |
. . . . 5
β’ (π β (πΆβ(π(.gβ(mulGrpβπΉ))((β€RHomβπΉ)βπΈ))) = (π β (πΆβ((β€RHomβπΉ)βπΈ)))) |
58 | 22 | a1i 11 |
. . . . . 6
β’ (π β π΄ = (πΆβ((β€RHomβπΉ)βπΈ))) |
59 | 58 | oveq2d 7377 |
. . . . 5
β’ (π β (π β π΄) = (π β (πΆβ((β€RHomβπΉ)βπΈ)))) |
60 | 57, 59 | eqtr4d 2776 |
. . . 4
β’ (π β (πΆβ(π(.gβ(mulGrpβπΉ))((β€RHomβπΉ)βπΈ))) = (π β π΄)) |
61 | | eqid 2733 |
. . . . . . 7
β’
((β€RHomβπΉ)βπΈ) = ((β€RHomβπΉ)βπΈ) |
62 | 14, 26, 55, 61, 16, 29, 8 | fermltlchr 32208 |
. . . . . 6
β’ (π β (π(.gβ(mulGrpβπΉ))((β€RHomβπΉ)βπΈ)) = ((β€RHomβπΉ)βπΈ)) |
63 | 62 | fveq2d 6850 |
. . . . 5
β’ (π β (πΆβ(π(.gβ(mulGrpβπΉ))((β€RHomβπΉ)βπΈ))) = (πΆβ((β€RHomβπΉ)βπΈ))) |
64 | 63, 22 | eqtr4di 2791 |
. . . 4
β’ (π β (πΆβ(π(.gβ(mulGrpβπΉ))((β€RHomβπΉ)βπΈ))) = π΄) |
65 | 38, 60, 64 | 3eqtr2d 2779 |
. . 3
β’ (π β ((chrβπ) β π΄) = π΄) |
66 | 37, 65 | oveq12d 7379 |
. 2
β’ (π β (((chrβπ) β π) + ((chrβπ) β π΄)) = ((π β π) + π΄)) |
67 | 35, 36, 66 | 3eqtr3d 2781 |
1
β’ (π β (π β (π + π΄)) = ((π β π) + π΄)) |