Users' Mathboxes Mathbox for Kunhao Zheng < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  amgmlemALT Structured version   Visualization version   GIF version

Theorem amgmlemALT 42358
Description: Alternative proof of amgmlem 24516 using amgmwlem 42357. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by Kunhao Zheng, 20-Jun-2021.)
Hypotheses
Ref Expression
amgmlemALT.0 𝑀 = (mulGrp‘ℂfld)
amgmlemALT.1 (𝜑𝐴 ∈ Fin)
amgmlemALT.2 (𝜑𝐴 ≠ ∅)
amgmlemALT.3 (𝜑𝐹:𝐴⟶ℝ+)
Assertion
Ref Expression
amgmlemALT (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (#‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (#‘𝐴)))

Proof of Theorem amgmlemALT
Dummy variables 𝑘 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 amgmlemALT.0 . . 3 𝑀 = (mulGrp‘ℂfld)
2 amgmlemALT.1 . . 3 (𝜑𝐴 ∈ Fin)
3 amgmlemALT.2 . . 3 (𝜑𝐴 ≠ ∅)
4 amgmlemALT.3 . . 3 (𝜑𝐹:𝐴⟶ℝ+)
5 hashnncl 13018 . . . . . . . 8 (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
62, 5syl 17 . . . . . . 7 (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
73, 6mpbird 246 . . . . . 6 (𝜑 → (#‘𝐴) ∈ ℕ)
87nnrpd 11746 . . . . 5 (𝜑 → (#‘𝐴) ∈ ℝ+)
98rpreccld 11758 . . . 4 (𝜑 → (1 / (#‘𝐴)) ∈ ℝ+)
10 fconst6g 6007 . . . 4 ((1 / (#‘𝐴)) ∈ ℝ+ → (𝐴 × {(1 / (#‘𝐴))}):𝐴⟶ℝ+)
119, 10syl 17 . . 3 (𝜑 → (𝐴 × {(1 / (#‘𝐴))}):𝐴⟶ℝ+)
12 fconstmpt 5085 . . . . . 6 (𝐴 × {(1 / (#‘𝐴))}) = (𝑘𝐴 ↦ (1 / (#‘𝐴)))
1312a1i 11 . . . . 5 (𝜑 → (𝐴 × {(1 / (#‘𝐴))}) = (𝑘𝐴 ↦ (1 / (#‘𝐴))))
1413oveq2d 6565 . . . 4 (𝜑 → (ℂfld Σg (𝐴 × {(1 / (#‘𝐴))})) = (ℂfld Σg (𝑘𝐴 ↦ (1 / (#‘𝐴)))))
15 hashnncl 13018 . . . . . . . . 9 (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
162, 15syl 17 . . . . . . . 8 (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
173, 16mpbird 246 . . . . . . 7 (𝜑 → (#‘𝐴) ∈ ℕ)
1817nnrecred 10943 . . . . . 6 (𝜑 → (1 / (#‘𝐴)) ∈ ℝ)
1918recnd 9947 . . . . 5 (𝜑 → (1 / (#‘𝐴)) ∈ ℂ)
20 simpl 472 . . . . . 6 ((𝐴 ∈ Fin ∧ (1 / (#‘𝐴)) ∈ ℂ) → 𝐴 ∈ Fin)
21 simplr 788 . . . . . 6 (((𝐴 ∈ Fin ∧ (1 / (#‘𝐴)) ∈ ℂ) ∧ 𝑘𝐴) → (1 / (#‘𝐴)) ∈ ℂ)
2220, 21gsumfsum 19632 . . . . 5 ((𝐴 ∈ Fin ∧ (1 / (#‘𝐴)) ∈ ℂ) → (ℂfld Σg (𝑘𝐴 ↦ (1 / (#‘𝐴)))) = Σ𝑘𝐴 (1 / (#‘𝐴)))
232, 19, 22syl2anc 691 . . . 4 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ (1 / (#‘𝐴)))) = Σ𝑘𝐴 (1 / (#‘𝐴)))
24 hashnncl 13018 . . . . . . . . . 10 (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
252, 24syl 17 . . . . . . . . 9 (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
263, 25mpbird 246 . . . . . . . 8 (𝜑 → (#‘𝐴) ∈ ℕ)
2726nnrecred 10943 . . . . . . 7 (𝜑 → (1 / (#‘𝐴)) ∈ ℝ)
2827recnd 9947 . . . . . 6 (𝜑 → (1 / (#‘𝐴)) ∈ ℂ)
29 fsumconst 14364 . . . . . 6 ((𝐴 ∈ Fin ∧ (1 / (#‘𝐴)) ∈ ℂ) → Σ𝑘𝐴 (1 / (#‘𝐴)) = ((#‘𝐴) · (1 / (#‘𝐴))))
302, 28, 29syl2anc 691 . . . . 5 (𝜑 → Σ𝑘𝐴 (1 / (#‘𝐴)) = ((#‘𝐴) · (1 / (#‘𝐴))))
31 hashnncl 13018 . . . . . . . . 9 (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
322, 31syl 17 . . . . . . . 8 (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
333, 32mpbird 246 . . . . . . 7 (𝜑 → (#‘𝐴) ∈ ℕ)
3433nncnd 10913 . . . . . 6 (𝜑 → (#‘𝐴) ∈ ℂ)
35 hashnncl 13018 . . . . . . . . 9 (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
362, 35syl 17 . . . . . . . 8 (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
373, 36mpbird 246 . . . . . . 7 (𝜑 → (#‘𝐴) ∈ ℕ)
3837nnne0d 10942 . . . . . 6 (𝜑 → (#‘𝐴) ≠ 0)
3934, 38recidd 10675 . . . . 5 (𝜑 → ((#‘𝐴) · (1 / (#‘𝐴))) = 1)
4030, 39eqtrd 2644 . . . 4 (𝜑 → Σ𝑘𝐴 (1 / (#‘𝐴)) = 1)
4114, 23, 403eqtrd 2648 . . 3 (𝜑 → (ℂfld Σg (𝐴 × {(1 / (#‘𝐴))})) = 1)
421, 2, 3, 4, 11, 41amgmwlem 42357 . 2 (𝜑 → (𝑀 Σg (𝐹𝑓𝑐(𝐴 × {(1 / (#‘𝐴))}))) ≤ (ℂfld Σg (𝐹𝑓 · (𝐴 × {(1 / (#‘𝐴))}))))
43 rpssre 11719 . . . . . 6 + ⊆ ℝ
44 ax-resscn 9872 . . . . . 6 ℝ ⊆ ℂ
4543, 44sstri 3577 . . . . 5 + ⊆ ℂ
46 eqid 2610 . . . . . 6 (𝑀s+) = (𝑀s+)
47 cnfldbas 19571 . . . . . . 7 ℂ = (Base‘ℂfld)
481, 47mgpbas 18318 . . . . . 6 ℂ = (Base‘𝑀)
4946, 48ressbas2 15758 . . . . 5 (ℝ+ ⊆ ℂ → ℝ+ = (Base‘(𝑀s+)))
5045, 49ax-mp 5 . . . 4 + = (Base‘(𝑀s+))
51 cnfld1 19590 . . . . . 6 1 = (1r‘ℂfld)
521, 51ringidval 18326 . . . . 5 1 = (0g𝑀)
531oveq1i 6559 . . . . . . . . . 10 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
5453rpmsubg 19629 . . . . . . . . 9 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
55 subgsubm 17439 . . . . . . . . 9 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
5654, 55ax-mp 5 . . . . . . . 8 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
57 cnring 19587 . . . . . . . . . 10 fld ∈ Ring
58 cnfld0 19589 . . . . . . . . . . . 12 0 = (0g‘ℂfld)
59 cndrng 19594 . . . . . . . . . . . 12 fld ∈ DivRing
6047, 58, 59drngui 18576 . . . . . . . . . . 11 (ℂ ∖ {0}) = (Unit‘ℂfld)
6160, 1unitsubm 18493 . . . . . . . . . 10 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
6257, 61ax-mp 5 . . . . . . . . 9 (ℂ ∖ {0}) ∈ (SubMnd‘𝑀)
63 eqid 2610 . . . . . . . . . 10 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
6463subsubm 17180 . . . . . . . . 9 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
6562, 64ax-mp 5 . . . . . . . 8 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
6656, 65mpbi 219 . . . . . . 7 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
6766simpli 473 . . . . . 6 + ∈ (SubMnd‘𝑀)
68 eqid 2610 . . . . . . 7 (𝑀s+) = (𝑀s+)
69 eqid 2610 . . . . . . 7 (0g𝑀) = (0g𝑀)
7068, 69subm0 17179 . . . . . 6 (ℝ+ ∈ (SubMnd‘𝑀) → (0g𝑀) = (0g‘(𝑀s+)))
7167, 70ax-mp 5 . . . . 5 (0g𝑀) = (0g‘(𝑀s+))
7252, 71eqtri 2632 . . . 4 1 = (0g‘(𝑀s+))
73 cncrng 19586 . . . . . 6 fld ∈ CRing
741crngmgp 18378 . . . . . 6 (ℂfld ∈ CRing → 𝑀 ∈ CMnd)
7573, 74ax-mp 5 . . . . 5 𝑀 ∈ CMnd
761oveq1i 6559 . . . . . . . . . 10 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
7776rpmsubg 19629 . . . . . . . . 9 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
78 subgsubm 17439 . . . . . . . . 9 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
7977, 78ax-mp 5 . . . . . . . 8 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
8047, 58, 59drngui 18576 . . . . . . . . . . 11 (ℂ ∖ {0}) = (Unit‘ℂfld)
8180, 1unitsubm 18493 . . . . . . . . . 10 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
8257, 81ax-mp 5 . . . . . . . . 9 (ℂ ∖ {0}) ∈ (SubMnd‘𝑀)
83 eqid 2610 . . . . . . . . . 10 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
8483subsubm 17180 . . . . . . . . 9 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
8582, 84ax-mp 5 . . . . . . . 8 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
8679, 85mpbi 219 . . . . . . 7 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
8786simpli 473 . . . . . 6 + ∈ (SubMnd‘𝑀)
88 eqid 2610 . . . . . . 7 (𝑀s+) = (𝑀s+)
8988submmnd 17177 . . . . . 6 (ℝ+ ∈ (SubMnd‘𝑀) → (𝑀s+) ∈ Mnd)
9087, 89mp1i 13 . . . . 5 (𝜑 → (𝑀s+) ∈ Mnd)
91 eqid 2610 . . . . . 6 (𝑀s+) = (𝑀s+)
9291subcmn 18065 . . . . 5 ((𝑀 ∈ CMnd ∧ (𝑀s+) ∈ Mnd) → (𝑀s+) ∈ CMnd)
9375, 90, 92sylancr 694 . . . 4 (𝜑 → (𝑀s+) ∈ CMnd)
941oveq1i 6559 . . . . . . . . 9 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
9594rpmsubg 19629 . . . . . . . 8 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
96 subgsubm 17439 . . . . . . . 8 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
9795, 96ax-mp 5 . . . . . . 7 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
9847, 58, 59drngui 18576 . . . . . . . . . 10 (ℂ ∖ {0}) = (Unit‘ℂfld)
9998, 1unitsubm 18493 . . . . . . . . 9 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
10057, 99ax-mp 5 . . . . . . . 8 (ℂ ∖ {0}) ∈ (SubMnd‘𝑀)
101 eqid 2610 . . . . . . . . 9 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
102101subsubm 17180 . . . . . . . 8 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
103100, 102ax-mp 5 . . . . . . 7 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
10497, 103mpbi 219 . . . . . 6 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
105104simpli 473 . . . . 5 + ∈ (SubMnd‘𝑀)
106 eqid 2610 . . . . . 6 (𝑀s+) = (𝑀s+)
107106submmnd 17177 . . . . 5 (ℝ+ ∈ (SubMnd‘𝑀) → (𝑀s+) ∈ Mnd)
108105, 107mp1i 13 . . . 4 (𝜑 → (𝑀s+) ∈ Mnd)
10943, 44sstri 3577 . . . . . . 7 + ⊆ ℂ
110 eqid 2610 . . . . . . . 8 (𝑀s+) = (𝑀s+)
1111, 47mgpbas 18318 . . . . . . . 8 ℂ = (Base‘𝑀)
112110, 111ressbas2 15758 . . . . . . 7 (ℝ+ ⊆ ℂ → ℝ+ = (Base‘(𝑀s+)))
113109, 112ax-mp 5 . . . . . 6 + = (Base‘(𝑀s+))
11443, 44sstri 3577 . . . . . . 7 + ⊆ ℂ
115 eqid 2610 . . . . . . . 8 (𝑀s+) = (𝑀s+)
1161, 47mgpbas 18318 . . . . . . . 8 ℂ = (Base‘𝑀)
117115, 116ressbas2 15758 . . . . . . 7 (ℝ+ ⊆ ℂ → ℝ+ = (Base‘(𝑀s+)))
118114, 117ax-mp 5 . . . . . 6 + = (Base‘(𝑀s+))
119 reex 9906 . . . . . . . 8 ℝ ∈ V
120119, 43ssexi 4731 . . . . . . 7 + ∈ V
121 eqid 2610 . . . . . . . 8 (𝑀s+) = (𝑀s+)
122 cnfldmul 19573 . . . . . . . . 9 · = (.r‘ℂfld)
1231, 122mgpplusg 18316 . . . . . . . 8 · = (+g𝑀)
124121, 123ressplusg 15818 . . . . . . 7 (ℝ+ ∈ V → · = (+g‘(𝑀s+)))
125120, 124ax-mp 5 . . . . . 6 · = (+g‘(𝑀s+))
126119, 43ssexi 4731 . . . . . . 7 + ∈ V
127 eqid 2610 . . . . . . . 8 (𝑀s+) = (𝑀s+)
1281, 122mgpplusg 18316 . . . . . . . 8 · = (+g𝑀)
129127, 128ressplusg 15818 . . . . . . 7 (ℝ+ ∈ V → · = (+g‘(𝑀s+)))
130126, 129ax-mp 5 . . . . . 6 · = (+g‘(𝑀s+))
131 eqid 2610 . . . . . . . 8 ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
132131rpmsubg 19629 . . . . . . 7 + ∈ (SubGrp‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
1331oveq1i 6559 . . . . . . . . 9 (𝑀s+) = ((mulGrp‘ℂfld) ↾s+)
134 cnex 9896 . . . . . . . . . . 11 ℂ ∈ V
135 difss 3699 . . . . . . . . . . 11 (ℂ ∖ {0}) ⊆ ℂ
136134, 135ssexi 4731 . . . . . . . . . 10 (ℂ ∖ {0}) ∈ V
137 rpcndif0 11727 . . . . . . . . . . 11 (𝑤 ∈ ℝ+𝑤 ∈ (ℂ ∖ {0}))
138137ssriv 3572 . . . . . . . . . 10 + ⊆ (ℂ ∖ {0})
139 ressabs 15766 . . . . . . . . . 10 (((ℂ ∖ {0}) ∈ V ∧ ℝ+ ⊆ (ℂ ∖ {0})) → (((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) ↾s+) = ((mulGrp‘ℂfld) ↾s+))
140136, 138, 139mp2an 704 . . . . . . . . 9 (((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) ↾s+) = ((mulGrp‘ℂfld) ↾s+)
141133, 140eqtr4i 2635 . . . . . . . 8 (𝑀s+) = (((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) ↾s+)
142141subggrp 17420 . . . . . . 7 (ℝ+ ∈ (SubGrp‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) → (𝑀s+) ∈ Grp)
143132, 142mp1i 13 . . . . . 6 (𝜑 → (𝑀s+) ∈ Grp)
144 eqid 2610 . . . . . . . 8 ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
145144rpmsubg 19629 . . . . . . 7 + ∈ (SubGrp‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})))
1461oveq1i 6559 . . . . . . . . 9 (𝑀s+) = ((mulGrp‘ℂfld) ↾s+)
147 difss 3699 . . . . . . . . . . 11 (ℂ ∖ {0}) ⊆ ℂ
148134, 147ssexi 4731 . . . . . . . . . 10 (ℂ ∖ {0}) ∈ V
149 rpcndif0 11727 . . . . . . . . . . 11 (𝑤 ∈ ℝ+𝑤 ∈ (ℂ ∖ {0}))
150149ssriv 3572 . . . . . . . . . 10 + ⊆ (ℂ ∖ {0})
151 ressabs 15766 . . . . . . . . . 10 (((ℂ ∖ {0}) ∈ V ∧ ℝ+ ⊆ (ℂ ∖ {0})) → (((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) ↾s+) = ((mulGrp‘ℂfld) ↾s+))
152148, 150, 151mp2an 704 . . . . . . . . 9 (((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) ↾s+) = ((mulGrp‘ℂfld) ↾s+)
153146, 152eqtr4i 2635 . . . . . . . 8 (𝑀s+) = (((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) ↾s+)
154153subggrp 17420 . . . . . . 7 (ℝ+ ∈ (SubGrp‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) → (𝑀s+) ∈ Grp)
155145, 154mp1i 13 . . . . . 6 (𝜑 → (𝑀s+) ∈ Grp)
156 simpr 476 . . . . . . . 8 ((𝜑𝑘 ∈ ℝ+) → 𝑘 ∈ ℝ+)
157 hashnncl 13018 . . . . . . . . . . . 12 (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
1582, 157syl 17 . . . . . . . . . . 11 (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
1593, 158mpbird 246 . . . . . . . . . 10 (𝜑 → (#‘𝐴) ∈ ℕ)
160159nnrecred 10943 . . . . . . . . 9 (𝜑 → (1 / (#‘𝐴)) ∈ ℝ)
161160adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℝ+) → (1 / (#‘𝐴)) ∈ ℝ)
162156, 161rpcxpcld 24276 . . . . . . 7 ((𝜑𝑘 ∈ ℝ+) → (𝑘𝑐(1 / (#‘𝐴))) ∈ ℝ+)
163 eqid 2610 . . . . . . 7 (𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴)))) = (𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))
164162, 163fmptd 6292 . . . . . 6 (𝜑 → (𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴)))):ℝ+⟶ℝ+)
165 simprl 790 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑥 ∈ ℝ+)
166165rprege0d 11755 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
167 simprr 792 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
168167rprege0d 11755 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑦 ∈ ℝ ∧ 0 ≤ 𝑦))
169 hashnncl 13018 . . . . . . . . . . . . 13 (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
1702, 169syl 17 . . . . . . . . . . . 12 (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
1713, 170mpbird 246 . . . . . . . . . . 11 (𝜑 → (#‘𝐴) ∈ ℕ)
172171nnrecred 10943 . . . . . . . . . 10 (𝜑 → (1 / (#‘𝐴)) ∈ ℝ)
173172recnd 9947 . . . . . . . . 9 (𝜑 → (1 / (#‘𝐴)) ∈ ℂ)
174173adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (1 / (#‘𝐴)) ∈ ℂ)
175 mulcxp 24231 . . . . . . . 8 (((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ (𝑦 ∈ ℝ ∧ 0 ≤ 𝑦) ∧ (1 / (#‘𝐴)) ∈ ℂ) → ((𝑥 · 𝑦)↑𝑐(1 / (#‘𝐴))) = ((𝑥𝑐(1 / (#‘𝐴))) · (𝑦𝑐(1 / (#‘𝐴)))))
176166, 168, 174, 175syl3anc 1318 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → ((𝑥 · 𝑦)↑𝑐(1 / (#‘𝐴))) = ((𝑥𝑐(1 / (#‘𝐴))) · (𝑦𝑐(1 / (#‘𝐴)))))
177 rpmulcl 11731 . . . . . . . . 9 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 · 𝑦) ∈ ℝ+)
178177adantl 481 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 · 𝑦) ∈ ℝ+)
179 oveq1 6556 . . . . . . . . 9 (𝑘 = (𝑥 · 𝑦) → (𝑘𝑐(1 / (#‘𝐴))) = ((𝑥 · 𝑦)↑𝑐(1 / (#‘𝐴))))
180 eqid 2610 . . . . . . . . 9 (𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴)))) = (𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))
181 ovex 6577 . . . . . . . . 9 (𝑘𝑐(1 / (#‘𝐴))) ∈ V
182179, 180, 181fvmpt3i 6196 . . . . . . . 8 ((𝑥 · 𝑦) ∈ ℝ+ → ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))‘(𝑥 · 𝑦)) = ((𝑥 · 𝑦)↑𝑐(1 / (#‘𝐴))))
183178, 182syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))‘(𝑥 · 𝑦)) = ((𝑥 · 𝑦)↑𝑐(1 / (#‘𝐴))))
184 simprl 790 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑥 ∈ ℝ+)
185 oveq1 6556 . . . . . . . . . 10 (𝑘 = 𝑥 → (𝑘𝑐(1 / (#‘𝐴))) = (𝑥𝑐(1 / (#‘𝐴))))
186 eqid 2610 . . . . . . . . . 10 (𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴)))) = (𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))
187 ovex 6577 . . . . . . . . . 10 (𝑘𝑐(1 / (#‘𝐴))) ∈ V
188185, 186, 187fvmpt3i 6196 . . . . . . . . 9 (𝑥 ∈ ℝ+ → ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))‘𝑥) = (𝑥𝑐(1 / (#‘𝐴))))
189184, 188syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))‘𝑥) = (𝑥𝑐(1 / (#‘𝐴))))
190 simprr 792 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
191 oveq1 6556 . . . . . . . . . 10 (𝑘 = 𝑦 → (𝑘𝑐(1 / (#‘𝐴))) = (𝑦𝑐(1 / (#‘𝐴))))
192 eqid 2610 . . . . . . . . . 10 (𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴)))) = (𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))
193 ovex 6577 . . . . . . . . . 10 (𝑘𝑐(1 / (#‘𝐴))) ∈ V
194191, 192, 193fvmpt3i 6196 . . . . . . . . 9 (𝑦 ∈ ℝ+ → ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))‘𝑦) = (𝑦𝑐(1 / (#‘𝐴))))
195190, 194syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))‘𝑦) = (𝑦𝑐(1 / (#‘𝐴))))
196189, 195oveq12d 6567 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))‘𝑥) · ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))‘𝑦)) = ((𝑥𝑐(1 / (#‘𝐴))) · (𝑦𝑐(1 / (#‘𝐴)))))
197176, 183, 1963eqtr4d 2654 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))‘(𝑥 · 𝑦)) = (((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))‘𝑥) · ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))‘𝑦)))
198113, 118, 125, 130, 143, 155, 164, 197isghmd 17492 . . . . 5 (𝜑 → (𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴)))) ∈ ((𝑀s+) GrpHom (𝑀s+)))
199 ghmmhm 17493 . . . . 5 ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴)))) ∈ ((𝑀s+) GrpHom (𝑀s+)) → (𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴)))) ∈ ((𝑀s+) MndHom (𝑀s+)))
200198, 199syl 17 . . . 4 (𝜑 → (𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴)))) ∈ ((𝑀s+) MndHom (𝑀s+)))
201 1red 9934 . . . . 5 (𝜑 → 1 ∈ ℝ)
2024, 2, 201fdmfifsupp 8168 . . . 4 (𝜑𝐹 finSupp 1)
20350, 72, 93, 108, 2, 200, 4, 202gsummhm 18161 . . 3 (𝜑 → ((𝑀s+) Σg ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴)))) ∘ 𝐹)) = ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))‘((𝑀s+) Σg 𝐹)))
2041oveq1i 6559 . . . . . . . . . 10 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
205204rpmsubg 19629 . . . . . . . . 9 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
206 subgsubm 17439 . . . . . . . . 9 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
207205, 206ax-mp 5 . . . . . . . 8 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
20847, 58, 59drngui 18576 . . . . . . . . . . 11 (ℂ ∖ {0}) = (Unit‘ℂfld)
209208, 1unitsubm 18493 . . . . . . . . . 10 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
21057, 209ax-mp 5 . . . . . . . . 9 (ℂ ∖ {0}) ∈ (SubMnd‘𝑀)
211 eqid 2610 . . . . . . . . . 10 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
212211subsubm 17180 . . . . . . . . 9 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
213210, 212ax-mp 5 . . . . . . . 8 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
214207, 213mpbi 219 . . . . . . 7 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
215214simpli 473 . . . . . 6 + ∈ (SubMnd‘𝑀)
216215a1i 11 . . . . 5 (𝜑 → ℝ+ ∈ (SubMnd‘𝑀))
2174ffvelrnda 6267 . . . . . . 7 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
218 hashnncl 13018 . . . . . . . . . . 11 (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
2192, 218syl 17 . . . . . . . . . 10 (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
2203, 219mpbird 246 . . . . . . . . 9 (𝜑 → (#‘𝐴) ∈ ℕ)
221220nnrecred 10943 . . . . . . . 8 (𝜑 → (1 / (#‘𝐴)) ∈ ℝ)
222221adantr 480 . . . . . . 7 ((𝜑𝑘𝐴) → (1 / (#‘𝐴)) ∈ ℝ)
223217, 222rpcxpcld 24276 . . . . . 6 ((𝜑𝑘𝐴) → ((𝐹𝑘)↑𝑐(1 / (#‘𝐴))) ∈ ℝ+)
224 eqid 2610 . . . . . 6 (𝑘𝐴 ↦ ((𝐹𝑘)↑𝑐(1 / (#‘𝐴)))) = (𝑘𝐴 ↦ ((𝐹𝑘)↑𝑐(1 / (#‘𝐴))))
225223, 224fmptd 6292 . . . . 5 (𝜑 → (𝑘𝐴 ↦ ((𝐹𝑘)↑𝑐(1 / (#‘𝐴)))):𝐴⟶ℝ+)
226 eqid 2610 . . . . 5 (𝑀s+) = (𝑀s+)
2272, 216, 225, 226gsumsubm 17196 . . . 4 (𝜑 → (𝑀 Σg (𝑘𝐴 ↦ ((𝐹𝑘)↑𝑐(1 / (#‘𝐴))))) = ((𝑀s+) Σg (𝑘𝐴 ↦ ((𝐹𝑘)↑𝑐(1 / (#‘𝐴))))))
2284ffvelrnda 6267 . . . . . 6 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
229 hashnncl 13018 . . . . . . . . . . 11 (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
2302, 229syl 17 . . . . . . . . . 10 (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
2313, 230mpbird 246 . . . . . . . . 9 (𝜑 → (#‘𝐴) ∈ ℕ)
232231nnrpd 11746 . . . . . . . 8 (𝜑 → (#‘𝐴) ∈ ℝ+)
233232rpreccld 11758 . . . . . . 7 (𝜑 → (1 / (#‘𝐴)) ∈ ℝ+)
234233adantr 480 . . . . . 6 ((𝜑𝑘𝐴) → (1 / (#‘𝐴)) ∈ ℝ+)
2354feqmptd 6159 . . . . . 6 (𝜑𝐹 = (𝑘𝐴 ↦ (𝐹𝑘)))
236 fconstmpt 5085 . . . . . . 7 (𝐴 × {(1 / (#‘𝐴))}) = (𝑘𝐴 ↦ (1 / (#‘𝐴)))
237236a1i 11 . . . . . 6 (𝜑 → (𝐴 × {(1 / (#‘𝐴))}) = (𝑘𝐴 ↦ (1 / (#‘𝐴))))
2382, 228, 234, 235, 237offval2 6812 . . . . 5 (𝜑 → (𝐹𝑓𝑐(𝐴 × {(1 / (#‘𝐴))})) = (𝑘𝐴 ↦ ((𝐹𝑘)↑𝑐(1 / (#‘𝐴)))))
239238oveq2d 6565 . . . 4 (𝜑 → (𝑀 Σg (𝐹𝑓𝑐(𝐴 × {(1 / (#‘𝐴))}))) = (𝑀 Σg (𝑘𝐴 ↦ ((𝐹𝑘)↑𝑐(1 / (#‘𝐴))))))
2404ffvelrnda 6267 . . . . . 6 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
2414feqmptd 6159 . . . . . 6 (𝜑𝐹 = (𝑘𝐴 ↦ (𝐹𝑘)))
242 oveq1 6556 . . . . . . . 8 (𝑘 = 𝑥 → (𝑘𝑐(1 / (#‘𝐴))) = (𝑥𝑐(1 / (#‘𝐴))))
243242cbvmptv 4678 . . . . . . 7 (𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴)))) = (𝑥 ∈ ℝ+ ↦ (𝑥𝑐(1 / (#‘𝐴))))
244243a1i 11 . . . . . 6 (𝜑 → (𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴)))) = (𝑥 ∈ ℝ+ ↦ (𝑥𝑐(1 / (#‘𝐴)))))
245 oveq1 6556 . . . . . 6 (𝑥 = (𝐹𝑘) → (𝑥𝑐(1 / (#‘𝐴))) = ((𝐹𝑘)↑𝑐(1 / (#‘𝐴))))
246240, 241, 244, 245fmptco 6303 . . . . 5 (𝜑 → ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴)))) ∘ 𝐹) = (𝑘𝐴 ↦ ((𝐹𝑘)↑𝑐(1 / (#‘𝐴)))))
247246oveq2d 6565 . . . 4 (𝜑 → ((𝑀s+) Σg ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴)))) ∘ 𝐹)) = ((𝑀s+) Σg (𝑘𝐴 ↦ ((𝐹𝑘)↑𝑐(1 / (#‘𝐴))))))
248227, 239, 2473eqtr4rd 2655 . . 3 (𝜑 → ((𝑀s+) Σg ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴)))) ∘ 𝐹)) = (𝑀 Σg (𝐹𝑓𝑐(𝐴 × {(1 / (#‘𝐴))}))))
24943, 44sstri 3577 . . . . . . 7 + ⊆ ℂ
250 eqid 2610 . . . . . . . 8 (𝑀s+) = (𝑀s+)
2511, 47mgpbas 18318 . . . . . . . 8 ℂ = (Base‘𝑀)
252250, 251ressbas2 15758 . . . . . . 7 (ℝ+ ⊆ ℂ → ℝ+ = (Base‘(𝑀s+)))
253249, 252ax-mp 5 . . . . . 6 + = (Base‘(𝑀s+))
2541, 51ringidval 18326 . . . . . . 7 1 = (0g𝑀)
2551oveq1i 6559 . . . . . . . . . . . 12 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
256255rpmsubg 19629 . . . . . . . . . . 11 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
257 subgsubm 17439 . . . . . . . . . . 11 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
258256, 257ax-mp 5 . . . . . . . . . 10 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
25947, 58, 59drngui 18576 . . . . . . . . . . . . 13 (ℂ ∖ {0}) = (Unit‘ℂfld)
260259, 1unitsubm 18493 . . . . . . . . . . . 12 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
26157, 260ax-mp 5 . . . . . . . . . . 11 (ℂ ∖ {0}) ∈ (SubMnd‘𝑀)
262 eqid 2610 . . . . . . . . . . . 12 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
263262subsubm 17180 . . . . . . . . . . 11 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
264261, 263ax-mp 5 . . . . . . . . . 10 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
265258, 264mpbi 219 . . . . . . . . 9 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
266265simpli 473 . . . . . . . 8 + ∈ (SubMnd‘𝑀)
267 eqid 2610 . . . . . . . . 9 (𝑀s+) = (𝑀s+)
268 eqid 2610 . . . . . . . . 9 (0g𝑀) = (0g𝑀)
269267, 268subm0 17179 . . . . . . . 8 (ℝ+ ∈ (SubMnd‘𝑀) → (0g𝑀) = (0g‘(𝑀s+)))
270266, 269ax-mp 5 . . . . . . 7 (0g𝑀) = (0g‘(𝑀s+))
271254, 270eqtri 2632 . . . . . 6 1 = (0g‘(𝑀s+))
2721crngmgp 18378 . . . . . . . 8 (ℂfld ∈ CRing → 𝑀 ∈ CMnd)
27373, 272ax-mp 5 . . . . . . 7 𝑀 ∈ CMnd
2741oveq1i 6559 . . . . . . . . . . . 12 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
275274rpmsubg 19629 . . . . . . . . . . 11 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
276 subgsubm 17439 . . . . . . . . . . 11 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
277275, 276ax-mp 5 . . . . . . . . . 10 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
27847, 58, 59drngui 18576 . . . . . . . . . . . . 13 (ℂ ∖ {0}) = (Unit‘ℂfld)
279278, 1unitsubm 18493 . . . . . . . . . . . 12 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
28057, 279ax-mp 5 . . . . . . . . . . 11 (ℂ ∖ {0}) ∈ (SubMnd‘𝑀)
281 eqid 2610 . . . . . . . . . . . 12 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
282281subsubm 17180 . . . . . . . . . . 11 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
283280, 282ax-mp 5 . . . . . . . . . 10 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
284277, 283mpbi 219 . . . . . . . . 9 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
285284simpli 473 . . . . . . . 8 + ∈ (SubMnd‘𝑀)
286 eqid 2610 . . . . . . . . 9 (𝑀s+) = (𝑀s+)
287286submmnd 17177 . . . . . . . 8 (ℝ+ ∈ (SubMnd‘𝑀) → (𝑀s+) ∈ Mnd)
288285, 287mp1i 13 . . . . . . 7 (𝜑 → (𝑀s+) ∈ Mnd)
289 eqid 2610 . . . . . . . 8 (𝑀s+) = (𝑀s+)
290289subcmn 18065 . . . . . . 7 ((𝑀 ∈ CMnd ∧ (𝑀s+) ∈ Mnd) → (𝑀s+) ∈ CMnd)
291273, 288, 290sylancr 694 . . . . . 6 (𝜑 → (𝑀s+) ∈ CMnd)
292 1red 9934 . . . . . . 7 (𝜑 → 1 ∈ ℝ)
2934, 2, 292fdmfifsupp 8168 . . . . . 6 (𝜑𝐹 finSupp 1)
294253, 271, 291, 2, 4, 293gsumcl 18139 . . . . 5 (𝜑 → ((𝑀s+) Σg 𝐹) ∈ ℝ+)
295 oveq1 6556 . . . . . 6 (𝑘 = ((𝑀s+) Σg 𝐹) → (𝑘𝑐(1 / (#‘𝐴))) = (((𝑀s+) Σg 𝐹)↑𝑐(1 / (#‘𝐴))))
296 eqid 2610 . . . . . 6 (𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴)))) = (𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))
297 ovex 6577 . . . . . 6 (𝑘𝑐(1 / (#‘𝐴))) ∈ V
298295, 296, 297fvmpt3i 6196 . . . . 5 (((𝑀s+) Σg 𝐹) ∈ ℝ+ → ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))‘((𝑀s+) Σg 𝐹)) = (((𝑀s+) Σg 𝐹)↑𝑐(1 / (#‘𝐴))))
299294, 298syl 17 . . . 4 (𝜑 → ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))‘((𝑀s+) Σg 𝐹)) = (((𝑀s+) Σg 𝐹)↑𝑐(1 / (#‘𝐴))))
3001oveq1i 6559 . . . . . . . . . . 11 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
301300rpmsubg 19629 . . . . . . . . . 10 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
302 subgsubm 17439 . . . . . . . . . 10 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
303301, 302ax-mp 5 . . . . . . . . 9 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
30447, 58, 59drngui 18576 . . . . . . . . . . . 12 (ℂ ∖ {0}) = (Unit‘ℂfld)
305304, 1unitsubm 18493 . . . . . . . . . . 11 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
30657, 305ax-mp 5 . . . . . . . . . 10 (ℂ ∖ {0}) ∈ (SubMnd‘𝑀)
307 eqid 2610 . . . . . . . . . . 11 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
308307subsubm 17180 . . . . . . . . . 10 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
309306, 308ax-mp 5 . . . . . . . . 9 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
310303, 309mpbi 219 . . . . . . . 8 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
311310simpli 473 . . . . . . 7 + ∈ (SubMnd‘𝑀)
312311a1i 11 . . . . . 6 (𝜑 → ℝ+ ∈ (SubMnd‘𝑀))
313 eqid 2610 . . . . . 6 (𝑀s+) = (𝑀s+)
3142, 312, 4, 313gsumsubm 17196 . . . . 5 (𝜑 → (𝑀 Σg 𝐹) = ((𝑀s+) Σg 𝐹))
315314oveq1d 6564 . . . 4 (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (#‘𝐴))) = (((𝑀s+) Σg 𝐹)↑𝑐(1 / (#‘𝐴))))
316299, 315eqtr4d 2647 . . 3 (𝜑 → ((𝑘 ∈ ℝ+ ↦ (𝑘𝑐(1 / (#‘𝐴))))‘((𝑀s+) Σg 𝐹)) = ((𝑀 Σg 𝐹)↑𝑐(1 / (#‘𝐴))))
317203, 248, 3163eqtr3d 2652 . 2 (𝜑 → (𝑀 Σg (𝐹𝑓𝑐(𝐴 × {(1 / (#‘𝐴))}))) = ((𝑀 Σg 𝐹)↑𝑐(1 / (#‘𝐴))))
3184ffvelrnda 6267 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
319318rpcnd 11750 . . . . . . 7 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℂ)
3202, 319fsumcl 14311 . . . . . 6 (𝜑 → Σ𝑘𝐴 (𝐹𝑘) ∈ ℂ)
321 hashnncl 13018 . . . . . . . . 9 (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
3222, 321syl 17 . . . . . . . 8 (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
3233, 322mpbird 246 . . . . . . 7 (𝜑 → (#‘𝐴) ∈ ℕ)
324323nncnd 10913 . . . . . 6 (𝜑 → (#‘𝐴) ∈ ℂ)
325 hashnncl 13018 . . . . . . . . 9 (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
3262, 325syl 17 . . . . . . . 8 (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
3273, 326mpbird 246 . . . . . . 7 (𝜑 → (#‘𝐴) ∈ ℕ)
328327nnne0d 10942 . . . . . 6 (𝜑 → (#‘𝐴) ≠ 0)
329320, 324, 328divrecd 10683 . . . . 5 (𝜑 → (Σ𝑘𝐴 (𝐹𝑘) / (#‘𝐴)) = (Σ𝑘𝐴 (𝐹𝑘) · (1 / (#‘𝐴))))
330 hashnncl 13018 . . . . . . . . . 10 (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
3312, 330syl 17 . . . . . . . . 9 (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
3323, 331mpbird 246 . . . . . . . 8 (𝜑 → (#‘𝐴) ∈ ℕ)
333332nnrecred 10943 . . . . . . 7 (𝜑 → (1 / (#‘𝐴)) ∈ ℝ)
334333recnd 9947 . . . . . 6 (𝜑 → (1 / (#‘𝐴)) ∈ ℂ)
3354ffvelrnda 6267 . . . . . . 7 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
336335rpcnd 11750 . . . . . 6 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℂ)
3372, 334, 336fsummulc1 14359 . . . . 5 (𝜑 → (Σ𝑘𝐴 (𝐹𝑘) · (1 / (#‘𝐴))) = Σ𝑘𝐴 ((𝐹𝑘) · (1 / (#‘𝐴))))
338329, 337eqtr2d 2645 . . . 4 (𝜑 → Σ𝑘𝐴 ((𝐹𝑘) · (1 / (#‘𝐴))) = (Σ𝑘𝐴 (𝐹𝑘) / (#‘𝐴)))
3394ffvelrnda 6267 . . . . . . 7 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
340339rpcnd 11750 . . . . . 6 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℂ)
341 hashnncl 13018 . . . . . . . . . . 11 (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
3422, 341syl 17 . . . . . . . . . 10 (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
3433, 342mpbird 246 . . . . . . . . 9 (𝜑 → (#‘𝐴) ∈ ℕ)
344343nnrecred 10943 . . . . . . . 8 (𝜑 → (1 / (#‘𝐴)) ∈ ℝ)
345344recnd 9947 . . . . . . 7 (𝜑 → (1 / (#‘𝐴)) ∈ ℂ)
346345adantr 480 . . . . . 6 ((𝜑𝑘𝐴) → (1 / (#‘𝐴)) ∈ ℂ)
347340, 346mulcld 9939 . . . . 5 ((𝜑𝑘𝐴) → ((𝐹𝑘) · (1 / (#‘𝐴))) ∈ ℂ)
3482, 347gsumfsum 19632 . . . 4 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ ((𝐹𝑘) · (1 / (#‘𝐴))))) = Σ𝑘𝐴 ((𝐹𝑘) · (1 / (#‘𝐴))))
3494ffvelrnda 6267 . . . . . . 7 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
350349rpcnd 11750 . . . . . 6 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℂ)
3512, 350gsumfsum 19632 . . . . 5 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ (𝐹𝑘))) = Σ𝑘𝐴 (𝐹𝑘))
352351oveq1d 6564 . . . 4 (𝜑 → ((ℂfld Σg (𝑘𝐴 ↦ (𝐹𝑘))) / (#‘𝐴)) = (Σ𝑘𝐴 (𝐹𝑘) / (#‘𝐴)))
353338, 348, 3523eqtr4d 2654 . . 3 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ ((𝐹𝑘) · (1 / (#‘𝐴))))) = ((ℂfld Σg (𝑘𝐴 ↦ (𝐹𝑘))) / (#‘𝐴)))
3544ffvelrnda 6267 . . . . 5 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
355 hashnncl 13018 . . . . . . . . . 10 (𝐴 ∈ Fin → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
3562, 355syl 17 . . . . . . . . 9 (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
3573, 356mpbird 246 . . . . . . . 8 (𝜑 → (#‘𝐴) ∈ ℕ)
358357nnrecred 10943 . . . . . . 7 (𝜑 → (1 / (#‘𝐴)) ∈ ℝ)
359358recnd 9947 . . . . . 6 (𝜑 → (1 / (#‘𝐴)) ∈ ℂ)
360359adantr 480 . . . . 5 ((𝜑𝑘𝐴) → (1 / (#‘𝐴)) ∈ ℂ)
3614feqmptd 6159 . . . . 5 (𝜑𝐹 = (𝑘𝐴 ↦ (𝐹𝑘)))
362 fconstmpt 5085 . . . . . 6 (𝐴 × {(1 / (#‘𝐴))}) = (𝑘𝐴 ↦ (1 / (#‘𝐴)))
363362a1i 11 . . . . 5 (𝜑 → (𝐴 × {(1 / (#‘𝐴))}) = (𝑘𝐴 ↦ (1 / (#‘𝐴))))
3642, 354, 360, 361, 363offval2 6812 . . . 4 (𝜑 → (𝐹𝑓 · (𝐴 × {(1 / (#‘𝐴))})) = (𝑘𝐴 ↦ ((𝐹𝑘) · (1 / (#‘𝐴)))))
365364oveq2d 6565 . . 3 (𝜑 → (ℂfld Σg (𝐹𝑓 · (𝐴 × {(1 / (#‘𝐴))}))) = (ℂfld Σg (𝑘𝐴 ↦ ((𝐹𝑘) · (1 / (#‘𝐴))))))
3664feqmptd 6159 . . . . 5 (𝜑𝐹 = (𝑘𝐴 ↦ (𝐹𝑘)))
367366oveq2d 6565 . . . 4 (𝜑 → (ℂfld Σg 𝐹) = (ℂfld Σg (𝑘𝐴 ↦ (𝐹𝑘))))
368367oveq1d 6564 . . 3 (𝜑 → ((ℂfld Σg 𝐹) / (#‘𝐴)) = ((ℂfld Σg (𝑘𝐴 ↦ (𝐹𝑘))) / (#‘𝐴)))
369353, 365, 3683eqtr4d 2654 . 2 (𝜑 → (ℂfld Σg (𝐹𝑓 · (𝐴 × {(1 / (#‘𝐴))}))) = ((ℂfld Σg 𝐹) / (#‘𝐴)))
37042, 317, 3693brtr3d 4614 1 (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (#‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (#‘𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977  wne 2780  Vcvv 3173  cdif 3537  wss 3540  c0 3874  {csn 4125   class class class wbr 4583  cmpt 4643   × cxp 5036  ccom 5042  wf 5800  cfv 5804  (class class class)co 6549  𝑓 cof 6793  Fincfn 7841  cc 9813  cr 9814  0cc0 9815  1c1 9816   · cmul 9820  cle 9954   / cdiv 10563  cn 10897  +crp 11708  #chash 12979  Σcsu 14264  Basecbs 15695  s cress 15696  +gcplusg 15768  0gc0g 15923   Σg cgsu 15924  Mndcmnd 17117   MndHom cmhm 17156  SubMndcsubmnd 17157  Grpcgrp 17245  SubGrpcsubg 17411   GrpHom cghm 17480  CMndccmn 18016  mulGrpcmgp 18312  Ringcrg 18370  CRingccrg 18371  fldccnfld 19567  𝑐ccxp 24106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-tpos 7239  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ioc 12051  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-fac 12923  df-bc 12952  df-hash 12980  df-shft 13655  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265  df-ef 14637  df-sin 14639  df-cos 14640  df-pi 14642  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-rest 15906  df-topn 15907  df-0g 15925  df-gsum 15926  df-topgen 15927  df-pt 15928  df-prds 15931  df-xrs 15985  df-qtop 15990  df-imas 15991  df-xps 15993  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-mhm 17158  df-submnd 17159  df-grp 17248  df-minusg 17249  df-mulg 17364  df-subg 17414  df-ghm 17481  df-gim 17524  df-cntz 17573  df-cmn 18018  df-abl 18019  df-mgp 18313  df-ur 18325  df-ring 18372  df-cring 18373  df-oppr 18446  df-dvdsr 18464  df-unit 18465  df-invr 18495  df-dvr 18506  df-drng 18572  df-subrg 18601  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-cnfld 19568  df-refld 19770  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-lp 20750  df-perf 20751  df-cn 20841  df-cnp 20842  df-haus 20929  df-cmp 21000  df-tx 21175  df-hmeo 21368  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-xms 21935  df-ms 21936  df-tms 21937  df-cncf 22489  df-limc 23436  df-dv 23437  df-log 24107  df-cxp 24108
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator