Step | Hyp | Ref
| Expression |
1 | | aacllem.0 |
. 2
⊢ (𝜑 → 𝐴 ∈ ℂ) |
2 | | aacllem.1 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
3 | 2 | nn0red 11229 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℝ) |
4 | 3 | ltp1d 10833 |
. . . . 5
⊢ (𝜑 → 𝑁 < (𝑁 + 1)) |
5 | | peano2nn0 11210 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
6 | 2, 5 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
7 | 6 | nn0red 11229 |
. . . . . 6
⊢ (𝜑 → (𝑁 + 1) ∈ ℝ) |
8 | 3, 7 | ltnled 10063 |
. . . . 5
⊢ (𝜑 → (𝑁 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑁)) |
9 | 4, 8 | mpbid 221 |
. . . 4
⊢ (𝜑 → ¬ (𝑁 + 1) ≤ 𝑁) |
10 | | aacllem.3 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ) |
11 | 10 | 3expa 1257 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ) |
12 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (1...𝑁) ↦ 𝐶) = (𝑛 ∈ (1...𝑁) ↦ 𝐶) |
13 | 11, 12 | fmptd 6292 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ) |
14 | | qex 11676 |
. . . . . . . . . . 11
⊢ ℚ
∈ V |
15 | | ovex 6577 |
. . . . . . . . . . 11
⊢
(1...𝑁) ∈
V |
16 | 14, 15 | elmap 7772 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑𝑚
(1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ) |
17 | 13, 16 | sylibr 223 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑𝑚
(1...𝑁))) |
18 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) |
19 | 17, 18 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑𝑚
(1...𝑁))) |
20 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(ℂfld ↾s ℚ) =
(ℂfld ↾s ℚ) |
21 | 20 | qdrng 25109 |
. . . . . . . . . . 11
⊢
(ℂfld ↾s ℚ) ∈
DivRing |
22 | | drngring 18577 |
. . . . . . . . . . 11
⊢
((ℂfld ↾s ℚ) ∈ DivRing
→ (ℂfld ↾s ℚ) ∈
Ring) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . 10
⊢
(ℂfld ↾s ℚ) ∈
Ring |
24 | | fzfi 12633 |
. . . . . . . . . 10
⊢
(1...𝑁) ∈
Fin |
25 | | eqid 2610 |
. . . . . . . . . . 11
⊢
((ℂfld ↾s ℚ) freeLMod (1...𝑁)) = ((ℂfld
↾s ℚ) freeLMod (1...𝑁)) |
26 | 25 | frlmlmod 19912 |
. . . . . . . . . 10
⊢
(((ℂfld ↾s ℚ) ∈ Ring ∧
(1...𝑁) ∈ Fin) →
((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod) |
27 | 23, 24, 26 | mp2an 704 |
. . . . . . . . 9
⊢
((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod |
28 | | fzfi 12633 |
. . . . . . . . 9
⊢
(0...𝑁) ∈
Fin |
29 | 20 | qrngbas 25108 |
. . . . . . . . . . . 12
⊢ ℚ =
(Base‘(ℂfld ↾s
ℚ)) |
30 | 25, 29 | frlmfibas 19924 |
. . . . . . . . . . 11
⊢
(((ℂfld ↾s ℚ) ∈ DivRing
∧ (1...𝑁) ∈ Fin)
→ (ℚ ↑𝑚 (1...𝑁)) = (Base‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))) |
31 | 21, 24, 30 | mp2an 704 |
. . . . . . . . . 10
⊢ (ℚ
↑𝑚 (1...𝑁)) = (Base‘((ℂfld
↾s ℚ) freeLMod (1...𝑁))) |
32 | 25 | frlmsca 19916 |
. . . . . . . . . . 11
⊢
(((ℂfld ↾s ℚ) ∈ DivRing
∧ (1...𝑁) ∈ Fin)
→ (ℂfld ↾s ℚ) =
(Scalar‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) |
33 | 21, 24, 32 | mp2an 704 |
. . . . . . . . . 10
⊢
(ℂfld ↾s ℚ) =
(Scalar‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) |
34 | | eqid 2610 |
. . . . . . . . . 10
⊢ (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁))) = ( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) |
35 | 20 | qrng0 25110 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘(ℂfld ↾s
ℚ)) |
36 | 25, 35 | frlm0 19917 |
. . . . . . . . . . 11
⊢
(((ℂfld ↾s ℚ) ∈ Ring ∧
(1...𝑁) ∈ Fin) →
((1...𝑁) × {0}) =
(0g‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))) |
37 | 23, 24, 36 | mp2an 704 |
. . . . . . . . . 10
⊢
((1...𝑁) ×
{0}) = (0g‘((ℂfld ↾s
ℚ) freeLMod (1...𝑁))) |
38 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
((ℂfld ↾s ℚ) freeLMod (0...𝑁)) = ((ℂfld
↾s ℚ) freeLMod (0...𝑁)) |
39 | 38, 29 | frlmfibas 19924 |
. . . . . . . . . . 11
⊢
(((ℂfld ↾s ℚ) ∈ DivRing
∧ (0...𝑁) ∈ Fin)
→ (ℚ ↑𝑚 (0...𝑁)) = (Base‘((ℂfld
↾s ℚ) freeLMod (0...𝑁)))) |
40 | 21, 28, 39 | mp2an 704 |
. . . . . . . . . 10
⊢ (ℚ
↑𝑚 (0...𝑁)) = (Base‘((ℂfld
↾s ℚ) freeLMod (0...𝑁))) |
41 | 31, 33, 34, 37, 35, 40 | islindf4 19996 |
. . . . . . . . 9
⊢
((((ℂfld ↾s ℚ) freeLMod
(1...𝑁)) ∈ LMod ∧
(0...𝑁) ∈ Fin ∧
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑𝑚
(1...𝑁))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld
↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑𝑚
(0...𝑁))((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})))) |
42 | 27, 28, 41 | mp3an12 1406 |
. . . . . . . 8
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑𝑚
(1...𝑁)) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld
↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑𝑚
(0...𝑁))((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})))) |
43 | 19, 42 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld
↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑𝑚
(0...𝑁))((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})))) |
44 | | elmapi 7765 |
. . . . . . . . 9
⊢ (𝑤 ∈ (ℚ
↑𝑚 (0...𝑁)) → 𝑤:(0...𝑁)⟶ℚ) |
45 | | fzfid 12634 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (0...𝑁) ∈ Fin) |
46 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤‘𝑘) ∈ V |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ V) |
48 | 15 | mptex 6390 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V) |
50 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑤:(0...𝑁)⟶ℚ) |
51 | 50 | feqmptd 6159 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑤 = (𝑘 ∈ (0...𝑁) ↦ (𝑤‘𝑘))) |
52 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) |
53 | 45, 47, 49, 51, 52 | offval2 6812 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘)( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)))) |
54 | | fzfid 12634 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin) |
55 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ) |
56 | 55 | adantll 746 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ) |
57 | 17 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑𝑚
(1...𝑁))) |
58 | | cnfldmul 19573 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ·
= (.r‘ℂfld) |
59 | 20, 58 | ressmulr 15829 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℚ
∈ V → · = (.r‘(ℂfld
↾s ℚ))) |
60 | 14, 59 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ·
= (.r‘(ℂfld ↾s
ℚ)) |
61 | 25, 31, 29, 54, 56, 57, 34, 60 | frlmvscafval 19928 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘)( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (((1...𝑁) × {(𝑤‘𝑘)}) ∘𝑓 ·
(𝑛 ∈ (1...𝑁) ↦ 𝐶))) |
62 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤‘𝑘) ∈ V) |
63 | 11 | adantllr 751 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ) |
64 | | fconstmpt 5085 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((1...𝑁) ×
{(𝑤‘𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤‘𝑘)) |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((1...𝑁) × {(𝑤‘𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤‘𝑘))) |
66 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) = (𝑛 ∈ (1...𝑁) ↦ 𝐶)) |
67 | 54, 62, 63, 65, 66 | offval2 6812 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (((1...𝑁) × {(𝑤‘𝑘)}) ∘𝑓 ·
(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) |
68 | 61, 67 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘)( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) |
69 | 68 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘)( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) |
70 | 53, 69 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) |
71 | 70 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤
∘𝑓 ( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))) |
72 | | fzfid 12634 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (1...𝑁) ∈ Fin) |
73 | 23 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
(ℂfld ↾s ℚ) ∈
Ring) |
74 | 56 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ) |
75 | 11 | an32s 842 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℚ) |
76 | 75 | adantllr 751 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℚ) |
77 | | qmulcl 11682 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤‘𝑘) ∈ ℚ ∧ 𝐶 ∈ ℚ) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ) |
78 | 74, 76, 77 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ) |
79 | 78 | an32s 842 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ) |
80 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) |
81 | 79, 80 | fmptd 6292 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ) |
82 | 14, 15 | elmap 7772 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ (ℚ
↑𝑚 (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ) |
83 | 81, 82 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ (ℚ
↑𝑚 (1...𝑁))) |
84 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) |
85 | 15 | mptex 6390 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ V |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ V) |
87 | | snex 4835 |
. . . . . . . . . . . . . . . . . . 19
⊢ {0}
∈ V |
88 | 15, 87 | xpex 6860 |
. . . . . . . . . . . . . . . . . 18
⊢
((1...𝑁) ×
{0}) ∈ V |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((1...𝑁) × {0}) ∈
V) |
90 | 84, 45, 86, 89 | fsuppmptdm 8169 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) finSupp ((1...𝑁) × {0})) |
91 | 25, 31, 37, 72, 45, 73, 83, 90 | frlmgsum 19930 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ ((ℂfld
↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))) |
92 | | cnfldbas 19571 |
. . . . . . . . . . . . . . . . . 18
⊢ ℂ =
(Base‘ℂfld) |
93 | | cnfldadd 19572 |
. . . . . . . . . . . . . . . . . 18
⊢ + =
(+g‘ℂfld) |
94 | | cnfldex 19570 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℂfld ∈ V |
95 | 94 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℂfld ∈
V) |
96 | | fzfid 12634 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (0...𝑁) ∈ Fin) |
97 | | qsscn 11675 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℚ
⊆ ℂ |
98 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℚ ⊆
ℂ) |
99 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) |
100 | 78, 99 | fmptd 6292 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(0...𝑁)⟶ℚ) |
101 | | 0z 11265 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ∈
ℤ |
102 | | zq 11670 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
ℤ → 0 ∈ ℚ) |
103 | 101, 102 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℚ |
104 | 103 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 0 ∈ ℚ) |
105 | | addid2 10098 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℂ → (0 +
𝑥) = 𝑥) |
106 | | addid1 10095 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℂ → (𝑥 + 0) = 𝑥) |
107 | 105, 106 | jca 553 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ → ((0 +
𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥)) |
108 | 107 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ ℂ) → ((0 + 𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥)) |
109 | 92, 93, 20, 95, 96, 98, 100, 104, 108 | gsumress 17099 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂfld
Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = ((ℂfld
↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) |
110 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑤:(0...𝑁)⟶ℚ) |
111 | | qcn 11678 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤‘𝑘) ∈ ℚ → (𝑤‘𝑘) ∈ ℂ) |
112 | 55, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ) |
113 | 110, 112 | sylan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ) |
114 | | qcn 11678 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐶 ∈ ℚ → 𝐶 ∈
ℂ) |
115 | 11, 114 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℂ) |
116 | 115 | an32s 842 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℂ) |
117 | 116 | adantllr 751 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℂ) |
118 | 113, 117 | mulcld 9939 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℂ) |
119 | 96, 118 | gsumfsum 19632 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂfld
Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) |
120 | 109, 119 | eqtr3d 2646 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((ℂfld
↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) |
121 | 120 | mpteq2dva 4672 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ ((ℂfld
↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))) |
122 | 71, 91, 121 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤
∘𝑓 ( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))) |
123 | | qaddcl 11680 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ) → (𝑥 + 𝑦) ∈ ℚ) |
124 | 123 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) ∈ ℚ) |
125 | 98, 124, 96, 78, 104 | fsumcllem 14310 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ ℚ) |
126 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) |
127 | 125, 126 | fmptd 6292 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ) |
128 | 14, 15 | elmap 7772 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) ∈ (ℚ
↑𝑚 (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ) |
129 | 127, 128 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) ∈ (ℚ
↑𝑚 (1...𝑁))) |
130 | 122, 129 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤
∘𝑓 ( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) ∈ (ℚ
↑𝑚 (1...𝑁))) |
131 | | elmapi 7765 |
. . . . . . . . . . . . 13
⊢
((((ℂfld ↾s ℚ) freeLMod
(1...𝑁))
Σg (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) ∈ (ℚ
↑𝑚 (1...𝑁)) → (((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))):(1...𝑁)⟶ℚ) |
132 | | ffn 5958 |
. . . . . . . . . . . . 13
⊢
((((ℂfld ↾s ℚ) freeLMod
(1...𝑁))
Σg (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))):(1...𝑁)⟶ℚ →
(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤
∘𝑓 ( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁)) |
133 | 130, 131,
132 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤
∘𝑓 ( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁)) |
134 | | c0ex 9913 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
135 | | fnconstg 6006 |
. . . . . . . . . . . . 13
⊢ (0 ∈
V → ((1...𝑁) ×
{0}) Fn (1...𝑁)) |
136 | 134, 135 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
((1...𝑁) ×
{0}) Fn (1...𝑁) |
137 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛((ℂfld ↾s
ℚ) freeLMod (1...𝑁)) |
138 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛
Σg |
139 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛𝑤 |
140 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛
∘𝑓 ( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) |
141 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛(0...𝑁) |
142 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛(𝑛 ∈ (1...𝑁) ↦ 𝐶) |
143 | 141, 142 | nfmpt 4674 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) |
144 | 139, 140,
143 | nfov 6575 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) |
145 | 137, 138,
144 | nfov 6575 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛(((ℂfld ↾s
ℚ) freeLMod (1...𝑁))
Σg (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) |
146 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛((1...𝑁) × {0}) |
147 | 145, 146 | eqfnfv2f 6223 |
. . . . . . . . . . . 12
⊢
(((((ℂfld ↾s ℚ) freeLMod
(1...𝑁))
Σg (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁) ∧ ((1...𝑁) × {0}) Fn (1...𝑁)) → ((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛))) |
148 | 133, 136,
147 | sylancl 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤
∘𝑓 ( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛))) |
149 | 122 | fveq1d 6105 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤
∘𝑓 ( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛)) |
150 | | sumex 14266 |
. . . . . . . . . . . . . . 15
⊢
Σ𝑘 ∈
(0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ V |
151 | 126 | fvmpt2 6200 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ (1...𝑁) ∧ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ V) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) |
152 | 150, 151 | mpan2 703 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) |
153 | 149, 152 | sylan9eq 2664 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) |
154 | 134 | fvconst2 6374 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0) |
155 | 154 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0) |
156 | 153, 155 | eqeq12d 2625 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
157 | 156 | ralbidva 2968 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (∀𝑛 ∈ (1...𝑁)((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
158 | 148, 157 | bitrd 267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤
∘𝑓 ( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
159 | 158 | imbi1d 330 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
(((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤
∘𝑓 ( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ (∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})))) |
160 | 44, 159 | sylan2 490 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (ℚ ↑𝑚
(0...𝑁))) →
(((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤
∘𝑓 ( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ (∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})))) |
161 | 160 | ralbidva 2968 |
. . . . . . 7
⊢ (𝜑 → (∀𝑤 ∈ (ℚ
↑𝑚 (0...𝑁))((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘𝑓 (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ ∀𝑤 ∈ (ℚ
↑𝑚 (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})))) |
162 | 43, 161 | bitrd 267 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld
↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑𝑚
(0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})))) |
163 | | drngnzr 19083 |
. . . . . . . . 9
⊢
((ℂfld ↾s ℚ) ∈ DivRing
→ (ℂfld ↾s ℚ) ∈
NzRing) |
164 | 21, 163 | ax-mp 5 |
. . . . . . . 8
⊢
(ℂfld ↾s ℚ) ∈
NzRing |
165 | 33 | islindf3 19984 |
. . . . . . . 8
⊢
((((ℂfld ↾s ℚ) freeLMod
(1...𝑁)) ∈ LMod ∧
(ℂfld ↾s ℚ) ∈ NzRing) →
((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld
↾s ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))))) |
166 | 27, 164, 165 | mp2an 704 |
. . . . . . 7
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld
↾s ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))))) |
167 | 48, 18 | dmmpti 5936 |
. . . . . . . . 9
⊢ dom
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (0...𝑁) |
168 | | f1eq2 6010 |
. . . . . . . . 9
⊢ (dom
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (0...𝑁) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ↔ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V)) |
169 | 167, 168 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ↔ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V) |
170 | 169 | anbi1i 727 |
. . . . . . 7
⊢ (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))))) |
171 | 166, 170 | bitri 263 |
. . . . . 6
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld
↾s ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))))) |
172 | | con34b 305 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ (¬ 𝑤 = ((0...𝑁) × {0}) → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
173 | | df-nel 2783 |
. . . . . . . . . . 11
⊢ (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬
𝑤 ∈ {((0...𝑁) ×
{0})}) |
174 | | velsn 4141 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {((0...𝑁) × {0})} ↔ 𝑤 = ((0...𝑁) × {0})) |
175 | 173, 174 | xchbinx 323 |
. . . . . . . . . 10
⊢ (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬
𝑤 = ((0...𝑁) × {0})) |
176 | 175 | imbi1i 338 |
. . . . . . . . 9
⊢ ((𝑤 ∉ {((0...𝑁) × {0})} → ¬
∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ↔ (¬ 𝑤 = ((0...𝑁) × {0}) → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
177 | 172, 176 | bitr4i 266 |
. . . . . . . 8
⊢
((∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ (𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
178 | 177 | ralbii 2963 |
. . . . . . 7
⊢
(∀𝑤 ∈
(ℚ ↑𝑚 (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ∀𝑤 ∈ (ℚ
↑𝑚 (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
179 | | raldifb 3712 |
. . . . . . 7
⊢
(∀𝑤 ∈
(ℚ ↑𝑚 (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ↔ ∀𝑤 ∈ ((ℚ ↑𝑚
(0...𝑁)) ∖
{((0...𝑁) × {0})})
¬ ∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) |
180 | | ralnex 2975 |
. . . . . . 7
⊢
(∀𝑤 ∈
((ℚ ↑𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})}) ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ↔ ¬ ∃𝑤 ∈ ((ℚ ↑𝑚
(0...𝑁)) ∖
{((0...𝑁) ×
{0})})∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) |
181 | 178, 179,
180 | 3bitri 285 |
. . . . . 6
⊢
(∀𝑤 ∈
(ℚ ↑𝑚 (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ¬ ∃𝑤 ∈ ((ℚ
↑𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) |
182 | 162, 171,
181 | 3bitr3g 301 |
. . . . 5
⊢ (𝜑 → (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) ↔ ¬
∃𝑤 ∈ ((ℚ
↑𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
183 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))) =
(LSubSp‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) |
184 | 31, 183 | lssmre 18787 |
. . . . . . . . . . . 12
⊢
(((ℂfld ↾s ℚ) freeLMod
(1...𝑁)) ∈ LMod →
(LSubSp‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) ∈
(Moore‘(ℚ ↑𝑚 (1...𝑁)))) |
185 | 27, 184 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))) ∈
(Moore‘(ℚ ↑𝑚 (1...𝑁))) |
186 | 185 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) →
(LSubSp‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) ∈
(Moore‘(ℚ ↑𝑚 (1...𝑁)))) |
187 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(LSpan‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))) =
(LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) |
188 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(mrCls‘(LSubSp‘((ℂfld ↾s
ℚ) freeLMod (1...𝑁)))) =
(mrCls‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))) |
189 | 183, 187,
188 | mrclsp 18810 |
. . . . . . . . . . 11
⊢
(((ℂfld ↾s ℚ) freeLMod
(1...𝑁)) ∈ LMod →
(LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) =
(mrCls‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))))) |
190 | 27, 189 | ax-mp 5 |
. . . . . . . . . 10
⊢
(LSpan‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))) =
(mrCls‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))) |
191 | | eqid 2610 |
. . . . . . . . . 10
⊢
(mrInd‘(LSubSp‘((ℂfld ↾s
ℚ) freeLMod (1...𝑁)))) =
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))) |
192 | 33 | islvec 18925 |
. . . . . . . . . . . . 13
⊢
(((ℂfld ↾s ℚ) freeLMod
(1...𝑁)) ∈ LVec ↔
(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧
(ℂfld ↾s ℚ) ∈
DivRing)) |
193 | 27, 21, 192 | mpbir2an 957 |
. . . . . . . . . . . 12
⊢
((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LVec |
194 | 183, 190,
31 | lssacsex 18965 |
. . . . . . . . . . . . 13
⊢
(((ℂfld ↾s ℚ) freeLMod
(1...𝑁)) ∈ LVec →
((LSubSp‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) ∈
(ACS‘(ℚ ↑𝑚 (1...𝑁))) ∧ ∀𝑧 ∈ 𝒫 (ℚ
↑𝑚 (1...𝑁))∀𝑥 ∈ (ℚ ↑𝑚
(1...𝑁))∀𝑦 ∈
(((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖
((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦})))) |
195 | 194 | simprd 478 |
. . . . . . . . . . . 12
⊢
(((ℂfld ↾s ℚ) freeLMod
(1...𝑁)) ∈ LVec →
∀𝑧 ∈ 𝒫
(ℚ ↑𝑚 (1...𝑁))∀𝑥 ∈ (ℚ ↑𝑚
(1...𝑁))∀𝑦 ∈
(((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖
((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦}))) |
196 | 193, 195 | ax-mp 5 |
. . . . . . . . . . 11
⊢
∀𝑧 ∈
𝒫 (ℚ ↑𝑚 (1...𝑁))∀𝑥 ∈ (ℚ ↑𝑚
(1...𝑁))∀𝑦 ∈
(((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖
((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦})) |
197 | 196 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) →
∀𝑧 ∈ 𝒫
(ℚ ↑𝑚 (1...𝑁))∀𝑥 ∈ (ℚ ↑𝑚
(1...𝑁))∀𝑦 ∈
(((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖
((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦}))) |
198 | | frn 5966 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑𝑚
(1...𝑁)) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ
↑𝑚 (1...𝑁))) |
199 | 19, 198 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ
↑𝑚 (1...𝑁))) |
200 | | dif0 3904 |
. . . . . . . . . . . 12
⊢ ((ℚ
↑𝑚 (1...𝑁)) ∖ ∅) = (ℚ
↑𝑚 (1...𝑁)) |
201 | 199, 200 | syl6sseqr 3615 |
. . . . . . . . . . 11
⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((ℚ
↑𝑚 (1...𝑁)) ∖ ∅)) |
202 | 201 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) → ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((ℚ
↑𝑚 (1...𝑁)) ∖ ∅)) |
203 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
((ℂfld ↾s ℚ) unitVec (1...𝑁)) = ((ℂfld
↾s ℚ) unitVec (1...𝑁)) |
204 | 203, 25, 31 | uvcff 19949 |
. . . . . . . . . . . . . 14
⊢
(((ℂfld ↾s ℚ) ∈ Ring ∧
(1...𝑁) ∈ Fin) →
((ℂfld ↾s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑𝑚
(1...𝑁))) |
205 | 23, 24, 204 | mp2an 704 |
. . . . . . . . . . . . 13
⊢
((ℂfld ↾s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑𝑚
(1...𝑁)) |
206 | | frn 5966 |
. . . . . . . . . . . . 13
⊢
(((ℂfld ↾s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑𝑚
(1...𝑁)) → ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ⊆ (ℚ
↑𝑚 (1...𝑁))) |
207 | 205, 206 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ⊆ (ℚ
↑𝑚 (1...𝑁)) |
208 | 207, 200 | sseqtr4i 3601 |
. . . . . . . . . . 11
⊢ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ⊆ ((ℚ
↑𝑚 (1...𝑁)) ∖ ∅) |
209 | 208 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) → ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ⊆ ((ℚ
↑𝑚 (1...𝑁)) ∖ ∅)) |
210 | | un0 3919 |
. . . . . . . . . . . . . 14
⊢ (ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅) = ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) |
211 | 210 | fveq2i 6106 |
. . . . . . . . . . . . 13
⊢
((LSpan‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))‘(ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) ∪ ∅)) =
((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘ran
((ℂfld ↾s ℚ) unitVec (1...𝑁))) |
212 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(LBasis‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))) =
(LBasis‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) |
213 | 25, 203, 212 | frlmlbs 19955 |
. . . . . . . . . . . . . . 15
⊢
(((ℂfld ↾s ℚ) ∈ Ring ∧
(1...𝑁) ∈ Fin) →
ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈
(LBasis‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) |
214 | 23, 24, 213 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈
(LBasis‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) |
215 | 31, 212, 187 | lbssp 18900 |
. . . . . . . . . . . . . 14
⊢ (ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈
(LBasis‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) →
((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘ran
((ℂfld ↾s ℚ) unitVec (1...𝑁))) = (ℚ
↑𝑚 (1...𝑁))) |
216 | 214, 215 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
((LSpan‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))‘ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) = (ℚ ↑𝑚
(1...𝑁)) |
217 | 211, 216 | eqtri 2632 |
. . . . . . . . . . . 12
⊢
((LSpan‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))‘(ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) ∪ ∅)) = (ℚ
↑𝑚 (1...𝑁)) |
218 | 199, 217 | syl6sseqr 3615 |
. . . . . . . . . . 11
⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆
((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘(ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪
∅))) |
219 | 218 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) → ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆
((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘(ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪
∅))) |
220 | | un0 3919 |
. . . . . . . . . . 11
⊢ (ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) = ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) |
221 | 27, 164 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢
(((ℂfld ↾s ℚ) freeLMod
(1...𝑁)) ∈ LMod ∧
(ℂfld ↾s ℚ) ∈
NzRing) |
222 | 187, 33 | lindsind2 19977 |
. . . . . . . . . . . . . 14
⊢
(((((ℂfld ↾s ℚ) freeLMod
(1...𝑁)) ∈ LMod ∧
(ℂfld ↾s ℚ) ∈ NzRing) ∧ ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) ∧ 𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) → ¬ 𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))) |
223 | 221, 222 | mp3an1 1403 |
. . . . . . . . . . . . 13
⊢ ((ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) ∧ 𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) → ¬ 𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))) |
224 | 223 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ (ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) →
∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))) |
225 | 190, 191 | ismri2 16115 |
. . . . . . . . . . . . . 14
⊢
(((LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))) ∈
(Moore‘(ℚ ↑𝑚 (1...𝑁))) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ
↑𝑚 (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))) ↔
∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))) |
226 | 185, 199,
225 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))) ↔
∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))) |
227 | 226 | biimpar 501 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))))) |
228 | 224, 227 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) → ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))))) |
229 | 220, 228 | syl5eqel 2692 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) → (ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))))) |
230 | | mptfi 8148 |
. . . . . . . . . . . . 13
⊢
((0...𝑁) ∈ Fin
→ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin) |
231 | | rnfi 8132 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin) |
232 | 28, 230, 231 | mp2b 10 |
. . . . . . . . . . . 12
⊢ ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin |
233 | 232 | orci 404 |
. . . . . . . . . . 11
⊢ (ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin ∨ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ Fin) |
234 | 233 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) → (ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin ∨ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ Fin)) |
235 | 186, 190,
191, 197, 202, 209, 219, 229, 234 | mreexexd 16131 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) →
∃𝑣 ∈ 𝒫
ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))))) |
236 | 235 | ex 449 |
. . . . . . . 8
⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) →
∃𝑣 ∈ 𝒫
ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))))))) |
237 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V |
238 | 237 | rnex 6992 |
. . . . . . . . . . . 12
⊢ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V |
239 | | elpwi 4117 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ 𝒫 ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) → 𝑣 ⊆ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) |
240 | | ssdomg 7887 |
. . . . . . . . . . . 12
⊢ (ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V → (𝑣 ⊆ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) → 𝑣 ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)))) |
241 | 238, 239,
240 | mpsyl 66 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ 𝒫 ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) → 𝑣 ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) |
242 | | endomtr 7900 |
. . . . . . . . . . . . . 14
⊢ ((ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ 𝑣 ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) |
243 | 242 | ancoms 468 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ≼ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) |
244 | | f1f1orn 6061 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1-onto→ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) |
245 | | ovex 6577 |
. . . . . . . . . . . . . . . . 17
⊢
(0...𝑁) ∈
V |
246 | 245 | f1oen 7862 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1-onto→ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) → (0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) |
247 | 244, 246 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) |
248 | | endomtr 7900 |
. . . . . . . . . . . . . . . . 17
⊢
(((0...𝑁) ≈
ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) → (0...𝑁) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) |
249 | 203 | uvcendim 20005 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℂfld ↾s ℚ) ∈ NzRing
∧ (1...𝑁) ∈ Fin)
→ (1...𝑁) ≈ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁))) |
250 | 164, 24, 249 | mp2an 704 |
. . . . . . . . . . . . . . . . . . 19
⊢
(1...𝑁) ≈ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) |
251 | 250 | ensymi 7892 |
. . . . . . . . . . . . . . . . . 18
⊢ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁) |
252 | | domentr 7901 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((0...𝑁) ≼
ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (0...𝑁) ≼ (1...𝑁)) |
253 | | hashdom 13029 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((0...𝑁) ∈ Fin
∧ (1...𝑁) ∈ Fin)
→ ((#‘(0...𝑁))
≤ (#‘(1...𝑁))
↔ (0...𝑁) ≼
(1...𝑁))) |
254 | 28, 24, 253 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘(0...𝑁))
≤ (#‘(1...𝑁))
↔ (0...𝑁) ≼
(1...𝑁)) |
255 | | hashfz0 13079 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (#‘(0...𝑁)) =
(𝑁 + 1)) |
256 | 2, 255 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (#‘(0...𝑁)) = (𝑁 + 1)) |
257 | | hashfz1 12996 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (#‘(1...𝑁)) =
𝑁) |
258 | 2, 257 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (#‘(1...𝑁)) = 𝑁) |
259 | 256, 258 | breq12d 4596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((#‘(0...𝑁)) ≤ (#‘(1...𝑁)) ↔ (𝑁 + 1) ≤ 𝑁)) |
260 | 254, 259 | syl5bbr 273 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((0...𝑁) ≼ (1...𝑁) ↔ (𝑁 + 1) ≤ 𝑁)) |
261 | 252, 260 | syl5ib 233 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((0...𝑁) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) ∧ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (𝑁 + 1) ≤ 𝑁)) |
262 | 251, 261 | mpan2i 709 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((0...𝑁) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁)) |
263 | 248, 262 | syl5 33 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) → (𝑁 + 1) ≤ 𝑁)) |
264 | 263 | expd 451 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁))) |
265 | 247, 264 | syl5 33 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁))) |
266 | 265 | com23 84 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁))) |
267 | 243, 266 | syl5 33 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑣 ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁))) |
268 | 267 | expdimp 452 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁))) |
269 | 241, 268 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝒫 ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁))) |
270 | 269 | adantrd 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ 𝒫 ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) → ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))))) →
((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁))) |
271 | 270 | rexlimdva 3013 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑣 ∈ 𝒫 ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))))) →
((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁))) |
272 | 236, 271 | syld 46 |
. . . . . . 7
⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁))) |
273 | 272 | impd 446 |
. . . . . 6
⊢ (𝜑 → ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) ∧ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V) → (𝑁 + 1) ≤ 𝑁)) |
274 | 273 | ancomsd 469 |
. . . . 5
⊢ (𝜑 → (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) → (𝑁 + 1) ≤ 𝑁)) |
275 | 182, 274 | sylbird 249 |
. . . 4
⊢ (𝜑 → (¬ ∃𝑤 ∈ ((ℚ
↑𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → (𝑁 + 1) ≤ 𝑁)) |
276 | 9, 275 | mt3d 139 |
. . 3
⊢ (𝜑 → ∃𝑤 ∈ ((ℚ ↑𝑚
(0...𝑁)) ∖
{((0...𝑁) ×
{0})})∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) |
277 | | eldifsn 4260 |
. . . . 5
⊢ (𝑤 ∈ ((ℚ
↑𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})}) ↔ (𝑤 ∈ (ℚ ↑𝑚
(0...𝑁)) ∧ 𝑤 ≠ ((0...𝑁) × {0}))) |
278 | 44 | anim1i 590 |
. . . . 5
⊢ ((𝑤 ∈ (ℚ
↑𝑚 (0...𝑁)) ∧ 𝑤 ≠ ((0...𝑁) × {0})) → (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) |
279 | 277, 278 | sylbi 206 |
. . . 4
⊢ (𝑤 ∈ ((ℚ
↑𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})}) → (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) |
280 | 97 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ℚ ⊆
ℂ) |
281 | 2 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑁 ∈
ℕ0) |
282 | 280, 281,
56 | elplyd 23762 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈
(Poly‘ℚ)) |
283 | 282 | adantrr 749 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈
(Poly‘ℚ)) |
284 | | uzdisj 12282 |
. . . . . . . . . . . . . . . . . 18
⊢
((0...((𝑁 + 1)
− 1)) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ |
285 | 2 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑁 ∈ ℂ) |
286 | | pncan1 10333 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
287 | 285, 286 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁) |
288 | 287 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁)) |
289 | 288 | ineq1d 3775 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∩
(ℤ≥‘(𝑁 + 1))) = ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) |
290 | 284, 289 | syl5eqr 2658 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∅ = ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1)))) |
291 | 290 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) =
∅) |
292 | 134 | fconst 6004 |
. . . . . . . . . . . . . . . . . 18
⊢
((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶{0} |
293 | | snssi 4280 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
ℚ → {0} ⊆ ℚ) |
294 | 101, 102,
293 | mp2b 10 |
. . . . . . . . . . . . . . . . . . 19
⊢ {0}
⊆ ℚ |
295 | 294, 97 | sstri 3577 |
. . . . . . . . . . . . . . . . . 18
⊢ {0}
⊆ ℂ |
296 | | fss 5969 |
. . . . . . . . . . . . . . . . . 18
⊢
((((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℂ)
→ ((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶ℂ) |
297 | 292, 295,
296 | mp2an 704 |
. . . . . . . . . . . . . . . . 17
⊢
((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶ℂ |
298 | | fun 5979 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤:(0...𝑁)⟶ℚ ∧
((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶ℂ) ∧ ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) = ∅) → (𝑤 ∪
((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪
ℂ)) |
299 | 297, 298 | mpanl2 713 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) = ∅) → (𝑤 ∪
((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪
ℂ)) |
300 | 291, 299 | sylan2 490 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝜑) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪
ℂ)) |
301 | 300 | ancoms 468 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪
ℂ)) |
302 | | nn0uz 11598 |
. . . . . . . . . . . . . . . . . 18
⊢
ℕ0 = (ℤ≥‘0) |
303 | 6, 302 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘0)) |
304 | | uzsplit 12281 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 + 1) ∈
(ℤ≥‘0) → (ℤ≥‘0) =
((0...((𝑁 + 1) − 1))
∪ (ℤ≥‘(𝑁 + 1)))) |
305 | 303, 304 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(ℤ≥‘0) = ((0...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1)))) |
306 | 302, 305 | syl5eq 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ℕ0 =
((0...((𝑁 + 1) − 1))
∪ (ℤ≥‘(𝑁 + 1)))) |
307 | 288 | uneq1d 3728 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1))) = ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) |
308 | 306, 307 | eqtr2d 2645 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))) =
ℕ0) |
309 | | ssequn1 3745 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℚ
⊆ ℂ ↔ (ℚ ∪ ℂ) = ℂ) |
310 | 97, 309 | mpbi 219 |
. . . . . . . . . . . . . . . . 17
⊢ (ℚ
∪ ℂ) = ℂ |
311 | 310 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℚ ∪ ℂ) =
ℂ) |
312 | 308, 311 | feq23d 5953 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ)
↔ (𝑤 ∪
((ℤ≥‘(𝑁 + 1)) ×
{0})):ℕ0⟶ℂ)) |
313 | 312 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪
((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪
ℂ) ↔ (𝑤 ∪
((ℤ≥‘(𝑁 + 1)) ×
{0})):ℕ0⟶ℂ)) |
314 | 301, 313 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) ×
{0})):ℕ0⟶ℂ) |
315 | | ffn 5958 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤:(0...𝑁)⟶ℚ → 𝑤 Fn (0...𝑁)) |
316 | | fnimadisj 5925 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) → (𝑤 “
(ℤ≥‘(𝑁 + 1))) = ∅) |
317 | 315, 291,
316 | syl2anr 494 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 “ (ℤ≥‘(𝑁 + 1))) =
∅) |
318 | 2 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℤ) |
319 | 318 | peano2zd 11361 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
320 | | uzid 11578 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 + 1) ∈ ℤ →
(𝑁 + 1) ∈
(ℤ≥‘(𝑁 + 1))) |
321 | | ne0i 3880 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 + 1) ∈
(ℤ≥‘(𝑁 + 1)) →
(ℤ≥‘(𝑁 + 1)) ≠ ∅) |
322 | 319, 320,
321 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(ℤ≥‘(𝑁 + 1)) ≠ ∅) |
323 | | inidm 3784 |
. . . . . . . . . . . . . . . . . . 19
⊢
((ℤ≥‘(𝑁 + 1)) ∩
(ℤ≥‘(𝑁 + 1))) =
(ℤ≥‘(𝑁 + 1)) |
324 | 323 | neeq1i 2846 |
. . . . . . . . . . . . . . . . . 18
⊢
(((ℤ≥‘(𝑁 + 1)) ∩
(ℤ≥‘(𝑁 + 1))) ≠ ∅ ↔
(ℤ≥‘(𝑁 + 1)) ≠ ∅) |
325 | 322, 324 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
((ℤ≥‘(𝑁 + 1)) ∩
(ℤ≥‘(𝑁 + 1))) ≠ ∅) |
326 | | xpima2 5497 |
. . . . . . . . . . . . . . . . 17
⊢
(((ℤ≥‘(𝑁 + 1)) ∩
(ℤ≥‘(𝑁 + 1))) ≠ ∅ →
(((ℤ≥‘(𝑁 + 1)) × {0}) “
(ℤ≥‘(𝑁 + 1))) = {0}) |
327 | 325, 326 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(((ℤ≥‘(𝑁 + 1)) × {0}) “
(ℤ≥‘(𝑁 + 1))) = {0}) |
328 | 327 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
(((ℤ≥‘(𝑁 + 1)) × {0}) “
(ℤ≥‘(𝑁 + 1))) = {0}) |
329 | 317, 328 | uneq12d 3730 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 “
(ℤ≥‘(𝑁 + 1))) ∪
(((ℤ≥‘(𝑁 + 1)) × {0}) “
(ℤ≥‘(𝑁 + 1)))) = (∅ ∪
{0})) |
330 | | imaundir 5465 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∪
((ℤ≥‘(𝑁 + 1)) × {0})) “
(ℤ≥‘(𝑁 + 1))) = ((𝑤 “ (ℤ≥‘(𝑁 + 1))) ∪
(((ℤ≥‘(𝑁 + 1)) × {0}) “
(ℤ≥‘(𝑁 + 1)))) |
331 | | uncom 3719 |
. . . . . . . . . . . . . . 15
⊢ (∅
∪ {0}) = ({0} ∪ ∅) |
332 | | un0 3919 |
. . . . . . . . . . . . . . 15
⊢ ({0}
∪ ∅) = {0} |
333 | 331, 332 | eqtr2i 2633 |
. . . . . . . . . . . . . 14
⊢ {0} =
(∅ ∪ {0}) |
334 | 329, 330,
333 | 3eqtr4g 2669 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪
((ℤ≥‘(𝑁 + 1)) × {0})) “
(ℤ≥‘(𝑁 + 1))) = {0}) |
335 | 291, 315 | anim12ci 589 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) =
∅)) |
336 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ∈
V → ((ℤ≥‘(𝑁 + 1)) × {0}) Fn
(ℤ≥‘(𝑁 + 1))) |
337 | 134, 336 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((ℤ≥‘(𝑁 + 1)) × {0}) Fn
(ℤ≥‘(𝑁 + 1)) |
338 | | fvun1 6179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 Fn (0...𝑁) ∧
((ℤ≥‘(𝑁 + 1)) × {0}) Fn
(ℤ≥‘(𝑁 + 1)) ∧ (((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ ∧ 𝑘 ∈ (0...𝑁))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘)) |
339 | 337, 338 | mp3an2 1404 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 Fn (0...𝑁) ∧ (((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ ∧ 𝑘 ∈ (0...𝑁))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘)) |
340 | 339 | anassrs 678 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘)) |
341 | 335, 340 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘)) |
342 | 341 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) = ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘)) |
343 | 342 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝑦↑𝑘)) = (((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘))) |
344 | 343 | sumeq2dv 14281 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘))) |
345 | 344 | mpteq2dv 4673 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘)))) |
346 | 282, 281,
314, 334, 345 | coeeq 23787 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (coeff‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) = (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) ×
{0}))) |
347 | 346 | reseq1d 5316 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
((coeff‘(𝑦 ∈
ℂ ↦ Σ𝑘
∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾
(0...𝑁))) |
348 | | res0 5321 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ↾ ∅) =
∅ |
349 | 290 | reseq2d 5317 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑤 ↾ ∅) = (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))))) |
350 | | res0 5321 |
. . . . . . . . . . . . . . 15
⊢
(((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ∅) =
∅ |
351 | 290 | reseq2d 5317 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ∅) =
(((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))))) |
352 | 350, 351 | syl5eqr 2658 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∅ =
(((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))))) |
353 | 348, 349,
352 | 3eqtr3a 2668 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) =
(((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))))) |
354 | | fss 5969 |
. . . . . . . . . . . . . . 15
⊢
((((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℚ)
→ ((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶ℚ) |
355 | 292, 294,
354 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢
((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶ℚ |
356 | | fresaunres1 5990 |
. . . . . . . . . . . . . 14
⊢ ((𝑤:(0...𝑁)⟶ℚ ∧
((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶ℚ ∧ (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) =
(((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾
(0...𝑁)) = 𝑤) |
357 | 355, 356 | mp3an2 1404 |
. . . . . . . . . . . . 13
⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) =
(((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾
(0...𝑁)) = 𝑤) |
358 | 353, 357 | sylan2 490 |
. . . . . . . . . . . 12
⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝜑) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾
(0...𝑁)) = 𝑤) |
359 | 358 | ancoms 468 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪
((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤) |
360 | 347, 359 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
((coeff‘(𝑦 ∈
ℂ ↦ Σ𝑘
∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤) |
361 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 →
(coeff‘(𝑦 ∈
ℂ ↦ Σ𝑘
∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) =
(coeff‘0𝑝)) |
362 | 361 | reseq1d 5316 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 →
((coeff‘(𝑦 ∈
ℂ ↦ Σ𝑘
∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝)
↾ (0...𝑁))) |
363 | | eqtr2 2630 |
. . . . . . . . . . . 12
⊢
((((coeff‘(𝑦
∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝)
↾ (0...𝑁))) →
𝑤 =
((coeff‘0𝑝) ↾ (0...𝑁))) |
364 | | coe0 23816 |
. . . . . . . . . . . . . 14
⊢
(coeff‘0𝑝) = (ℕ0 ×
{0}) |
365 | 364 | reseq1i 5313 |
. . . . . . . . . . . . 13
⊢
((coeff‘0𝑝) ↾ (0...𝑁)) = ((ℕ0 × {0})
↾ (0...𝑁)) |
366 | | elfznn0 12302 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℕ0) |
367 | 366 | ssriv 3572 |
. . . . . . . . . . . . . 14
⊢
(0...𝑁) ⊆
ℕ0 |
368 | | xpssres 5354 |
. . . . . . . . . . . . . 14
⊢
((0...𝑁) ⊆
ℕ0 → ((ℕ0 × {0}) ↾
(0...𝑁)) = ((0...𝑁) × {0})) |
369 | 367, 368 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
((ℕ0 × {0}) ↾ (0...𝑁)) = ((0...𝑁) × {0}) |
370 | 365, 369 | eqtri 2632 |
. . . . . . . . . . . 12
⊢
((coeff‘0𝑝) ↾ (0...𝑁)) = ((0...𝑁) × {0}) |
371 | 363, 370 | syl6eq 2660 |
. . . . . . . . . . 11
⊢
((((coeff‘(𝑦
∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝)
↾ (0...𝑁))) →
𝑤 = ((0...𝑁) × {0})) |
372 | 371 | ex 449 |
. . . . . . . . . 10
⊢
(((coeff‘(𝑦
∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 → (((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝)
↾ (0...𝑁)) →
𝑤 = ((0...𝑁) × {0}))) |
373 | 360, 362,
372 | syl2im 39 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 → 𝑤 = ((0...𝑁) × {0}))) |
374 | 373 | necon3d 2803 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ≠ ((0...𝑁) × {0}) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠
0𝑝)) |
375 | 374 | impr 647 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠
0𝑝) |
376 | | eldifsn 4260 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖
{0𝑝}) ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ (Poly‘ℚ) ∧ (𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠
0𝑝)) |
377 | 283, 375,
376 | sylanbrc 695 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖
{0𝑝})) |
378 | 377 | adantrr 749 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖
{0𝑝})) |
379 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → (𝑦↑𝑘) = (𝐴↑𝑘)) |
380 | 379 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → ((𝑤‘𝑘) · (𝑦↑𝑘)) = ((𝑤‘𝑘) · (𝐴↑𝑘))) |
381 | 380 | sumeq2sdv 14282 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘))) |
382 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) |
383 | | sumex 14266 |
. . . . . . . . . 10
⊢
Σ𝑘 ∈
(0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) ∈ V |
384 | 381, 382,
383 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘))) |
385 | 1, 384 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘))) |
386 | 385 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘))) |
387 | 112 | adantll 746 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ) |
388 | | aacllem.2 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ) |
389 | 388 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ) |
390 | 115, 389 | mulcld 9939 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ) |
391 | 390 | adantllr 751 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ) |
392 | 54, 387, 391 | fsummulc2 14358 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)) = Σ𝑛 ∈ (1...𝑁)((𝑤‘𝑘) · (𝐶 · 𝑋))) |
393 | | aacllem.4 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑𝑘) = Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)) |
394 | 393 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋))) |
395 | 394 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋))) |
396 | 387 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤‘𝑘) ∈ ℂ) |
397 | 115 | adantllr 751 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℂ) |
398 | | simpll 786 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → 𝜑) |
399 | 398, 388 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ) |
400 | 396, 397,
399 | mulassd 9942 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑤‘𝑘) · 𝐶) · 𝑋) = ((𝑤‘𝑘) · (𝐶 · 𝑋))) |
401 | 400 | sumeq2dv 14281 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)((𝑤‘𝑘) · (𝐶 · 𝑋))) |
402 | 392, 395,
401 | 3eqtr4d 2654 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋)) |
403 | 402 | sumeq2dv 14281 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑘 ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋)) |
404 | 112 | ad2ant2lr 780 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (𝑤‘𝑘) ∈ ℂ) |
405 | 115 | anasss 677 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝐶 ∈ ℂ) |
406 | 405 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝐶 ∈ ℂ) |
407 | 404, 406 | mulcld 9939 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → ((𝑤‘𝑘) · 𝐶) ∈ ℂ) |
408 | 388 | ad2ant2rl 781 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝑋 ∈ ℂ) |
409 | 407, 408 | mulcld 9939 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (((𝑤‘𝑘) · 𝐶) · 𝑋) ∈ ℂ) |
410 | 45, 72, 409 | fsumcom 14349 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋)) |
411 | 403, 410 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋)) |
412 | 411 | adantrr 749 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋)) |
413 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛𝜑 |
414 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛 𝑤:(0...𝑁)⟶ℚ |
415 | | nfra1 2925 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 |
416 | 414, 415 | nfan 1816 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) |
417 | 413, 416 | nfan 1816 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛(𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
418 | | rspa 2914 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) |
419 | 418 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋)) |
420 | 419 | adantll 746 |
. . . . . . . . . . . . . 14
⊢ (((𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋)) |
421 | 420 | adantll 746 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋)) |
422 | 388 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ) |
423 | 96, 422, 118 | fsummulc1 14359 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋)) |
424 | 423 | adantlrr 753 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋)) |
425 | 388 | mul02d 10113 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0) |
426 | 425 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0) |
427 | 421, 424,
426 | 3eqtr3d 2652 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0) |
428 | 427 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → (𝑛 ∈ (1...𝑁) → Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0)) |
429 | 417, 428 | ralrimi 2940 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0) |
430 | 429 | sumeq2d 14280 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)0) |
431 | 412, 430 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)0) |
432 | 24 | olci 405 |
. . . . . . . . 9
⊢
((1...𝑁) ⊆
(ℤ≥‘𝐵) ∨ (1...𝑁) ∈ Fin) |
433 | | sumz 14300 |
. . . . . . . . 9
⊢
(((1...𝑁) ⊆
(ℤ≥‘𝐵) ∨ (1...𝑁) ∈ Fin) → Σ𝑛 ∈ (1...𝑁)0 = 0) |
434 | 432, 433 | ax-mp 5 |
. . . . . . . 8
⊢
Σ𝑛 ∈
(1...𝑁)0 =
0 |
435 | 431, 434 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = 0) |
436 | 386, 435 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0) |
437 | 436 | adantrlr 755 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0) |
438 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) → (𝑥‘𝐴) = ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴)) |
439 | 438 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) → ((𝑥‘𝐴) = 0 ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0)) |
440 | 439 | rspcev 3282 |
. . . . 5
⊢ (((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖
{0𝑝}) ∧ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0) → ∃𝑥 ∈ ((Poly‘ℚ) ∖
{0𝑝})(𝑥‘𝐴) = 0) |
441 | 378, 437,
440 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∃𝑥 ∈ ((Poly‘ℚ) ∖
{0𝑝})(𝑥‘𝐴) = 0) |
442 | 279, 441 | sylanr1 682 |
. . 3
⊢ ((𝜑 ∧ (𝑤 ∈ ((ℚ ↑𝑚
(0...𝑁)) ∖
{((0...𝑁) × {0})})
∧ ∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∃𝑥 ∈ ((Poly‘ℚ) ∖
{0𝑝})(𝑥‘𝐴) = 0) |
443 | 276, 442 | rexlimddv 3017 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ ((Poly‘ℚ) ∖
{0𝑝})(𝑥‘𝐴) = 0) |
444 | | elqaa 23881 |
. 2
⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧
∃𝑥 ∈
((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0)) |
445 | 1, 443, 444 | sylanbrc 695 |
1
⊢ (𝜑 → 𝐴 ∈ 𝔸) |