Step |
Hyp |
Ref |
Expression |
1 |
|
amgm.1 |
⊢ 𝑀 = ( mulGrp ‘ ℂfld ) |
2 |
|
cnfldbas |
⊢ ℂ = ( Base ‘ ℂfld ) |
3 |
1 2
|
mgpbas |
⊢ ℂ = ( Base ‘ 𝑀 ) |
4 |
|
cnfld1 |
⊢ 1 = ( 1r ‘ ℂfld ) |
5 |
1 4
|
ringidval |
⊢ 1 = ( 0g ‘ 𝑀 ) |
6 |
|
cnfldmul |
⊢ · = ( .r ‘ ℂfld ) |
7 |
1 6
|
mgpplusg |
⊢ · = ( +g ‘ 𝑀 ) |
8 |
|
cncrng |
⊢ ℂfld ∈ CRing |
9 |
1
|
crngmgp |
⊢ ( ℂfld ∈ CRing → 𝑀 ∈ CMnd ) |
10 |
8 9
|
mp1i |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝑀 ∈ CMnd ) |
11 |
|
simpl1 |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝐴 ∈ Fin ) |
12 |
|
simpl3 |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) |
13 |
|
rge0ssre |
⊢ ( 0 [,) +∞ ) ⊆ ℝ |
14 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
15 |
13 14
|
sstri |
⊢ ( 0 [,) +∞ ) ⊆ ℂ |
16 |
|
fss |
⊢ ( ( 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ ) |
17 |
12 15 16
|
sylancl |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝐹 : 𝐴 ⟶ ℂ ) |
18 |
|
1ex |
⊢ 1 ∈ V |
19 |
18
|
a1i |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 1 ∈ V ) |
20 |
17 11 19
|
fdmfifsupp |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝐹 finSupp 1 ) |
21 |
|
disjdif |
⊢ ( { 𝑥 } ∩ ( 𝐴 ∖ { 𝑥 } ) ) = ∅ |
22 |
21
|
a1i |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( { 𝑥 } ∩ ( 𝐴 ∖ { 𝑥 } ) ) = ∅ ) |
23 |
|
undif2 |
⊢ ( { 𝑥 } ∪ ( 𝐴 ∖ { 𝑥 } ) ) = ( { 𝑥 } ∪ 𝐴 ) |
24 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝑥 ∈ 𝐴 ) |
25 |
24
|
snssd |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → { 𝑥 } ⊆ 𝐴 ) |
26 |
|
ssequn1 |
⊢ ( { 𝑥 } ⊆ 𝐴 ↔ ( { 𝑥 } ∪ 𝐴 ) = 𝐴 ) |
27 |
25 26
|
sylib |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( { 𝑥 } ∪ 𝐴 ) = 𝐴 ) |
28 |
23 27
|
eqtr2id |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝐴 = ( { 𝑥 } ∪ ( 𝐴 ∖ { 𝑥 } ) ) ) |
29 |
3 5 7 10 11 17 20 22 28
|
gsumsplit |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝑀 Σg 𝐹 ) = ( ( 𝑀 Σg ( 𝐹 ↾ { 𝑥 } ) ) · ( 𝑀 Σg ( 𝐹 ↾ ( 𝐴 ∖ { 𝑥 } ) ) ) ) ) |
30 |
12 25
|
feqresmpt |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝐹 ↾ { 𝑥 } ) = ( 𝑦 ∈ { 𝑥 } ↦ ( 𝐹 ‘ 𝑦 ) ) ) |
31 |
30
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝑀 Σg ( 𝐹 ↾ { 𝑥 } ) ) = ( 𝑀 Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝐹 ‘ 𝑦 ) ) ) ) |
32 |
|
cnring |
⊢ ℂfld ∈ Ring |
33 |
1
|
ringmgp |
⊢ ( ℂfld ∈ Ring → 𝑀 ∈ Mnd ) |
34 |
32 33
|
mp1i |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝑀 ∈ Mnd ) |
35 |
17 24
|
ffvelrnd |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ ) |
36 |
|
fveq2 |
⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) |
37 |
3 36
|
gsumsn |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℂ ) → ( 𝑀 Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝐹 ‘ 𝑥 ) ) |
38 |
34 24 35 37
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝑀 Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝐹 ‘ 𝑥 ) ) |
39 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝐹 ‘ 𝑥 ) = 0 ) |
40 |
31 38 39
|
3eqtrd |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝑀 Σg ( 𝐹 ↾ { 𝑥 } ) ) = 0 ) |
41 |
40
|
oveq1d |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( ( 𝑀 Σg ( 𝐹 ↾ { 𝑥 } ) ) · ( 𝑀 Σg ( 𝐹 ↾ ( 𝐴 ∖ { 𝑥 } ) ) ) ) = ( 0 · ( 𝑀 Σg ( 𝐹 ↾ ( 𝐴 ∖ { 𝑥 } ) ) ) ) ) |
42 |
|
diffi |
⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ { 𝑥 } ) ∈ Fin ) |
43 |
11 42
|
syl |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝐴 ∖ { 𝑥 } ) ∈ Fin ) |
44 |
|
difss |
⊢ ( 𝐴 ∖ { 𝑥 } ) ⊆ 𝐴 |
45 |
|
fssres |
⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐴 ∖ { 𝑥 } ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ∖ { 𝑥 } ) ) : ( 𝐴 ∖ { 𝑥 } ) ⟶ ℂ ) |
46 |
17 44 45
|
sylancl |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝐹 ↾ ( 𝐴 ∖ { 𝑥 } ) ) : ( 𝐴 ∖ { 𝑥 } ) ⟶ ℂ ) |
47 |
46 43 19
|
fdmfifsupp |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝐹 ↾ ( 𝐴 ∖ { 𝑥 } ) ) finSupp 1 ) |
48 |
3 5 10 43 46 47
|
gsumcl |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝑀 Σg ( 𝐹 ↾ ( 𝐴 ∖ { 𝑥 } ) ) ) ∈ ℂ ) |
49 |
48
|
mul02d |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 0 · ( 𝑀 Σg ( 𝐹 ↾ ( 𝐴 ∖ { 𝑥 } ) ) ) ) = 0 ) |
50 |
29 41 49
|
3eqtrd |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 𝑀 Σg 𝐹 ) = 0 ) |
51 |
50
|
oveq1d |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) = ( 0 ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ) |
52 |
|
simpl2 |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝐴 ≠ ∅ ) |
53 |
|
hashnncl |
⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ 𝐴 ≠ ∅ ) ) |
54 |
11 53
|
syl |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ 𝐴 ≠ ∅ ) ) |
55 |
52 54
|
mpbird |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ ) |
56 |
55
|
nncnd |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℂ ) |
57 |
55
|
nnne0d |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( ♯ ‘ 𝐴 ) ≠ 0 ) |
58 |
56 57
|
reccld |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 1 / ( ♯ ‘ 𝐴 ) ) ∈ ℂ ) |
59 |
56 57
|
recne0d |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 1 / ( ♯ ‘ 𝐴 ) ) ≠ 0 ) |
60 |
58 59
|
0cxpd |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 0 ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) = 0 ) |
61 |
51 60
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) = 0 ) |
62 |
|
cnfld0 |
⊢ 0 = ( 0g ‘ ℂfld ) |
63 |
|
ringcmn |
⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd ) |
64 |
32 63
|
mp1i |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ℂfld ∈ CMnd ) |
65 |
|
rege0subm |
⊢ ( 0 [,) +∞ ) ∈ ( SubMnd ‘ ℂfld ) |
66 |
65
|
a1i |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( 0 [,) +∞ ) ∈ ( SubMnd ‘ ℂfld ) ) |
67 |
|
c0ex |
⊢ 0 ∈ V |
68 |
67
|
a1i |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 0 ∈ V ) |
69 |
12 11 68
|
fdmfifsupp |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 𝐹 finSupp 0 ) |
70 |
62 64 11 66 12 69
|
gsumsubmcl |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( ℂfld Σg 𝐹 ) ∈ ( 0 [,) +∞ ) ) |
71 |
|
elrege0 |
⊢ ( ( ℂfld Σg 𝐹 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ℂfld Σg 𝐹 ) ∈ ℝ ∧ 0 ≤ ( ℂfld Σg 𝐹 ) ) ) |
72 |
70 71
|
sylib |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( ( ℂfld Σg 𝐹 ) ∈ ℝ ∧ 0 ≤ ( ℂfld Σg 𝐹 ) ) ) |
73 |
55
|
nnred |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℝ ) |
74 |
55
|
nngt0d |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 0 < ( ♯ ‘ 𝐴 ) ) |
75 |
|
divge0 |
⊢ ( ( ( ( ℂfld Σg 𝐹 ) ∈ ℝ ∧ 0 ≤ ( ℂfld Σg 𝐹 ) ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( ♯ ‘ 𝐴 ) ) ) → 0 ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) |
76 |
72 73 74 75
|
syl12anc |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → 0 ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) |
77 |
61 76
|
eqbrtrd |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) ) → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) |
78 |
77
|
rexlimdvaa |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 0 → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) ) |
79 |
|
ralnex |
⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑥 ) = 0 ↔ ¬ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 0 ) |
80 |
|
simpl1 |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑥 ) = 0 ) → 𝐴 ∈ Fin ) |
81 |
|
simpl2 |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑥 ) = 0 ) → 𝐴 ≠ ∅ ) |
82 |
|
simpl3 |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑥 ) = 0 ) → 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) |
83 |
82
|
ffnd |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑥 ) = 0 ) → 𝐹 Fn 𝐴 ) |
84 |
|
ffvelrn |
⊢ ( ( 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) |
85 |
84
|
3ad2antl3 |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) |
86 |
|
elrege0 |
⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
87 |
85 86
|
sylib |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
88 |
87
|
simprd |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) ) |
89 |
|
0re |
⊢ 0 ∈ ℝ |
90 |
87
|
simpld |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) |
91 |
|
leloe |
⊢ ( ( 0 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 0 < ( 𝐹 ‘ 𝑥 ) ∨ 0 = ( 𝐹 ‘ 𝑥 ) ) ) ) |
92 |
89 90 91
|
sylancr |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 0 < ( 𝐹 ‘ 𝑥 ) ∨ 0 = ( 𝐹 ‘ 𝑥 ) ) ) ) |
93 |
88 92
|
mpbid |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 0 < ( 𝐹 ‘ 𝑥 ) ∨ 0 = ( 𝐹 ‘ 𝑥 ) ) ) |
94 |
93
|
ord |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 0 < ( 𝐹 ‘ 𝑥 ) → 0 = ( 𝐹 ‘ 𝑥 ) ) ) |
95 |
|
eqcom |
⊢ ( 0 = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 0 ) |
96 |
94 95
|
syl6ib |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 0 < ( 𝐹 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 ) ) |
97 |
96
|
con1d |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ ( 𝐹 ‘ 𝑥 ) = 0 → 0 < ( 𝐹 ‘ 𝑥 ) ) ) |
98 |
|
elrp |
⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ+ ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 < ( 𝐹 ‘ 𝑥 ) ) ) |
99 |
98
|
baib |
⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ+ ↔ 0 < ( 𝐹 ‘ 𝑥 ) ) ) |
100 |
90 99
|
syl |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ+ ↔ 0 < ( 𝐹 ‘ 𝑥 ) ) ) |
101 |
97 100
|
sylibrd |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ ( 𝐹 ‘ 𝑥 ) = 0 → ( 𝐹 ‘ 𝑥 ) ∈ ℝ+ ) ) |
102 |
101
|
ralimdva |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑥 ) = 0 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ℝ+ ) ) |
103 |
102
|
imp |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑥 ) = 0 ) → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ℝ+ ) |
104 |
|
ffnfv |
⊢ ( 𝐹 : 𝐴 ⟶ ℝ+ ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ℝ+ ) ) |
105 |
83 103 104
|
sylanbrc |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑥 ) = 0 ) → 𝐹 : 𝐴 ⟶ ℝ+ ) |
106 |
1 80 81 105
|
amgmlem |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑥 ) = 0 ) → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) |
107 |
106
|
ex |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑥 ) = 0 → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) ) |
108 |
79 107
|
syl5bir |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ¬ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 0 → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) ) |
109 |
78 108
|
pm2.61d |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) |