Step | Hyp | Ref
| Expression |
1 | | reprval.a |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℕ) |
2 | | reprval.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | | reprval.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
4 | | 1nn0 12249 |
. . . . 5
⊢ 1 ∈
ℕ0 |
5 | 4 | a1i 11 |
. . . 4
⊢ (𝜑 → 1 ∈
ℕ0) |
6 | 3, 5 | nn0addcld 12297 |
. . 3
⊢ (𝜑 → (𝑆 + 1) ∈
ℕ0) |
7 | 1, 2, 6 | reprval 32590 |
. 2
⊢ (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = {𝑐 ∈ (𝐴 ↑m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀}) |
8 | | simplr 766 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) |
9 | | elmapi 8637 |
. . . . . . . . . 10
⊢ (𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒:(0..^(𝑆 + 1))⟶𝐴) |
11 | 3 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑆 ∈
ℕ0) |
12 | | fzonn0p1 13464 |
. . . . . . . . . 10
⊢ (𝑆 ∈ ℕ0
→ 𝑆 ∈ (0..^(𝑆 + 1))) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑆 ∈ (0..^(𝑆 + 1))) |
14 | 10, 13 | ffvelrnd 6962 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒‘𝑆) ∈ 𝐴) |
15 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → 𝑏 = (𝑒‘𝑆)) |
16 | 15 | oveq2d 7291 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (𝑀 − 𝑏) = (𝑀 − (𝑒‘𝑆))) |
17 | 16 | oveq2d 7291 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (𝐴(repr‘𝑆)(𝑀 − 𝑏)) = (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆)))) |
18 | | opeq2 4805 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑒‘𝑆) → 〈𝑆, 𝑏〉 = 〈𝑆, (𝑒‘𝑆)〉) |
19 | 18 | sneqd 4573 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑒‘𝑆) → {〈𝑆, 𝑏〉} = {〈𝑆, (𝑒‘𝑆)〉}) |
20 | 19 | uneq2d 4097 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑒‘𝑆) → (𝑐 ∪ {〈𝑆, 𝑏〉}) = (𝑐 ∪ {〈𝑆, (𝑒‘𝑆)〉})) |
21 | 20 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑏 = (𝑒‘𝑆) → (𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉}) ↔ 𝑒 = (𝑐 ∪ {〈𝑆, (𝑒‘𝑆)〉}))) |
22 | 21 | adantl 482 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉}) ↔ 𝑒 = (𝑐 ∪ {〈𝑆, (𝑒‘𝑆)〉}))) |
23 | 17, 22 | rexeqbidv 3337 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑏 = (𝑒‘𝑆)) → (∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉}) ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆)))𝑒 = (𝑐 ∪ {〈𝑆, (𝑒‘𝑆)〉}))) |
24 | 9 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → 𝑒:(0..^(𝑆 + 1))⟶𝐴) |
25 | 3 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → 𝑆 ∈
ℕ0) |
26 | | fzossfzop1 13465 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∈ ℕ0
→ (0..^𝑆) ⊆
(0..^(𝑆 +
1))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → (0..^𝑆) ⊆ (0..^(𝑆 + 1))) |
28 | 24, 27 | fssresd 6641 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴) |
29 | 28 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴) |
30 | | nnex 11979 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ
∈ V |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ℕ ∈
V) |
32 | 31, 1 | ssexd 5248 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ V) |
33 | | fzofi 13694 |
. . . . . . . . . . . . . . . 16
⊢
(0..^𝑆) ∈
Fin |
34 | 33 | elexi 3451 |
. . . . . . . . . . . . . . 15
⊢
(0..^𝑆) ∈
V |
35 | | elmapg 8628 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑m (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)) |
36 | 32, 34, 35 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑m (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)) |
37 | 36 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑m (0..^𝑆)) ↔ (𝑒 ↾ (0..^𝑆)):(0..^𝑆)⟶𝐴)) |
38 | 29, 37 | mpbird 256 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑m (0..^𝑆))) |
39 | 33 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → (0..^𝑆) ∈ Fin) |
40 | | nnsscn 11978 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℕ
⊆ ℂ |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ℕ ⊆
ℂ) |
42 | 1, 41 | sstrd 3931 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
43 | 42 | ad2antrr 723 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ) |
44 | 28 | ffvelrnda 6961 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ 𝐴) |
45 | 43, 44 | sseldd 3922 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ) |
46 | 39, 45 | fsumcl 15445 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) ∈ ℂ) |
48 | 42 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → 𝐴 ⊆ ℂ) |
49 | 25, 12 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → 𝑆 ∈ (0..^(𝑆 + 1))) |
50 | 24, 49 | ffvelrnd 6962 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → (𝑒‘𝑆) ∈ 𝐴) |
51 | 48, 50 | sseldd 3922 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → (𝑒‘𝑆) ∈ ℂ) |
52 | 51 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒‘𝑆) ∈ ℂ) |
53 | 47, 52 | pncand 11333 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) − (𝑒‘𝑆)) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎)) |
54 | | nfv 1917 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑎(𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) |
55 | | nfcv 2907 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑎(𝑒‘𝑆) |
56 | | fzonel 13401 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬
𝑆 ∈ (0..^𝑆) |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → ¬ 𝑆 ∈ (0..^𝑆)) |
58 | 24 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴) |
59 | 27 | sselda 3921 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1))) |
60 | 58, 59 | ffvelrnd 6962 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ 𝐴) |
61 | 43, 60 | sseldd 3922 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ ℂ) |
62 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑆 → (𝑒‘𝑎) = (𝑒‘𝑆)) |
63 | 54, 55, 39, 25, 57, 61, 62, 51 | fsumsplitsn 15456 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆))) |
64 | | fzosplitsn 13495 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆 ∈
(ℤ≥‘0) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆})) |
65 | | nn0uz 12620 |
. . . . . . . . . . . . . . . . . . . 20
⊢
ℕ0 = (ℤ≥‘0) |
66 | 64, 65 | eleq2s 2857 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 ∈ ℕ0
→ (0..^(𝑆 + 1)) =
((0..^𝑆) ∪ {𝑆})) |
67 | 25, 66 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆})) |
68 | 67 | sumeq1d 15413 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎)) |
69 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆)) |
70 | 69 | fvresd 6794 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑒‘𝑎)) |
71 | 70 | sumeq2dv 15415 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎)) |
72 | 71 | oveq1d 7290 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) = (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆))) |
73 | 63, 68, 72 | 3eqtr4d 2788 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆))) |
74 | 73 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆))) |
75 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) |
76 | 74, 75 | eqtr3d 2780 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) = 𝑀) |
77 | 76 | oveq1d 7290 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) + (𝑒‘𝑆)) − (𝑒‘𝑆)) = (𝑀 − (𝑒‘𝑆))) |
78 | 53, 77 | eqtr3d 2780 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆))) |
79 | 38, 78 | jca 512 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆)))) |
80 | | fveq1 6773 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = (𝑒 ↾ (0..^𝑆)) → (𝑑‘𝑎) = ((𝑒 ↾ (0..^𝑆))‘𝑎)) |
81 | 80 | sumeq2sdv 15416 |
. . . . . . . . . . . . 13
⊢ (𝑑 = (𝑒 ↾ (0..^𝑆)) → Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎)) |
82 | 81 | eqeq1d 2740 |
. . . . . . . . . . . 12
⊢ (𝑑 = (𝑒 ↾ (0..^𝑆)) → (Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆)) ↔ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆)))) |
83 | 82 | elrab 3624 |
. . . . . . . . . . 11
⊢ ((𝑒 ↾ (0..^𝑆)) ∈ {𝑑 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆))} ↔ ((𝑒 ↾ (0..^𝑆)) ∈ (𝐴 ↑m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑒 ↾ (0..^𝑆))‘𝑎) = (𝑀 − (𝑒‘𝑆)))) |
84 | 79, 83 | sylibr 233 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ {𝑑 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆))}) |
85 | 1 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝐴 ⊆ ℕ) |
86 | 2 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑀 ∈ ℤ) |
87 | | nnssz 12340 |
. . . . . . . . . . . . . . 15
⊢ ℕ
⊆ ℤ |
88 | 1, 87 | sstrdi 3933 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ ℤ) |
89 | 88 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝐴 ⊆ ℤ) |
90 | 89, 14 | sseldd 3922 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒‘𝑆) ∈ ℤ) |
91 | 86, 90 | zsubcld 12431 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑀 − (𝑒‘𝑆)) ∈ ℤ) |
92 | 85, 91, 11 | reprval 32590 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆))) = {𝑑 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = (𝑀 − (𝑒‘𝑆))}) |
93 | 84, 92 | eleqtrrd 2842 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ (0..^𝑆)) ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆)))) |
94 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → 𝑐 = (𝑒 ↾ (0..^𝑆))) |
95 | 94 | uneq1d 4096 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑐 ∪ {〈𝑆, (𝑒‘𝑆)〉}) = ((𝑒 ↾ (0..^𝑆)) ∪ {〈𝑆, (𝑒‘𝑆)〉})) |
96 | 95 | eqeq2d 2749 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ∧ 𝑐 = (𝑒 ↾ (0..^𝑆))) → (𝑒 = (𝑐 ∪ {〈𝑆, (𝑒‘𝑆)〉}) ↔ 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {〈𝑆, (𝑒‘𝑆)〉}))) |
97 | 10 | ffnd 6601 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 Fn (0..^(𝑆 + 1))) |
98 | | fnsnsplit 7056 |
. . . . . . . . . . 11
⊢ ((𝑒 Fn (0..^(𝑆 + 1)) ∧ 𝑆 ∈ (0..^(𝑆 + 1))) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {〈𝑆, (𝑒‘𝑆)〉})) |
99 | 97, 13, 98 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {〈𝑆, (𝑒‘𝑆)〉})) |
100 | 11, 65 | eleqtrdi 2849 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑆 ∈
(ℤ≥‘0)) |
101 | | fzodif2 31113 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈
(ℤ≥‘0) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆)) |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((0..^(𝑆 + 1)) ∖ {𝑆}) = (0..^𝑆)) |
103 | 102 | reseq2d 5891 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → (𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) = (𝑒 ↾ (0..^𝑆))) |
104 | 103 | uneq1d 4096 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ((𝑒 ↾ ((0..^(𝑆 + 1)) ∖ {𝑆})) ∪ {〈𝑆, (𝑒‘𝑆)〉}) = ((𝑒 ↾ (0..^𝑆)) ∪ {〈𝑆, (𝑒‘𝑆)〉})) |
105 | 99, 104 | eqtrd 2778 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → 𝑒 = ((𝑒 ↾ (0..^𝑆)) ∪ {〈𝑆, (𝑒‘𝑆)〉})) |
106 | 93, 96, 105 | rspcedvd 3563 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − (𝑒‘𝑆)))𝑒 = (𝑐 ∪ {〈𝑆, (𝑒‘𝑆)〉})) |
107 | 14, 23, 106 | rspcedvd 3563 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) → ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) |
108 | 107 | anasss 467 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)) → ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) |
109 | | simpr 485 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) |
110 | 1 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝐴 ⊆ ℕ) |
111 | 110 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝐴 ⊆ ℕ) |
112 | 2 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑀 ∈ ℤ) |
113 | 88 | sselda 3921 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ ℤ) |
114 | 112, 113 | zsubcld 12431 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (𝑀 − 𝑏) ∈ ℤ) |
115 | 114 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑀 − 𝑏) ∈ ℤ) |
116 | 3 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑆 ∈
ℕ0) |
117 | 116 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑆 ∈
ℕ0) |
118 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) |
119 | 111, 115,
117, 118 | reprf 32592 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑐:(0..^𝑆)⟶𝐴) |
120 | | simplr 766 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑏 ∈ 𝐴) |
121 | 117, 120 | fsnd 6759 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → {〈𝑆, 𝑏〉}:{𝑆}⟶𝐴) |
122 | | fzodisjsn 13425 |
. . . . . . . . . . . . . 14
⊢
((0..^𝑆) ∩
{𝑆}) =
∅ |
123 | 122 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → ((0..^𝑆) ∩ {𝑆}) = ∅) |
124 | 119, 121,
123 | fun2d 6638 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑐 ∪ {〈𝑆, 𝑏〉}):((0..^𝑆) ∪ {𝑆})⟶𝐴) |
125 | 117, 66 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆})) |
126 | 125 | feq2d 6586 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑐 ∪ {〈𝑆, 𝑏〉}):(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {〈𝑆, 𝑏〉}):((0..^𝑆) ∪ {𝑆})⟶𝐴)) |
127 | 124, 126 | mpbird 256 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑐 ∪ {〈𝑆, 𝑏〉}):(0..^(𝑆 + 1))⟶𝐴) |
128 | | ovex 7308 |
. . . . . . . . . . . . 13
⊢
(0..^(𝑆 + 1)) ∈
V |
129 | | elmapg 8628 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ V ∧ (0..^(𝑆 + 1)) ∈ V) → ((𝑐 ∪ {〈𝑆, 𝑏〉}) ∈ (𝐴 ↑m (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {〈𝑆, 𝑏〉}):(0..^(𝑆 + 1))⟶𝐴)) |
130 | 32, 128, 129 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑐 ∪ {〈𝑆, 𝑏〉}) ∈ (𝐴 ↑m (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {〈𝑆, 𝑏〉}):(0..^(𝑆 + 1))⟶𝐴)) |
131 | 130 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑐 ∪ {〈𝑆, 𝑏〉}) ∈ (𝐴 ↑m (0..^(𝑆 + 1))) ↔ (𝑐 ∪ {〈𝑆, 𝑏〉}):(0..^(𝑆 + 1))⟶𝐴)) |
132 | 127, 131 | mpbird 256 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → (𝑐 ∪ {〈𝑆, 𝑏〉}) ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) |
133 | 132 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → (𝑐 ∪ {〈𝑆, 𝑏〉}) ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) |
134 | 109, 133 | eqeltrd 2839 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → 𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1)))) |
135 | 125 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆})) |
136 | 135 | sumeq1d 15413 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎)) |
137 | | nfv 1917 |
. . . . . . . . . 10
⊢
Ⅎ𝑎(((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) |
138 | 33 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → (0..^𝑆) ∈ Fin) |
139 | 117 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → 𝑆 ∈
ℕ0) |
140 | 56 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → ¬ 𝑆 ∈ (0..^𝑆)) |
141 | 42 | ad4antr 729 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℂ) |
142 | 127 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → (𝑐 ∪ {〈𝑆, 𝑏〉}):(0..^(𝑆 + 1))⟶𝐴) |
143 | 109 | feq1d 6585 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → (𝑒:(0..^(𝑆 + 1))⟶𝐴 ↔ (𝑐 ∪ {〈𝑆, 𝑏〉}):(0..^(𝑆 + 1))⟶𝐴)) |
144 | 142, 143 | mpbird 256 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → 𝑒:(0..^(𝑆 + 1))⟶𝐴) |
145 | 144 | adantr 481 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒:(0..^(𝑆 + 1))⟶𝐴) |
146 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆)) |
147 | | elun1 4110 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (0..^𝑆) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆})) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ ((0..^𝑆) ∪ {𝑆})) |
149 | 125 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) ∧ 𝑎 ∈ (0..^𝑆)) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆})) |
150 | 148, 149 | eleqtrrd 2842 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1))) |
151 | 145, 150 | ffvelrnd 6962 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ 𝐴) |
152 | 141, 151 | sseldd 3922 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ ℂ) |
153 | 42 | ad3antrrr 727 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → 𝐴 ⊆ ℂ) |
154 | 139, 12 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → 𝑆 ∈ (0..^(𝑆 + 1))) |
155 | 144, 154 | ffvelrnd 6962 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → (𝑒‘𝑆) ∈ 𝐴) |
156 | 153, 155 | sseldd 3922 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → (𝑒‘𝑆) ∈ ℂ) |
157 | 137, 55, 138, 139, 140, 152, 62, 156 | fsumsplitsn 15456 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → Σ𝑎 ∈ ((0..^𝑆) ∪ {𝑆})(𝑒‘𝑎) = (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆))) |
158 | | simplr 766 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) |
159 | 158 | fveq1d 6776 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) = ((𝑐 ∪ {〈𝑆, 𝑏〉})‘𝑎)) |
160 | 119 | ffnd 6601 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → 𝑐 Fn (0..^𝑆)) |
161 | 160 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑐 Fn (0..^𝑆)) |
162 | 121 | ffnd 6601 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) → {〈𝑆, 𝑏〉} Fn {𝑆}) |
163 | 162 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) ∧ 𝑎 ∈ (0..^𝑆)) → {〈𝑆, 𝑏〉} Fn {𝑆}) |
164 | 122 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) ∧ 𝑎 ∈ (0..^𝑆)) → ((0..^𝑆) ∩ {𝑆}) = ∅) |
165 | | fvun1 6859 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 Fn (0..^𝑆) ∧ {〈𝑆, 𝑏〉} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑎 ∈ (0..^𝑆))) → ((𝑐 ∪ {〈𝑆, 𝑏〉})‘𝑎) = (𝑐‘𝑎)) |
166 | 161, 163,
164, 146, 165 | syl112anc 1373 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐 ∪ {〈𝑆, 𝑏〉})‘𝑎) = (𝑐‘𝑎)) |
167 | 159, 166 | eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) = (𝑐‘𝑎)) |
168 | 167 | ralrimiva 3103 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → ∀𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) = (𝑐‘𝑎)) |
169 | 168 | sumeq2d 15414 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) |
170 | 111 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → 𝐴 ⊆ ℕ) |
171 | 115 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → (𝑀 − 𝑏) ∈ ℤ) |
172 | 118 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) |
173 | 170, 171,
139, 172 | reprsum 32593 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = (𝑀 − 𝑏)) |
174 | 169, 173 | eqtrd 2778 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) = (𝑀 − 𝑏)) |
175 | 109 | fveq1d 6776 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → (𝑒‘𝑆) = ((𝑐 ∪ {〈𝑆, 𝑏〉})‘𝑆)) |
176 | 160 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → 𝑐 Fn (0..^𝑆)) |
177 | 162 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → {〈𝑆, 𝑏〉} Fn {𝑆}) |
178 | 122 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → ((0..^𝑆) ∩ {𝑆}) = ∅) |
179 | | snidg 4595 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ ℕ0
→ 𝑆 ∈ {𝑆}) |
180 | 139, 179 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → 𝑆 ∈ {𝑆}) |
181 | | fvun2 6860 |
. . . . . . . . . . . . 13
⊢ ((𝑐 Fn (0..^𝑆) ∧ {〈𝑆, 𝑏〉} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑆 ∈ {𝑆})) → ((𝑐 ∪ {〈𝑆, 𝑏〉})‘𝑆) = ({〈𝑆, 𝑏〉}‘𝑆)) |
182 | 176, 177,
178, 180, 181 | syl112anc 1373 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → ((𝑐 ∪ {〈𝑆, 𝑏〉})‘𝑆) = ({〈𝑆, 𝑏〉}‘𝑆)) |
183 | 120 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → 𝑏 ∈ 𝐴) |
184 | | fvsng 7052 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ ℕ0
∧ 𝑏 ∈ 𝐴) → ({〈𝑆, 𝑏〉}‘𝑆) = 𝑏) |
185 | 139, 183,
184 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → ({〈𝑆, 𝑏〉}‘𝑆) = 𝑏) |
186 | 175, 182,
185 | 3eqtrd 2782 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → (𝑒‘𝑆) = 𝑏) |
187 | 174, 186 | oveq12d 7293 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)) = ((𝑀 − 𝑏) + 𝑏)) |
188 | | zsscn 12327 |
. . . . . . . . . . . 12
⊢ ℤ
⊆ ℂ |
189 | 112 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → 𝑀 ∈ ℤ) |
190 | 188, 189 | sselid 3919 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → 𝑀 ∈ ℂ) |
191 | 186, 156 | eqeltrrd 2840 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → 𝑏 ∈ ℂ) |
192 | 190, 191 | npcand 11336 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → ((𝑀 − 𝑏) + 𝑏) = 𝑀) |
193 | 187, 192 | eqtrd 2778 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → (Σ𝑎 ∈ (0..^𝑆)(𝑒‘𝑎) + (𝑒‘𝑆)) = 𝑀) |
194 | 136, 157,
193 | 3eqtrd 2782 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) |
195 | 134, 194 | jca 512 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → (𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)) |
196 | 195 | r19.29ffa 30822 |
. . . . . 6
⊢ ((𝜑 ∧ ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) → (𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)) |
197 | 108, 196 | impbida 798 |
. . . . 5
⊢ (𝜑 → ((𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ↔ ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉}))) |
198 | | reprsuc.f |
. . . . . . 7
⊢ 𝐹 = (𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑐 ∪ {〈𝑆, 𝑏〉})) |
199 | | vex 3436 |
. . . . . . . 8
⊢ 𝑐 ∈ V |
200 | | snex 5354 |
. . . . . . . 8
⊢
{〈𝑆, 𝑏〉} ∈
V |
201 | 199, 200 | unex 7596 |
. . . . . . 7
⊢ (𝑐 ∪ {〈𝑆, 𝑏〉}) ∈ V |
202 | 198, 201 | elrnmpti 5869 |
. . . . . 6
⊢ (𝑒 ∈ ran 𝐹 ↔ ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) |
203 | 202 | rexbii 3181 |
. . . . 5
⊢
(∃𝑏 ∈
𝐴 𝑒 ∈ ran 𝐹 ↔ ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ (𝐴(repr‘𝑆)(𝑀 − 𝑏))𝑒 = (𝑐 ∪ {〈𝑆, 𝑏〉})) |
204 | 197, 203 | bitr4di 289 |
. . . 4
⊢ (𝜑 → ((𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀) ↔ ∃𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹)) |
205 | | fveq1 6773 |
. . . . . . . 8
⊢ (𝑐 = 𝑒 → (𝑐‘𝑎) = (𝑒‘𝑎)) |
206 | 205 | sumeq2sdv 15416 |
. . . . . . 7
⊢ (𝑐 = 𝑒 → Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎)) |
207 | 206 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑐 = 𝑒 → (Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)) |
208 | 207 | cbvrabv 3426 |
. . . . 5
⊢ {𝑐 ∈ (𝐴 ↑m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} = {𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀} |
209 | 208 | rabeq2i 3422 |
. . . 4
⊢ (𝑒 ∈ {𝑐 ∈ (𝐴 ↑m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} ↔ (𝑒 ∈ (𝐴 ↑m (0..^(𝑆 + 1))) ∧ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑒‘𝑎) = 𝑀)) |
210 | | eliun 4928 |
. . . 4
⊢ (𝑒 ∈ ∪ 𝑏 ∈ 𝐴 ran 𝐹 ↔ ∃𝑏 ∈ 𝐴 𝑒 ∈ ran 𝐹) |
211 | 204, 209,
210 | 3bitr4g 314 |
. . 3
⊢ (𝜑 → (𝑒 ∈ {𝑐 ∈ (𝐴 ↑m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} ↔ 𝑒 ∈ ∪
𝑏 ∈ 𝐴 ran 𝐹)) |
212 | 211 | eqrdv 2736 |
. 2
⊢ (𝜑 → {𝑐 ∈ (𝐴 ↑m (0..^(𝑆 + 1))) ∣ Σ𝑎 ∈ (0..^(𝑆 + 1))(𝑐‘𝑎) = 𝑀} = ∪
𝑏 ∈ 𝐴 ran 𝐹) |
213 | 7, 212 | eqtrd 2778 |
1
⊢ (𝜑 → (𝐴(repr‘(𝑆 + 1))𝑀) = ∪
𝑏 ∈ 𝐴 ran 𝐹) |