Step | Hyp | Ref
| Expression |
1 | | expclzlem 13998 |
. . . 4
β’ ((π΄ β β β§ π΄ β 0 β§ π₯ β β€) β (π΄βπ₯) β (β β
{0})) |
2 | 1 | 3expa 1119 |
. . 3
β’ (((π΄ β β β§ π΄ β 0) β§ π₯ β β€) β (π΄βπ₯) β (β β
{0})) |
3 | 2 | fmpttd 7067 |
. 2
β’ ((π΄ β β β§ π΄ β 0) β (π₯ β β€ β¦ (π΄βπ₯)):β€βΆ(β β
{0})) |
4 | | expaddz 14021 |
. . . 4
β’ (((π΄ β β β§ π΄ β 0) β§ (π¦ β β€ β§ π§ β β€)) β (π΄β(π¦ + π§)) = ((π΄βπ¦) Β· (π΄βπ§))) |
5 | | zaddcl 12551 |
. . . . . 6
β’ ((π¦ β β€ β§ π§ β β€) β (π¦ + π§) β β€) |
6 | 5 | adantl 483 |
. . . . 5
β’ (((π΄ β β β§ π΄ β 0) β§ (π¦ β β€ β§ π§ β β€)) β (π¦ + π§) β β€) |
7 | | oveq2 7369 |
. . . . . 6
β’ (π₯ = (π¦ + π§) β (π΄βπ₯) = (π΄β(π¦ + π§))) |
8 | | eqid 2733 |
. . . . . 6
β’ (π₯ β β€ β¦ (π΄βπ₯)) = (π₯ β β€ β¦ (π΄βπ₯)) |
9 | | ovex 7394 |
. . . . . 6
β’ (π΄β(π¦ + π§)) β V |
10 | 7, 8, 9 | fvmpt 6952 |
. . . . 5
β’ ((π¦ + π§) β β€ β ((π₯ β β€ β¦ (π΄βπ₯))β(π¦ + π§)) = (π΄β(π¦ + π§))) |
11 | 6, 10 | syl 17 |
. . . 4
β’ (((π΄ β β β§ π΄ β 0) β§ (π¦ β β€ β§ π§ β β€)) β ((π₯ β β€ β¦ (π΄βπ₯))β(π¦ + π§)) = (π΄β(π¦ + π§))) |
12 | | oveq2 7369 |
. . . . . . 7
β’ (π₯ = π¦ β (π΄βπ₯) = (π΄βπ¦)) |
13 | | ovex 7394 |
. . . . . . 7
β’ (π΄βπ¦) β V |
14 | 12, 8, 13 | fvmpt 6952 |
. . . . . 6
β’ (π¦ β β€ β ((π₯ β β€ β¦ (π΄βπ₯))βπ¦) = (π΄βπ¦)) |
15 | | oveq2 7369 |
. . . . . . 7
β’ (π₯ = π§ β (π΄βπ₯) = (π΄βπ§)) |
16 | | ovex 7394 |
. . . . . . 7
β’ (π΄βπ§) β V |
17 | 15, 8, 16 | fvmpt 6952 |
. . . . . 6
β’ (π§ β β€ β ((π₯ β β€ β¦ (π΄βπ₯))βπ§) = (π΄βπ§)) |
18 | 14, 17 | oveqan12d 7380 |
. . . . 5
β’ ((π¦ β β€ β§ π§ β β€) β (((π₯ β β€ β¦ (π΄βπ₯))βπ¦) Β· ((π₯ β β€ β¦ (π΄βπ₯))βπ§)) = ((π΄βπ¦) Β· (π΄βπ§))) |
19 | 18 | adantl 483 |
. . . 4
β’ (((π΄ β β β§ π΄ β 0) β§ (π¦ β β€ β§ π§ β β€)) β
(((π₯ β β€ β¦
(π΄βπ₯))βπ¦) Β· ((π₯ β β€ β¦ (π΄βπ₯))βπ§)) = ((π΄βπ¦) Β· (π΄βπ§))) |
20 | 4, 11, 19 | 3eqtr4d 2783 |
. . 3
β’ (((π΄ β β β§ π΄ β 0) β§ (π¦ β β€ β§ π§ β β€)) β ((π₯ β β€ β¦ (π΄βπ₯))β(π¦ + π§)) = (((π₯ β β€ β¦ (π΄βπ₯))βπ¦) Β· ((π₯ β β€ β¦ (π΄βπ₯))βπ§))) |
21 | 20 | ralrimivva 3194 |
. 2
β’ ((π΄ β β β§ π΄ β 0) β βπ¦ β β€ βπ§ β β€ ((π₯ β β€ β¦ (π΄βπ₯))β(π¦ + π§)) = (((π₯ β β€ β¦ (π΄βπ₯))βπ¦) Β· ((π₯ β β€ β¦ (π΄βπ₯))βπ§))) |
22 | | zringgrp 20897 |
. . . 4
β’
β€ring β Grp |
23 | | cnring 20842 |
. . . . 5
β’
βfld β Ring |
24 | | cnfldbas 20823 |
. . . . . . 7
β’ β =
(Baseββfld) |
25 | | cnfld0 20844 |
. . . . . . 7
β’ 0 =
(0gββfld) |
26 | | cndrng 20849 |
. . . . . . 7
β’
βfld β DivRing |
27 | 24, 25, 26 | drngui 20225 |
. . . . . 6
β’ (β
β {0}) = (Unitββfld) |
28 | | expghm.u |
. . . . . . 7
β’ π = (π βΎs (β β
{0})) |
29 | | expghm.m |
. . . . . . . 8
β’ π =
(mulGrpββfld) |
30 | 29 | oveq1i 7371 |
. . . . . . 7
β’ (π βΎs (β
β {0})) = ((mulGrpββfld) βΎs
(β β {0})) |
31 | 28, 30 | eqtri 2761 |
. . . . . 6
β’ π =
((mulGrpββfld) βΎs (β β
{0})) |
32 | 27, 31 | unitgrp 20104 |
. . . . 5
β’
(βfld β Ring β π β Grp) |
33 | 23, 32 | ax-mp 5 |
. . . 4
β’ π β Grp |
34 | 22, 33 | pm3.2i 472 |
. . 3
β’
(β€ring β Grp β§ π β Grp) |
35 | | zringbas 20898 |
. . . 4
β’ β€ =
(Baseββ€ring) |
36 | | difss 4095 |
. . . . 5
β’ (β
β {0}) β β |
37 | 29, 24 | mgpbas 19910 |
. . . . . 6
β’ β =
(Baseβπ) |
38 | 28, 37 | ressbas2 17128 |
. . . . 5
β’ ((β
β {0}) β β β (β β {0}) = (Baseβπ)) |
39 | 36, 38 | ax-mp 5 |
. . . 4
β’ (β
β {0}) = (Baseβπ) |
40 | | zringplusg 20899 |
. . . 4
β’ + =
(+gββ€ring) |
41 | 27 | fvexi 6860 |
. . . . 5
β’ (β
β {0}) β V |
42 | | cnfldmul 20825 |
. . . . . . 7
β’ Β·
= (.rββfld) |
43 | 29, 42 | mgpplusg 19908 |
. . . . . 6
β’ Β·
= (+gβπ) |
44 | 28, 43 | ressplusg 17179 |
. . . . 5
β’ ((β
β {0}) β V β Β· = (+gβπ)) |
45 | 41, 44 | ax-mp 5 |
. . . 4
β’ Β·
= (+gβπ) |
46 | 35, 39, 40, 45 | isghm 19016 |
. . 3
β’ ((π₯ β β€ β¦ (π΄βπ₯)) β (β€ring GrpHom
π) β
((β€ring β Grp β§ π β Grp) β§ ((π₯ β β€ β¦ (π΄βπ₯)):β€βΆ(β β {0}) β§
βπ¦ β β€
βπ§ β β€
((π₯ β β€ β¦
(π΄βπ₯))β(π¦ + π§)) = (((π₯ β β€ β¦ (π΄βπ₯))βπ¦) Β· ((π₯ β β€ β¦ (π΄βπ₯))βπ§))))) |
47 | 34, 46 | mpbiran 708 |
. 2
β’ ((π₯ β β€ β¦ (π΄βπ₯)) β (β€ring GrpHom
π) β ((π₯ β β€ β¦ (π΄βπ₯)):β€βΆ(β β {0}) β§
βπ¦ β β€
βπ§ β β€
((π₯ β β€ β¦
(π΄βπ₯))β(π¦ + π§)) = (((π₯ β β€ β¦ (π΄βπ₯))βπ¦) Β· ((π₯ β β€ β¦ (π΄βπ₯))βπ§)))) |
48 | 3, 21, 47 | sylanbrc 584 |
1
β’ ((π΄ β β β§ π΄ β 0) β (π₯ β β€ β¦ (π΄βπ₯)) β (β€ring GrpHom
π)) |