| Step |
Hyp |
Ref |
Expression |
| 1 |
|
aacllem.0 |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
| 2 |
|
aacllem.1 |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
| 3 |
|
aacllem.2 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑋 ∈ ℂ ) |
| 4 |
|
aacllem.3 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝐶 ∈ ℚ ) |
| 5 |
|
aacllem.4 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ↑ 𝑘 ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( 𝐶 · 𝑋 ) ) |
| 6 |
2
|
nn0red |
⊢ ( 𝜑 → 𝑁 ∈ ℝ ) |
| 7 |
6
|
ltp1d |
⊢ ( 𝜑 → 𝑁 < ( 𝑁 + 1 ) ) |
| 8 |
|
peano2nn0 |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 ) |
| 9 |
2 8
|
syl |
⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 ) |
| 10 |
9
|
nn0red |
⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℝ ) |
| 11 |
6 10
|
ltnled |
⊢ ( 𝜑 → ( 𝑁 < ( 𝑁 + 1 ) ↔ ¬ ( 𝑁 + 1 ) ≤ 𝑁 ) ) |
| 12 |
7 11
|
mpbid |
⊢ ( 𝜑 → ¬ ( 𝑁 + 1 ) ≤ 𝑁 ) |
| 13 |
4
|
3expa |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝐶 ∈ ℚ ) |
| 14 |
13
|
fmpttd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) : ( 1 ... 𝑁 ) ⟶ ℚ ) |
| 15 |
|
qex |
⊢ ℚ ∈ V |
| 16 |
|
ovex |
⊢ ( 1 ... 𝑁 ) ∈ V |
| 17 |
15 16
|
elmap |
⊢ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ∈ ( ℚ ↑m ( 1 ... 𝑁 ) ) ↔ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) : ( 1 ... 𝑁 ) ⟶ ℚ ) |
| 18 |
14 17
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ∈ ( ℚ ↑m ( 1 ... 𝑁 ) ) ) |
| 19 |
18
|
fmpttd |
⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) ⟶ ( ℚ ↑m ( 1 ... 𝑁 ) ) ) |
| 20 |
|
eqid |
⊢ ( ℂfld ↾s ℚ ) = ( ℂfld ↾s ℚ ) |
| 21 |
20
|
qdrng |
⊢ ( ℂfld ↾s ℚ ) ∈ DivRing |
| 22 |
|
drngring |
⊢ ( ( ℂfld ↾s ℚ ) ∈ DivRing → ( ℂfld ↾s ℚ ) ∈ Ring ) |
| 23 |
21 22
|
ax-mp |
⊢ ( ℂfld ↾s ℚ ) ∈ Ring |
| 24 |
|
fzfi |
⊢ ( 1 ... 𝑁 ) ∈ Fin |
| 25 |
|
eqid |
⊢ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) = ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) |
| 26 |
25
|
frlmlmod |
⊢ ( ( ( ℂfld ↾s ℚ ) ∈ Ring ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ∈ LMod ) |
| 27 |
23 24 26
|
mp2an |
⊢ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ∈ LMod |
| 28 |
|
fzfi |
⊢ ( 0 ... 𝑁 ) ∈ Fin |
| 29 |
20
|
qrngbas |
⊢ ℚ = ( Base ‘ ( ℂfld ↾s ℚ ) ) |
| 30 |
25 29
|
frlmfibas |
⊢ ( ( ( ℂfld ↾s ℚ ) ∈ DivRing ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( ℚ ↑m ( 1 ... 𝑁 ) ) = ( Base ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) |
| 31 |
21 24 30
|
mp2an |
⊢ ( ℚ ↑m ( 1 ... 𝑁 ) ) = ( Base ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) |
| 32 |
25
|
frlmsca |
⊢ ( ( ( ℂfld ↾s ℚ ) ∈ DivRing ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( ℂfld ↾s ℚ ) = ( Scalar ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) |
| 33 |
21 24 32
|
mp2an |
⊢ ( ℂfld ↾s ℚ ) = ( Scalar ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) |
| 34 |
|
eqid |
⊢ ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) = ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) |
| 35 |
20
|
qrng0 |
⊢ 0 = ( 0g ‘ ( ℂfld ↾s ℚ ) ) |
| 36 |
25 35
|
frlm0 |
⊢ ( ( ( ℂfld ↾s ℚ ) ∈ Ring ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( ( 1 ... 𝑁 ) × { 0 } ) = ( 0g ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) |
| 37 |
23 24 36
|
mp2an |
⊢ ( ( 1 ... 𝑁 ) × { 0 } ) = ( 0g ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) |
| 38 |
|
eqid |
⊢ ( ( ℂfld ↾s ℚ ) freeLMod ( 0 ... 𝑁 ) ) = ( ( ℂfld ↾s ℚ ) freeLMod ( 0 ... 𝑁 ) ) |
| 39 |
38 29
|
frlmfibas |
⊢ ( ( ( ℂfld ↾s ℚ ) ∈ DivRing ∧ ( 0 ... 𝑁 ) ∈ Fin ) → ( ℚ ↑m ( 0 ... 𝑁 ) ) = ( Base ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 0 ... 𝑁 ) ) ) ) |
| 40 |
21 28 39
|
mp2an |
⊢ ( ℚ ↑m ( 0 ... 𝑁 ) ) = ( Base ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 0 ... 𝑁 ) ) ) |
| 41 |
31 33 34 37 35 40
|
islindf4 |
⊢ ( ( ( ( ℂ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 } ) ) ) ) |
| 42 |
27 28 41
|
mp3an12 |
⊢ ( ( 𝑘 ∈ ( 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 } ) ) ) ) |
| 43 |
19 42
|
syl |
⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 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 } ) ) ) ) |
| 44 |
|
elmapi |
⊢ ( 𝑤 ∈ ( ℚ ↑m ( 0 ... 𝑁 ) ) → 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) |
| 45 |
|
fzfid |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 0 ... 𝑁 ) ∈ Fin ) |
| 46 |
|
fvexd |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑤 ‘ 𝑘 ) ∈ V ) |
| 47 |
16
|
mptex |
⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ∈ V |
| 48 |
47
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ∈ V ) |
| 49 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) |
| 50 |
49
|
feqmptd |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → 𝑤 = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ) |
| 51 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) |
| 52 |
45 46 48 50 51
|
offval2 |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 𝑤 ∘f ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) ) |
| 53 |
|
fzfid |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 1 ... 𝑁 ) ∈ Fin ) |
| 54 |
|
ffvelcdm |
⊢ ( ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑤 ‘ 𝑘 ) ∈ ℚ ) |
| 55 |
54
|
adantll |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑤 ‘ 𝑘 ) ∈ ℚ ) |
| 56 |
18
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ∈ ( ℚ ↑m ( 1 ... 𝑁 ) ) ) |
| 57 |
|
cnfldmul |
⊢ · = ( .r ‘ ℂfld ) |
| 58 |
20 57
|
ressmulr |
⊢ ( ℚ ∈ V → · = ( .r ‘ ( ℂfld ↾s ℚ ) ) ) |
| 59 |
15 58
|
ax-mp |
⊢ · = ( .r ‘ ( ℂfld ↾s ℚ ) ) |
| 60 |
25 31 29 53 55 56 34 59
|
frlmvscafval |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑤 ‘ 𝑘 ) ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) = ( ( ( 1 ... 𝑁 ) × { ( 𝑤 ‘ 𝑘 ) } ) ∘f · ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) |
| 61 |
|
fvexd |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑤 ‘ 𝑘 ) ∈ V ) |
| 62 |
13
|
adantllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝐶 ∈ ℚ ) |
| 63 |
|
fconstmpt |
⊢ ( ( 1 ... 𝑁 ) × { ( 𝑤 ‘ 𝑘 ) } ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( 𝑤 ‘ 𝑘 ) ) |
| 64 |
63
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 1 ... 𝑁 ) × { ( 𝑤 ‘ 𝑘 ) } ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ) |
| 65 |
|
eqidd |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) |
| 66 |
53 61 62 64 65
|
offval2 |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 1 ... 𝑁 ) × { ( 𝑤 ‘ 𝑘 ) } ) ∘f · ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) |
| 67 |
60 66
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑤 ‘ 𝑘 ) ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) |
| 68 |
67
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) ) |
| 69 |
52 68
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 𝑤 ∘f ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) ) |
| 70 |
69
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) Σg ( 𝑤 ∘f ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) ) = ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) ) ) |
| 71 |
|
fzfid |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 1 ... 𝑁 ) ∈ Fin ) |
| 72 |
23
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ℂfld ↾s ℚ ) ∈ Ring ) |
| 73 |
55
|
adantlr |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑤 ‘ 𝑘 ) ∈ ℚ ) |
| 74 |
13
|
an32s |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐶 ∈ ℚ ) |
| 75 |
74
|
adantllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐶 ∈ ℚ ) |
| 76 |
|
qmulcl |
⊢ ( ( ( 𝑤 ‘ 𝑘 ) ∈ ℚ ∧ 𝐶 ∈ ℚ ) → ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ∈ ℚ ) |
| 77 |
73 75 76
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ∈ ℚ ) |
| 78 |
77
|
an32s |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ∈ ℚ ) |
| 79 |
78
|
fmpttd |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) : ( 1 ... 𝑁 ) ⟶ ℚ ) |
| 80 |
15 16
|
elmap |
⊢ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ∈ ( ℚ ↑m ( 1 ... 𝑁 ) ) ↔ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) : ( 1 ... 𝑁 ) ⟶ ℚ ) |
| 81 |
79 80
|
sylibr |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ∈ ( ℚ ↑m ( 1 ... 𝑁 ) ) ) |
| 82 |
|
eqid |
⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) |
| 83 |
16
|
mptex |
⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ∈ V |
| 84 |
83
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ∈ V ) |
| 85 |
|
snex |
⊢ { 0 } ∈ V |
| 86 |
16 85
|
xpex |
⊢ ( ( 1 ... 𝑁 ) × { 0 } ) ∈ V |
| 87 |
86
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( 1 ... 𝑁 ) × { 0 } ) ∈ V ) |
| 88 |
82 45 84 87
|
fsuppmptdm |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) finSupp ( ( 1 ... 𝑁 ) × { 0 } ) ) |
| 89 |
25 31 37 71 45 72 81 88
|
frlmgsum |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ℂfld ↾s ℚ ) Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) ) ) |
| 90 |
|
cnfldbas |
⊢ ℂ = ( Base ‘ ℂfld ) |
| 91 |
|
cnfldadd |
⊢ + = ( +g ‘ ℂfld ) |
| 92 |
|
cnfldex |
⊢ ℂfld ∈ V |
| 93 |
92
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ℂfld ∈ V ) |
| 94 |
|
fzfid |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 0 ... 𝑁 ) ∈ Fin ) |
| 95 |
|
qsscn |
⊢ ℚ ⊆ ℂ |
| 96 |
95
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ℚ ⊆ ℂ ) |
| 97 |
77
|
fmpttd |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) : ( 0 ... 𝑁 ) ⟶ ℚ ) |
| 98 |
|
0z |
⊢ 0 ∈ ℤ |
| 99 |
|
zq |
⊢ ( 0 ∈ ℤ → 0 ∈ ℚ ) |
| 100 |
98 99
|
ax-mp |
⊢ 0 ∈ ℚ |
| 101 |
100
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 0 ∈ ℚ ) |
| 102 |
|
addlid |
⊢ ( 𝑥 ∈ ℂ → ( 0 + 𝑥 ) = 𝑥 ) |
| 103 |
|
addrid |
⊢ ( 𝑥 ∈ ℂ → ( 𝑥 + 0 ) = 𝑥 ) |
| 104 |
102 103
|
jca |
⊢ ( 𝑥 ∈ ℂ → ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) |
| 105 |
104
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑥 ∈ ℂ ) → ( ( 0 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 0 ) = 𝑥 ) ) |
| 106 |
90 91 20 93 94 96 97 101 105
|
gsumress |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ℂfld Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) = ( ( ℂfld ↾s ℚ ) Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) ) |
| 107 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) |
| 108 |
|
qcn |
⊢ ( ( 𝑤 ‘ 𝑘 ) ∈ ℚ → ( 𝑤 ‘ 𝑘 ) ∈ ℂ ) |
| 109 |
54 108
|
syl |
⊢ ( ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑤 ‘ 𝑘 ) ∈ ℂ ) |
| 110 |
107 109
|
sylan |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑤 ‘ 𝑘 ) ∈ ℂ ) |
| 111 |
|
qcn |
⊢ ( 𝐶 ∈ ℚ → 𝐶 ∈ ℂ ) |
| 112 |
13 111
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝐶 ∈ ℂ ) |
| 113 |
112
|
an32s |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐶 ∈ ℂ ) |
| 114 |
113
|
adantllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐶 ∈ ℂ ) |
| 115 |
110 114
|
mulcld |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ∈ ℂ ) |
| 116 |
94 115
|
gsumfsum |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ℂfld Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) |
| 117 |
106 116
|
eqtr3d |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ℂfld ↾s ℚ ) Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) |
| 118 |
117
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ( ( ℂfld ↾s ℚ ) Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) |
| 119 |
70 89 118
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) Σg ( 𝑤 ∘f ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ) |
| 120 |
|
qaddcl |
⊢ ( ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) → ( 𝑥 + 𝑦 ) ∈ ℚ ) |
| 121 |
120
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝑥 + 𝑦 ) ∈ ℚ ) |
| 122 |
96 121 94 77 101
|
fsumcllem |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ∈ ℚ ) |
| 123 |
122
|
fmpttd |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) : ( 1 ... 𝑁 ) ⟶ ℚ ) |
| 124 |
15 16
|
elmap |
⊢ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ∈ ( ℚ ↑m ( 1 ... 𝑁 ) ) ↔ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) : ( 1 ... 𝑁 ) ⟶ ℚ ) |
| 125 |
123 124
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ∈ ( ℚ ↑m ( 1 ... 𝑁 ) ) ) |
| 126 |
119 125
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) Σg ( 𝑤 ∘f ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) ) ∈ ( ℚ ↑m ( 1 ... 𝑁 ) ) ) |
| 127 |
|
elmapi |
⊢ ( ( ( ( ℂ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 ... 𝑁 ) ⟶ ℚ ) |
| 128 |
|
ffn |
⊢ ( ( ( ( ℂ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 ... 𝑁 ) ) |
| 129 |
126 127 128
|
3syl |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) Σg ( 𝑤 ∘f ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) ) Fn ( 1 ... 𝑁 ) ) |
| 130 |
|
c0ex |
⊢ 0 ∈ V |
| 131 |
|
fnconstg |
⊢ ( 0 ∈ V → ( ( 1 ... 𝑁 ) × { 0 } ) Fn ( 1 ... 𝑁 ) ) |
| 132 |
130 131
|
ax-mp |
⊢ ( ( 1 ... 𝑁 ) × { 0 } ) Fn ( 1 ... 𝑁 ) |
| 133 |
|
nfcv |
⊢ Ⅎ 𝑛 ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) |
| 134 |
|
nfcv |
⊢ Ⅎ 𝑛 Σg |
| 135 |
|
nfcv |
⊢ Ⅎ 𝑛 𝑤 |
| 136 |
|
nfcv |
⊢ Ⅎ 𝑛 ∘f ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) |
| 137 |
|
nfcv |
⊢ Ⅎ 𝑛 ( 0 ... 𝑁 ) |
| 138 |
|
nfmpt1 |
⊢ Ⅎ 𝑛 ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) |
| 139 |
137 138
|
nfmpt |
⊢ Ⅎ 𝑛 ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) |
| 140 |
135 136 139
|
nfov |
⊢ Ⅎ 𝑛 ( 𝑤 ∘f ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) |
| 141 |
133 134 140
|
nfov |
⊢ Ⅎ 𝑛 ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) Σg ( 𝑤 ∘f ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) ) |
| 142 |
|
nfcv |
⊢ Ⅎ 𝑛 ( ( 1 ... 𝑁 ) × { 0 } ) |
| 143 |
141 142
|
eqfnfv2f |
⊢ ( ( ( ( ( ℂ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 } ) ‘ 𝑛 ) ) ) |
| 144 |
129 132 143
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 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 } ) ‘ 𝑛 ) ) ) |
| 145 |
119
|
fveq1d |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) Σg ( 𝑤 ∘f ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) ) ‘ 𝑛 ) = ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ‘ 𝑛 ) ) |
| 146 |
|
sumex |
⊢ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ∈ V |
| 147 |
|
eqid |
⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) |
| 148 |
147
|
fvmpt2 |
⊢ ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ∧ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ∈ V ) → ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ‘ 𝑛 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) |
| 149 |
146 148
|
mpan2 |
⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) ‘ 𝑛 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) |
| 150 |
145 149
|
sylan9eq |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) Σg ( 𝑤 ∘f ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) ) ‘ 𝑛 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ) |
| 151 |
130
|
fvconst2 |
⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( ( 1 ... 𝑁 ) × { 0 } ) ‘ 𝑛 ) = 0 ) |
| 152 |
151
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 ... 𝑁 ) × { 0 } ) ‘ 𝑛 ) = 0 ) |
| 153 |
150 152
|
eqeq12d |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) Σg ( 𝑤 ∘f ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) ) ‘ 𝑛 ) = ( ( ( 1 ... 𝑁 ) × { 0 } ) ‘ 𝑛 ) ↔ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) |
| 154 |
153
|
ralbidva |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) Σg ( 𝑤 ∘f ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) ) ‘ 𝑛 ) = ( ( ( 1 ... 𝑁 ) × { 0 } ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) |
| 155 |
144 154
|
bitrd |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) Σg ( 𝑤 ∘f ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) ) = ( ( 1 ... 𝑁 ) × { 0 } ) ↔ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) |
| 156 |
155
|
imbi1d |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) Σg ( 𝑤 ∘f ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) ) = ( ( 1 ... 𝑁 ) × { 0 } ) → 𝑤 = ( ( 0 ... 𝑁 ) × { 0 } ) ) ↔ ( ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 → 𝑤 = ( ( 0 ... 𝑁 ) × { 0 } ) ) ) ) |
| 157 |
44 156
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ℚ ↑m ( 0 ... 𝑁 ) ) ) → ( ( ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) Σg ( 𝑤 ∘f ( ·𝑠 ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) ) = ( ( 1 ... 𝑁 ) × { 0 } ) → 𝑤 = ( ( 0 ... 𝑁 ) × { 0 } ) ) ↔ ( ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 → 𝑤 = ( ( 0 ... 𝑁 ) × { 0 } ) ) ) ) |
| 158 |
157
|
ralbidva |
⊢ ( 𝜑 → ( ∀ 𝑤 ∈ ( ℚ ↑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 } ) ) ) ) |
| 159 |
43 158
|
bitrd |
⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) LIndF ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ↔ ∀ 𝑤 ∈ ( ℚ ↑m ( 0 ... 𝑁 ) ) ( ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 → 𝑤 = ( ( 0 ... 𝑁 ) × { 0 } ) ) ) ) |
| 160 |
|
drngnzr |
⊢ ( ( ℂfld ↾s ℚ ) ∈ DivRing → ( ℂfld ↾s ℚ ) ∈ NzRing ) |
| 161 |
21 160
|
ax-mp |
⊢ ( ℂfld ↾s ℚ ) ∈ NzRing |
| 162 |
33
|
islindf3 |
⊢ ( ( ( ( ℂ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 ... 𝑁 ) ) ) ) ) ) |
| 163 |
27 161 162
|
mp2an |
⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) LIndF ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ↔ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : dom ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) –1-1→ V ∧ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) ) |
| 164 |
|
eqid |
⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) |
| 165 |
47 164
|
dmmpti |
⊢ dom ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) = ( 0 ... 𝑁 ) |
| 166 |
|
f1eq2 |
⊢ ( dom ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) = ( 0 ... 𝑁 ) → ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : dom ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) –1-1→ V ↔ ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1→ V ) ) |
| 167 |
165 166
|
ax-mp |
⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : dom ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) –1-1→ V ↔ ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1→ V ) |
| 168 |
167
|
anbi1i |
⊢ ( ( ( 𝑘 ∈ ( 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 ... 𝑁 ) ) ) ) ) |
| 169 |
163 168
|
bitri |
⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) LIndF ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ↔ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1→ V ∧ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) ) |
| 170 |
|
con34b |
⊢ ( ( ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 → 𝑤 = ( ( 0 ... 𝑁 ) × { 0 } ) ) ↔ ( ¬ 𝑤 = ( ( 0 ... 𝑁 ) × { 0 } ) → ¬ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) |
| 171 |
|
df-nel |
⊢ ( 𝑤 ∉ { ( ( 0 ... 𝑁 ) × { 0 } ) } ↔ ¬ 𝑤 ∈ { ( ( 0 ... 𝑁 ) × { 0 } ) } ) |
| 172 |
|
velsn |
⊢ ( 𝑤 ∈ { ( ( 0 ... 𝑁 ) × { 0 } ) } ↔ 𝑤 = ( ( 0 ... 𝑁 ) × { 0 } ) ) |
| 173 |
171 172
|
xchbinx |
⊢ ( 𝑤 ∉ { ( ( 0 ... 𝑁 ) × { 0 } ) } ↔ ¬ 𝑤 = ( ( 0 ... 𝑁 ) × { 0 } ) ) |
| 174 |
173
|
imbi1i |
⊢ ( ( 𝑤 ∉ { ( ( 0 ... 𝑁 ) × { 0 } ) } → ¬ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ↔ ( ¬ 𝑤 = ( ( 0 ... 𝑁 ) × { 0 } ) → ¬ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) |
| 175 |
170 174
|
bitr4i |
⊢ ( ( ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 → 𝑤 = ( ( 0 ... 𝑁 ) × { 0 } ) ) ↔ ( 𝑤 ∉ { ( ( 0 ... 𝑁 ) × { 0 } ) } → ¬ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) |
| 176 |
175
|
ralbii |
⊢ ( ∀ 𝑤 ∈ ( ℚ ↑m ( 0 ... 𝑁 ) ) ( ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 → 𝑤 = ( ( 0 ... 𝑁 ) × { 0 } ) ) ↔ ∀ 𝑤 ∈ ( ℚ ↑m ( 0 ... 𝑁 ) ) ( 𝑤 ∉ { ( ( 0 ... 𝑁 ) × { 0 } ) } → ¬ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) |
| 177 |
|
raldifb |
⊢ ( ∀ 𝑤 ∈ ( ℚ ↑m ( 0 ... 𝑁 ) ) ( 𝑤 ∉ { ( ( 0 ... 𝑁 ) × { 0 } ) } → ¬ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ↔ ∀ 𝑤 ∈ ( ( ℚ ↑m ( 0 ... 𝑁 ) ) ∖ { ( ( 0 ... 𝑁 ) × { 0 } ) } ) ¬ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) |
| 178 |
|
ralnex |
⊢ ( ∀ 𝑤 ∈ ( ( ℚ ↑m ( 0 ... 𝑁 ) ) ∖ { ( ( 0 ... 𝑁 ) × { 0 } ) } ) ¬ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ↔ ¬ ∃ 𝑤 ∈ ( ( ℚ ↑m ( 0 ... 𝑁 ) ) ∖ { ( ( 0 ... 𝑁 ) × { 0 } ) } ) ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) |
| 179 |
176 177 178
|
3bitri |
⊢ ( ∀ 𝑤 ∈ ( ℚ ↑m ( 0 ... 𝑁 ) ) ( ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 → 𝑤 = ( ( 0 ... 𝑁 ) × { 0 } ) ) ↔ ¬ ∃ 𝑤 ∈ ( ( ℚ ↑m ( 0 ... 𝑁 ) ) ∖ { ( ( 0 ... 𝑁 ) × { 0 } ) } ) ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) |
| 180 |
159 169 179
|
3bitr3g |
⊢ ( 𝜑 → ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1→ V ∧ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) ↔ ¬ ∃ 𝑤 ∈ ( ( ℚ ↑m ( 0 ... 𝑁 ) ) ∖ { ( ( 0 ... 𝑁 ) × { 0 } ) } ) ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) |
| 181 |
|
eqid |
⊢ ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) = ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) |
| 182 |
31 181
|
lssmre |
⊢ ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ∈ LMod → ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ∈ ( Moore ‘ ( ℚ ↑m ( 1 ... 𝑁 ) ) ) ) |
| 183 |
27 182
|
ax-mp |
⊢ ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ∈ ( Moore ‘ ( ℚ ↑m ( 1 ... 𝑁 ) ) ) |
| 184 |
183
|
a1i |
⊢ ( ( 𝜑 ∧ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) → ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ∈ ( Moore ‘ ( ℚ ↑m ( 1 ... 𝑁 ) ) ) ) |
| 185 |
|
eqid |
⊢ ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) = ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) |
| 186 |
|
eqid |
⊢ ( mrCls ‘ ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) = ( mrCls ‘ ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) |
| 187 |
181 185 186
|
mrclsp |
⊢ ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ∈ LMod → ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) = ( mrCls ‘ ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) ) |
| 188 |
27 187
|
ax-mp |
⊢ ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) = ( mrCls ‘ ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) |
| 189 |
|
eqid |
⊢ ( mrInd ‘ ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) = ( mrInd ‘ ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) |
| 190 |
33
|
islvec |
⊢ ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ∈ LVec ↔ ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ∈ LMod ∧ ( ℂfld ↾s ℚ ) ∈ DivRing ) ) |
| 191 |
27 21 190
|
mpbir2an |
⊢ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ∈ LVec |
| 192 |
181 188 31
|
lssacsex |
⊢ ( ( ( ℂ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 ... 𝑁 ) ) ) ‘ ( 𝑧 ∪ { 𝑦 } ) ) ) ) |
| 193 |
192
|
simprd |
⊢ ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ∈ LVec → ∀ 𝑧 ∈ 𝒫 ( ℚ ↑m ( 1 ... 𝑁 ) ) ∀ 𝑥 ∈ ( ℚ ↑m ( 1 ... 𝑁 ) ) ∀ 𝑦 ∈ ( ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ ( 𝑧 ∪ { 𝑥 } ) ) ∖ ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ 𝑧 ) ) 𝑥 ∈ ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ ( 𝑧 ∪ { 𝑦 } ) ) ) |
| 194 |
191 193
|
ax-mp |
⊢ ∀ 𝑧 ∈ 𝒫 ( ℚ ↑m ( 1 ... 𝑁 ) ) ∀ 𝑥 ∈ ( ℚ ↑m ( 1 ... 𝑁 ) ) ∀ 𝑦 ∈ ( ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ ( 𝑧 ∪ { 𝑥 } ) ) ∖ ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ 𝑧 ) ) 𝑥 ∈ ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ ( 𝑧 ∪ { 𝑦 } ) ) |
| 195 |
194
|
a1i |
⊢ ( ( 𝜑 ∧ 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 ... 𝑁 ) ) ) ‘ ( 𝑧 ∪ { 𝑦 } ) ) ) |
| 196 |
19
|
frnd |
⊢ ( 𝜑 → ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ⊆ ( ℚ ↑m ( 1 ... 𝑁 ) ) ) |
| 197 |
|
dif0 |
⊢ ( ( ℚ ↑m ( 1 ... 𝑁 ) ) ∖ ∅ ) = ( ℚ ↑m ( 1 ... 𝑁 ) ) |
| 198 |
196 197
|
sseqtrrdi |
⊢ ( 𝜑 → ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ⊆ ( ( ℚ ↑m ( 1 ... 𝑁 ) ) ∖ ∅ ) ) |
| 199 |
198
|
adantr |
⊢ ( ( 𝜑 ∧ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) → ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ⊆ ( ( ℚ ↑m ( 1 ... 𝑁 ) ) ∖ ∅ ) ) |
| 200 |
|
eqid |
⊢ ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) = ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) |
| 201 |
200 25 31
|
uvcff |
⊢ ( ( ( ℂfld ↾s ℚ ) ∈ Ring ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) : ( 1 ... 𝑁 ) ⟶ ( ℚ ↑m ( 1 ... 𝑁 ) ) ) |
| 202 |
23 24 201
|
mp2an |
⊢ ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) : ( 1 ... 𝑁 ) ⟶ ( ℚ ↑m ( 1 ... 𝑁 ) ) |
| 203 |
|
frn |
⊢ ( ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) : ( 1 ... 𝑁 ) ⟶ ( ℚ ↑m ( 1 ... 𝑁 ) ) → ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ⊆ ( ℚ ↑m ( 1 ... 𝑁 ) ) ) |
| 204 |
202 203
|
ax-mp |
⊢ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ⊆ ( ℚ ↑m ( 1 ... 𝑁 ) ) |
| 205 |
204 197
|
sseqtrri |
⊢ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ⊆ ( ( ℚ ↑m ( 1 ... 𝑁 ) ) ∖ ∅ ) |
| 206 |
205
|
a1i |
⊢ ( ( 𝜑 ∧ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) → ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ⊆ ( ( ℚ ↑m ( 1 ... 𝑁 ) ) ∖ ∅ ) ) |
| 207 |
|
un0 |
⊢ ( ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∪ ∅ ) = ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) |
| 208 |
207
|
fveq2i |
⊢ ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ ( ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∪ ∅ ) ) = ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ) |
| 209 |
|
eqid |
⊢ ( LBasis ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) = ( LBasis ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) |
| 210 |
25 200 209
|
frlmlbs |
⊢ ( ( ( ℂfld ↾s ℚ ) ∈ Ring ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∈ ( LBasis ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) |
| 211 |
23 24 210
|
mp2an |
⊢ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∈ ( LBasis ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) |
| 212 |
31 209 185
|
lbssp |
⊢ ( ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∈ ( LBasis ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) → ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ) = ( ℚ ↑m ( 1 ... 𝑁 ) ) ) |
| 213 |
211 212
|
ax-mp |
⊢ ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ) = ( ℚ ↑m ( 1 ... 𝑁 ) ) |
| 214 |
208 213
|
eqtri |
⊢ ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ ( ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∪ ∅ ) ) = ( ℚ ↑m ( 1 ... 𝑁 ) ) |
| 215 |
196 214
|
sseqtrrdi |
⊢ ( 𝜑 → ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ⊆ ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ ( ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∪ ∅ ) ) ) |
| 216 |
215
|
adantr |
⊢ ( ( 𝜑 ∧ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) → ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ⊆ ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ ( ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∪ ∅ ) ) ) |
| 217 |
|
un0 |
⊢ ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∪ ∅ ) = ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) |
| 218 |
27 161
|
pm3.2i |
⊢ ( ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ∈ LMod ∧ ( ℂfld ↾s ℚ ) ∈ NzRing ) |
| 219 |
185 33
|
lindsind2 |
⊢ ( ( ( ( ( ℂ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 ... 𝑁 ) ↦ 𝐶 ) ) ∖ { 𝑥 } ) ) ) |
| 220 |
218 219
|
mp3an1 |
⊢ ( ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ∧ 𝑥 ∈ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) → ¬ 𝑥 ∈ ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∖ { 𝑥 } ) ) ) |
| 221 |
220
|
ralrimiva |
⊢ ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) → ∀ 𝑥 ∈ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ¬ 𝑥 ∈ ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∖ { 𝑥 } ) ) ) |
| 222 |
188 189
|
ismri2 |
⊢ ( ( ( 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 ... 𝑁 ) ↦ 𝐶 ) ) ∖ { 𝑥 } ) ) ) ) |
| 223 |
183 196 222
|
sylancr |
⊢ ( 𝜑 → ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( mrInd ‘ ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) ↔ ∀ 𝑥 ∈ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ¬ 𝑥 ∈ ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∖ { 𝑥 } ) ) ) ) |
| 224 |
223
|
biimpar |
⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ¬ 𝑥 ∈ ( ( LSpan ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ‘ ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∖ { 𝑥 } ) ) ) → ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( mrInd ‘ ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) ) |
| 225 |
221 224
|
sylan2 |
⊢ ( ( 𝜑 ∧ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) → ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( mrInd ‘ ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) ) |
| 226 |
217 225
|
eqeltrid |
⊢ ( ( 𝜑 ∧ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) → ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∪ ∅ ) ∈ ( mrInd ‘ ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) ) |
| 227 |
|
mptfi |
⊢ ( ( 0 ... 𝑁 ) ∈ Fin → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ Fin ) |
| 228 |
|
rnfi |
⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ Fin → ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ Fin ) |
| 229 |
28 227 228
|
mp2b |
⊢ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ Fin |
| 230 |
229
|
orci |
⊢ ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ Fin ∨ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∈ Fin ) |
| 231 |
230
|
a1i |
⊢ ( ( 𝜑 ∧ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) → ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ Fin ∨ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∈ Fin ) ) |
| 232 |
184 188 189 195 199 206 216 226 231
|
mreexexd |
⊢ ( ( 𝜑 ∧ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) → ∃ 𝑣 ∈ 𝒫 ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ≈ 𝑣 ∧ ( 𝑣 ∪ ∅ ) ∈ ( mrInd ‘ ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) ) ) |
| 233 |
232
|
ex |
⊢ ( 𝜑 → ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) → ∃ 𝑣 ∈ 𝒫 ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ≈ 𝑣 ∧ ( 𝑣 ∪ ∅ ) ∈ ( mrInd ‘ ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) ) ) ) |
| 234 |
|
ovex |
⊢ ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∈ V |
| 235 |
234
|
rnex |
⊢ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∈ V |
| 236 |
|
elpwi |
⊢ ( 𝑣 ∈ 𝒫 ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) → 𝑣 ⊆ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ) |
| 237 |
|
ssdomg |
⊢ ( ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∈ V → ( 𝑣 ⊆ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) → 𝑣 ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ) ) |
| 238 |
235 236 237
|
mpsyl |
⊢ ( 𝑣 ∈ 𝒫 ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) → 𝑣 ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ) |
| 239 |
|
endomtr |
⊢ ( ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ≈ 𝑣 ∧ 𝑣 ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ) → ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ) |
| 240 |
239
|
ancoms |
⊢ ( ( 𝑣 ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∧ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ≈ 𝑣 ) → ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ) |
| 241 |
|
f1f1orn |
⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1→ V → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1-onto→ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) |
| 242 |
|
ovex |
⊢ ( 0 ... 𝑁 ) ∈ V |
| 243 |
242
|
f1oen |
⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1-onto→ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) → ( 0 ... 𝑁 ) ≈ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) |
| 244 |
241 243
|
syl |
⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1→ V → ( 0 ... 𝑁 ) ≈ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ) |
| 245 |
|
endomtr |
⊢ ( ( ( 0 ... 𝑁 ) ≈ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∧ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ) → ( 0 ... 𝑁 ) ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ) |
| 246 |
200
|
uvcendim |
⊢ ( ( ( ℂfld ↾s ℚ ) ∈ NzRing ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( 1 ... 𝑁 ) ≈ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ) |
| 247 |
161 24 246
|
mp2an |
⊢ ( 1 ... 𝑁 ) ≈ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) |
| 248 |
247
|
ensymi |
⊢ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ≈ ( 1 ... 𝑁 ) |
| 249 |
|
domentr |
⊢ ( ( ( 0 ... 𝑁 ) ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∧ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ≈ ( 1 ... 𝑁 ) ) → ( 0 ... 𝑁 ) ≼ ( 1 ... 𝑁 ) ) |
| 250 |
|
hashdom |
⊢ ( ( ( 0 ... 𝑁 ) ∈ Fin ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( ( ♯ ‘ ( 0 ... 𝑁 ) ) ≤ ( ♯ ‘ ( 1 ... 𝑁 ) ) ↔ ( 0 ... 𝑁 ) ≼ ( 1 ... 𝑁 ) ) ) |
| 251 |
28 24 250
|
mp2an |
⊢ ( ( ♯ ‘ ( 0 ... 𝑁 ) ) ≤ ( ♯ ‘ ( 1 ... 𝑁 ) ) ↔ ( 0 ... 𝑁 ) ≼ ( 1 ... 𝑁 ) ) |
| 252 |
|
hashfz0 |
⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ... 𝑁 ) ) = ( 𝑁 + 1 ) ) |
| 253 |
2 252
|
syl |
⊢ ( 𝜑 → ( ♯ ‘ ( 0 ... 𝑁 ) ) = ( 𝑁 + 1 ) ) |
| 254 |
|
hashfz1 |
⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 ) |
| 255 |
2 254
|
syl |
⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 ) |
| 256 |
253 255
|
breq12d |
⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ... 𝑁 ) ) ≤ ( ♯ ‘ ( 1 ... 𝑁 ) ) ↔ ( 𝑁 + 1 ) ≤ 𝑁 ) ) |
| 257 |
251 256
|
bitr3id |
⊢ ( 𝜑 → ( ( 0 ... 𝑁 ) ≼ ( 1 ... 𝑁 ) ↔ ( 𝑁 + 1 ) ≤ 𝑁 ) ) |
| 258 |
249 257
|
imbitrid |
⊢ ( 𝜑 → ( ( ( 0 ... 𝑁 ) ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∧ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ≈ ( 1 ... 𝑁 ) ) → ( 𝑁 + 1 ) ≤ 𝑁 ) ) |
| 259 |
248 258
|
mpan2i |
⊢ ( 𝜑 → ( ( 0 ... 𝑁 ) ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) → ( 𝑁 + 1 ) ≤ 𝑁 ) ) |
| 260 |
245 259
|
syl5 |
⊢ ( 𝜑 → ( ( ( 0 ... 𝑁 ) ≈ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∧ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ) → ( 𝑁 + 1 ) ≤ 𝑁 ) ) |
| 261 |
260
|
expd |
⊢ ( 𝜑 → ( ( 0 ... 𝑁 ) ≈ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) → ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) → ( 𝑁 + 1 ) ≤ 𝑁 ) ) ) |
| 262 |
244 261
|
syl5 |
⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1→ V → ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) → ( 𝑁 + 1 ) ≤ 𝑁 ) ) ) |
| 263 |
262
|
com23 |
⊢ ( 𝜑 → ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) → ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1→ V → ( 𝑁 + 1 ) ≤ 𝑁 ) ) ) |
| 264 |
240 263
|
syl5 |
⊢ ( 𝜑 → ( ( 𝑣 ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ∧ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ≈ 𝑣 ) → ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1→ V → ( 𝑁 + 1 ) ≤ 𝑁 ) ) ) |
| 265 |
264
|
expdimp |
⊢ ( ( 𝜑 ∧ 𝑣 ≼ ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ) → ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ≈ 𝑣 → ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1→ V → ( 𝑁 + 1 ) ≤ 𝑁 ) ) ) |
| 266 |
238 265
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝒫 ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ) → ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ≈ 𝑣 → ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1→ V → ( 𝑁 + 1 ) ≤ 𝑁 ) ) ) |
| 267 |
266
|
adantrd |
⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝒫 ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ) → ( ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ≈ 𝑣 ∧ ( 𝑣 ∪ ∅ ) ∈ ( mrInd ‘ ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) ) → ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1→ V → ( 𝑁 + 1 ) ≤ 𝑁 ) ) ) |
| 268 |
267
|
rexlimdva |
⊢ ( 𝜑 → ( ∃ 𝑣 ∈ 𝒫 ran ( ( ℂfld ↾s ℚ ) unitVec ( 1 ... 𝑁 ) ) ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ≈ 𝑣 ∧ ( 𝑣 ∪ ∅ ) ∈ ( mrInd ‘ ( LSubSp ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) ) → ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1→ V → ( 𝑁 + 1 ) ≤ 𝑁 ) ) ) |
| 269 |
233 268
|
syld |
⊢ ( 𝜑 → ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) → ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1→ V → ( 𝑁 + 1 ) ≤ 𝑁 ) ) ) |
| 270 |
269
|
impd |
⊢ ( 𝜑 → ( ( ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1→ V ) → ( 𝑁 + 1 ) ≤ 𝑁 ) ) |
| 271 |
270
|
ancomsd |
⊢ ( 𝜑 → ( ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) : ( 0 ... 𝑁 ) –1-1→ V ∧ ran ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ 𝐶 ) ) ∈ ( LIndS ‘ ( ( ℂfld ↾s ℚ ) freeLMod ( 1 ... 𝑁 ) ) ) ) → ( 𝑁 + 1 ) ≤ 𝑁 ) ) |
| 272 |
180 271
|
sylbird |
⊢ ( 𝜑 → ( ¬ ∃ 𝑤 ∈ ( ( ℚ ↑m ( 0 ... 𝑁 ) ) ∖ { ( ( 0 ... 𝑁 ) × { 0 } ) } ) ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 → ( 𝑁 + 1 ) ≤ 𝑁 ) ) |
| 273 |
12 272
|
mt3d |
⊢ ( 𝜑 → ∃ 𝑤 ∈ ( ( ℚ ↑m ( 0 ... 𝑁 ) ) ∖ { ( ( 0 ... 𝑁 ) × { 0 } ) } ) ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) |
| 274 |
|
eldifsn |
⊢ ( 𝑤 ∈ ( ( ℚ ↑m ( 0 ... 𝑁 ) ) ∖ { ( ( 0 ... 𝑁 ) × { 0 } ) } ) ↔ ( 𝑤 ∈ ( ℚ ↑m ( 0 ... 𝑁 ) ) ∧ 𝑤 ≠ ( ( 0 ... 𝑁 ) × { 0 } ) ) ) |
| 275 |
44
|
anim1i |
⊢ ( ( 𝑤 ∈ ( ℚ ↑m ( 0 ... 𝑁 ) ) ∧ 𝑤 ≠ ( ( 0 ... 𝑁 ) × { 0 } ) ) → ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ 𝑤 ≠ ( ( 0 ... 𝑁 ) × { 0 } ) ) ) |
| 276 |
274 275
|
sylbi |
⊢ ( 𝑤 ∈ ( ( ℚ ↑m ( 0 ... 𝑁 ) ) ∖ { ( ( 0 ... 𝑁 ) × { 0 } ) } ) → ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ 𝑤 ≠ ( ( 0 ... 𝑁 ) × { 0 } ) ) ) |
| 277 |
95
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ℚ ⊆ ℂ ) |
| 278 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → 𝑁 ∈ ℕ0 ) |
| 279 |
277 278 55
|
elplyd |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ ℚ ) ) |
| 280 |
279
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ 𝑤 ≠ ( ( 0 ... 𝑁 ) × { 0 } ) ) ) → ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ ℚ ) ) |
| 281 |
|
uzdisj |
⊢ ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅ |
| 282 |
2
|
nn0cnd |
⊢ ( 𝜑 → 𝑁 ∈ ℂ ) |
| 283 |
|
pncan1 |
⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 ) |
| 284 |
282 283
|
syl |
⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 ) |
| 285 |
284
|
oveq2d |
⊢ ( 𝜑 → ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ... 𝑁 ) ) |
| 286 |
285
|
ineq1d |
⊢ ( 𝜑 → ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
| 287 |
281 286
|
eqtr3id |
⊢ ( 𝜑 → ∅ = ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
| 288 |
287
|
eqcomd |
⊢ ( 𝜑 → ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅ ) |
| 289 |
130
|
fconst |
⊢ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) : ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⟶ { 0 } |
| 290 |
|
snssi |
⊢ ( 0 ∈ ℚ → { 0 } ⊆ ℚ ) |
| 291 |
98 99 290
|
mp2b |
⊢ { 0 } ⊆ ℚ |
| 292 |
291 95
|
sstri |
⊢ { 0 } ⊆ ℂ |
| 293 |
|
fss |
⊢ ( ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) : ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⟶ { 0 } ∧ { 0 } ⊆ ℂ ) → ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) : ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⟶ ℂ ) |
| 294 |
289 292 293
|
mp2an |
⊢ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) : ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⟶ ℂ |
| 295 |
|
fun |
⊢ ( ( ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) : ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⟶ ℂ ) ∧ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅ ) → ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) : ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ⟶ ( ℚ ∪ ℂ ) ) |
| 296 |
294 295
|
mpanl2 |
⊢ ( ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅ ) → ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) : ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ⟶ ( ℚ ∪ ℂ ) ) |
| 297 |
288 296
|
sylan2 |
⊢ ( ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ 𝜑 ) → ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) : ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ⟶ ( ℚ ∪ ℂ ) ) |
| 298 |
297
|
ancoms |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) : ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ⟶ ( ℚ ∪ ℂ ) ) |
| 299 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
| 300 |
9 299
|
eleqtrdi |
⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 0 ) ) |
| 301 |
|
uzsplit |
⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 0 ) → ( ℤ≥ ‘ 0 ) = ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
| 302 |
300 301
|
syl |
⊢ ( 𝜑 → ( ℤ≥ ‘ 0 ) = ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
| 303 |
299 302
|
eqtrid |
⊢ ( 𝜑 → ℕ0 = ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
| 304 |
285
|
uneq1d |
⊢ ( 𝜑 → ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
| 305 |
303 304
|
eqtr2d |
⊢ ( 𝜑 → ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ℕ0 ) |
| 306 |
|
ssequn1 |
⊢ ( ℚ ⊆ ℂ ↔ ( ℚ ∪ ℂ ) = ℂ ) |
| 307 |
95 306
|
mpbi |
⊢ ( ℚ ∪ ℂ ) = ℂ |
| 308 |
307
|
a1i |
⊢ ( 𝜑 → ( ℚ ∪ ℂ ) = ℂ ) |
| 309 |
305 308
|
feq23d |
⊢ ( 𝜑 → ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) : ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ⟶ ( ℚ ∪ ℂ ) ↔ ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) : ℕ0 ⟶ ℂ ) ) |
| 310 |
309
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) : ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ⟶ ( ℚ ∪ ℂ ) ↔ ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) : ℕ0 ⟶ ℂ ) ) |
| 311 |
298 310
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) : ℕ0 ⟶ ℂ ) |
| 312 |
|
ffn |
⊢ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ → 𝑤 Fn ( 0 ... 𝑁 ) ) |
| 313 |
|
fnimadisj |
⊢ ( ( 𝑤 Fn ( 0 ... 𝑁 ) ∧ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅ ) → ( 𝑤 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅ ) |
| 314 |
312 288 313
|
syl2anr |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 𝑤 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅ ) |
| 315 |
2
|
nn0zd |
⊢ ( 𝜑 → 𝑁 ∈ ℤ ) |
| 316 |
315
|
peano2zd |
⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ ) |
| 317 |
|
uzid |
⊢ ( ( 𝑁 + 1 ) ∈ ℤ → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) |
| 318 |
|
ne0i |
⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ≠ ∅ ) |
| 319 |
316 317 318
|
3syl |
⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ≠ ∅ ) |
| 320 |
|
inidm |
⊢ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ( ℤ≥ ‘ ( 𝑁 + 1 ) ) |
| 321 |
320
|
neeq1i |
⊢ ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ≠ ∅ ↔ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ≠ ∅ ) |
| 322 |
319 321
|
sylibr |
⊢ ( 𝜑 → ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ≠ ∅ ) |
| 323 |
|
xpima2 |
⊢ ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ≠ ∅ → ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ) |
| 324 |
322 323
|
syl |
⊢ ( 𝜑 → ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ) |
| 325 |
324
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ) |
| 326 |
314 325
|
uneq12d |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( 𝑤 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∪ ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) = ( ∅ ∪ { 0 } ) ) |
| 327 |
|
imaundir |
⊢ ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ( ( 𝑤 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∪ ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) |
| 328 |
|
uncom |
⊢ ( ∅ ∪ { 0 } ) = ( { 0 } ∪ ∅ ) |
| 329 |
|
un0 |
⊢ ( { 0 } ∪ ∅ ) = { 0 } |
| 330 |
328 329
|
eqtr2i |
⊢ { 0 } = ( ∅ ∪ { 0 } ) |
| 331 |
326 327 330
|
3eqtr4g |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ) |
| 332 |
288 312
|
anim12ci |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 𝑤 Fn ( 0 ... 𝑁 ) ∧ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅ ) ) |
| 333 |
|
fnconstg |
⊢ ( 0 ∈ V → ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) Fn ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) |
| 334 |
130 333
|
ax-mp |
⊢ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) Fn ( ℤ≥ ‘ ( 𝑁 + 1 ) ) |
| 335 |
|
fvun1 |
⊢ ( ( 𝑤 Fn ( 0 ... 𝑁 ) ∧ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) Fn ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ∧ ( ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ) → ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) ‘ 𝑘 ) = ( 𝑤 ‘ 𝑘 ) ) |
| 336 |
334 335
|
mp3an2 |
⊢ ( ( 𝑤 Fn ( 0 ... 𝑁 ) ∧ ( ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ) → ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) ‘ 𝑘 ) = ( 𝑤 ‘ 𝑘 ) ) |
| 337 |
336
|
anassrs |
⊢ ( ( ( 𝑤 Fn ( 0 ... 𝑁 ) ∧ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) ‘ 𝑘 ) = ( 𝑤 ‘ 𝑘 ) ) |
| 338 |
332 337
|
sylan |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) ‘ 𝑘 ) = ( 𝑤 ‘ 𝑘 ) ) |
| 339 |
338
|
eqcomd |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑤 ‘ 𝑘 ) = ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) ‘ 𝑘 ) ) |
| 340 |
339
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) = ( ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) |
| 341 |
340
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) |
| 342 |
341
|
mpteq2dv |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) = ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ) |
| 343 |
279 278 311 331 342
|
coeeq |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( coeff ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ) = ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) ) |
| 344 |
343
|
reseq1d |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( coeff ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ↾ ( 0 ... 𝑁 ) ) = ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) ↾ ( 0 ... 𝑁 ) ) ) |
| 345 |
|
res0 |
⊢ ( 𝑤 ↾ ∅ ) = ∅ |
| 346 |
287
|
reseq2d |
⊢ ( 𝜑 → ( 𝑤 ↾ ∅ ) = ( 𝑤 ↾ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) |
| 347 |
|
res0 |
⊢ ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ↾ ∅ ) = ∅ |
| 348 |
287
|
reseq2d |
⊢ ( 𝜑 → ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ↾ ∅ ) = ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ↾ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) |
| 349 |
347 348
|
eqtr3id |
⊢ ( 𝜑 → ∅ = ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ↾ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) |
| 350 |
345 346 349
|
3eqtr3a |
⊢ ( 𝜑 → ( 𝑤 ↾ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) = ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ↾ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) |
| 351 |
|
fss |
⊢ ( ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) : ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⟶ { 0 } ∧ { 0 } ⊆ ℚ ) → ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) : ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⟶ ℚ ) |
| 352 |
289 291 351
|
mp2an |
⊢ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) : ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⟶ ℚ |
| 353 |
|
fresaunres1 |
⊢ ( ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) : ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⟶ ℚ ∧ ( 𝑤 ↾ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) = ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ↾ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) → ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) ↾ ( 0 ... 𝑁 ) ) = 𝑤 ) |
| 354 |
352 353
|
mp3an2 |
⊢ ( ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ( 𝑤 ↾ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) = ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ↾ ( ( 0 ... 𝑁 ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) ) → ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) ↾ ( 0 ... 𝑁 ) ) = 𝑤 ) |
| 355 |
350 354
|
sylan2 |
⊢ ( ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ 𝜑 ) → ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) ↾ ( 0 ... 𝑁 ) ) = 𝑤 ) |
| 356 |
355
|
ancoms |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( 𝑤 ∪ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) × { 0 } ) ) ↾ ( 0 ... 𝑁 ) ) = 𝑤 ) |
| 357 |
344 356
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( coeff ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ↾ ( 0 ... 𝑁 ) ) = 𝑤 ) |
| 358 |
|
fveq2 |
⊢ ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) = 0𝑝 → ( coeff ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ) = ( coeff ‘ 0𝑝 ) ) |
| 359 |
358
|
reseq1d |
⊢ ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) = 0𝑝 → ( ( coeff ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ↾ ( 0 ... 𝑁 ) ) = ( ( coeff ‘ 0𝑝 ) ↾ ( 0 ... 𝑁 ) ) ) |
| 360 |
|
eqtr2 |
⊢ ( ( ( ( coeff ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ↾ ( 0 ... 𝑁 ) ) = 𝑤 ∧ ( ( coeff ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ↾ ( 0 ... 𝑁 ) ) = ( ( coeff ‘ 0𝑝 ) ↾ ( 0 ... 𝑁 ) ) ) → 𝑤 = ( ( coeff ‘ 0𝑝 ) ↾ ( 0 ... 𝑁 ) ) ) |
| 361 |
|
coe0 |
⊢ ( coeff ‘ 0𝑝 ) = ( ℕ0 × { 0 } ) |
| 362 |
361
|
reseq1i |
⊢ ( ( coeff ‘ 0𝑝 ) ↾ ( 0 ... 𝑁 ) ) = ( ( ℕ0 × { 0 } ) ↾ ( 0 ... 𝑁 ) ) |
| 363 |
|
elfznn0 |
⊢ ( 𝑥 ∈ ( 0 ... 𝑁 ) → 𝑥 ∈ ℕ0 ) |
| 364 |
363
|
ssriv |
⊢ ( 0 ... 𝑁 ) ⊆ ℕ0 |
| 365 |
|
xpssres |
⊢ ( ( 0 ... 𝑁 ) ⊆ ℕ0 → ( ( ℕ0 × { 0 } ) ↾ ( 0 ... 𝑁 ) ) = ( ( 0 ... 𝑁 ) × { 0 } ) ) |
| 366 |
364 365
|
ax-mp |
⊢ ( ( ℕ0 × { 0 } ) ↾ ( 0 ... 𝑁 ) ) = ( ( 0 ... 𝑁 ) × { 0 } ) |
| 367 |
362 366
|
eqtri |
⊢ ( ( coeff ‘ 0𝑝 ) ↾ ( 0 ... 𝑁 ) ) = ( ( 0 ... 𝑁 ) × { 0 } ) |
| 368 |
360 367
|
eqtrdi |
⊢ ( ( ( ( coeff ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ↾ ( 0 ... 𝑁 ) ) = 𝑤 ∧ ( ( coeff ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ↾ ( 0 ... 𝑁 ) ) = ( ( coeff ‘ 0𝑝 ) ↾ ( 0 ... 𝑁 ) ) ) → 𝑤 = ( ( 0 ... 𝑁 ) × { 0 } ) ) |
| 369 |
368
|
ex |
⊢ ( ( ( coeff ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ↾ ( 0 ... 𝑁 ) ) = 𝑤 → ( ( ( coeff ‘ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ) ↾ ( 0 ... 𝑁 ) ) = ( ( coeff ‘ 0𝑝 ) ↾ ( 0 ... 𝑁 ) ) → 𝑤 = ( ( 0 ... 𝑁 ) × { 0 } ) ) ) |
| 370 |
357 359 369
|
syl2im |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) = 0𝑝 → 𝑤 = ( ( 0 ... 𝑁 ) × { 0 } ) ) ) |
| 371 |
370
|
necon3d |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → ( 𝑤 ≠ ( ( 0 ... 𝑁 ) × { 0 } ) → ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ≠ 0𝑝 ) ) |
| 372 |
371
|
impr |
⊢ ( ( 𝜑 ∧ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ 𝑤 ≠ ( ( 0 ... 𝑁 ) × { 0 } ) ) ) → ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ≠ 0𝑝 ) |
| 373 |
|
eldifsn |
⊢ ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ↔ ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ∈ ( Poly ‘ ℚ ) ∧ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ≠ 0𝑝 ) ) |
| 374 |
280 372 373
|
sylanbrc |
⊢ ( ( 𝜑 ∧ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ 𝑤 ≠ ( ( 0 ... 𝑁 ) × { 0 } ) ) ) → ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ) |
| 375 |
374
|
adantrr |
⊢ ( ( 𝜑 ∧ ( ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ 𝑤 ≠ ( ( 0 ... 𝑁 ) × { 0 } ) ) ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) → ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ) |
| 376 |
|
oveq1 |
⊢ ( 𝑦 = 𝐴 → ( 𝑦 ↑ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) ) |
| 377 |
376
|
oveq2d |
⊢ ( 𝑦 = 𝐴 → ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) = ( ( 𝑤 ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) |
| 378 |
377
|
sumeq2sdv |
⊢ ( 𝑦 = 𝐴 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) |
| 379 |
|
eqid |
⊢ ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) = ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) |
| 380 |
|
sumex |
⊢ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ V |
| 381 |
378 379 380
|
fvmpt |
⊢ ( 𝐴 ∈ ℂ → ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ‘ 𝐴 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) |
| 382 |
1 381
|
syl |
⊢ ( 𝜑 → ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ‘ 𝐴 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) |
| 383 |
382
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) → ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ‘ 𝐴 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) |
| 384 |
109
|
adantll |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑤 ‘ 𝑘 ) ∈ ℂ ) |
| 385 |
3
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑋 ∈ ℂ ) |
| 386 |
112 385
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 · 𝑋 ) ∈ ℂ ) |
| 387 |
386
|
adantllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 · 𝑋 ) ∈ ℂ ) |
| 388 |
53 384 387
|
fsummulc2 |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑤 ‘ 𝑘 ) · Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( 𝐶 · 𝑋 ) ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝐶 · 𝑋 ) ) ) |
| 389 |
5
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑤 ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) = ( ( 𝑤 ‘ 𝑘 ) · Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( 𝐶 · 𝑋 ) ) ) |
| 390 |
389
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑤 ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) = ( ( 𝑤 ‘ 𝑘 ) · Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( 𝐶 · 𝑋 ) ) ) |
| 391 |
384
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝑤 ‘ 𝑘 ) ∈ ℂ ) |
| 392 |
112
|
adantllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝐶 ∈ ℂ ) |
| 393 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝜑 ) |
| 394 |
393 3
|
sylan |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑋 ∈ ℂ ) |
| 395 |
391 392 394
|
mulassd |
⊢ ( ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) = ( ( 𝑤 ‘ 𝑘 ) · ( 𝐶 · 𝑋 ) ) ) |
| 396 |
395
|
sumeq2dv |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝐶 · 𝑋 ) ) ) |
| 397 |
388 390 396
|
3eqtr4d |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑤 ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) ) |
| 398 |
397
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) ) |
| 399 |
109
|
ad2ant2lr |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝑤 ‘ 𝑘 ) ∈ ℂ ) |
| 400 |
112
|
anasss |
⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → 𝐶 ∈ ℂ ) |
| 401 |
400
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → 𝐶 ∈ ℂ ) |
| 402 |
399 401
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) ∈ ℂ ) |
| 403 |
3
|
ad2ant2rl |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → 𝑋 ∈ ℂ ) |
| 404 |
402 403
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) ) → ( ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) ∈ ℂ ) |
| 405 |
45 71 404
|
fsumcom |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) ) |
| 406 |
398 405
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) ) |
| 407 |
406
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) ) |
| 408 |
|
nfv |
⊢ Ⅎ 𝑛 𝜑 |
| 409 |
|
nfv |
⊢ Ⅎ 𝑛 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ |
| 410 |
|
nfra1 |
⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 |
| 411 |
409 410
|
nfan |
⊢ Ⅎ 𝑛 ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) |
| 412 |
408 411
|
nfan |
⊢ Ⅎ 𝑛 ( 𝜑 ∧ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) |
| 413 |
|
rspa |
⊢ ( ( ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) |
| 414 |
413
|
oveq1d |
⊢ ( ( ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) = ( 0 · 𝑋 ) ) |
| 415 |
414
|
adantll |
⊢ ( ( ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) = ( 0 · 𝑋 ) ) |
| 416 |
415
|
adantll |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) = ( 0 · 𝑋 ) ) |
| 417 |
3
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑋 ∈ ℂ ) |
| 418 |
94 417 115
|
fsummulc1 |
⊢ ( ( ( 𝜑 ∧ 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) ) |
| 419 |
418
|
adantlrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) ) |
| 420 |
3
|
mul02d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 0 · 𝑋 ) = 0 ) |
| 421 |
420
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 0 · 𝑋 ) = 0 ) |
| 422 |
416 419 421
|
3eqtr3d |
⊢ ( ( ( 𝜑 ∧ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) = 0 ) |
| 423 |
422
|
ex |
⊢ ( ( 𝜑 ∧ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) → ( 𝑛 ∈ ( 1 ... 𝑁 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) = 0 ) ) |
| 424 |
412 423
|
ralrimi |
⊢ ( ( 𝜑 ∧ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) = 0 ) |
| 425 |
424
|
sumeq2d |
⊢ ( ( 𝜑 ∧ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) → Σ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) · 𝑋 ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) 0 ) |
| 426 |
407 425
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) = Σ 𝑛 ∈ ( 1 ... 𝑁 ) 0 ) |
| 427 |
24
|
olci |
⊢ ( ( 1 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 𝐵 ) ∨ ( 1 ... 𝑁 ) ∈ Fin ) |
| 428 |
|
sumz |
⊢ ( ( ( 1 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 𝐵 ) ∨ ( 1 ... 𝑁 ) ∈ Fin ) → Σ 𝑛 ∈ ( 1 ... 𝑁 ) 0 = 0 ) |
| 429 |
427 428
|
ax-mp |
⊢ Σ 𝑛 ∈ ( 1 ... 𝑁 ) 0 = 0 |
| 430 |
426 429
|
eqtrdi |
⊢ ( ( 𝜑 ∧ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) = 0 ) |
| 431 |
383 430
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) → ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ‘ 𝐴 ) = 0 ) |
| 432 |
431
|
adantrlr |
⊢ ( ( 𝜑 ∧ ( ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ 𝑤 ≠ ( ( 0 ... 𝑁 ) × { 0 } ) ) ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) → ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ‘ 𝐴 ) = 0 ) |
| 433 |
|
fveq1 |
⊢ ( 𝑥 = ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) → ( 𝑥 ‘ 𝐴 ) = ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ‘ 𝐴 ) ) |
| 434 |
433
|
eqeq1d |
⊢ ( 𝑥 = ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) → ( ( 𝑥 ‘ 𝐴 ) = 0 ↔ ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ‘ 𝐴 ) = 0 ) ) |
| 435 |
434
|
rspcev |
⊢ ( ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ‘ 𝐴 ) = 0 ) → ∃ 𝑥 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑥 ‘ 𝐴 ) = 0 ) |
| 436 |
375 432 435
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( ( 𝑤 : ( 0 ... 𝑁 ) ⟶ ℚ ∧ 𝑤 ≠ ( ( 0 ... 𝑁 ) × { 0 } ) ) ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) → ∃ 𝑥 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑥 ‘ 𝐴 ) = 0 ) |
| 437 |
276 436
|
sylanr1 |
⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( ( ℚ ↑m ( 0 ... 𝑁 ) ) ∖ { ( ( 0 ... 𝑁 ) × { 0 } ) } ) ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑤 ‘ 𝑘 ) · 𝐶 ) = 0 ) ) → ∃ 𝑥 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑥 ‘ 𝐴 ) = 0 ) |
| 438 |
273 437
|
rexlimddv |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑥 ‘ 𝐴 ) = 0 ) |
| 439 |
|
elqaa |
⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑥 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑥 ‘ 𝐴 ) = 0 ) ) |
| 440 |
1 438 439
|
sylanbrc |
⊢ ( 𝜑 → 𝐴 ∈ 𝔸 ) |