| Step | Hyp | Ref
| Expression |
| 1 | | aacllem.0 |
. 2
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 2 | | aacllem.1 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 3 | 2 | nn0red 12588 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 4 | 3 | ltp1d 12198 |
. . . . 5
⊢ (𝜑 → 𝑁 < (𝑁 + 1)) |
| 5 | | peano2nn0 12566 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
| 6 | 2, 5 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
| 7 | 6 | nn0red 12588 |
. . . . . 6
⊢ (𝜑 → (𝑁 + 1) ∈ ℝ) |
| 8 | 3, 7 | ltnled 11408 |
. . . . 5
⊢ (𝜑 → (𝑁 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑁)) |
| 9 | 4, 8 | mpbid 232 |
. . . 4
⊢ (𝜑 → ¬ (𝑁 + 1) ≤ 𝑁) |
| 10 | | aacllem.3 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ) |
| 11 | 10 | 3expa 1119 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ) |
| 12 | 11 | fmpttd 7135 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ) |
| 13 | | qex 13003 |
. . . . . . . . . . 11
⊢ ℚ
∈ V |
| 14 | | ovex 7464 |
. . . . . . . . . . 11
⊢
(1...𝑁) ∈
V |
| 15 | 13, 14 | elmap 8911 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m
(1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ) |
| 16 | 12, 15 | sylibr 234 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m
(1...𝑁))) |
| 17 | 16 | fmpttd 7135 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑m
(1...𝑁))) |
| 18 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(ℂfld ↾s ℚ) =
(ℂfld ↾s ℚ) |
| 19 | 18 | qdrng 27664 |
. . . . . . . . . . 11
⊢
(ℂfld ↾s ℚ) ∈
DivRing |
| 20 | | drngring 20736 |
. . . . . . . . . . 11
⊢
((ℂfld ↾s ℚ) ∈ DivRing
→ (ℂfld ↾s ℚ) ∈
Ring) |
| 21 | 19, 20 | ax-mp 5 |
. . . . . . . . . 10
⊢
(ℂfld ↾s ℚ) ∈
Ring |
| 22 | | fzfi 14013 |
. . . . . . . . . 10
⊢
(1...𝑁) ∈
Fin |
| 23 | | eqid 2737 |
. . . . . . . . . . 11
⊢
((ℂfld ↾s ℚ) freeLMod (1...𝑁)) = ((ℂfld
↾s ℚ) freeLMod (1...𝑁)) |
| 24 | 23 | frlmlmod 21769 |
. . . . . . . . . 10
⊢
(((ℂfld ↾s ℚ) ∈ Ring ∧
(1...𝑁) ∈ Fin) →
((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod) |
| 25 | 21, 22, 24 | mp2an 692 |
. . . . . . . . 9
⊢
((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod |
| 26 | | fzfi 14013 |
. . . . . . . . 9
⊢
(0...𝑁) ∈
Fin |
| 27 | 18 | qrngbas 27663 |
. . . . . . . . . . . 12
⊢ ℚ =
(Base‘(ℂfld ↾s
ℚ)) |
| 28 | 23, 27 | frlmfibas 21782 |
. . . . . . . . . . 11
⊢
(((ℂfld ↾s ℚ) ∈ DivRing
∧ (1...𝑁) ∈ Fin)
→ (ℚ ↑m (1...𝑁)) = (Base‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))) |
| 29 | 19, 22, 28 | mp2an 692 |
. . . . . . . . . 10
⊢ (ℚ
↑m (1...𝑁))
= (Base‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) |
| 30 | 23 | frlmsca 21773 |
. . . . . . . . . . 11
⊢
(((ℂfld ↾s ℚ) ∈ DivRing
∧ (1...𝑁) ∈ Fin)
→ (ℂfld ↾s ℚ) =
(Scalar‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) |
| 31 | 19, 22, 30 | mp2an 692 |
. . . . . . . . . 10
⊢
(ℂfld ↾s ℚ) =
(Scalar‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) |
| 32 | | eqid 2737 |
. . . . . . . . . 10
⊢ (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁))) = ( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) |
| 33 | 18 | qrng0 27665 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘(ℂfld ↾s
ℚ)) |
| 34 | 23, 33 | frlm0 21774 |
. . . . . . . . . . 11
⊢
(((ℂfld ↾s ℚ) ∈ Ring ∧
(1...𝑁) ∈ Fin) →
((1...𝑁) × {0}) =
(0g‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))) |
| 35 | 21, 22, 34 | mp2an 692 |
. . . . . . . . . 10
⊢
((1...𝑁) ×
{0}) = (0g‘((ℂfld ↾s
ℚ) freeLMod (1...𝑁))) |
| 36 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
((ℂfld ↾s ℚ) freeLMod (0...𝑁)) = ((ℂfld
↾s ℚ) freeLMod (0...𝑁)) |
| 37 | 36, 27 | frlmfibas 21782 |
. . . . . . . . . . 11
⊢
(((ℂfld ↾s ℚ) ∈ DivRing
∧ (0...𝑁) ∈ Fin)
→ (ℚ ↑m (0...𝑁)) = (Base‘((ℂfld
↾s ℚ) freeLMod (0...𝑁)))) |
| 38 | 19, 26, 37 | mp2an 692 |
. . . . . . . . . 10
⊢ (ℚ
↑m (0...𝑁))
= (Base‘((ℂfld ↾s ℚ) freeLMod
(0...𝑁))) |
| 39 | 29, 31, 32, 35, 33, 38 | islindf4 21858 |
. . . . . . . . 9
⊢
((((ℂfld ↾s ℚ) freeLMod
(1...𝑁)) ∈ LMod ∧
(0...𝑁) ∈ Fin ∧
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑m
(1...𝑁))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld
↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m
(0...𝑁))((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})))) |
| 40 | 25, 26, 39 | mp3an12 1453 |
. . . . . . . 8
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑m
(1...𝑁)) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld
↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m
(0...𝑁))((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})))) |
| 41 | 17, 40 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld
↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m
(0...𝑁))((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})))) |
| 42 | | elmapi 8889 |
. . . . . . . . 9
⊢ (𝑤 ∈ (ℚ
↑m (0...𝑁))
→ 𝑤:(0...𝑁)⟶ℚ) |
| 43 | | fzfid 14014 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (0...𝑁) ∈ Fin) |
| 44 | | fvexd 6921 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ V) |
| 45 | 14 | mptex 7243 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V |
| 46 | 45 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V) |
| 47 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑤:(0...𝑁)⟶ℚ) |
| 48 | 47 | feqmptd 6977 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑤 = (𝑘 ∈ (0...𝑁) ↦ (𝑤‘𝑘))) |
| 49 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) |
| 50 | 43, 44, 46, 48, 49 | offval2 7717 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘)( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)))) |
| 51 | | fzfid 14014 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin) |
| 52 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ) |
| 53 | 52 | adantll 714 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ) |
| 54 | 16 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m
(1...𝑁))) |
| 55 | | cnfldmul 21372 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ·
= (.r‘ℂfld) |
| 56 | 18, 55 | ressmulr 17351 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℚ
∈ V → · = (.r‘(ℂfld
↾s ℚ))) |
| 57 | 13, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ·
= (.r‘(ℂfld ↾s
ℚ)) |
| 58 | 23, 29, 27, 51, 53, 54, 32, 57 | frlmvscafval 21786 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘)( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (((1...𝑁) × {(𝑤‘𝑘)}) ∘f · (𝑛 ∈ (1...𝑁) ↦ 𝐶))) |
| 59 | | fvexd 6921 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤‘𝑘) ∈ V) |
| 60 | 11 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ) |
| 61 | | fconstmpt 5747 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((1...𝑁) ×
{(𝑤‘𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤‘𝑘)) |
| 62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((1...𝑁) × {(𝑤‘𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤‘𝑘))) |
| 63 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) = (𝑛 ∈ (1...𝑁) ↦ 𝐶)) |
| 64 | 51, 59, 60, 62, 63 | offval2 7717 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (((1...𝑁) × {(𝑤‘𝑘)}) ∘f · (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) |
| 65 | 58, 64 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘)( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) |
| 66 | 65 | mpteq2dva 5242 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘)( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) |
| 67 | 50, 66 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) |
| 68 | 67 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))) |
| 69 | | fzfid 14014 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (1...𝑁) ∈ Fin) |
| 70 | 21 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
(ℂfld ↾s ℚ) ∈
Ring) |
| 71 | 53 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ) |
| 72 | 11 | an32s 652 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℚ) |
| 73 | 72 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℚ) |
| 74 | | qmulcl 13009 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤‘𝑘) ∈ ℚ ∧ 𝐶 ∈ ℚ) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ) |
| 75 | 71, 73, 74 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ) |
| 76 | 75 | an32s 652 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ) |
| 77 | 76 | fmpttd 7135 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ) |
| 78 | 13, 14 | elmap 8911 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m
(1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ) |
| 79 | 77, 78 | sylibr 234 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m
(1...𝑁))) |
| 80 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) |
| 81 | 14 | mptex 7243 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ V |
| 82 | 81 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ V) |
| 83 | | snex 5436 |
. . . . . . . . . . . . . . . . . . 19
⊢ {0}
∈ V |
| 84 | 14, 83 | xpex 7773 |
. . . . . . . . . . . . . . . . . 18
⊢
((1...𝑁) ×
{0}) ∈ V |
| 85 | 84 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((1...𝑁) × {0}) ∈
V) |
| 86 | 80, 43, 82, 85 | fsuppmptdm 9416 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) finSupp ((1...𝑁) × {0})) |
| 87 | 23, 29, 35, 69, 43, 70, 79, 86 | frlmgsum 21792 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ ((ℂfld
↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))) |
| 88 | | cnfldbas 21368 |
. . . . . . . . . . . . . . . . . 18
⊢ ℂ =
(Base‘ℂfld) |
| 89 | | cnfldadd 21370 |
. . . . . . . . . . . . . . . . . 18
⊢ + =
(+g‘ℂfld) |
| 90 | | cnfldex 21367 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℂfld ∈ V |
| 91 | 90 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℂfld ∈
V) |
| 92 | | fzfid 14014 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (0...𝑁) ∈ Fin) |
| 93 | | qsscn 13002 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℚ
⊆ ℂ |
| 94 | 93 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℚ ⊆
ℂ) |
| 95 | 75 | fmpttd 7135 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(0...𝑁)⟶ℚ) |
| 96 | | 0z 12624 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ∈
ℤ |
| 97 | | zq 12996 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
ℤ → 0 ∈ ℚ) |
| 98 | 96, 97 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℚ |
| 99 | 98 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 0 ∈ ℚ) |
| 100 | | addlid 11444 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℂ → (0 +
𝑥) = 𝑥) |
| 101 | | addrid 11441 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℂ → (𝑥 + 0) = 𝑥) |
| 102 | 100, 101 | jca 511 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ → ((0 +
𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥)) |
| 103 | 102 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ ℂ) → ((0 + 𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥)) |
| 104 | 88, 89, 18, 91, 92, 94, 95, 99, 103 | gsumress 18695 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂfld
Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = ((ℂfld
↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) |
| 105 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑤:(0...𝑁)⟶ℚ) |
| 106 | | qcn 13005 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑤‘𝑘) ∈ ℚ → (𝑤‘𝑘) ∈ ℂ) |
| 107 | 52, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ) |
| 108 | 105, 107 | sylan 580 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ) |
| 109 | | qcn 13005 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐶 ∈ ℚ → 𝐶 ∈
ℂ) |
| 110 | 11, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℂ) |
| 111 | 110 | an32s 652 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℂ) |
| 112 | 111 | adantllr 719 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℂ) |
| 113 | 108, 112 | mulcld 11281 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℂ) |
| 114 | 92, 113 | gsumfsum 21452 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂfld
Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) |
| 115 | 104, 114 | eqtr3d 2779 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((ℂfld
↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) |
| 116 | 115 | mpteq2dva 5242 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ ((ℂfld
↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))) |
| 117 | 68, 87, 116 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))) |
| 118 | | qaddcl 13007 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ) → (𝑥 + 𝑦) ∈ ℚ) |
| 119 | 118 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) ∈ ℚ) |
| 120 | 94, 119, 92, 75, 99 | fsumcllem 15768 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ ℚ) |
| 121 | 120 | fmpttd 7135 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ) |
| 122 | 13, 14 | elmap 8911 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m
(1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ) |
| 123 | 121, 122 | sylibr 234 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m
(1...𝑁))) |
| 124 | 117, 123 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) ∈ (ℚ ↑m
(1...𝑁))) |
| 125 | | elmapi 8889 |
. . . . . . . . . . . . 13
⊢
((((ℂfld ↾s ℚ) freeLMod
(1...𝑁))
Σg (𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) ∈ (ℚ ↑m
(1...𝑁)) →
(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))):(1...𝑁)⟶ℚ) |
| 126 | | ffn 6736 |
. . . . . . . . . . . . 13
⊢
((((ℂfld ↾s ℚ) freeLMod
(1...𝑁))
Σg (𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))):(1...𝑁)⟶ℚ →
(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁)) |
| 127 | 124, 125,
126 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁)) |
| 128 | | c0ex 11255 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
| 129 | | fnconstg 6796 |
. . . . . . . . . . . . 13
⊢ (0 ∈
V → ((1...𝑁) ×
{0}) Fn (1...𝑁)) |
| 130 | 128, 129 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
((1...𝑁) ×
{0}) Fn (1...𝑁) |
| 131 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛((ℂfld ↾s
ℚ) freeLMod (1...𝑁)) |
| 132 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛
Σg |
| 133 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛𝑤 |
| 134 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛
∘f ( ·𝑠
‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) |
| 135 | | nfcv 2905 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛(0...𝑁) |
| 136 | | nfmpt1 5250 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛(𝑛 ∈ (1...𝑁) ↦ 𝐶) |
| 137 | 135, 136 | nfmpt 5249 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) |
| 138 | 133, 134,
137 | nfov 7461 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) |
| 139 | 131, 132,
138 | nfov 7461 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛(((ℂfld ↾s
ℚ) freeLMod (1...𝑁))
Σg (𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) |
| 140 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛((1...𝑁) × {0}) |
| 141 | 139, 140 | eqfnfv2f 7055 |
. . . . . . . . . . . 12
⊢
(((((ℂfld ↾s ℚ) freeLMod
(1...𝑁))
Σg (𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁) ∧ ((1...𝑁) × {0}) Fn (1...𝑁)) → ((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛))) |
| 142 | 127, 130,
141 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛))) |
| 143 | 117 | fveq1d 6908 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛)) |
| 144 | | sumex 15724 |
. . . . . . . . . . . . . . 15
⊢
Σ𝑘 ∈
(0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ V |
| 145 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) |
| 146 | 145 | fvmpt2 7027 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ (1...𝑁) ∧ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ V) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) |
| 147 | 144, 146 | mpan2 691 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) |
| 148 | 143, 147 | sylan9eq 2797 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) |
| 149 | 128 | fvconst2 7224 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0) |
| 150 | 149 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0) |
| 151 | 148, 150 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
| 152 | 151 | ralbidva 3176 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (∀𝑛 ∈ (1...𝑁)((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
| 153 | 142, 152 | bitrd 279 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
| 154 | 153 | imbi1d 341 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
(((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ (∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})))) |
| 155 | 42, 154 | sylan2 593 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (ℚ ↑m
(0...𝑁))) →
(((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg
(𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ (∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})))) |
| 156 | 155 | ralbidva 3176 |
. . . . . . 7
⊢ (𝜑 → (∀𝑤 ∈ (ℚ
↑m (0...𝑁))((((ℂfld
↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f (
·𝑠 ‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ ∀𝑤 ∈ (ℚ
↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})))) |
| 157 | 41, 156 | bitrd 279 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld
↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m
(0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})))) |
| 158 | | drngnzr 20748 |
. . . . . . . . 9
⊢
((ℂfld ↾s ℚ) ∈ DivRing
→ (ℂfld ↾s ℚ) ∈
NzRing) |
| 159 | 19, 158 | ax-mp 5 |
. . . . . . . 8
⊢
(ℂfld ↾s ℚ) ∈
NzRing |
| 160 | 31 | islindf3 21846 |
. . . . . . . 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...𝑁)))))) |
| 161 | 25, 159, 160 | mp2an 692 |
. . . . . . 7
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld
↾s ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))))) |
| 162 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) |
| 163 | 45, 162 | dmmpti 6712 |
. . . . . . . . 9
⊢ dom
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (0...𝑁) |
| 164 | | f1eq2 6800 |
. . . . . . . . 9
⊢ (dom
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (0...𝑁) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ↔ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V)) |
| 165 | 163, 164 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ↔ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V) |
| 166 | 165 | anbi1i 624 |
. . . . . . 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...𝑁))))) |
| 167 | 161, 166 | bitri 275 |
. . . . . 6
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld
↾s ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))))) |
| 168 | | con34b 316 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ (¬ 𝑤 = ((0...𝑁) × {0}) → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
| 169 | | df-nel 3047 |
. . . . . . . . . . 11
⊢ (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬
𝑤 ∈ {((0...𝑁) ×
{0})}) |
| 170 | | velsn 4642 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {((0...𝑁) × {0})} ↔ 𝑤 = ((0...𝑁) × {0})) |
| 171 | 169, 170 | xchbinx 334 |
. . . . . . . . . 10
⊢ (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬
𝑤 = ((0...𝑁) × {0})) |
| 172 | 171 | imbi1i 349 |
. . . . . . . . 9
⊢ ((𝑤 ∉ {((0...𝑁) × {0})} → ¬
∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ↔ (¬ 𝑤 = ((0...𝑁) × {0}) → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
| 173 | 168, 172 | bitr4i 278 |
. . . . . . . 8
⊢
((∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ (𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
| 174 | 173 | ralbii 3093 |
. . . . . . 7
⊢
(∀𝑤 ∈
(ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ∀𝑤 ∈ (ℚ
↑m (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
| 175 | | raldifb 4149 |
. . . . . . 7
⊢
(∀𝑤 ∈
(ℚ ↑m (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ↔ ∀𝑤 ∈ ((ℚ ↑m
(0...𝑁)) ∖
{((0...𝑁) × {0})})
¬ ∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) |
| 176 | | ralnex 3072 |
. . . . . . 7
⊢
(∀𝑤 ∈
((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ↔ ¬ ∃𝑤 ∈ ((ℚ ↑m
(0...𝑁)) ∖
{((0...𝑁) ×
{0})})∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) |
| 177 | 174, 175,
176 | 3bitri 297 |
. . . . . 6
⊢
(∀𝑤 ∈
(ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ¬ ∃𝑤 ∈ ((ℚ
↑m (0...𝑁))
∖ {((0...𝑁) ×
{0})})∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) |
| 178 | 157, 167,
177 | 3bitr3g 313 |
. . . . 5
⊢ (𝜑 → (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) ↔ ¬
∃𝑤 ∈ ((ℚ
↑m (0...𝑁))
∖ {((0...𝑁) ×
{0})})∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
| 179 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))) =
(LSubSp‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) |
| 180 | 29, 179 | lssmre 20964 |
. . . . . . . . . . . 12
⊢
(((ℂfld ↾s ℚ) freeLMod
(1...𝑁)) ∈ LMod →
(LSubSp‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) ∈
(Moore‘(ℚ ↑m (1...𝑁)))) |
| 181 | 25, 180 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))) ∈
(Moore‘(ℚ ↑m (1...𝑁))) |
| 182 | 181 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) →
(LSubSp‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) ∈
(Moore‘(ℚ ↑m (1...𝑁)))) |
| 183 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(LSpan‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))) =
(LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) |
| 184 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(mrCls‘(LSubSp‘((ℂfld ↾s
ℚ) freeLMod (1...𝑁)))) =
(mrCls‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))) |
| 185 | 179, 183,
184 | mrclsp 20987 |
. . . . . . . . . . 11
⊢
(((ℂfld ↾s ℚ) freeLMod
(1...𝑁)) ∈ LMod →
(LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) =
(mrCls‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))))) |
| 186 | 25, 185 | ax-mp 5 |
. . . . . . . . . 10
⊢
(LSpan‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))) =
(mrCls‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))) |
| 187 | | eqid 2737 |
. . . . . . . . . 10
⊢
(mrInd‘(LSubSp‘((ℂfld ↾s
ℚ) freeLMod (1...𝑁)))) =
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))) |
| 188 | 31 | islvec 21103 |
. . . . . . . . . . . . 13
⊢
(((ℂfld ↾s ℚ) freeLMod
(1...𝑁)) ∈ LVec ↔
(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧
(ℂfld ↾s ℚ) ∈
DivRing)) |
| 189 | 25, 19, 188 | mpbir2an 711 |
. . . . . . . . . . . 12
⊢
((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LVec |
| 190 | 179, 186,
29 | lssacsex 21146 |
. . . . . . . . . . . . 13
⊢
(((ℂfld ↾s ℚ) freeLMod
(1...𝑁)) ∈ LVec →
((LSubSp‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) ∈
(ACS‘(ℚ ↑m (1...𝑁))) ∧ ∀𝑧 ∈ 𝒫 (ℚ ↑m
(1...𝑁))∀𝑥 ∈ (ℚ
↑m (1...𝑁))∀𝑦 ∈
(((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖
((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦})))) |
| 191 | 190 | simprd 495 |
. . . . . . . . . . . 12
⊢
(((ℂfld ↾s ℚ) freeLMod
(1...𝑁)) ∈ LVec →
∀𝑧 ∈ 𝒫
(ℚ ↑m (1...𝑁))∀𝑥 ∈ (ℚ ↑m
(1...𝑁))∀𝑦 ∈
(((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖
((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦}))) |
| 192 | 189, 191 | ax-mp 5 |
. . . . . . . . . . 11
⊢
∀𝑧 ∈
𝒫 (ℚ ↑m (1...𝑁))∀𝑥 ∈ (ℚ ↑m
(1...𝑁))∀𝑦 ∈
(((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖
((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦})) |
| 193 | 192 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) →
∀𝑧 ∈ 𝒫
(ℚ ↑m (1...𝑁))∀𝑥 ∈ (ℚ ↑m
(1...𝑁))∀𝑦 ∈
(((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖
((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦}))) |
| 194 | 17 | frnd 6744 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ ↑m
(1...𝑁))) |
| 195 | | dif0 4378 |
. . . . . . . . . . . 12
⊢ ((ℚ
↑m (1...𝑁))
∖ ∅) = (ℚ ↑m (1...𝑁)) |
| 196 | 194, 195 | sseqtrrdi 4025 |
. . . . . . . . . . 11
⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((ℚ ↑m
(1...𝑁)) ∖
∅)) |
| 197 | 196 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) → ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((ℚ ↑m
(1...𝑁)) ∖
∅)) |
| 198 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
((ℂfld ↾s ℚ) unitVec (1...𝑁)) = ((ℂfld
↾s ℚ) unitVec (1...𝑁)) |
| 199 | 198, 23, 29 | uvcff 21811 |
. . . . . . . . . . . . . 14
⊢
(((ℂfld ↾s ℚ) ∈ Ring ∧
(1...𝑁) ∈ Fin) →
((ℂfld ↾s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑m
(1...𝑁))) |
| 200 | 21, 22, 199 | mp2an 692 |
. . . . . . . . . . . . 13
⊢
((ℂfld ↾s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑m
(1...𝑁)) |
| 201 | | frn 6743 |
. . . . . . . . . . . . 13
⊢
(((ℂfld ↾s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑m
(1...𝑁)) → ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ⊆ (ℚ
↑m (1...𝑁))) |
| 202 | 200, 201 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ⊆ (ℚ
↑m (1...𝑁)) |
| 203 | 202, 195 | sseqtrri 4033 |
. . . . . . . . . . 11
⊢ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ⊆ ((ℚ
↑m (1...𝑁))
∖ ∅) |
| 204 | 203 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) → ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ⊆ ((ℚ
↑m (1...𝑁))
∖ ∅)) |
| 205 | | un0 4394 |
. . . . . . . . . . . . . 14
⊢ (ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅) = ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) |
| 206 | 205 | fveq2i 6909 |
. . . . . . . . . . . . 13
⊢
((LSpan‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))‘(ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) ∪ ∅)) =
((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘ran
((ℂfld ↾s ℚ) unitVec (1...𝑁))) |
| 207 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(LBasis‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))) =
(LBasis‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) |
| 208 | 23, 198, 207 | frlmlbs 21817 |
. . . . . . . . . . . . . . 15
⊢
(((ℂfld ↾s ℚ) ∈ Ring ∧
(1...𝑁) ∈ Fin) →
ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈
(LBasis‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) |
| 209 | 21, 22, 208 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈
(LBasis‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) |
| 210 | 29, 207, 183 | lbssp 21078 |
. . . . . . . . . . . . . 14
⊢ (ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈
(LBasis‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) →
((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘ran
((ℂfld ↾s ℚ) unitVec (1...𝑁))) = (ℚ
↑m (1...𝑁))) |
| 211 | 209, 210 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
((LSpan‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))‘ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) = (ℚ ↑m (1...𝑁)) |
| 212 | 206, 211 | eqtri 2765 |
. . . . . . . . . . . 12
⊢
((LSpan‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))‘(ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) ∪ ∅)) = (ℚ
↑m (1...𝑁)) |
| 213 | 194, 212 | sseqtrrdi 4025 |
. . . . . . . . . . 11
⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆
((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘(ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪
∅))) |
| 214 | 213 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) → ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆
((LSpan‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))‘(ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪
∅))) |
| 215 | | un0 4394 |
. . . . . . . . . . 11
⊢ (ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) = ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) |
| 216 | 25, 159 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢
(((ℂfld ↾s ℚ) freeLMod
(1...𝑁)) ∈ LMod ∧
(ℂfld ↾s ℚ) ∈
NzRing) |
| 217 | 183, 31 | lindsind2 21839 |
. . . . . . . . . . . . . 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...𝑁) ↦ 𝐶)) ∖ {𝑥}))) |
| 218 | 216, 217 | mp3an1 1450 |
. . . . . . . . . . . . 13
⊢ ((ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) ∧ 𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) → ¬ 𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))) |
| 219 | 218 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) →
∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))) |
| 220 | 186, 187 | ismri2 17675 |
. . . . . . . . . . . . . 14
⊢
(((LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))) ∈
(Moore‘(ℚ ↑m (1...𝑁))) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ ↑m
(1...𝑁))) → (ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))) ↔
∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))) |
| 221 | 181, 194,
220 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))) ↔
∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))) |
| 222 | 221 | biimpar 477 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld
↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))))) |
| 223 | 219, 222 | sylan2 593 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) → ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))))) |
| 224 | 215, 223 | eqeltrid 2845 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) → (ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))))) |
| 225 | | mptfi 9391 |
. . . . . . . . . . . . 13
⊢
((0...𝑁) ∈ Fin
→ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin) |
| 226 | | rnfi 9380 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin) |
| 227 | 26, 225, 226 | mp2b 10 |
. . . . . . . . . . . 12
⊢ ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin |
| 228 | 227 | orci 866 |
. . . . . . . . . . 11
⊢ (ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin ∨ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ Fin) |
| 229 | 228 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) → (ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin ∨ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ Fin)) |
| 230 | 182, 186,
187, 193, 197, 204, 214, 224, 229 | mreexexd 17691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) →
∃𝑣 ∈ 𝒫
ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁)))))) |
| 231 | 230 | ex 412 |
. . . . . . . 8
⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) →
∃𝑣 ∈ 𝒫
ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))))))) |
| 232 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V |
| 233 | 232 | rnex 7932 |
. . . . . . . . . . . 12
⊢ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V |
| 234 | | elpwi 4607 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ 𝒫 ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) → 𝑣 ⊆ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) |
| 235 | | ssdomg 9040 |
. . . . . . . . . . . 12
⊢ (ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V → (𝑣 ⊆ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) → 𝑣 ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)))) |
| 236 | 233, 234,
235 | mpsyl 68 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ 𝒫 ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) → 𝑣 ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) |
| 237 | | endomtr 9052 |
. . . . . . . . . . . . . 14
⊢ ((ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ 𝑣 ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) |
| 238 | 237 | ancoms 458 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ≼ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) |
| 239 | | f1f1orn 6859 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1-onto→ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) |
| 240 | | ovex 7464 |
. . . . . . . . . . . . . . . . 17
⊢
(0...𝑁) ∈
V |
| 241 | 240 | f1oen 9013 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1-onto→ran
(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) → (0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) |
| 242 | 239, 241 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) |
| 243 | | endomtr 9052 |
. . . . . . . . . . . . . . . . 17
⊢
(((0...𝑁) ≈
ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) → (0...𝑁) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) |
| 244 | 198 | uvcendim 21867 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℂfld ↾s ℚ) ∈ NzRing
∧ (1...𝑁) ∈ Fin)
→ (1...𝑁) ≈ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁))) |
| 245 | 159, 22, 244 | mp2an 692 |
. . . . . . . . . . . . . . . . . . 19
⊢
(1...𝑁) ≈ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) |
| 246 | 245 | ensymi 9044 |
. . . . . . . . . . . . . . . . . 18
⊢ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁) |
| 247 | | domentr 9053 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((0...𝑁) ≼
ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran
((ℂfld ↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (0...𝑁) ≼ (1...𝑁)) |
| 248 | | hashdom 14418 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((0...𝑁) ∈ Fin
∧ (1...𝑁) ∈ Fin)
→ ((♯‘(0...𝑁)) ≤ (♯‘(1...𝑁)) ↔ (0...𝑁) ≼ (1...𝑁))) |
| 249 | 26, 22, 248 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘(0...𝑁)) ≤ (♯‘(1...𝑁)) ↔ (0...𝑁) ≼ (1...𝑁)) |
| 250 | | hashfz0 14471 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (♯‘(0...𝑁)) = (𝑁 + 1)) |
| 251 | 2, 250 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (♯‘(0...𝑁)) = (𝑁 + 1)) |
| 252 | | hashfz1 14385 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (♯‘(1...𝑁)) = 𝑁) |
| 253 | 2, 252 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁) |
| 254 | 251, 253 | breq12d 5156 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((♯‘(0...𝑁)) ≤
(♯‘(1...𝑁))
↔ (𝑁 + 1) ≤ 𝑁)) |
| 255 | 249, 254 | bitr3id 285 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((0...𝑁) ≼ (1...𝑁) ↔ (𝑁 + 1) ≤ 𝑁)) |
| 256 | 247, 255 | imbitrid 244 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((0...𝑁) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) ∧ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (𝑁 + 1) ≤ 𝑁)) |
| 257 | 246, 256 | mpan2i 697 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((0...𝑁) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁)) |
| 258 | 243, 257 | syl5 34 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) → (𝑁 + 1) ≤ 𝑁)) |
| 259 | 258 | expd 415 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁))) |
| 260 | 242, 259 | syl5 34 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁))) |
| 261 | 260 | com23 86 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁))) |
| 262 | 238, 261 | syl5 34 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑣 ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁))) |
| 263 | 262 | expdimp 452 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ≼ ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁))) |
| 264 | 236, 263 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝒫 ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁))) |
| 265 | 264 | adantrd 491 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ 𝒫 ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))) → ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))))) →
((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁))) |
| 266 | 265 | rexlimdva 3155 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑣 ∈ 𝒫 ran ((ℂfld
↾s ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈
(mrInd‘(LSubSp‘((ℂfld ↾s ℚ)
freeLMod (1...𝑁))))) →
((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁))) |
| 267 | 231, 266 | syld 47 |
. . . . . . 7
⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁))) |
| 268 | 267 | impd 410 |
. . . . . 6
⊢ (𝜑 → ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁))) ∧ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V) → (𝑁 + 1) ≤ 𝑁)) |
| 269 | 268 | ancomsd 465 |
. . . . 5
⊢ (𝜑 → (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈
(LIndS‘((ℂfld ↾s ℚ) freeLMod
(1...𝑁)))) → (𝑁 + 1) ≤ 𝑁)) |
| 270 | 178, 269 | sylbird 260 |
. . . 4
⊢ (𝜑 → (¬ ∃𝑤 ∈ ((ℚ
↑m (0...𝑁))
∖ {((0...𝑁) ×
{0})})∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → (𝑁 + 1) ≤ 𝑁)) |
| 271 | 9, 270 | mt3d 148 |
. . 3
⊢ (𝜑 → ∃𝑤 ∈ ((ℚ ↑m
(0...𝑁)) ∖
{((0...𝑁) ×
{0})})∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) |
| 272 | | eldifsn 4786 |
. . . . 5
⊢ (𝑤 ∈ ((ℚ
↑m (0...𝑁))
∖ {((0...𝑁) ×
{0})}) ↔ (𝑤 ∈
(ℚ ↑m (0...𝑁)) ∧ 𝑤 ≠ ((0...𝑁) × {0}))) |
| 273 | 42 | anim1i 615 |
. . . . 5
⊢ ((𝑤 ∈ (ℚ
↑m (0...𝑁))
∧ 𝑤 ≠ ((0...𝑁) × {0})) → (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) |
| 274 | 272, 273 | sylbi 217 |
. . . 4
⊢ (𝑤 ∈ ((ℚ
↑m (0...𝑁))
∖ {((0...𝑁) ×
{0})}) → (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) |
| 275 | 93 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ℚ ⊆
ℂ) |
| 276 | 2 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑁 ∈
ℕ0) |
| 277 | 275, 276,
53 | elplyd 26241 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈
(Poly‘ℚ)) |
| 278 | 277 | adantrr 717 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈
(Poly‘ℚ)) |
| 279 | | uzdisj 13637 |
. . . . . . . . . . . . . . . . . 18
⊢
((0...((𝑁 + 1)
− 1)) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ |
| 280 | 2 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 281 | | pncan1 11687 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
| 282 | 280, 281 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁) |
| 283 | 282 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁)) |
| 284 | 283 | ineq1d 4219 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∩
(ℤ≥‘(𝑁 + 1))) = ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) |
| 285 | 279, 284 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∅ = ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1)))) |
| 286 | 285 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) =
∅) |
| 287 | 128 | fconst 6794 |
. . . . . . . . . . . . . . . . . 18
⊢
((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶{0} |
| 288 | | snssi 4808 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
ℚ → {0} ⊆ ℚ) |
| 289 | 96, 97, 288 | mp2b 10 |
. . . . . . . . . . . . . . . . . . 19
⊢ {0}
⊆ ℚ |
| 290 | 289, 93 | sstri 3993 |
. . . . . . . . . . . . . . . . . 18
⊢ {0}
⊆ ℂ |
| 291 | | fss 6752 |
. . . . . . . . . . . . . . . . . 18
⊢
((((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℂ)
→ ((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶ℂ) |
| 292 | 287, 290,
291 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢
((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶ℂ |
| 293 | | fun 6770 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤:(0...𝑁)⟶ℚ ∧
((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶ℂ) ∧ ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) = ∅) → (𝑤 ∪
((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪
ℂ)) |
| 294 | 292, 293 | mpanl2 701 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))) = ∅) → (𝑤 ∪
((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪
ℂ)) |
| 295 | 286, 294 | sylan2 593 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝜑) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪
ℂ)) |
| 296 | 295 | ancoms 458 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪
ℂ)) |
| 297 | | nn0uz 12920 |
. . . . . . . . . . . . . . . . . 18
⊢
ℕ0 = (ℤ≥‘0) |
| 298 | 6, 297 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘0)) |
| 299 | | uzsplit 13636 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 + 1) ∈
(ℤ≥‘0) → (ℤ≥‘0) =
((0...((𝑁 + 1) − 1))
∪ (ℤ≥‘(𝑁 + 1)))) |
| 300 | 298, 299 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(ℤ≥‘0) = ((0...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1)))) |
| 301 | 297, 300 | eqtrid 2789 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ℕ0 =
((0...((𝑁 + 1) − 1))
∪ (ℤ≥‘(𝑁 + 1)))) |
| 302 | 283 | uneq1d 4167 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1))) = ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) |
| 303 | 301, 302 | eqtr2d 2778 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))) =
ℕ0) |
| 304 | | ssequn1 4186 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℚ
⊆ ℂ ↔ (ℚ ∪ ℂ) = ℂ) |
| 305 | 93, 304 | mpbi 230 |
. . . . . . . . . . . . . . . . 17
⊢ (ℚ
∪ ℂ) = ℂ |
| 306 | 305 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℚ ∪ ℂ) =
ℂ) |
| 307 | 303, 306 | feq23d 6731 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ)
↔ (𝑤 ∪
((ℤ≥‘(𝑁 + 1)) ×
{0})):ℕ0⟶ℂ)) |
| 308 | 307 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪
((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪
ℂ) ↔ (𝑤 ∪
((ℤ≥‘(𝑁 + 1)) ×
{0})):ℕ0⟶ℂ)) |
| 309 | 296, 308 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) ×
{0})):ℕ0⟶ℂ) |
| 310 | | ffn 6736 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤:(0...𝑁)⟶ℚ → 𝑤 Fn (0...𝑁)) |
| 311 | | fnimadisj 6700 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) → (𝑤 “
(ℤ≥‘(𝑁 + 1))) = ∅) |
| 312 | 310, 286,
311 | syl2anr 597 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 “ (ℤ≥‘(𝑁 + 1))) =
∅) |
| 313 | 2 | nn0zd 12639 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 314 | 313 | peano2zd 12725 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
| 315 | | uzid 12893 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 + 1) ∈ ℤ →
(𝑁 + 1) ∈
(ℤ≥‘(𝑁 + 1))) |
| 316 | | ne0i 4341 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 + 1) ∈
(ℤ≥‘(𝑁 + 1)) →
(ℤ≥‘(𝑁 + 1)) ≠ ∅) |
| 317 | 314, 315,
316 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(ℤ≥‘(𝑁 + 1)) ≠ ∅) |
| 318 | | inidm 4227 |
. . . . . . . . . . . . . . . . . . 19
⊢
((ℤ≥‘(𝑁 + 1)) ∩
(ℤ≥‘(𝑁 + 1))) =
(ℤ≥‘(𝑁 + 1)) |
| 319 | 318 | neeq1i 3005 |
. . . . . . . . . . . . . . . . . 18
⊢
(((ℤ≥‘(𝑁 + 1)) ∩
(ℤ≥‘(𝑁 + 1))) ≠ ∅ ↔
(ℤ≥‘(𝑁 + 1)) ≠ ∅) |
| 320 | 317, 319 | sylibr 234 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
((ℤ≥‘(𝑁 + 1)) ∩
(ℤ≥‘(𝑁 + 1))) ≠ ∅) |
| 321 | | xpima2 6204 |
. . . . . . . . . . . . . . . . 17
⊢
(((ℤ≥‘(𝑁 + 1)) ∩
(ℤ≥‘(𝑁 + 1))) ≠ ∅ →
(((ℤ≥‘(𝑁 + 1)) × {0}) “
(ℤ≥‘(𝑁 + 1))) = {0}) |
| 322 | 320, 321 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(((ℤ≥‘(𝑁 + 1)) × {0}) “
(ℤ≥‘(𝑁 + 1))) = {0}) |
| 323 | 322 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
(((ℤ≥‘(𝑁 + 1)) × {0}) “
(ℤ≥‘(𝑁 + 1))) = {0}) |
| 324 | 312, 323 | uneq12d 4169 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 “
(ℤ≥‘(𝑁 + 1))) ∪
(((ℤ≥‘(𝑁 + 1)) × {0}) “
(ℤ≥‘(𝑁 + 1)))) = (∅ ∪
{0})) |
| 325 | | imaundir 6170 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∪
((ℤ≥‘(𝑁 + 1)) × {0})) “
(ℤ≥‘(𝑁 + 1))) = ((𝑤 “ (ℤ≥‘(𝑁 + 1))) ∪
(((ℤ≥‘(𝑁 + 1)) × {0}) “
(ℤ≥‘(𝑁 + 1)))) |
| 326 | | uncom 4158 |
. . . . . . . . . . . . . . 15
⊢ (∅
∪ {0}) = ({0} ∪ ∅) |
| 327 | | un0 4394 |
. . . . . . . . . . . . . . 15
⊢ ({0}
∪ ∅) = {0} |
| 328 | 326, 327 | eqtr2i 2766 |
. . . . . . . . . . . . . 14
⊢ {0} =
(∅ ∪ {0}) |
| 329 | 324, 325,
328 | 3eqtr4g 2802 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪
((ℤ≥‘(𝑁 + 1)) × {0})) “
(ℤ≥‘(𝑁 + 1))) = {0}) |
| 330 | 286, 310 | anim12ci 614 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) =
∅)) |
| 331 | | fnconstg 6796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ∈
V → ((ℤ≥‘(𝑁 + 1)) × {0}) Fn
(ℤ≥‘(𝑁 + 1))) |
| 332 | 128, 331 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((ℤ≥‘(𝑁 + 1)) × {0}) Fn
(ℤ≥‘(𝑁 + 1)) |
| 333 | | fvun1 7000 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 Fn (0...𝑁) ∧
((ℤ≥‘(𝑁 + 1)) × {0}) Fn
(ℤ≥‘(𝑁 + 1)) ∧ (((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ ∧ 𝑘 ∈ (0...𝑁))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘)) |
| 334 | 332, 333 | mp3an2 1451 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 Fn (0...𝑁) ∧ (((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ ∧ 𝑘 ∈ (0...𝑁))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘)) |
| 335 | 334 | anassrs 467 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘)) |
| 336 | 330, 335 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘)) |
| 337 | 336 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) = ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘)) |
| 338 | 337 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝑦↑𝑘)) = (((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘))) |
| 339 | 338 | sumeq2dv 15738 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘))) |
| 340 | 339 | mpteq2dv 5244 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘)))) |
| 341 | 277, 276,
309, 329, 340 | coeeq 26266 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (coeff‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) = (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) ×
{0}))) |
| 342 | 341 | reseq1d 5996 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
((coeff‘(𝑦 ∈
ℂ ↦ Σ𝑘
∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾
(0...𝑁))) |
| 343 | | res0 6001 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ↾ ∅) =
∅ |
| 344 | 285 | reseq2d 5997 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑤 ↾ ∅) = (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))))) |
| 345 | | res0 6001 |
. . . . . . . . . . . . . . 15
⊢
(((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ∅) =
∅ |
| 346 | 285 | reseq2d 5997 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ∅) =
(((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))))) |
| 347 | 345, 346 | eqtr3id 2791 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∅ =
(((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))))) |
| 348 | 343, 344,
347 | 3eqtr3a 2801 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) =
(((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))))) |
| 349 | | fss 6752 |
. . . . . . . . . . . . . . 15
⊢
((((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℚ)
→ ((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶ℚ) |
| 350 | 287, 289,
349 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢
((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶ℚ |
| 351 | | fresaunres1 6781 |
. . . . . . . . . . . . . 14
⊢ ((𝑤:(0...𝑁)⟶ℚ ∧
((ℤ≥‘(𝑁 + 1)) ×
{0}):(ℤ≥‘(𝑁 + 1))⟶ℚ ∧ (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) =
(((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾
(0...𝑁)) = 𝑤) |
| 352 | 350, 351 | mp3an2 1451 |
. . . . . . . . . . . . 13
⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) =
(((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩
(ℤ≥‘(𝑁 + 1))))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾
(0...𝑁)) = 𝑤) |
| 353 | 348, 352 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝜑) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾
(0...𝑁)) = 𝑤) |
| 354 | 353 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪
((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤) |
| 355 | 342, 354 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) →
((coeff‘(𝑦 ∈
ℂ ↦ Σ𝑘
∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤) |
| 356 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 →
(coeff‘(𝑦 ∈
ℂ ↦ Σ𝑘
∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) =
(coeff‘0𝑝)) |
| 357 | 356 | reseq1d 5996 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 →
((coeff‘(𝑦 ∈
ℂ ↦ Σ𝑘
∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝)
↾ (0...𝑁))) |
| 358 | | eqtr2 2761 |
. . . . . . . . . . . 12
⊢
((((coeff‘(𝑦
∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝)
↾ (0...𝑁))) →
𝑤 =
((coeff‘0𝑝) ↾ (0...𝑁))) |
| 359 | | coe0 26295 |
. . . . . . . . . . . . . 14
⊢
(coeff‘0𝑝) = (ℕ0 ×
{0}) |
| 360 | 359 | reseq1i 5993 |
. . . . . . . . . . . . 13
⊢
((coeff‘0𝑝) ↾ (0...𝑁)) = ((ℕ0 × {0})
↾ (0...𝑁)) |
| 361 | | elfznn0 13660 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℕ0) |
| 362 | 361 | ssriv 3987 |
. . . . . . . . . . . . . 14
⊢
(0...𝑁) ⊆
ℕ0 |
| 363 | | xpssres 6036 |
. . . . . . . . . . . . . 14
⊢
((0...𝑁) ⊆
ℕ0 → ((ℕ0 × {0}) ↾
(0...𝑁)) = ((0...𝑁) × {0})) |
| 364 | 362, 363 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
((ℕ0 × {0}) ↾ (0...𝑁)) = ((0...𝑁) × {0}) |
| 365 | 360, 364 | eqtri 2765 |
. . . . . . . . . . . 12
⊢
((coeff‘0𝑝) ↾ (0...𝑁)) = ((0...𝑁) × {0}) |
| 366 | 358, 365 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢
((((coeff‘(𝑦
∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝)
↾ (0...𝑁))) →
𝑤 = ((0...𝑁) × {0})) |
| 367 | 366 | ex 412 |
. . . . . . . . . 10
⊢
(((coeff‘(𝑦
∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 → (((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝)
↾ (0...𝑁)) →
𝑤 = ((0...𝑁) × {0}))) |
| 368 | 355, 357,
367 | syl2im 40 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 → 𝑤 = ((0...𝑁) × {0}))) |
| 369 | 368 | necon3d 2961 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ≠ ((0...𝑁) × {0}) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠
0𝑝)) |
| 370 | 369 | impr 454 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠
0𝑝) |
| 371 | | eldifsn 4786 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖
{0𝑝}) ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ (Poly‘ℚ) ∧ (𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠
0𝑝)) |
| 372 | 278, 370,
371 | sylanbrc 583 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖
{0𝑝})) |
| 373 | 372 | adantrr 717 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖
{0𝑝})) |
| 374 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → (𝑦↑𝑘) = (𝐴↑𝑘)) |
| 375 | 374 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → ((𝑤‘𝑘) · (𝑦↑𝑘)) = ((𝑤‘𝑘) · (𝐴↑𝑘))) |
| 376 | 375 | sumeq2sdv 15739 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘))) |
| 377 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) |
| 378 | | sumex 15724 |
. . . . . . . . . 10
⊢
Σ𝑘 ∈
(0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) ∈ V |
| 379 | 376, 377,
378 | fvmpt 7016 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘))) |
| 380 | 1, 379 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘))) |
| 381 | 380 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘))) |
| 382 | 107 | adantll 714 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ) |
| 383 | | aacllem.2 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ) |
| 384 | 383 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ) |
| 385 | 110, 384 | mulcld 11281 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ) |
| 386 | 385 | adantllr 719 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ) |
| 387 | 51, 382, 386 | fsummulc2 15820 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)) = Σ𝑛 ∈ (1...𝑁)((𝑤‘𝑘) · (𝐶 · 𝑋))) |
| 388 | | aacllem.4 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑𝑘) = Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)) |
| 389 | 388 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋))) |
| 390 | 389 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋))) |
| 391 | 382 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤‘𝑘) ∈ ℂ) |
| 392 | 110 | adantllr 719 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℂ) |
| 393 | | simpll 767 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → 𝜑) |
| 394 | 393, 383 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ) |
| 395 | 391, 392,
394 | mulassd 11284 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑤‘𝑘) · 𝐶) · 𝑋) = ((𝑤‘𝑘) · (𝐶 · 𝑋))) |
| 396 | 395 | sumeq2dv 15738 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)((𝑤‘𝑘) · (𝐶 · 𝑋))) |
| 397 | 387, 390,
396 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋)) |
| 398 | 397 | sumeq2dv 15738 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑘 ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋)) |
| 399 | 107 | ad2ant2lr 748 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (𝑤‘𝑘) ∈ ℂ) |
| 400 | 110 | anasss 466 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝐶 ∈ ℂ) |
| 401 | 400 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝐶 ∈ ℂ) |
| 402 | 399, 401 | mulcld 11281 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → ((𝑤‘𝑘) · 𝐶) ∈ ℂ) |
| 403 | 383 | ad2ant2rl 749 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝑋 ∈ ℂ) |
| 404 | 402, 403 | mulcld 11281 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (((𝑤‘𝑘) · 𝐶) · 𝑋) ∈ ℂ) |
| 405 | 43, 69, 404 | fsumcom 15811 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋)) |
| 406 | 398, 405 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋)) |
| 407 | 406 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋)) |
| 408 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛𝜑 |
| 409 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛 𝑤:(0...𝑁)⟶ℚ |
| 410 | | nfra1 3284 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 |
| 411 | 409, 410 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) |
| 412 | 408, 411 | nfan 1899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛(𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) |
| 413 | | rspa 3248 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) |
| 414 | 413 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋)) |
| 415 | 414 | adantll 714 |
. . . . . . . . . . . . . 14
⊢ (((𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋)) |
| 416 | 415 | adantll 714 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋)) |
| 417 | 383 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ) |
| 418 | 92, 417, 113 | fsummulc1 15821 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋)) |
| 419 | 418 | adantlrr 721 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋)) |
| 420 | 383 | mul02d 11459 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0) |
| 421 | 420 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0) |
| 422 | 416, 419,
421 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0) |
| 423 | 422 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → (𝑛 ∈ (1...𝑁) → Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0)) |
| 424 | 412, 423 | ralrimi 3257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0) |
| 425 | 424 | sumeq2d 15737 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)0) |
| 426 | 407, 425 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)0) |
| 427 | 22 | olci 867 |
. . . . . . . . 9
⊢
((1...𝑁) ⊆
(ℤ≥‘𝐵) ∨ (1...𝑁) ∈ Fin) |
| 428 | | sumz 15758 |
. . . . . . . . 9
⊢
(((1...𝑁) ⊆
(ℤ≥‘𝐵) ∨ (1...𝑁) ∈ Fin) → Σ𝑛 ∈ (1...𝑁)0 = 0) |
| 429 | 427, 428 | ax-mp 5 |
. . . . . . . 8
⊢
Σ𝑛 ∈
(1...𝑁)0 =
0 |
| 430 | 426, 429 | eqtrdi 2793 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = 0) |
| 431 | 381, 430 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0) |
| 432 | 431 | adantrlr 723 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0) |
| 433 | | fveq1 6905 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) → (𝑥‘𝐴) = ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴)) |
| 434 | 433 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) → ((𝑥‘𝐴) = 0 ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0)) |
| 435 | 434 | rspcev 3622 |
. . . . 5
⊢ (((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖
{0𝑝}) ∧ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0) → ∃𝑥 ∈ ((Poly‘ℚ) ∖
{0𝑝})(𝑥‘𝐴) = 0) |
| 436 | 373, 432,
435 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∃𝑥 ∈ ((Poly‘ℚ) ∖
{0𝑝})(𝑥‘𝐴) = 0) |
| 437 | 274, 436 | sylanr1 682 |
. . 3
⊢ ((𝜑 ∧ (𝑤 ∈ ((ℚ ↑m
(0...𝑁)) ∖
{((0...𝑁) × {0})})
∧ ∀𝑛 ∈
(1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∃𝑥 ∈ ((Poly‘ℚ) ∖
{0𝑝})(𝑥‘𝐴) = 0) |
| 438 | 271, 437 | rexlimddv 3161 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ ((Poly‘ℚ) ∖
{0𝑝})(𝑥‘𝐴) = 0) |
| 439 | | elqaa 26364 |
. 2
⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧
∃𝑥 ∈
((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0)) |
| 440 | 1, 438, 439 | sylanbrc 583 |
1
⊢ (𝜑 → 𝐴 ∈ 𝔸) |