Step | Hyp | Ref
| Expression |
1 | | simpl3 1059 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ 𝐴 = ∅) → 𝑋 ∈ 𝐵) |
2 | | gsumconst.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
3 | | eqid 2610 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
4 | | gsumconst.m |
. . . . . 6
⊢ · =
(.g‘𝐺) |
5 | 2, 3, 4 | mulg0 17369 |
. . . . 5
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = (0g‘𝐺)) |
6 | 1, 5 | syl 17 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ 𝐴 = ∅) → (0 · 𝑋) = (0g‘𝐺)) |
7 | | fveq2 6103 |
. . . . . . 7
⊢ (𝐴 = ∅ → (#‘𝐴) =
(#‘∅)) |
8 | 7 | adantl 481 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ 𝐴 = ∅) → (#‘𝐴) =
(#‘∅)) |
9 | | hash0 13019 |
. . . . . 6
⊢
(#‘∅) = 0 |
10 | 8, 9 | syl6eq 2660 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ 𝐴 = ∅) → (#‘𝐴) = 0) |
11 | 10 | oveq1d 6564 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ 𝐴 = ∅) → ((#‘𝐴) · 𝑋) = (0 · 𝑋)) |
12 | | mpteq1 4665 |
. . . . . . . 8
⊢ (𝐴 = ∅ → (𝑘 ∈ 𝐴 ↦ 𝑋) = (𝑘 ∈ ∅ ↦ 𝑋)) |
13 | 12 | adantl 481 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ 𝐴 = ∅) → (𝑘 ∈ 𝐴 ↦ 𝑋) = (𝑘 ∈ ∅ ↦ 𝑋)) |
14 | | mpt0 5934 |
. . . . . . 7
⊢ (𝑘 ∈ ∅ ↦ 𝑋) = ∅ |
15 | 13, 14 | syl6eq 2660 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ 𝐴 = ∅) → (𝑘 ∈ 𝐴 ↦ 𝑋) = ∅) |
16 | 15 | oveq2d 6565 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ 𝐴 = ∅) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = (𝐺 Σg
∅)) |
17 | 3 | gsum0 17101 |
. . . . 5
⊢ (𝐺 Σg
∅) = (0g‘𝐺) |
18 | 16, 17 | syl6eq 2660 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ 𝐴 = ∅) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = (0g‘𝐺)) |
19 | 6, 11, 18 | 3eqtr4rd 2655 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ 𝐴 = ∅) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((#‘𝐴) · 𝑋)) |
20 | 19 | ex 449 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) → (𝐴 = ∅ → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((#‘𝐴) · 𝑋))) |
21 | | simprl 790 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (#‘𝐴) ∈
ℕ) |
22 | | nnuz 11599 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
23 | 21, 22 | syl6eleq 2698 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (#‘𝐴) ∈
(ℤ≥‘1)) |
24 | | simpr 476 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(#‘𝐴))) → 𝑥 ∈ (1...(#‘𝐴))) |
25 | | simpl3 1059 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → 𝑋 ∈ 𝐵) |
26 | 25 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(#‘𝐴))) → 𝑋 ∈ 𝐵) |
27 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1...(#‘𝐴)) ↦ 𝑋) = (𝑥 ∈ (1...(#‘𝐴)) ↦ 𝑋) |
28 | 27 | fvmpt2 6200 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (1...(#‘𝐴)) ∧ 𝑋 ∈ 𝐵) → ((𝑥 ∈ (1...(#‘𝐴)) ↦ 𝑋)‘𝑥) = 𝑋) |
29 | 24, 26, 28 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(#‘𝐴))) → ((𝑥 ∈ (1...(#‘𝐴)) ↦ 𝑋)‘𝑥) = 𝑋) |
30 | | f1of 6050 |
. . . . . . . . . . . . 13
⊢ (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(#‘𝐴))⟶𝐴) |
31 | 30 | ad2antll 761 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(#‘𝐴))⟶𝐴) |
32 | 31 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(#‘𝐴))) → (𝑓‘𝑥) ∈ 𝐴) |
33 | 31 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → 𝑓 = (𝑥 ∈ (1...(#‘𝐴)) ↦ (𝑓‘𝑥))) |
34 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝑋) = (𝑘 ∈ 𝐴 ↦ 𝑋)) |
35 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑓‘𝑥) → 𝑋 = 𝑋) |
36 | 32, 33, 34, 35 | fmptco 6303 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝑋) ∘ 𝑓) = (𝑥 ∈ (1...(#‘𝐴)) ↦ 𝑋)) |
37 | 36 | fveq1d 6105 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (((𝑘 ∈ 𝐴 ↦ 𝑋) ∘ 𝑓)‘𝑥) = ((𝑥 ∈ (1...(#‘𝐴)) ↦ 𝑋)‘𝑥)) |
38 | 37 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(#‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝑋) ∘ 𝑓)‘𝑥) = ((𝑥 ∈ (1...(#‘𝐴)) ↦ 𝑋)‘𝑥)) |
39 | | elfznn 12241 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1...(#‘𝐴)) → 𝑥 ∈ ℕ) |
40 | | fvconst2g 6372 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑥 ∈ ℕ) → ((ℕ ×
{𝑋})‘𝑥) = 𝑋) |
41 | 25, 39, 40 | syl2an 493 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(#‘𝐴))) → ((ℕ × {𝑋})‘𝑥) = 𝑋) |
42 | 29, 38, 41 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(#‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝑋) ∘ 𝑓)‘𝑥) = ((ℕ × {𝑋})‘𝑥)) |
43 | 23, 42 | seqfveq 12687 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) →
(seq1((+g‘𝐺), ((𝑘 ∈ 𝐴 ↦ 𝑋) ∘ 𝑓))‘(#‘𝐴)) = (seq1((+g‘𝐺), (ℕ × {𝑋}))‘(#‘𝐴))) |
44 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘𝐺) = (+g‘𝐺) |
45 | | eqid 2610 |
. . . . . . 7
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
46 | | simpl1 1057 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → 𝐺 ∈ Mnd) |
47 | | simpl2 1058 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → 𝐴 ∈ Fin) |
48 | 25 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) |
49 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝐴 ↦ 𝑋) = (𝑘 ∈ 𝐴 ↦ 𝑋) |
50 | 48, 49 | fmptd 6292 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝑋):𝐴⟶𝐵) |
51 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (𝑋(+g‘𝐺)𝑋) = (𝑋(+g‘𝐺)𝑋)) |
52 | 2, 44, 45 | elcntzsn 17581 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐵 → (𝑋 ∈ ((Cntz‘𝐺)‘{𝑋}) ↔ (𝑋 ∈ 𝐵 ∧ (𝑋(+g‘𝐺)𝑋) = (𝑋(+g‘𝐺)𝑋)))) |
53 | 25, 52 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (𝑋 ∈ ((Cntz‘𝐺)‘{𝑋}) ↔ (𝑋 ∈ 𝐵 ∧ (𝑋(+g‘𝐺)𝑋) = (𝑋(+g‘𝐺)𝑋)))) |
54 | 25, 51, 53 | mpbir2and 959 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → 𝑋 ∈ ((Cntz‘𝐺)‘{𝑋})) |
55 | 54 | snssd 4281 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → {𝑋} ⊆ ((Cntz‘𝐺)‘{𝑋})) |
56 | | snidg 4153 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ {𝑋}) |
57 | 25, 56 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → 𝑋 ∈ {𝑋}) |
58 | 57 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ {𝑋}) |
59 | 58, 49 | fmptd 6292 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝑋):𝐴⟶{𝑋}) |
60 | | frn 5966 |
. . . . . . . . 9
⊢ ((𝑘 ∈ 𝐴 ↦ 𝑋):𝐴⟶{𝑋} → ran (𝑘 ∈ 𝐴 ↦ 𝑋) ⊆ {𝑋}) |
61 | 59, 60 | syl 17 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ran (𝑘 ∈ 𝐴 ↦ 𝑋) ⊆ {𝑋}) |
62 | 45 | cntzidss 17593 |
. . . . . . . 8
⊢ (({𝑋} ⊆ ((Cntz‘𝐺)‘{𝑋}) ∧ ran (𝑘 ∈ 𝐴 ↦ 𝑋) ⊆ {𝑋}) → ran (𝑘 ∈ 𝐴 ↦ 𝑋) ⊆ ((Cntz‘𝐺)‘ran (𝑘 ∈ 𝐴 ↦ 𝑋))) |
63 | 55, 61, 62 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ran (𝑘 ∈ 𝐴 ↦ 𝑋) ⊆ ((Cntz‘𝐺)‘ran (𝑘 ∈ 𝐴 ↦ 𝑋))) |
64 | | f1of1 6049 |
. . . . . . . 8
⊢ (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(#‘𝐴))–1-1→𝐴) |
65 | 64 | ad2antll 761 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(#‘𝐴))–1-1→𝐴) |
66 | | suppssdm 7195 |
. . . . . . . . 9
⊢ ((𝑘 ∈ 𝐴 ↦ 𝑋) supp (0g‘𝐺)) ⊆ dom (𝑘 ∈ 𝐴 ↦ 𝑋) |
67 | 49 | dmmptss 5548 |
. . . . . . . . . 10
⊢ dom
(𝑘 ∈ 𝐴 ↦ 𝑋) ⊆ 𝐴 |
68 | 67 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → dom (𝑘 ∈ 𝐴 ↦ 𝑋) ⊆ 𝐴) |
69 | 66, 68 | syl5ss 3579 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝑋) supp (0g‘𝐺)) ⊆ 𝐴) |
70 | | f1ofo 6057 |
. . . . . . . . . 10
⊢ (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(#‘𝐴))–onto→𝐴) |
71 | | forn 6031 |
. . . . . . . . . 10
⊢ (𝑓:(1...(#‘𝐴))–onto→𝐴 → ran 𝑓 = 𝐴) |
72 | 70, 71 | syl 17 |
. . . . . . . . 9
⊢ (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → ran 𝑓 = 𝐴) |
73 | 72 | ad2antll 761 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ran 𝑓 = 𝐴) |
74 | 69, 73 | sseqtr4d 3605 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝑋) supp (0g‘𝐺)) ⊆ ran 𝑓) |
75 | | eqid 2610 |
. . . . . . 7
⊢ (((𝑘 ∈ 𝐴 ↦ 𝑋) ∘ 𝑓) supp (0g‘𝐺)) = (((𝑘 ∈ 𝐴 ↦ 𝑋) ∘ 𝑓) supp (0g‘𝐺)) |
76 | 2, 3, 44, 45, 46, 47, 50, 63, 21, 65, 74, 75 | gsumval3 18131 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = (seq1((+g‘𝐺), ((𝑘 ∈ 𝐴 ↦ 𝑋) ∘ 𝑓))‘(#‘𝐴))) |
77 | | eqid 2610 |
. . . . . . . 8
⊢
seq1((+g‘𝐺), (ℕ × {𝑋})) = seq1((+g‘𝐺), (ℕ × {𝑋})) |
78 | 2, 44, 4, 77 | mulgnn 17370 |
. . . . . . 7
⊢
(((#‘𝐴) ∈
ℕ ∧ 𝑋 ∈
𝐵) → ((#‘𝐴) · 𝑋) = (seq1((+g‘𝐺), (ℕ × {𝑋}))‘(#‘𝐴))) |
79 | 21, 25, 78 | syl2anc 691 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ((#‘𝐴) · 𝑋) = (seq1((+g‘𝐺), (ℕ × {𝑋}))‘(#‘𝐴))) |
80 | 43, 76, 79 | 3eqtr4d 2654 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((#‘𝐴) · 𝑋)) |
81 | 80 | expr 641 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ (#‘𝐴) ∈ ℕ) → (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((#‘𝐴) · 𝑋))) |
82 | 81 | exlimdv 1848 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) ∧ (#‘𝐴) ∈ ℕ) → (∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((#‘𝐴) · 𝑋))) |
83 | 82 | expimpd 627 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) → (((#‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((#‘𝐴) · 𝑋))) |
84 | | fz1f1o 14288 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ((#‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴))) |
85 | 84 | 3ad2ant2 1076 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) → (𝐴 = ∅ ∨ ((#‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴))) |
86 | 20, 83, 85 | mpjaod 395 |
1
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((#‘𝐴) · 𝑋)) |