Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. 2
β’
(Baseβ(βfld βΎs π)) = (Baseβ(βfld
βΎs π)) |
2 | | eqid 2733 |
. 2
β’
(BaseβπΊ) =
(BaseβπΊ) |
3 | | eqid 2733 |
. 2
β’
(+gβ(βfld βΎs π)) =
(+gβ(βfld βΎs π)) |
4 | | eqid 2733 |
. 2
β’
(+gβπΊ) = (+gβπΊ) |
5 | | simp1 1137 |
. . 3
β’ ((π β§ π₯ β (Baseβ(βfld
βΎs π))
β§ π¦ β
(Baseβ(βfld βΎs π))) β π) |
6 | | simp2 1138 |
. . . 4
β’ ((π β§ π₯ β (Baseβ(βfld
βΎs π))
β§ π¦ β
(Baseβ(βfld βΎs π))) β π₯ β (Baseβ(βfld
βΎs π))) |
7 | | efabl.4 |
. . . . . 6
β’ (π β π β
(SubGrpββfld)) |
8 | | eqid 2733 |
. . . . . . 7
β’
(βfld βΎs π) = (βfld
βΎs π) |
9 | 8 | subgbas 19005 |
. . . . . 6
β’ (π β
(SubGrpββfld) β π = (Baseβ(βfld
βΎs π))) |
10 | 7, 9 | syl 17 |
. . . . 5
β’ (π β π = (Baseβ(βfld
βΎs π))) |
11 | 10 | 3ad2ant1 1134 |
. . . 4
β’ ((π β§ π₯ β (Baseβ(βfld
βΎs π))
β§ π¦ β
(Baseβ(βfld βΎs π))) β π = (Baseβ(βfld
βΎs π))) |
12 | 6, 11 | eleqtrrd 2837 |
. . 3
β’ ((π β§ π₯ β (Baseβ(βfld
βΎs π))
β§ π¦ β
(Baseβ(βfld βΎs π))) β π₯ β π) |
13 | | simp3 1139 |
. . . 4
β’ ((π β§ π₯ β (Baseβ(βfld
βΎs π))
β§ π¦ β
(Baseβ(βfld βΎs π))) β π¦ β (Baseβ(βfld
βΎs π))) |
14 | 13, 11 | eleqtrrd 2837 |
. . 3
β’ ((π β§ π₯ β (Baseβ(βfld
βΎs π))
β§ π¦ β
(Baseβ(βfld βΎs π))) β π¦ β π) |
15 | | efabl.3 |
. . . . . 6
β’ (π β π΄ β β) |
16 | 15, 7 | jca 513 |
. . . . 5
β’ (π β (π΄ β β β§ π β
(SubGrpββfld))) |
17 | | efabl.1 |
. . . . . 6
β’ πΉ = (π₯ β π β¦ (expβ(π΄ Β· π₯))) |
18 | 17 | efgh 26042 |
. . . . 5
β’ (((π΄ β β β§ π β
(SubGrpββfld)) β§ π₯ β π β§ π¦ β π) β (πΉβ(π₯ + π¦)) = ((πΉβπ₯) Β· (πΉβπ¦))) |
19 | 16, 18 | syl3an1 1164 |
. . . 4
β’ ((π β§ π₯ β π β§ π¦ β π) β (πΉβ(π₯ + π¦)) = ((πΉβπ₯) Β· (πΉβπ¦))) |
20 | | cnfldadd 20942 |
. . . . . . . . 9
β’ + =
(+gββfld) |
21 | 8, 20 | ressplusg 17232 |
. . . . . . . 8
β’ (π β
(SubGrpββfld) β + =
(+gβ(βfld βΎs π))) |
22 | 7, 21 | syl 17 |
. . . . . . 7
β’ (π β + =
(+gβ(βfld βΎs π))) |
23 | 22 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β§ π₯ β π β§ π¦ β π) β + =
(+gβ(βfld βΎs π))) |
24 | 23 | oveqd 7423 |
. . . . 5
β’ ((π β§ π₯ β π β§ π¦ β π) β (π₯ + π¦) = (π₯(+gβ(βfld
βΎs π))π¦)) |
25 | 24 | fveq2d 6893 |
. . . 4
β’ ((π β§ π₯ β π β§ π¦ β π) β (πΉβ(π₯ + π¦)) = (πΉβ(π₯(+gβ(βfld
βΎs π))π¦))) |
26 | | mptexg 7220 |
. . . . . . . . 9
β’ (π β
(SubGrpββfld) β (π₯ β π β¦ (expβ(π΄ Β· π₯))) β V) |
27 | 17, 26 | eqeltrid 2838 |
. . . . . . . 8
β’ (π β
(SubGrpββfld) β πΉ β V) |
28 | | rnexg 7892 |
. . . . . . . 8
β’ (πΉ β V β ran πΉ β V) |
29 | 7, 27, 28 | 3syl 18 |
. . . . . . 7
β’ (π β ran πΉ β V) |
30 | | efabl.2 |
. . . . . . . 8
β’ πΊ =
((mulGrpββfld) βΎs ran πΉ) |
31 | | eqid 2733 |
. . . . . . . . 9
β’
(mulGrpββfld) =
(mulGrpββfld) |
32 | | cnfldmul 20943 |
. . . . . . . . 9
β’ Β·
= (.rββfld) |
33 | 31, 32 | mgpplusg 19986 |
. . . . . . . 8
β’ Β·
= (+gβ(mulGrpββfld)) |
34 | 30, 33 | ressplusg 17232 |
. . . . . . 7
β’ (ran
πΉ β V β Β·
= (+gβπΊ)) |
35 | 29, 34 | syl 17 |
. . . . . 6
β’ (π β Β· =
(+gβπΊ)) |
36 | 35 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π₯ β π β§ π¦ β π) β Β· =
(+gβπΊ)) |
37 | 36 | oveqd 7423 |
. . . 4
β’ ((π β§ π₯ β π β§ π¦ β π) β ((πΉβπ₯) Β· (πΉβπ¦)) = ((πΉβπ₯)(+gβπΊ)(πΉβπ¦))) |
38 | 19, 25, 37 | 3eqtr3d 2781 |
. . 3
β’ ((π β§ π₯ β π β§ π¦ β π) β (πΉβ(π₯(+gβ(βfld
βΎs π))π¦)) = ((πΉβπ₯)(+gβπΊ)(πΉβπ¦))) |
39 | 5, 12, 14, 38 | syl3anc 1372 |
. 2
β’ ((π β§ π₯ β (Baseβ(βfld
βΎs π))
β§ π¦ β
(Baseβ(βfld βΎs π))) β (πΉβ(π₯(+gβ(βfld
βΎs π))π¦)) = ((πΉβπ₯)(+gβπΊ)(πΉβπ¦))) |
40 | | fvex 6902 |
. . . . 5
β’
(expβ(π΄
Β· π₯)) β
V |
41 | 40, 17 | fnmpti 6691 |
. . . 4
β’ πΉ Fn π |
42 | | dffn4 6809 |
. . . 4
β’ (πΉ Fn π β πΉ:πβontoβran πΉ) |
43 | 41, 42 | mpbi 229 |
. . 3
β’ πΉ:πβontoβran πΉ |
44 | | eqidd 2734 |
. . . 4
β’ (π β πΉ = πΉ) |
45 | | eff 16022 |
. . . . . . . 8
β’
exp:ββΆβ |
46 | 45 | a1i 11 |
. . . . . . 7
β’ ((π β§ π₯ β π) β
exp:ββΆβ) |
47 | 15 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β π΄ β β) |
48 | | cnfldbas 20941 |
. . . . . . . . . . 11
β’ β =
(Baseββfld) |
49 | 48 | subgss 19002 |
. . . . . . . . . 10
β’ (π β
(SubGrpββfld) β π β β) |
50 | 7, 49 | syl 17 |
. . . . . . . . 9
β’ (π β π β β) |
51 | 50 | sselda 3982 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β π₯ β β) |
52 | 47, 51 | mulcld 11231 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (π΄ Β· π₯) β β) |
53 | 46, 52 | ffvelcdmd 7085 |
. . . . . 6
β’ ((π β§ π₯ β π) β (expβ(π΄ Β· π₯)) β β) |
54 | 53 | ralrimiva 3147 |
. . . . 5
β’ (π β βπ₯ β π (expβ(π΄ Β· π₯)) β β) |
55 | 17 | rnmptss 7119 |
. . . . 5
β’
(βπ₯ β
π (expβ(π΄ Β· π₯)) β β β ran πΉ β
β) |
56 | 31, 48 | mgpbas 19988 |
. . . . . 6
β’ β =
(Baseβ(mulGrpββfld)) |
57 | 30, 56 | ressbas2 17179 |
. . . . 5
β’ (ran
πΉ β β β
ran πΉ = (BaseβπΊ)) |
58 | 54, 55, 57 | 3syl 18 |
. . . 4
β’ (π β ran πΉ = (BaseβπΊ)) |
59 | 44, 10, 58 | foeq123d 6824 |
. . 3
β’ (π β (πΉ:πβontoβran πΉ β πΉ:(Baseβ(βfld
βΎs π))βontoβ(BaseβπΊ))) |
60 | 43, 59 | mpbii 232 |
. 2
β’ (π β πΉ:(Baseβ(βfld
βΎs π))βontoβ(BaseβπΊ)) |
61 | | cnring 20960 |
. . . 4
β’
βfld β Ring |
62 | | ringabl 20092 |
. . . 4
β’
(βfld β Ring β βfld β
Abel) |
63 | 61, 62 | ax-mp 5 |
. . 3
β’
βfld β Abel |
64 | 8 | subgabl 19699 |
. . 3
β’
((βfld β Abel β§ π β
(SubGrpββfld)) β (βfld
βΎs π)
β Abel) |
65 | 63, 7, 64 | sylancr 588 |
. 2
β’ (π β (βfld
βΎs π)
β Abel) |
66 | 1, 2, 3, 4, 39, 60, 65 | ghmabl 19695 |
1
β’ (π β πΊ β Abel) |