Step | Hyp | Ref
| Expression |
1 | | amgmlemALT.0 |
. . 3
β’ π =
(mulGrpββfld) |
2 | | amgmlemALT.1 |
. . 3
β’ (π β π΄ β Fin) |
3 | | amgmlemALT.2 |
. . 3
β’ (π β π΄ β β
) |
4 | | amgmlemALT.3 |
. . 3
β’ (π β πΉ:π΄βΆβ+) |
5 | | hashnncl 14272 |
. . . . . . . 8
β’ (π΄ β Fin β
((β―βπ΄) β
β β π΄ β
β
)) |
6 | 2, 5 | syl 17 |
. . . . . . 7
β’ (π β ((β―βπ΄) β β β π΄ β β
)) |
7 | 3, 6 | mpbird 257 |
. . . . . 6
β’ (π β (β―βπ΄) β
β) |
8 | 7 | nnrpd 12960 |
. . . . 5
β’ (π β (β―βπ΄) β
β+) |
9 | 8 | rpreccld 12972 |
. . . 4
β’ (π β (1 / (β―βπ΄)) β
β+) |
10 | | fconst6g 6732 |
. . . 4
β’ ((1 /
(β―βπ΄)) β
β+ β (π΄ Γ {(1 / (β―βπ΄))}):π΄βΆβ+) |
11 | 9, 10 | syl 17 |
. . 3
β’ (π β (π΄ Γ {(1 / (β―βπ΄))}):π΄βΆβ+) |
12 | | fconstmpt 5695 |
. . . . . 6
β’ (π΄ Γ {(1 /
(β―βπ΄))}) =
(π β π΄ β¦ (1 / (β―βπ΄))) |
13 | 12 | a1i 11 |
. . . . 5
β’ (π β (π΄ Γ {(1 / (β―βπ΄))}) = (π β π΄ β¦ (1 / (β―βπ΄)))) |
14 | 13 | oveq2d 7374 |
. . . 4
β’ (π β (βfld
Ξ£g (π΄ Γ {(1 / (β―βπ΄))})) = (βfld
Ξ£g (π β π΄ β¦ (1 / (β―βπ΄))))) |
15 | 7 | nnrecred 12209 |
. . . . . 6
β’ (π β (1 / (β―βπ΄)) β
β) |
16 | 15 | recnd 11188 |
. . . . 5
β’ (π β (1 / (β―βπ΄)) β
β) |
17 | | simpl 484 |
. . . . . 6
β’ ((π΄ β Fin β§ (1 /
(β―βπ΄)) β
β) β π΄ β
Fin) |
18 | | simplr 768 |
. . . . . 6
β’ (((π΄ β Fin β§ (1 /
(β―βπ΄)) β
β) β§ π β
π΄) β (1 /
(β―βπ΄)) β
β) |
19 | 17, 18 | gsumfsum 20880 |
. . . . 5
β’ ((π΄ β Fin β§ (1 /
(β―βπ΄)) β
β) β (βfld Ξ£g (π β π΄ β¦ (1 / (β―βπ΄)))) = Ξ£π β π΄ (1 / (β―βπ΄))) |
20 | 2, 16, 19 | syl2anc 585 |
. . . 4
β’ (π β (βfld
Ξ£g (π β π΄ β¦ (1 / (β―βπ΄)))) = Ξ£π β π΄ (1 / (β―βπ΄))) |
21 | | fsumconst 15680 |
. . . . . 6
β’ ((π΄ β Fin β§ (1 /
(β―βπ΄)) β
β) β Ξ£π
β π΄ (1 /
(β―βπ΄)) =
((β―βπ΄) Β·
(1 / (β―βπ΄)))) |
22 | 2, 16, 21 | syl2anc 585 |
. . . . 5
β’ (π β Ξ£π β π΄ (1 / (β―βπ΄)) = ((β―βπ΄) Β· (1 / (β―βπ΄)))) |
23 | 7 | nncnd 12174 |
. . . . . 6
β’ (π β (β―βπ΄) β
β) |
24 | 7 | nnne0d 12208 |
. . . . . 6
β’ (π β (β―βπ΄) β 0) |
25 | 23, 24 | recidd 11931 |
. . . . 5
β’ (π β ((β―βπ΄) Β· (1 /
(β―βπ΄))) =
1) |
26 | 22, 25 | eqtrd 2773 |
. . . 4
β’ (π β Ξ£π β π΄ (1 / (β―βπ΄)) = 1) |
27 | 14, 20, 26 | 3eqtrd 2777 |
. . 3
β’ (π β (βfld
Ξ£g (π΄ Γ {(1 / (β―βπ΄))})) = 1) |
28 | 1, 2, 3, 4, 11, 27 | amgmwlem 47335 |
. 2
β’ (π β (π Ξ£g (πΉ βf
βπ(π΄ Γ {(1 / (β―βπ΄))}))) β€
(βfld Ξ£g (πΉ βf Β· (π΄ Γ {(1 /
(β―βπ΄))})))) |
29 | | rpssre 12927 |
. . . . . 6
β’
β+ β β |
30 | | ax-resscn 11113 |
. . . . . 6
β’ β
β β |
31 | 29, 30 | sstri 3954 |
. . . . 5
β’
β+ β β |
32 | | eqid 2733 |
. . . . . 6
β’ (π βΎs
β+) = (π
βΎs β+) |
33 | | cnfldbas 20816 |
. . . . . . 7
β’ β =
(Baseββfld) |
34 | 1, 33 | mgpbas 19907 |
. . . . . 6
β’ β =
(Baseβπ) |
35 | 32, 34 | ressbas2 17125 |
. . . . 5
β’
(β+ β β β β+ =
(Baseβ(π
βΎs β+))) |
36 | 31, 35 | ax-mp 5 |
. . . 4
β’
β+ = (Baseβ(π βΎs
β+)) |
37 | | cnfld1 20838 |
. . . . . 6
β’ 1 =
(1rββfld) |
38 | 1, 37 | ringidval 19920 |
. . . . 5
β’ 1 =
(0gβπ) |
39 | 1 | oveq1i 7368 |
. . . . . . . . . 10
β’ (π βΎs (β
β {0})) = ((mulGrpββfld) βΎs
(β β {0})) |
40 | 39 | rpmsubg 20877 |
. . . . . . . . 9
β’
β+ β (SubGrpβ(π βΎs (β β
{0}))) |
41 | | subgsubm 18955 |
. . . . . . . . 9
β’
(β+ β (SubGrpβ(π βΎs (β β {0})))
β β+ β (SubMndβ(π βΎs (β β
{0})))) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . 8
β’
β+ β (SubMndβ(π βΎs (β β
{0}))) |
43 | | cnring 20835 |
. . . . . . . . . 10
β’
βfld β Ring |
44 | | cnfld0 20837 |
. . . . . . . . . . . 12
β’ 0 =
(0gββfld) |
45 | | cndrng 20842 |
. . . . . . . . . . . 12
β’
βfld β DivRing |
46 | 33, 44, 45 | drngui 20203 |
. . . . . . . . . . 11
β’ (β
β {0}) = (Unitββfld) |
47 | 46, 1 | unitsubm 20104 |
. . . . . . . . . 10
β’
(βfld β Ring β (β β {0}) β
(SubMndβπ)) |
48 | 43, 47 | ax-mp 5 |
. . . . . . . . 9
β’ (β
β {0}) β (SubMndβπ) |
49 | | eqid 2733 |
. . . . . . . . . 10
β’ (π βΎs (β
β {0})) = (π
βΎs (β β {0})) |
50 | 49 | subsubm 18632 |
. . . . . . . . 9
β’ ((β
β {0}) β (SubMndβπ) β (β+ β
(SubMndβ(π
βΎs (β β {0}))) β (β+ β
(SubMndβπ) β§
β+ β (β β {0})))) |
51 | 48, 50 | ax-mp 5 |
. . . . . . . 8
β’
(β+ β (SubMndβ(π βΎs (β β {0})))
β (β+ β (SubMndβπ) β§ β+ β (β
β {0}))) |
52 | 42, 51 | mpbi 229 |
. . . . . . 7
β’
(β+ β (SubMndβπ) β§ β+ β (β
β {0})) |
53 | 52 | simpli 485 |
. . . . . 6
β’
β+ β (SubMndβπ) |
54 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
55 | 32, 54 | subm0 18631 |
. . . . . 6
β’
(β+ β (SubMndβπ) β (0gβπ) = (0gβ(π βΎs
β+))) |
56 | 53, 55 | ax-mp 5 |
. . . . 5
β’
(0gβπ) = (0gβ(π βΎs
β+)) |
57 | 38, 56 | eqtri 2761 |
. . . 4
β’ 1 =
(0gβ(π
βΎs β+)) |
58 | | cncrng 20834 |
. . . . . 6
β’
βfld β CRing |
59 | 1 | crngmgp 19977 |
. . . . . 6
β’
(βfld β CRing β π β CMnd) |
60 | 58, 59 | ax-mp 5 |
. . . . 5
β’ π β CMnd |
61 | 32 | submmnd 18629 |
. . . . . 6
β’
(β+ β (SubMndβπ) β (π βΎs β+)
β Mnd) |
62 | 53, 61 | mp1i 13 |
. . . . 5
β’ (π β (π βΎs β+)
β Mnd) |
63 | 32 | subcmn 19620 |
. . . . 5
β’ ((π β CMnd β§ (π βΎs
β+) β Mnd) β (π βΎs β+)
β CMnd) |
64 | 60, 62, 63 | sylancr 588 |
. . . 4
β’ (π β (π βΎs β+)
β CMnd) |
65 | | reex 11147 |
. . . . . . . 8
β’ β
β V |
66 | 65, 29 | ssexi 5280 |
. . . . . . 7
β’
β+ β V |
67 | | cnfldmul 20818 |
. . . . . . . . 9
β’ Β·
= (.rββfld) |
68 | 1, 67 | mgpplusg 19905 |
. . . . . . . 8
β’ Β·
= (+gβπ) |
69 | 32, 68 | ressplusg 17176 |
. . . . . . 7
β’
(β+ β V β Β· =
(+gβ(π
βΎs β+))) |
70 | 66, 69 | ax-mp 5 |
. . . . . 6
β’ Β·
= (+gβ(π
βΎs β+)) |
71 | | eqid 2733 |
. . . . . . . 8
β’
((mulGrpββfld) βΎs (β
β {0})) = ((mulGrpββfld) βΎs
(β β {0})) |
72 | 71 | rpmsubg 20877 |
. . . . . . 7
β’
β+ β
(SubGrpβ((mulGrpββfld) βΎs
(β β {0}))) |
73 | 1 | oveq1i 7368 |
. . . . . . . . 9
β’ (π βΎs
β+) = ((mulGrpββfld)
βΎs β+) |
74 | | cnex 11137 |
. . . . . . . . . . 11
β’ β
β V |
75 | | difss 4092 |
. . . . . . . . . . 11
β’ (β
β {0}) β β |
76 | 74, 75 | ssexi 5280 |
. . . . . . . . . 10
β’ (β
β {0}) β V |
77 | | rpcndif0 12939 |
. . . . . . . . . . 11
β’ (π€ β β+
β π€ β (β
β {0})) |
78 | 77 | ssriv 3949 |
. . . . . . . . . 10
β’
β+ β (β β {0}) |
79 | | ressabs 17135 |
. . . . . . . . . 10
β’
(((β β {0}) β V β§ β+ β
(β β {0})) β (((mulGrpββfld)
βΎs (β β {0})) βΎs
β+) = ((mulGrpββfld)
βΎs β+)) |
80 | 76, 78, 79 | mp2an 691 |
. . . . . . . . 9
β’
(((mulGrpββfld) βΎs (β
β {0})) βΎs β+) =
((mulGrpββfld) βΎs
β+) |
81 | 73, 80 | eqtr4i 2764 |
. . . . . . . 8
β’ (π βΎs
β+) = (((mulGrpββfld)
βΎs (β β {0})) βΎs
β+) |
82 | 81 | subggrp 18936 |
. . . . . . 7
β’
(β+ β
(SubGrpβ((mulGrpββfld) βΎs
(β β {0}))) β (π βΎs β+)
β Grp) |
83 | 72, 82 | mp1i 13 |
. . . . . 6
β’ (π β (π βΎs β+)
β Grp) |
84 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β β+) β π β
β+) |
85 | 15 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β+) β (1 /
(β―βπ΄)) β
β) |
86 | 84, 85 | rpcxpcld 26103 |
. . . . . . 7
β’ ((π β§ π β β+) β (πβπ(1 /
(β―βπ΄))) β
β+) |
87 | | eqid 2733 |
. . . . . . 7
β’ (π β β+
β¦ (πβπ(1 /
(β―βπ΄)))) =
(π β
β+ β¦ (πβπ(1 /
(β―βπ΄)))) |
88 | 86, 87 | fmptd 7063 |
. . . . . 6
β’ (π β (π β β+ β¦ (πβπ(1 /
(β―βπ΄)))):β+βΆβ+) |
89 | | simprl 770 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ π¦ β β+))
β π₯ β
β+) |
90 | 89 | rprege0d 12969 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ π¦ β β+))
β (π₯ β β
β§ 0 β€ π₯)) |
91 | | simprr 772 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ π¦ β β+))
β π¦ β
β+) |
92 | 91 | rprege0d 12969 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ π¦ β β+))
β (π¦ β β
β§ 0 β€ π¦)) |
93 | 16 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ π¦ β β+))
β (1 / (β―βπ΄)) β β) |
94 | | mulcxp 26056 |
. . . . . . . 8
β’ (((π₯ β β β§ 0 β€
π₯) β§ (π¦ β β β§ 0 β€
π¦) β§ (1 /
(β―βπ΄)) β
β) β ((π₯
Β· π¦)βπ(1 /
(β―βπ΄))) =
((π₯βπ(1 /
(β―βπ΄)))
Β· (π¦βπ(1 /
(β―βπ΄))))) |
95 | 90, 92, 93, 94 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ π¦ β β+))
β ((π₯ Β· π¦)βπ(1 /
(β―βπ΄))) =
((π₯βπ(1 /
(β―βπ΄)))
Β· (π¦βπ(1 /
(β―βπ΄))))) |
96 | | rpmulcl 12943 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π¦ β
β+) β (π₯ Β· π¦) β
β+) |
97 | 96 | adantl 483 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ π¦ β β+))
β (π₯ Β· π¦) β
β+) |
98 | | oveq1 7365 |
. . . . . . . . 9
β’ (π = (π₯ Β· π¦) β (πβπ(1 /
(β―βπ΄))) =
((π₯ Β· π¦)βπ(1 /
(β―βπ΄)))) |
99 | | ovex 7391 |
. . . . . . . . 9
β’ (πβπ(1 /
(β―βπ΄))) β
V |
100 | 98, 87, 99 | fvmpt3i 6954 |
. . . . . . . 8
β’ ((π₯ Β· π¦) β β+ β ((π β β+
β¦ (πβπ(1 /
(β―βπ΄))))β(π₯ Β· π¦)) = ((π₯ Β· π¦)βπ(1 /
(β―βπ΄)))) |
101 | 97, 100 | syl 17 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ π¦ β β+))
β ((π β
β+ β¦ (πβπ(1 /
(β―βπ΄))))β(π₯ Β· π¦)) = ((π₯ Β· π¦)βπ(1 /
(β―βπ΄)))) |
102 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = π₯ β (πβπ(1 /
(β―βπ΄))) =
(π₯βπ(1 /
(β―βπ΄)))) |
103 | 102, 87, 99 | fvmpt3i 6954 |
. . . . . . . . 9
β’ (π₯ β β+
β ((π β
β+ β¦ (πβπ(1 /
(β―βπ΄))))βπ₯) = (π₯βπ(1 /
(β―βπ΄)))) |
104 | 89, 103 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ π¦ β β+))
β ((π β
β+ β¦ (πβπ(1 /
(β―βπ΄))))βπ₯) = (π₯βπ(1 /
(β―βπ΄)))) |
105 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = π¦ β (πβπ(1 /
(β―βπ΄))) =
(π¦βπ(1 /
(β―βπ΄)))) |
106 | 105, 87, 99 | fvmpt3i 6954 |
. . . . . . . . 9
β’ (π¦ β β+
β ((π β
β+ β¦ (πβπ(1 /
(β―βπ΄))))βπ¦) = (π¦βπ(1 /
(β―βπ΄)))) |
107 | 91, 106 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ π¦ β β+))
β ((π β
β+ β¦ (πβπ(1 /
(β―βπ΄))))βπ¦) = (π¦βπ(1 /
(β―βπ΄)))) |
108 | 104, 107 | oveq12d 7376 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ π¦ β β+))
β (((π β
β+ β¦ (πβπ(1 /
(β―βπ΄))))βπ₯) Β· ((π β β+ β¦ (πβπ(1 /
(β―βπ΄))))βπ¦)) = ((π₯βπ(1 /
(β―βπ΄)))
Β· (π¦βπ(1 /
(β―βπ΄))))) |
109 | 95, 101, 108 | 3eqtr4d 2783 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ π¦ β β+))
β ((π β
β+ β¦ (πβπ(1 /
(β―βπ΄))))β(π₯ Β· π¦)) = (((π β β+ β¦ (πβπ(1 /
(β―βπ΄))))βπ₯) Β· ((π β β+ β¦ (πβπ(1 /
(β―βπ΄))))βπ¦))) |
110 | 36, 36, 70, 70, 83, 83, 88, 109 | isghmd 19022 |
. . . . 5
β’ (π β (π β β+ β¦ (πβπ(1 /
(β―βπ΄)))) β
((π βΎs
β+) GrpHom (π βΎs
β+))) |
111 | | ghmmhm 19023 |
. . . . 5
β’ ((π β β+
β¦ (πβπ(1 /
(β―βπ΄)))) β
((π βΎs
β+) GrpHom (π βΎs β+))
β (π β
β+ β¦ (πβπ(1 /
(β―βπ΄)))) β
((π βΎs
β+) MndHom (π βΎs
β+))) |
112 | 110, 111 | syl 17 |
. . . 4
β’ (π β (π β β+ β¦ (πβπ(1 /
(β―βπ΄)))) β
((π βΎs
β+) MndHom (π βΎs
β+))) |
113 | | 1red 11161 |
. . . . 5
β’ (π β 1 β
β) |
114 | 4, 2, 113 | fdmfifsupp 9320 |
. . . 4
β’ (π β πΉ finSupp 1) |
115 | 36, 57, 64, 62, 2, 112, 4, 114 | gsummhm 19720 |
. . 3
β’ (π β ((π βΎs β+)
Ξ£g ((π β β+ β¦ (πβπ(1 /
(β―βπ΄))))
β πΉ)) = ((π β β+
β¦ (πβπ(1 /
(β―βπ΄))))β((π βΎs β+)
Ξ£g πΉ))) |
116 | 53 | a1i 11 |
. . . . 5
β’ (π β β+ β
(SubMndβπ)) |
117 | 4 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((π β§ π β π΄) β (πΉβπ) β
β+) |
118 | 15 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π΄) β (1 / (β―βπ΄)) β
β) |
119 | 117, 118 | rpcxpcld 26103 |
. . . . . 6
β’ ((π β§ π β π΄) β ((πΉβπ)βπ(1 /
(β―βπ΄))) β
β+) |
120 | | eqid 2733 |
. . . . . 6
β’ (π β π΄ β¦ ((πΉβπ)βπ(1 /
(β―βπ΄)))) =
(π β π΄ β¦ ((πΉβπ)βπ(1 /
(β―βπ΄)))) |
121 | 119, 120 | fmptd 7063 |
. . . . 5
β’ (π β (π β π΄ β¦ ((πΉβπ)βπ(1 /
(β―βπ΄)))):π΄βΆβ+) |
122 | 2, 116, 121, 32 | gsumsubm 18650 |
. . . 4
β’ (π β (π Ξ£g (π β π΄ β¦ ((πΉβπ)βπ(1 /
(β―βπ΄))))) =
((π βΎs
β+) Ξ£g (π β π΄ β¦ ((πΉβπ)βπ(1 /
(β―βπ΄)))))) |
123 | 9 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΄) β (1 / (β―βπ΄)) β
β+) |
124 | 4 | feqmptd 6911 |
. . . . . 6
β’ (π β πΉ = (π β π΄ β¦ (πΉβπ))) |
125 | 2, 117, 123, 124, 13 | offval2 7638 |
. . . . 5
β’ (π β (πΉ βf
βπ(π΄ Γ {(1 / (β―βπ΄))})) = (π β π΄ β¦ ((πΉβπ)βπ(1 /
(β―βπ΄))))) |
126 | 125 | oveq2d 7374 |
. . . 4
β’ (π β (π Ξ£g (πΉ βf
βπ(π΄ Γ {(1 / (β―βπ΄))}))) = (π Ξ£g (π β π΄ β¦ ((πΉβπ)βπ(1 /
(β―βπ΄)))))) |
127 | 102 | cbvmptv 5219 |
. . . . . . 7
β’ (π β β+
β¦ (πβπ(1 /
(β―βπ΄)))) =
(π₯ β
β+ β¦ (π₯βπ(1 /
(β―βπ΄)))) |
128 | 127 | a1i 11 |
. . . . . 6
β’ (π β (π β β+ β¦ (πβπ(1 /
(β―βπ΄)))) =
(π₯ β
β+ β¦ (π₯βπ(1 /
(β―βπ΄))))) |
129 | | oveq1 7365 |
. . . . . 6
β’ (π₯ = (πΉβπ) β (π₯βπ(1 /
(β―βπ΄))) =
((πΉβπ)βπ(1 /
(β―βπ΄)))) |
130 | 117, 124,
128, 129 | fmptco 7076 |
. . . . 5
β’ (π β ((π β β+ β¦ (πβπ(1 /
(β―βπ΄))))
β πΉ) = (π β π΄ β¦ ((πΉβπ)βπ(1 /
(β―βπ΄))))) |
131 | 130 | oveq2d 7374 |
. . . 4
β’ (π β ((π βΎs β+)
Ξ£g ((π β β+ β¦ (πβπ(1 /
(β―βπ΄))))
β πΉ)) = ((π βΎs
β+) Ξ£g (π β π΄ β¦ ((πΉβπ)βπ(1 /
(β―βπ΄)))))) |
132 | 122, 126,
131 | 3eqtr4rd 2784 |
. . 3
β’ (π β ((π βΎs β+)
Ξ£g ((π β β+ β¦ (πβπ(1 /
(β―βπ΄))))
β πΉ)) = (π Ξ£g
(πΉ βf
βπ(π΄ Γ {(1 / (β―βπ΄))})))) |
133 | 36, 57, 64, 2, 4, 114 | gsumcl 19697 |
. . . . 5
β’ (π β ((π βΎs β+)
Ξ£g πΉ) β
β+) |
134 | | oveq1 7365 |
. . . . . 6
β’ (π = ((π βΎs β+)
Ξ£g πΉ) β (πβπ(1 /
(β―βπ΄))) =
(((π βΎs
β+) Ξ£g πΉ)βπ(1 /
(β―βπ΄)))) |
135 | 134, 87, 99 | fvmpt3i 6954 |
. . . . 5
β’ (((π βΎs
β+) Ξ£g πΉ) β β+ β ((π β β+
β¦ (πβπ(1 /
(β―βπ΄))))β((π βΎs β+)
Ξ£g πΉ)) = (((π βΎs β+)
Ξ£g πΉ)βπ(1 /
(β―βπ΄)))) |
136 | 133, 135 | syl 17 |
. . . 4
β’ (π β ((π β β+ β¦ (πβπ(1 /
(β―βπ΄))))β((π βΎs β+)
Ξ£g πΉ)) = (((π βΎs β+)
Ξ£g πΉ)βπ(1 /
(β―βπ΄)))) |
137 | 2, 116, 4, 32 | gsumsubm 18650 |
. . . . 5
β’ (π β (π Ξ£g πΉ) = ((π βΎs β+)
Ξ£g πΉ)) |
138 | 137 | oveq1d 7373 |
. . . 4
β’ (π β ((π Ξ£g πΉ)βπ(1 /
(β―βπ΄))) =
(((π βΎs
β+) Ξ£g πΉ)βπ(1 /
(β―βπ΄)))) |
139 | 136, 138 | eqtr4d 2776 |
. . 3
β’ (π β ((π β β+ β¦ (πβπ(1 /
(β―βπ΄))))β((π βΎs β+)
Ξ£g πΉ)) = ((π Ξ£g πΉ)βπ(1 /
(β―βπ΄)))) |
140 | 115, 132,
139 | 3eqtr3d 2781 |
. 2
β’ (π β (π Ξ£g (πΉ βf
βπ(π΄ Γ {(1 / (β―βπ΄))}))) = ((π Ξ£g πΉ)βπ(1 /
(β―βπ΄)))) |
141 | 117 | rpcnd 12964 |
. . . . . . 7
β’ ((π β§ π β π΄) β (πΉβπ) β β) |
142 | 2, 141 | fsumcl 15623 |
. . . . . 6
β’ (π β Ξ£π β π΄ (πΉβπ) β β) |
143 | 142, 23, 24 | divrecd 11939 |
. . . . 5
β’ (π β (Ξ£π β π΄ (πΉβπ) / (β―βπ΄)) = (Ξ£π β π΄ (πΉβπ) Β· (1 / (β―βπ΄)))) |
144 | 2, 16, 141 | fsummulc1 15675 |
. . . . 5
β’ (π β (Ξ£π β π΄ (πΉβπ) Β· (1 / (β―βπ΄))) = Ξ£π β π΄ ((πΉβπ) Β· (1 / (β―βπ΄)))) |
145 | 143, 144 | eqtr2d 2774 |
. . . 4
β’ (π β Ξ£π β π΄ ((πΉβπ) Β· (1 / (β―βπ΄))) = (Ξ£π β π΄ (πΉβπ) / (β―βπ΄))) |
146 | 16 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π΄) β (1 / (β―βπ΄)) β
β) |
147 | 141, 146 | mulcld 11180 |
. . . . 5
β’ ((π β§ π β π΄) β ((πΉβπ) Β· (1 / (β―βπ΄))) β
β) |
148 | 2, 147 | gsumfsum 20880 |
. . . 4
β’ (π β (βfld
Ξ£g (π β π΄ β¦ ((πΉβπ) Β· (1 / (β―βπ΄))))) = Ξ£π β π΄ ((πΉβπ) Β· (1 / (β―βπ΄)))) |
149 | 2, 141 | gsumfsum 20880 |
. . . . 5
β’ (π β (βfld
Ξ£g (π β π΄ β¦ (πΉβπ))) = Ξ£π β π΄ (πΉβπ)) |
150 | 149 | oveq1d 7373 |
. . . 4
β’ (π β ((βfld
Ξ£g (π β π΄ β¦ (πΉβπ))) / (β―βπ΄)) = (Ξ£π β π΄ (πΉβπ) / (β―βπ΄))) |
151 | 145, 148,
150 | 3eqtr4d 2783 |
. . 3
β’ (π β (βfld
Ξ£g (π β π΄ β¦ ((πΉβπ) Β· (1 / (β―βπ΄))))) = ((βfld
Ξ£g (π β π΄ β¦ (πΉβπ))) / (β―βπ΄))) |
152 | 2, 117, 146, 124, 13 | offval2 7638 |
. . . 4
β’ (π β (πΉ βf Β· (π΄ Γ {(1 /
(β―βπ΄))})) =
(π β π΄ β¦ ((πΉβπ) Β· (1 / (β―βπ΄))))) |
153 | 152 | oveq2d 7374 |
. . 3
β’ (π β (βfld
Ξ£g (πΉ βf Β· (π΄ Γ {(1 /
(β―βπ΄))}))) =
(βfld Ξ£g (π β π΄ β¦ ((πΉβπ) Β· (1 / (β―βπ΄)))))) |
154 | 124 | oveq2d 7374 |
. . . 4
β’ (π β (βfld
Ξ£g πΉ) = (βfld
Ξ£g (π β π΄ β¦ (πΉβπ)))) |
155 | 154 | oveq1d 7373 |
. . 3
β’ (π β ((βfld
Ξ£g πΉ) / (β―βπ΄)) = ((βfld
Ξ£g (π β π΄ β¦ (πΉβπ))) / (β―βπ΄))) |
156 | 151, 153,
155 | 3eqtr4d 2783 |
. 2
β’ (π β (βfld
Ξ£g (πΉ βf Β· (π΄ Γ {(1 /
(β―βπ΄))}))) =
((βfld Ξ£g πΉ) / (β―βπ΄))) |
157 | 28, 140, 156 | 3brtr3d 5137 |
1
β’ (π β ((π Ξ£g πΉ)βπ(1 /
(β―βπ΄))) β€
((βfld Ξ£g πΉ) / (β―βπ΄))) |