Users' Mathboxes Mathbox for David A. Wheeler < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aacllem Structured version   Visualization version   GIF version

Theorem aacllem 42422
Description: Lemma for other theorems about 𝔸. (Contributed by Brendan Leahy, 3-Jan-2020.) (Revised by Alexander van der Vekens and David A. Wheeler, 25-Apr-2020.)
Hypotheses
Ref Expression
aacllem.0 (𝜑𝐴 ∈ ℂ)
aacllem.1 (𝜑𝑁 ∈ ℕ0)
aacllem.2 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
aacllem.3 ((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
aacllem.4 ((𝜑𝑘 ∈ (0...𝑁)) → (𝐴𝑘) = Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋))
Assertion
Ref Expression
aacllem (𝜑𝐴 ∈ 𝔸)
Distinct variable groups:   𝐴,𝑘,𝑛   𝑘,𝑁,𝑛   𝑘,𝑋   𝜑,𝑘,𝑛
Allowed substitution hints:   𝐶(𝑘,𝑛)   𝑋(𝑛)

Proof of Theorem aacllem
Dummy variables 𝑤 𝑥 𝑦 𝐵 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 aacllem.0 . 2 (𝜑𝐴 ∈ ℂ)
2 aacllem.1 . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
32nn0red 11107 . . . . . 6 (𝜑𝑁 ∈ ℝ)
43ltp1d 10704 . . . . 5 (𝜑𝑁 < (𝑁 + 1))
5 peano2nn0 11088 . . . . . . . 8 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
62, 5syl 17 . . . . . . 7 (𝜑 → (𝑁 + 1) ∈ ℕ0)
76nn0red 11107 . . . . . 6 (𝜑 → (𝑁 + 1) ∈ ℝ)
83, 7ltnled 9935 . . . . 5 (𝜑 → (𝑁 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑁))
94, 8mpbid 220 . . . 4 (𝜑 → ¬ (𝑁 + 1) ≤ 𝑁)
10 aacllem.3 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
11103expa 1256 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
12 eqid 2514 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) ↦ 𝐶) = (𝑛 ∈ (1...𝑁) ↦ 𝐶)
1311, 12fmptd 6176 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ)
14 qex 11542 . . . . . . . . . . 11 ℚ ∈ V
15 ovex 6454 . . . . . . . . . . 11 (1...𝑁) ∈ V
1614, 15elmap 7648 . . . . . . . . . 10 ((𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑𝑚 (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ)
1713, 16sylibr 222 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑𝑚 (1...𝑁)))
18 eqid 2514 . . . . . . . . 9 (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
1917, 18fmptd 6176 . . . . . . . 8 (𝜑 → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑𝑚 (1...𝑁)))
20 eqid 2514 . . . . . . . . . . . 12 (ℂflds ℚ) = (ℂflds ℚ)
2120qdrng 24998 . . . . . . . . . . 11 (ℂflds ℚ) ∈ DivRing
22 drngring 18484 . . . . . . . . . . 11 ((ℂflds ℚ) ∈ DivRing → (ℂflds ℚ) ∈ Ring)
2321, 22ax-mp 5 . . . . . . . . . 10 (ℂflds ℚ) ∈ Ring
24 fzfi 12501 . . . . . . . . . 10 (1...𝑁) ∈ Fin
25 eqid 2514 . . . . . . . . . . 11 ((ℂflds ℚ) freeLMod (1...𝑁)) = ((ℂflds ℚ) freeLMod (1...𝑁))
2625frlmlmod 19815 . . . . . . . . . 10 (((ℂflds ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod)
2723, 24, 26mp2an 703 . . . . . . . . 9 ((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod
28 fzfi 12501 . . . . . . . . 9 (0...𝑁) ∈ Fin
2920qrngbas 24997 . . . . . . . . . . . 12 ℚ = (Base‘(ℂflds ℚ))
3025, 29frlmfibas 19827 . . . . . . . . . . 11 (((ℂflds ℚ) ∈ DivRing ∧ (1...𝑁) ∈ Fin) → (ℚ ↑𝑚 (1...𝑁)) = (Base‘((ℂflds ℚ) freeLMod (1...𝑁))))
3121, 24, 30mp2an 703 . . . . . . . . . 10 (ℚ ↑𝑚 (1...𝑁)) = (Base‘((ℂflds ℚ) freeLMod (1...𝑁)))
3225frlmsca 19819 . . . . . . . . . . 11 (((ℂflds ℚ) ∈ DivRing ∧ (1...𝑁) ∈ Fin) → (ℂflds ℚ) = (Scalar‘((ℂflds ℚ) freeLMod (1...𝑁))))
3321, 24, 32mp2an 703 . . . . . . . . . 10 (ℂflds ℚ) = (Scalar‘((ℂflds ℚ) freeLMod (1...𝑁)))
34 eqid 2514 . . . . . . . . . 10 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁))) = ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))
3520qrng0 24999 . . . . . . . . . . . 12 0 = (0g‘(ℂflds ℚ))
3625, 35frlm0 19820 . . . . . . . . . . 11 (((ℂflds ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((1...𝑁) × {0}) = (0g‘((ℂflds ℚ) freeLMod (1...𝑁))))
3723, 24, 36mp2an 703 . . . . . . . . . 10 ((1...𝑁) × {0}) = (0g‘((ℂflds ℚ) freeLMod (1...𝑁)))
38 eqid 2514 . . . . . . . . . . . 12 ((ℂflds ℚ) freeLMod (0...𝑁)) = ((ℂflds ℚ) freeLMod (0...𝑁))
3938, 29frlmfibas 19827 . . . . . . . . . . 11 (((ℂflds ℚ) ∈ DivRing ∧ (0...𝑁) ∈ Fin) → (ℚ ↑𝑚 (0...𝑁)) = (Base‘((ℂflds ℚ) freeLMod (0...𝑁))))
4021, 28, 39mp2an 703 . . . . . . . . . 10 (ℚ ↑𝑚 (0...𝑁)) = (Base‘((ℂflds ℚ) freeLMod (0...𝑁)))
4131, 33, 34, 37, 35, 40islindf4 19899 . . . . . . . . 9 ((((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (0...𝑁) ∈ Fin ∧ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑𝑚 (1...𝑁))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂflds ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑𝑚 (0...𝑁))((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0}))))
4227, 28, 41mp3an12 1405 . . . . . . . 8 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑𝑚 (1...𝑁)) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂflds ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑𝑚 (0...𝑁))((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0}))))
4319, 42syl 17 . . . . . . 7 (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂflds ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑𝑚 (0...𝑁))((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0}))))
44 elmapi 7641 . . . . . . . . 9 (𝑤 ∈ (ℚ ↑𝑚 (0...𝑁)) → 𝑤:(0...𝑁)⟶ℚ)
45 fzfid 12502 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (0...𝑁) ∈ Fin)
46 fvex 5997 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑘) ∈ V
4746a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤𝑘) ∈ V)
4815mptex 6267 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V
4948a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V)
50 simpr 475 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤:(0...𝑁)⟶ℚ) → 𝑤:(0...𝑁)⟶ℚ)
5150feqmptd 6043 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤:(0...𝑁)⟶ℚ) → 𝑤 = (𝑘 ∈ (0...𝑁) ↦ (𝑤𝑘)))
52 eqidd 2515 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
5345, 47, 49, 51, 52offval2 6688 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘)( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶))))
54 fzfid 12502 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
55 ffvelrn 6149 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤𝑘) ∈ ℚ)
5655adantll 745 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤𝑘) ∈ ℚ)
5717adantlr 746 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑𝑚 (1...𝑁)))
58 cnfldmul 19477 . . . . . . . . . . . . . . . . . . . . . 22 · = (.r‘ℂfld)
5920, 58ressmulr 15713 . . . . . . . . . . . . . . . . . . . . 21 (ℚ ∈ V → · = (.r‘(ℂflds ℚ)))
6014, 59ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 · = (.r‘(ℂflds ℚ))
6125, 31, 29, 54, 56, 57, 34, 60frlmvscafval 19831 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤𝑘)( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (((1...𝑁) × {(𝑤𝑘)}) ∘𝑓 · (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
6246a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤𝑘) ∈ V)
6311adantllr 750 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
64 fconstmpt 4979 . . . . . . . . . . . . . . . . . . . . 21 ((1...𝑁) × {(𝑤𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤𝑘))
6564a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((1...𝑁) × {(𝑤𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤𝑘)))
66 eqidd 2515 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) = (𝑛 ∈ (1...𝑁) ↦ 𝐶))
6754, 62, 63, 65, 66offval2 6688 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (((1...𝑁) × {(𝑤𝑘)}) ∘𝑓 · (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)))
6861, 67eqtrd 2548 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤𝑘)( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)))
6968mpteq2dva 4570 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘)( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶))))
7053, 69eqtrd 2548 . . . . . . . . . . . . . . . 16 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶))))
7170oveq2d 6442 . . . . . . . . . . . . . . 15 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)))))
72 fzfid 12502 . . . . . . . . . . . . . . . 16 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (1...𝑁) ∈ Fin)
7323a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (ℂflds ℚ) ∈ Ring)
7456adantlr 746 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤𝑘) ∈ ℚ)
7511an32s 841 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℚ)
7675adantllr 750 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℚ)
77 qmulcl 11548 . . . . . . . . . . . . . . . . . . . 20 (((𝑤𝑘) ∈ ℚ ∧ 𝐶 ∈ ℚ) → ((𝑤𝑘) · 𝐶) ∈ ℚ)
7874, 76, 77syl2anc 690 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤𝑘) · 𝐶) ∈ ℚ)
7978an32s 841 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑤𝑘) · 𝐶) ∈ ℚ)
80 eqid 2514 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶))
8179, 80fmptd 6176 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
8214, 15elmap 7648 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)) ∈ (ℚ ↑𝑚 (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
8381, 82sylibr 222 . . . . . . . . . . . . . . . 16 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)) ∈ (ℚ ↑𝑚 (1...𝑁)))
84 eqid 2514 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)))
8515mptex 6267 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)) ∈ V
8685a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)) ∈ V)
87 snex 4734 . . . . . . . . . . . . . . . . . . 19 {0} ∈ V
8815, 87xpex 6736 . . . . . . . . . . . . . . . . . 18 ((1...𝑁) × {0}) ∈ V
8988a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((1...𝑁) × {0}) ∈ V)
9084, 45, 86, 89fsuppmptdm 8045 . . . . . . . . . . . . . . . 16 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶))) finSupp ((1...𝑁) × {0}))
9125, 31, 37, 72, 45, 73, 83, 90frlmgsum 19833 . . . . . . . . . . . . . . 15 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ ((ℂflds ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘) · 𝐶)))))
92 cnfldbas 19475 . . . . . . . . . . . . . . . . . 18 ℂ = (Base‘ℂfld)
93 cnfldadd 19476 . . . . . . . . . . . . . . . . . 18 + = (+g‘ℂfld)
94 cnfldex 19474 . . . . . . . . . . . . . . . . . . 19 fld ∈ V
9594a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℂfld ∈ V)
96 fzfid 12502 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (0...𝑁) ∈ Fin)
97 qsscn 11541 . . . . . . . . . . . . . . . . . . 19 ℚ ⊆ ℂ
9897a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℚ ⊆ ℂ)
99 eqid 2514 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘) · 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘) · 𝐶))
10078, 99fmptd 6176 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘) · 𝐶)):(0...𝑁)⟶ℚ)
101 0z 11129 . . . . . . . . . . . . . . . . . . . 20 0 ∈ ℤ
102 zq 11536 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℤ → 0 ∈ ℚ)
103101, 102ax-mp 5 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℚ
104103a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 0 ∈ ℚ)
105 addid2 9970 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℂ → (0 + 𝑥) = 𝑥)
106 addid1 9967 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℂ → (𝑥 + 0) = 𝑥)
107105, 106jca 552 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ → ((0 + 𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥))
108107adantl 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ ℂ) → ((0 + 𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥))
10992, 93, 20, 95, 96, 98, 100, 104, 108gsumress 16991 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂfld Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘) · 𝐶))) = ((ℂflds ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘) · 𝐶))))
110 simplr 787 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑤:(0...𝑁)⟶ℚ)
111 qcn 11544 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤𝑘) ∈ ℚ → (𝑤𝑘) ∈ ℂ)
11255, 111syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤𝑘) ∈ ℂ)
113110, 112sylan 486 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤𝑘) ∈ ℂ)
114 qcn 11544 . . . . . . . . . . . . . . . . . . . . . 22 (𝐶 ∈ ℚ → 𝐶 ∈ ℂ)
11511, 114syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℂ)
116115an32s 841 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℂ)
117116adantllr 750 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℂ)
118113, 117mulcld 9815 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤𝑘) · 𝐶) ∈ ℂ)
11996, 118gsumfsum 19536 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂfld Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))
120109, 119eqtr3d 2550 . . . . . . . . . . . . . . . 16 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((ℂflds ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))
121120mpteq2dva 4570 . . . . . . . . . . . . . . 15 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ ((ℂflds ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶)))
12271, 91, 1213eqtrd 2552 . . . . . . . . . . . . . 14 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶)))
123 qaddcl 11546 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ) → (𝑥 + 𝑦) ∈ ℚ)
124123adantl 480 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) ∈ ℚ)
12598, 124, 96, 78, 104fsumcllem 14179 . . . . . . . . . . . . . . . 16 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) ∈ ℚ)
126 eqid 2514 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))
127125, 126fmptd 6176 . . . . . . . . . . . . . . 15 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
12814, 15elmap 7648 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶)) ∈ (ℚ ↑𝑚 (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
129127, 128sylibr 222 . . . . . . . . . . . . . 14 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶)) ∈ (ℚ ↑𝑚 (1...𝑁)))
130122, 129eqeltrd 2592 . . . . . . . . . . . . 13 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) ∈ (ℚ ↑𝑚 (1...𝑁)))
131 elmapi 7641 . . . . . . . . . . . . 13 ((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) ∈ (ℚ ↑𝑚 (1...𝑁)) → (((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))):(1...𝑁)⟶ℚ)
132 ffn 5843 . . . . . . . . . . . . 13 ((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))):(1...𝑁)⟶ℚ → (((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁))
133130, 131, 1323syl 18 . . . . . . . . . . . 12 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁))
134 c0ex 9789 . . . . . . . . . . . . 13 0 ∈ V
135 fnconstg 5890 . . . . . . . . . . . . 13 (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
136134, 135ax-mp 5 . . . . . . . . . . . 12 ((1...𝑁) × {0}) Fn (1...𝑁)
137 nfcv 2655 . . . . . . . . . . . . . 14 𝑛((ℂflds ℚ) freeLMod (1...𝑁))
138 nfcv 2655 . . . . . . . . . . . . . 14 𝑛 Σg
139 nfcv 2655 . . . . . . . . . . . . . . 15 𝑛𝑤
140 nfcv 2655 . . . . . . . . . . . . . . 15 𝑛𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))
141 nfcv 2655 . . . . . . . . . . . . . . . 16 𝑛(0...𝑁)
142 nfmpt1 4573 . . . . . . . . . . . . . . . 16 𝑛(𝑛 ∈ (1...𝑁) ↦ 𝐶)
143141, 142nfmpt 4572 . . . . . . . . . . . . . . 15 𝑛(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
144139, 140, 143nfov 6452 . . . . . . . . . . . . . 14 𝑛(𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
145137, 138, 144nfov 6452 . . . . . . . . . . . . 13 𝑛(((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))
146 nfcv 2655 . . . . . . . . . . . . 13 𝑛((1...𝑁) × {0})
147145, 146eqfnfv2f 6107 . . . . . . . . . . . 12 (((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁) ∧ ((1...𝑁) × {0}) Fn (1...𝑁)) → ((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
148133, 136, 147sylancl 692 . . . . . . . . . . 11 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
149122fveq1d 5989 . . . . . . . . . . . . . 14 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))‘𝑛))
150 sumex 14135 . . . . . . . . . . . . . . 15 Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) ∈ V
151126fvmpt2 6084 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ∧ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) ∈ V) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))
152150, 151mpan2 702 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))
153149, 152sylan9eq 2568 . . . . . . . . . . . . 13 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))
154134fvconst2 6251 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
155154adantl 480 . . . . . . . . . . . . 13 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
156153, 155eqeq12d 2529 . . . . . . . . . . . 12 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
157156ralbidva 2872 . . . . . . . . . . 11 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (∀𝑛 ∈ (1...𝑁)((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
158148, 157bitrd 266 . . . . . . . . . 10 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
159158imbi1d 329 . . . . . . . . 9 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ (∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
16044, 159sylan2 489 . . . . . . . 8 ((𝜑𝑤 ∈ (ℚ ↑𝑚 (0...𝑁))) → (((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ (∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
161160ralbidva 2872 . . . . . . 7 (𝜑 → (∀𝑤 ∈ (ℚ ↑𝑚 (0...𝑁))((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤𝑓 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ ∀𝑤 ∈ (ℚ ↑𝑚 (0...𝑁))(∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
16243, 161bitrd 266 . . . . . 6 (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂflds ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑𝑚 (0...𝑁))(∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
163 drngnzr 18987 . . . . . . . . 9 ((ℂflds ℚ) ∈ DivRing → (ℂflds ℚ) ∈ NzRing)
16421, 163ax-mp 5 . . . . . . . 8 (ℂflds ℚ) ∈ NzRing
16533islindf3 19887 . . . . . . . 8 ((((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂflds ℚ) ∈ NzRing) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂflds ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁))))))
16627, 164, 165mp2an 703 . . . . . . 7 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂflds ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))))
16748, 18dmmpti 5821 . . . . . . . . 9 dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (0...𝑁)
168 f1eq2 5894 . . . . . . . . 9 (dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (0...𝑁) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ↔ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V))
169167, 168ax-mp 5 . . . . . . . 8 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ↔ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V)
170169anbi1i 726 . . . . . . 7 (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))))
171166, 170bitri 262 . . . . . 6 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂflds ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))))
172 con34b 304 . . . . . . . . 9 ((∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ (¬ 𝑤 = ((0...𝑁) × {0}) → ¬ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
173 df-nel 2687 . . . . . . . . . . 11 (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬ 𝑤 ∈ {((0...𝑁) × {0})})
174 velsn 4044 . . . . . . . . . . 11 (𝑤 ∈ {((0...𝑁) × {0})} ↔ 𝑤 = ((0...𝑁) × {0}))
175173, 174xchbinx 322 . . . . . . . . . 10 (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬ 𝑤 = ((0...𝑁) × {0}))
176175imbi1i 337 . . . . . . . . 9 ((𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0) ↔ (¬ 𝑤 = ((0...𝑁) × {0}) → ¬ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
177172, 176bitr4i 265 . . . . . . . 8 ((∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ (𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
178177ralbii 2867 . . . . . . 7 (∀𝑤 ∈ (ℚ ↑𝑚 (0...𝑁))(∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ∀𝑤 ∈ (ℚ ↑𝑚 (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
179 raldifb 3616 . . . . . . 7 (∀𝑤 ∈ (ℚ ↑𝑚 (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0) ↔ ∀𝑤 ∈ ((ℚ ↑𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})}) ¬ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)
180 ralnex 2879 . . . . . . 7 (∀𝑤 ∈ ((ℚ ↑𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})}) ¬ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 ↔ ¬ ∃𝑤 ∈ ((ℚ ↑𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)
181178, 179, 1803bitri 284 . . . . . 6 (∀𝑤 ∈ (ℚ ↑𝑚 (0...𝑁))(∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ¬ ∃𝑤 ∈ ((ℚ ↑𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)
182162, 171, 1813bitr3g 300 . . . . 5 (𝜑 → (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) ↔ ¬ ∃𝑤 ∈ ((ℚ ↑𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
183 eqid 2514 . . . . . . . . . . . . 13 (LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))) = (LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))
18431, 183lssmre 18691 . . . . . . . . . . . 12 (((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod → (LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑𝑚 (1...𝑁))))
18527, 184ax-mp 5 . . . . . . . . . . 11 (LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑𝑚 (1...𝑁)))
186185a1i 11 . . . . . . . . . 10 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → (LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑𝑚 (1...𝑁))))
187 eqid 2514 . . . . . . . . . . . 12 (LSpan‘((ℂflds ℚ) freeLMod (1...𝑁))) = (LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))
188 eqid 2514 . . . . . . . . . . . 12 (mrCls‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))) = (mrCls‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))))
189183, 187, 188mrclsp 18714 . . . . . . . . . . 11 (((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod → (LSpan‘((ℂflds ℚ) freeLMod (1...𝑁))) = (mrCls‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))))
19027, 189ax-mp 5 . . . . . . . . . 10 (LSpan‘((ℂflds ℚ) freeLMod (1...𝑁))) = (mrCls‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))))
191 eqid 2514 . . . . . . . . . 10 (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))) = (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))))
19233islvec 18829 . . . . . . . . . . . . 13 (((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LVec ↔ (((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂflds ℚ) ∈ DivRing))
19327, 21, 192mpbir2an 956 . . . . . . . . . . . 12 ((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LVec
194183, 190, 31lssacsex 18869 . . . . . . . . . . . . 13 (((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LVec → ((LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))) ∈ (ACS‘(ℚ ↑𝑚 (1...𝑁))) ∧ ∀𝑧 ∈ 𝒫 (ℚ ↑𝑚 (1...𝑁))∀𝑥 ∈ (ℚ ↑𝑚 (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦}))))
195194simprd 477 . . . . . . . . . . . 12 (((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LVec → ∀𝑧 ∈ 𝒫 (ℚ ↑𝑚 (1...𝑁))∀𝑥 ∈ (ℚ ↑𝑚 (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦})))
196193, 195ax-mp 5 . . . . . . . . . . 11 𝑧 ∈ 𝒫 (ℚ ↑𝑚 (1...𝑁))∀𝑥 ∈ (ℚ ↑𝑚 (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦}))
197196a1i 11 . . . . . . . . . 10 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → ∀𝑧 ∈ 𝒫 (ℚ ↑𝑚 (1...𝑁))∀𝑥 ∈ (ℚ ↑𝑚 (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦})))
198 frn 5851 . . . . . . . . . . . . 13 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑𝑚 (1...𝑁)) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ ↑𝑚 (1...𝑁)))
19919, 198syl 17 . . . . . . . . . . . 12 (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ ↑𝑚 (1...𝑁)))
200 dif0 3807 . . . . . . . . . . . 12 ((ℚ ↑𝑚 (1...𝑁)) ∖ ∅) = (ℚ ↑𝑚 (1...𝑁))
201199, 200syl6sseqr 3519 . . . . . . . . . . 11 (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((ℚ ↑𝑚 (1...𝑁)) ∖ ∅))
202201adantr 479 . . . . . . . . . 10 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((ℚ ↑𝑚 (1...𝑁)) ∖ ∅))
203 eqid 2514 . . . . . . . . . . . . . . 15 ((ℂflds ℚ) unitVec (1...𝑁)) = ((ℂflds ℚ) unitVec (1...𝑁))
204203, 25, 31uvcff 19852 . . . . . . . . . . . . . 14 (((ℂflds ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((ℂflds ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑𝑚 (1...𝑁)))
20523, 24, 204mp2an 703 . . . . . . . . . . . . 13 ((ℂflds ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑𝑚 (1...𝑁))
206 frn 5851 . . . . . . . . . . . . 13 (((ℂflds ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑𝑚 (1...𝑁)) → ran ((ℂflds ℚ) unitVec (1...𝑁)) ⊆ (ℚ ↑𝑚 (1...𝑁)))
207205, 206ax-mp 5 . . . . . . . . . . . 12 ran ((ℂflds ℚ) unitVec (1...𝑁)) ⊆ (ℚ ↑𝑚 (1...𝑁))
208207, 200sseqtr4i 3505 . . . . . . . . . . 11 ran ((ℂflds ℚ) unitVec (1...𝑁)) ⊆ ((ℚ ↑𝑚 (1...𝑁)) ∖ ∅)
209208a1i 11 . . . . . . . . . 10 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → ran ((ℂflds ℚ) unitVec (1...𝑁)) ⊆ ((ℚ ↑𝑚 (1...𝑁)) ∖ ∅))
210 un0 3822 . . . . . . . . . . . . . 14 (ran ((ℂflds ℚ) unitVec (1...𝑁)) ∪ ∅) = ran ((ℂflds ℚ) unitVec (1...𝑁))
211210fveq2i 5990 . . . . . . . . . . . . 13 ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran ((ℂflds ℚ) unitVec (1...𝑁)) ∪ ∅)) = ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘ran ((ℂflds ℚ) unitVec (1...𝑁)))
212 eqid 2514 . . . . . . . . . . . . . . . 16 (LBasis‘((ℂflds ℚ) freeLMod (1...𝑁))) = (LBasis‘((ℂflds ℚ) freeLMod (1...𝑁)))
21325, 203, 212frlmlbs 19858 . . . . . . . . . . . . . . 15 (((ℂflds ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ran ((ℂflds ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂflds ℚ) freeLMod (1...𝑁))))
21423, 24, 213mp2an 703 . . . . . . . . . . . . . 14 ran ((ℂflds ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂflds ℚ) freeLMod (1...𝑁)))
21531, 212, 187lbssp 18804 . . . . . . . . . . . . . 14 (ran ((ℂflds ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂflds ℚ) freeLMod (1...𝑁))) → ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘ran ((ℂflds ℚ) unitVec (1...𝑁))) = (ℚ ↑𝑚 (1...𝑁)))
216214, 215ax-mp 5 . . . . . . . . . . . . 13 ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘ran ((ℂflds ℚ) unitVec (1...𝑁))) = (ℚ ↑𝑚 (1...𝑁))
217211, 216eqtri 2536 . . . . . . . . . . . 12 ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran ((ℂflds ℚ) unitVec (1...𝑁)) ∪ ∅)) = (ℚ ↑𝑚 (1...𝑁))
218199, 217syl6sseqr 3519 . . . . . . . . . . 11 (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran ((ℂflds ℚ) unitVec (1...𝑁)) ∪ ∅)))
219218adantr 479 . . . . . . . . . 10 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran ((ℂflds ℚ) unitVec (1...𝑁)) ∪ ∅)))
220 un0 3822 . . . . . . . . . . 11 (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) = ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
22127, 164pm3.2i 469 . . . . . . . . . . . . . 14 (((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂflds ℚ) ∈ NzRing)
222187, 33lindsind2 19880 . . . . . . . . . . . . . 14 (((((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂflds ℚ) ∈ NzRing) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁))) ∧ 𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) → ¬ 𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
223221, 222mp3an1 1402 . . . . . . . . . . . . 13 ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁))) ∧ 𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) → ¬ 𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
224223ralrimiva 2853 . . . . . . . . . . . 12 (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁))) → ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
225190, 191ismri2 16007 . . . . . . . . . . . . . 14 (((LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑𝑚 (1...𝑁))) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ ↑𝑚 (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))) ↔ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))))
226185, 199, 225sylancr 693 . . . . . . . . . . . . 13 (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))) ↔ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))))
227226biimpar 500 . . . . . . . . . . . 12 ((𝜑 ∧ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))))
228224, 227sylan2 489 . . . . . . . . . . 11 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))))
229220, 228syl5eqel 2596 . . . . . . . . . 10 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))))
230 mptfi 8024 . . . . . . . . . . . . 13 ((0...𝑁) ∈ Fin → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin)
231 rnfi 8008 . . . . . . . . . . . . 13 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin)
23228, 230, 231mp2b 10 . . . . . . . . . . . 12 ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin
233232orci 403 . . . . . . . . . . 11 (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin ∨ ran ((ℂflds ℚ) unitVec (1...𝑁)) ∈ Fin)
234233a1i 11 . . . . . . . . . 10 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin ∨ ran ((ℂflds ℚ) unitVec (1...𝑁)) ∈ Fin))
235186, 190, 191, 197, 202, 209, 219, 229, 234mreexexd 16023 . . . . . . . . 9 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → ∃𝑣 ∈ 𝒫 ran ((ℂflds ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))))))
236235ex 448 . . . . . . . 8 (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁))) → ∃𝑣 ∈ 𝒫 ran ((ℂflds ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))))))
237 ovex 6454 . . . . . . . . . . . . 13 ((ℂflds ℚ) unitVec (1...𝑁)) ∈ V
238237rnex 6868 . . . . . . . . . . . 12 ran ((ℂflds ℚ) unitVec (1...𝑁)) ∈ V
239 elpwi 4020 . . . . . . . . . . . 12 (𝑣 ∈ 𝒫 ran ((ℂflds ℚ) unitVec (1...𝑁)) → 𝑣 ⊆ ran ((ℂflds ℚ) unitVec (1...𝑁)))
240 ssdomg 7763 . . . . . . . . . . . 12 (ran ((ℂflds ℚ) unitVec (1...𝑁)) ∈ V → (𝑣 ⊆ ran ((ℂflds ℚ) unitVec (1...𝑁)) → 𝑣 ≼ ran ((ℂflds ℚ) unitVec (1...𝑁))))
241238, 239, 240mpsyl 65 . . . . . . . . . . 11 (𝑣 ∈ 𝒫 ran ((ℂflds ℚ) unitVec (1...𝑁)) → 𝑣 ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)))
242 endomtr 7776 . . . . . . . . . . . . . 14 ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣𝑣 ≼ ran ((ℂflds ℚ) unitVec (1...𝑁))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)))
243242ancoms 467 . . . . . . . . . . . . 13 ((𝑣 ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)))
244 f1f1orn 5945 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1-onto→ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
245 ovex 6454 . . . . . . . . . . . . . . . . 17 (0...𝑁) ∈ V
246245f1oen 7738 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1-onto→ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) → (0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
247244, 246syl 17 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
248 endomtr 7776 . . . . . . . . . . . . . . . . 17 (((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁))) → (0...𝑁) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)))
249203uvcendim 19908 . . . . . . . . . . . . . . . . . . . 20 (((ℂflds ℚ) ∈ NzRing ∧ (1...𝑁) ∈ Fin) → (1...𝑁) ≈ ran ((ℂflds ℚ) unitVec (1...𝑁)))
250164, 24, 249mp2an 703 . . . . . . . . . . . . . . . . . . 19 (1...𝑁) ≈ ran ((ℂflds ℚ) unitVec (1...𝑁))
251250ensymi 7768 . . . . . . . . . . . . . . . . . 18 ran ((ℂflds ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)
252 domentr 7777 . . . . . . . . . . . . . . . . . . 19 (((0...𝑁) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)) ∧ ran ((ℂflds ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (0...𝑁) ≼ (1...𝑁))
253 hashdom 12894 . . . . . . . . . . . . . . . . . . . . 21 (((0...𝑁) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((#‘(0...𝑁)) ≤ (#‘(1...𝑁)) ↔ (0...𝑁) ≼ (1...𝑁)))
25428, 24, 253mp2an 703 . . . . . . . . . . . . . . . . . . . 20 ((#‘(0...𝑁)) ≤ (#‘(1...𝑁)) ↔ (0...𝑁) ≼ (1...𝑁))
255 hashfz0 12944 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ0 → (#‘(0...𝑁)) = (𝑁 + 1))
2562, 255syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (#‘(0...𝑁)) = (𝑁 + 1))
257 hashfz1 12861 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ0 → (#‘(1...𝑁)) = 𝑁)
2582, 257syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (#‘(1...𝑁)) = 𝑁)
259256, 258breq12d 4494 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((#‘(0...𝑁)) ≤ (#‘(1...𝑁)) ↔ (𝑁 + 1) ≤ 𝑁))
260254, 259syl5bbr 272 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((0...𝑁) ≼ (1...𝑁) ↔ (𝑁 + 1) ≤ 𝑁))
261252, 260syl5ib 232 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((0...𝑁) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)) ∧ ran ((ℂflds ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (𝑁 + 1) ≤ 𝑁))
262251, 261mpan2i 708 . . . . . . . . . . . . . . . . 17 (𝜑 → ((0...𝑁) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁))
263248, 262syl5 33 . . . . . . . . . . . . . . . 16 (𝜑 → (((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁))) → (𝑁 + 1) ≤ 𝑁))
264263expd 450 . . . . . . . . . . . . . . 15 (𝜑 → ((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁)))
265247, 264syl5 33 . . . . . . . . . . . . . 14 (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁)))
266265com23 83 . . . . . . . . . . . . 13 (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
267243, 266syl5 33 . . . . . . . . . . . 12 (𝜑 → ((𝑣 ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
268267expdimp 451 . . . . . . . . . . 11 ((𝜑𝑣 ≼ ran ((ℂflds ℚ) unitVec (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
269241, 268sylan2 489 . . . . . . . . . 10 ((𝜑𝑣 ∈ 𝒫 ran ((ℂflds ℚ) unitVec (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
270269adantrd 482 . . . . . . . . 9 ((𝜑𝑣 ∈ 𝒫 ran ((ℂflds ℚ) unitVec (1...𝑁))) → ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
271270rexlimdva 2917 . . . . . . . 8 (𝜑 → (∃𝑣 ∈ 𝒫 ran ((ℂflds ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
272236, 271syld 45 . . . . . . 7 (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
273272impd 445 . . . . . 6 (𝜑 → ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁))) ∧ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V) → (𝑁 + 1) ≤ 𝑁))
274273ancomsd 468 . . . . 5 (𝜑 → (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → (𝑁 + 1) ≤ 𝑁))
275182, 274sylbird 248 . . . 4 (𝜑 → (¬ ∃𝑤 ∈ ((ℚ ↑𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → (𝑁 + 1) ≤ 𝑁))
2769, 275mt3d 138 . . 3 (𝜑 → ∃𝑤 ∈ ((ℚ ↑𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)
277 eldifsn 4163 . . . . 5 (𝑤 ∈ ((ℚ ↑𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})}) ↔ (𝑤 ∈ (ℚ ↑𝑚 (0...𝑁)) ∧ 𝑤 ≠ ((0...𝑁) × {0})))
27844anim1i 589 . . . . 5 ((𝑤 ∈ (ℚ ↑𝑚 (0...𝑁)) ∧ 𝑤 ≠ ((0...𝑁) × {0})) → (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})))
279277, 278sylbi 205 . . . 4 (𝑤 ∈ ((ℚ ↑𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})}) → (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})))
28097a1i 11 . . . . . . . . 9 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ℚ ⊆ ℂ)
2812adantr 479 . . . . . . . . 9 ((𝜑𝑤:(0...𝑁)⟶ℚ) → 𝑁 ∈ ℕ0)
282280, 281, 56elplyd 23646 . . . . . . . 8 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ∈ (Poly‘ℚ))
283282adantrr 748 . . . . . . 7 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ∈ (Poly‘ℚ))
284 uzdisj 12150 . . . . . . . . . . . . . . . . . 18 ((0...((𝑁 + 1) − 1)) ∩ (ℤ‘(𝑁 + 1))) = ∅
2852nn0cnd 11108 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑁 ∈ ℂ)
286 pncan1 10205 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
287285, 286syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
288287oveq2d 6442 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁))
289288ineq1d 3678 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((0...((𝑁 + 1) − 1)) ∩ (ℤ‘(𝑁 + 1))) = ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))))
290284, 289syl5eqr 2562 . . . . . . . . . . . . . . . . 17 (𝜑 → ∅ = ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))))
291290eqcomd 2520 . . . . . . . . . . . . . . . 16 (𝜑 → ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅)
292134fconst 5888 . . . . . . . . . . . . . . . . . 18 ((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶{0}
293 snssi 4183 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℚ → {0} ⊆ ℚ)
294101, 102, 293mp2b 10 . . . . . . . . . . . . . . . . . . 19 {0} ⊆ ℚ
295294, 97sstri 3481 . . . . . . . . . . . . . . . . . 18 {0} ⊆ ℂ
296 fss 5854 . . . . . . . . . . . . . . . . . 18 ((((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℂ) → ((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶ℂ)
297292, 295, 296mp2an 703 . . . . . . . . . . . . . . . . 17 ((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶ℂ
298 fun 5864 . . . . . . . . . . . . . . . . 17 (((𝑤:(0...𝑁)⟶ℚ ∧ ((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶ℂ) ∧ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅) → (𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
299297, 298mpanl2 712 . . . . . . . . . . . . . . . 16 ((𝑤:(0...𝑁)⟶ℚ ∧ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅) → (𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
300291, 299sylan2 489 . . . . . . . . . . . . . . 15 ((𝑤:(0...𝑁)⟶ℚ ∧ 𝜑) → (𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
301300ancoms 467 . . . . . . . . . . . . . 14 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
302 nn0uz 11462 . . . . . . . . . . . . . . . . . 18 0 = (ℤ‘0)
3036, 302syl6eleq 2602 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 + 1) ∈ (ℤ‘0))
304 uzsplit 12149 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ (ℤ‘0) → (ℤ‘0) = ((0...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))))
305303, 304syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℤ‘0) = ((0...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))))
306302, 305syl5eq 2560 . . . . . . . . . . . . . . . . 17 (𝜑 → ℕ0 = ((0...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))))
307288uneq1d 3632 . . . . . . . . . . . . . . . . 17 (𝜑 → ((0...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))) = ((0...𝑁) ∪ (ℤ‘(𝑁 + 1))))
308306, 307eqtr2d 2549 . . . . . . . . . . . . . . . 16 (𝜑 → ((0...𝑁) ∪ (ℤ‘(𝑁 + 1))) = ℕ0)
309 ssequn1 3649 . . . . . . . . . . . . . . . . . 18 (ℚ ⊆ ℂ ↔ (ℚ ∪ ℂ) = ℂ)
31097, 309mpbi 218 . . . . . . . . . . . . . . . . 17 (ℚ ∪ ℂ) = ℂ
311310a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (ℚ ∪ ℂ) = ℂ)
312308, 311feq23d 5838 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ‘(𝑁 + 1)))⟶(ℚ ∪ ℂ) ↔ (𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):ℕ0⟶ℂ))
313312adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ‘(𝑁 + 1)))⟶(ℚ ∪ ℂ) ↔ (𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):ℕ0⟶ℂ))
314301, 313mpbid 220 . . . . . . . . . . . . 13 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):ℕ0⟶ℂ)
315 ffn 5843 . . . . . . . . . . . . . . . 16 (𝑤:(0...𝑁)⟶ℚ → 𝑤 Fn (0...𝑁))
316 fnimadisj 5810 . . . . . . . . . . . . . . . 16 ((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅) → (𝑤 “ (ℤ‘(𝑁 + 1))) = ∅)
317315, 291, 316syl2anr 493 . . . . . . . . . . . . . . 15 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑤 “ (ℤ‘(𝑁 + 1))) = ∅)
3182nn0zd 11220 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℤ)
319318peano2zd 11225 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 + 1) ∈ ℤ)
320 uzid 11442 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ ℤ → (𝑁 + 1) ∈ (ℤ‘(𝑁 + 1)))
321 ne0i 3783 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ (ℤ‘(𝑁 + 1)) → (ℤ‘(𝑁 + 1)) ≠ ∅)
322319, 320, 3213syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℤ‘(𝑁 + 1)) ≠ ∅)
323 inidm 3687 . . . . . . . . . . . . . . . . . . 19 ((ℤ‘(𝑁 + 1)) ∩ (ℤ‘(𝑁 + 1))) = (ℤ‘(𝑁 + 1))
324323neeq1i 2750 . . . . . . . . . . . . . . . . . 18 (((ℤ‘(𝑁 + 1)) ∩ (ℤ‘(𝑁 + 1))) ≠ ∅ ↔ (ℤ‘(𝑁 + 1)) ≠ ∅)
325322, 324sylibr 222 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℤ‘(𝑁 + 1)) ∩ (ℤ‘(𝑁 + 1))) ≠ ∅)
326 xpima2 5387 . . . . . . . . . . . . . . . . 17 (((ℤ‘(𝑁 + 1)) ∩ (ℤ‘(𝑁 + 1))) ≠ ∅ → (((ℤ‘(𝑁 + 1)) × {0}) “ (ℤ‘(𝑁 + 1))) = {0})
327325, 326syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (((ℤ‘(𝑁 + 1)) × {0}) “ (ℤ‘(𝑁 + 1))) = {0})
328327adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (((ℤ‘(𝑁 + 1)) × {0}) “ (ℤ‘(𝑁 + 1))) = {0})
329317, 328uneq12d 3634 . . . . . . . . . . . . . 14 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((𝑤 “ (ℤ‘(𝑁 + 1))) ∪ (((ℤ‘(𝑁 + 1)) × {0}) “ (ℤ‘(𝑁 + 1)))) = (∅ ∪ {0}))
330 imaundir 5355 . . . . . . . . . . . . . 14 ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})) “ (ℤ‘(𝑁 + 1))) = ((𝑤 “ (ℤ‘(𝑁 + 1))) ∪ (((ℤ‘(𝑁 + 1)) × {0}) “ (ℤ‘(𝑁 + 1))))
331 uncom 3623 . . . . . . . . . . . . . . 15 (∅ ∪ {0}) = ({0} ∪ ∅)
332 un0 3822 . . . . . . . . . . . . . . 15 ({0} ∪ ∅) = {0}
333331, 332eqtr2i 2537 . . . . . . . . . . . . . 14 {0} = (∅ ∪ {0})
334329, 330, 3333eqtr4g 2573 . . . . . . . . . . . . 13 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})) “ (ℤ‘(𝑁 + 1))) = {0})
335291, 315anim12ci 588 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅))
336 fnconstg 5890 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V → ((ℤ‘(𝑁 + 1)) × {0}) Fn (ℤ‘(𝑁 + 1)))
337134, 336ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((ℤ‘(𝑁 + 1)) × {0}) Fn (ℤ‘(𝑁 + 1))
338 fvun1 6063 . . . . . . . . . . . . . . . . . . . 20 ((𝑤 Fn (0...𝑁) ∧ ((ℤ‘(𝑁 + 1)) × {0}) Fn (ℤ‘(𝑁 + 1)) ∧ (((0...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅ ∧ 𝑘 ∈ (0...𝑁))) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤𝑘))
339337, 338mp3an2 1403 . . . . . . . . . . . . . . . . . . 19 ((𝑤 Fn (0...𝑁) ∧ (((0...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅ ∧ 𝑘 ∈ (0...𝑁))) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤𝑘))
340339anassrs 677 . . . . . . . . . . . . . . . . . 18 (((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤𝑘))
341335, 340sylan 486 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤𝑘))
342341eqcomd 2520 . . . . . . . . . . . . . . . 16 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤𝑘) = ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0}))‘𝑘))
343342oveq1d 6441 . . . . . . . . . . . . . . 15 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤𝑘) · (𝑦𝑘)) = (((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦𝑘)))
344343sumeq2dv 14150 . . . . . . . . . . . . . 14 ((𝜑𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)) = Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦𝑘)))
345344mpteq2dv 4571 . . . . . . . . . . . . 13 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦𝑘))))
346282, 281, 314, 334, 345coeeq 23671 . . . . . . . . . . . 12 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) = (𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})))
347346reseq1d 5207 . . . . . . . . . . 11 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)))
348 res0 5212 . . . . . . . . . . . . . 14 (𝑤 ↾ ∅) = ∅
349290reseq2d 5208 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ↾ ∅) = (𝑤 ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1)))))
350 res0 5212 . . . . . . . . . . . . . . 15 (((ℤ‘(𝑁 + 1)) × {0}) ↾ ∅) = ∅
351290reseq2d 5208 . . . . . . . . . . . . . . 15 (𝜑 → (((ℤ‘(𝑁 + 1)) × {0}) ↾ ∅) = (((ℤ‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1)))))
352350, 351syl5eqr 2562 . . . . . . . . . . . . . 14 (𝜑 → ∅ = (((ℤ‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1)))))
353348, 349, 3523eqtr3a 2572 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1)))) = (((ℤ‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1)))))
354 fss 5854 . . . . . . . . . . . . . . 15 ((((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℚ) → ((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶ℚ)
355292, 294, 354mp2an 703 . . . . . . . . . . . . . 14 ((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶ℚ
356 fresaunres1 5874 . . . . . . . . . . . . . 14 ((𝑤:(0...𝑁)⟶ℚ ∧ ((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶ℚ ∧ (𝑤 ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1)))) = (((ℤ‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))))) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
357355, 356mp3an2 1403 . . . . . . . . . . . . 13 ((𝑤:(0...𝑁)⟶ℚ ∧ (𝑤 ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1)))) = (((ℤ‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))))) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
358353, 357sylan2 489 . . . . . . . . . . . 12 ((𝑤:(0...𝑁)⟶ℚ ∧ 𝜑) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
359358ancoms 467 . . . . . . . . . . 11 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
360347, 359eqtrd 2548 . . . . . . . . . 10 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = 𝑤)
361 fveq2 5987 . . . . . . . . . . 11 ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) = 0𝑝 → (coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) = (coeff‘0𝑝))
362361reseq1d 5207 . . . . . . . . . 10 ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) = 0𝑝 → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁)))
363 eqtr2 2534 . . . . . . . . . . . 12 ((((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁))) → 𝑤 = ((coeff‘0𝑝) ↾ (0...𝑁)))
364 coe0 23700 . . . . . . . . . . . . . 14 (coeff‘0𝑝) = (ℕ0 × {0})
365364reseq1i 5204 . . . . . . . . . . . . 13 ((coeff‘0𝑝) ↾ (0...𝑁)) = ((ℕ0 × {0}) ↾ (0...𝑁))
366 elfznn0 12170 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℕ0)
367366ssriv 3476 . . . . . . . . . . . . . 14 (0...𝑁) ⊆ ℕ0
368 xpssres 5245 . . . . . . . . . . . . . 14 ((0...𝑁) ⊆ ℕ0 → ((ℕ0 × {0}) ↾ (0...𝑁)) = ((0...𝑁) × {0}))
369367, 368ax-mp 5 . . . . . . . . . . . . 13 ((ℕ0 × {0}) ↾ (0...𝑁)) = ((0...𝑁) × {0})
370365, 369eqtri 2536 . . . . . . . . . . . 12 ((coeff‘0𝑝) ↾ (0...𝑁)) = ((0...𝑁) × {0})
371363, 370syl6eq 2564 . . . . . . . . . . 11 ((((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁))) → 𝑤 = ((0...𝑁) × {0}))
372371ex 448 . . . . . . . . . 10 (((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = 𝑤 → (((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁)) → 𝑤 = ((0...𝑁) × {0})))
373360, 362, 372syl2im 39 . . . . . . . . 9 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) = 0𝑝𝑤 = ((0...𝑁) × {0})))
374373necon3d 2707 . . . . . . . 8 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑤 ≠ ((0...𝑁) × {0}) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ≠ 0𝑝))
375374impr 646 . . . . . . 7 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ≠ 0𝑝)
376 eldifsn 4163 . . . . . . 7 ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}) ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ∈ (Poly‘ℚ) ∧ (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ≠ 0𝑝))
377283, 375, 376sylanbrc 694 . . . . . 6 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}))
378377adantrr 748 . . . . 5 ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}))
379 oveq1 6433 . . . . . . . . . . . 12 (𝑦 = 𝐴 → (𝑦𝑘) = (𝐴𝑘))
380379oveq2d 6442 . . . . . . . . . . 11 (𝑦 = 𝐴 → ((𝑤𝑘) · (𝑦𝑘)) = ((𝑤𝑘) · (𝐴𝑘)))
381380sumeq2sdv 14151 . . . . . . . . . 10 (𝑦 = 𝐴 → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)))
382 eqid 2514 . . . . . . . . . 10 (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))
383 sumex 14135 . . . . . . . . . 10 Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)) ∈ V
384381, 382, 383fvmpt 6075 . . . . . . . . 9 (𝐴 ∈ ℂ → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)))
3851, 384syl 17 . . . . . . . 8 (𝜑 → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)))
386385adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)))
387112adantll 745 . . . . . . . . . . . . . 14 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤𝑘) ∈ ℂ)
388 aacllem.2 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
389388adantlr 746 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
390115, 389mulcld 9815 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ)
391390adantllr 750 . . . . . . . . . . . . . 14 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ)
39254, 387, 391fsummulc2 14227 . . . . . . . . . . . . 13 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)) = Σ𝑛 ∈ (1...𝑁)((𝑤𝑘) · (𝐶 · 𝑋)))
393 aacllem.4 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → (𝐴𝑘) = Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋))
394393oveq2d 6442 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝑁)) → ((𝑤𝑘) · (𝐴𝑘)) = ((𝑤𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)))
395394adantlr 746 . . . . . . . . . . . . 13 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤𝑘) · (𝐴𝑘)) = ((𝑤𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)))
396387adantr 479 . . . . . . . . . . . . . . 15 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤𝑘) ∈ ℂ)
397115adantllr 750 . . . . . . . . . . . . . . 15 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℂ)
398 simpll 785 . . . . . . . . . . . . . . . 16 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → 𝜑)
399398, 388sylan 486 . . . . . . . . . . . . . . 15 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
400396, 397, 399mulassd 9818 . . . . . . . . . . . . . 14 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑤𝑘) · 𝐶) · 𝑋) = ((𝑤𝑘) · (𝐶 · 𝑋)))
401400sumeq2dv 14150 . . . . . . . . . . . . 13 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)((𝑤𝑘) · (𝐶 · 𝑋)))
402392, 395, 4013eqtr4d 2558 . . . . . . . . . . . 12 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤𝑘) · (𝐴𝑘)) = Σ𝑛 ∈ (1...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋))
403402sumeq2dv 14150 . . . . . . . . . . 11 ((𝜑𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)) = Σ𝑘 ∈ (0...𝑁𝑛 ∈ (1...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋))
404112ad2ant2lr 779 . . . . . . . . . . . . . 14 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (𝑤𝑘) ∈ ℂ)
405115anasss 676 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝐶 ∈ ℂ)
406405adantlr 746 . . . . . . . . . . . . . 14 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝐶 ∈ ℂ)
407404, 406mulcld 9815 . . . . . . . . . . . . 13 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → ((𝑤𝑘) · 𝐶) ∈ ℂ)
408388ad2ant2rl 780 . . . . . . . . . . . . 13 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝑋 ∈ ℂ)
409407, 408mulcld 9815 . . . . . . . . . . . 12 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (((𝑤𝑘) · 𝐶) · 𝑋) ∈ ℂ)
41045, 72, 409fsumcom 14218 . . . . . . . . . . 11 ((𝜑𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁𝑛 ∈ (1...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋))
411403, 410eqtrd 2548 . . . . . . . . . 10 ((𝜑𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)) = Σ𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋))
412411adantrr 748 . . . . . . . . 9 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)) = Σ𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋))
413 nfv 1796 . . . . . . . . . . . 12 𝑛𝜑
414 nfv 1796 . . . . . . . . . . . . 13 𝑛 𝑤:(0...𝑁)⟶ℚ
415 nfra1 2829 . . . . . . . . . . . . 13 𝑛𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0
416414, 415nfan 2059 . . . . . . . . . . . 12 𝑛(𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)
417413, 416nfan 2059 . . . . . . . . . . 11 𝑛(𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
418 rspa 2818 . . . . . . . . . . . . . . . 16 ((∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)
419418oveq1d 6441 . . . . . . . . . . . . . . 15 ((∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
420419adantll 745 . . . . . . . . . . . . . 14 (((𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
421420adantll 745 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
422388adantlr 746 . . . . . . . . . . . . . . 15 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
42396, 422, 118fsummulc1 14228 . . . . . . . . . . . . . 14 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋))
424423adantlrr 752 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋))
425388mul02d 9985 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0)
426425adantlr 746 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0)
427421, 424, 4263eqtr3d 2556 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋) = 0)
428427ex 448 . . . . . . . . . . 11 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → (𝑛 ∈ (1...𝑁) → Σ𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋) = 0))
429417, 428ralrimi 2844 . . . . . . . . . 10 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋) = 0)
430429sumeq2d 14149 . . . . . . . . 9 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → Σ𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)0)
431412, 430eqtrd 2548 . . . . . . . 8 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)) = Σ𝑛 ∈ (1...𝑁)0)
43224olci 404 . . . . . . . . 9 ((1...𝑁) ⊆ (ℤ𝐵) ∨ (1...𝑁) ∈ Fin)
433 sumz 14169 . . . . . . . . 9 (((1...𝑁) ⊆ (ℤ𝐵) ∨ (1...𝑁) ∈ Fin) → Σ𝑛 ∈ (1...𝑁)0 = 0)
434432, 433ax-mp 5 . . . . . . . 8 Σ𝑛 ∈ (1...𝑁)0 = 0
435431, 434syl6eq 2564 . . . . . . 7 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)) = 0)
436386, 435eqtrd 2548 . . . . . 6 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))‘𝐴) = 0)
437436adantrlr 754 . . . . 5 ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))‘𝐴) = 0)
438 fveq1 5986 . . . . . . 7 (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) → (𝑥𝐴) = ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))‘𝐴))
439438eqeq1d 2516 . . . . . 6 (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) → ((𝑥𝐴) = 0 ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))‘𝐴) = 0))
440439rspcev 3186 . . . . 5 (((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}) ∧ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))‘𝐴) = 0) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥𝐴) = 0)
441378, 437, 440syl2anc 690 . . . 4 ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥𝐴) = 0)
442279, 441sylanr1 681 . . 3 ((𝜑 ∧ (𝑤 ∈ ((ℚ ↑𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})}) ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥𝐴) = 0)
443276, 442rexlimddv 2921 . 2 (𝜑 → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥𝐴) = 0)
444 elqaa 23768 . 2 (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧ ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥𝐴) = 0))
4451, 443, 444sylanbrc 694 1 (𝜑𝐴 ∈ 𝔸)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1938  wne 2684  wnel 2685  wral 2800  wrex 2801  Vcvv 3077  cdif 3441  cun 3442  cin 3443  wss 3444  c0 3777  𝒫 cpw 4011  {csn 4028   class class class wbr 4481  cmpt 4541   × cxp 4930  dom cdm 4932  ran crn 4933  cres 4934  cima 4935   Fn wfn 5684  wf 5685  1-1wf1 5686  1-1-ontowf1o 5688  cfv 5689  (class class class)co 6426  𝑓 cof 6669  𝑚 cmap 7620  cen 7714  cdom 7715  Fincfn 7717  cc 9689  0cc0 9691  1c1 9692   + caddc 9694   · cmul 9696   < clt 9829  cle 9830  cmin 10017  0cn0 11047  cz 11118  cuz 11427  cq 11530  ...cfz 12065  cexp 12590  #chash 12847  Σcsu 14133  Basecbs 15579  s cress 15580  .rcmulr 15653  Scalarcsca 15655   ·𝑠 cvsca 15656  0gc0g 15807   Σg cgsu 15808  Moorecmre 15957  mrClscmrc 15958  mrIndcmri 15959  ACScacs 15960  Ringcrg 18277  DivRingcdr 18477  LModclmod 18593  LSubSpclss 18657  LSpanclspn 18696  LBasisclbs 18799  LVecclvec 18827  NzRingcnzr 18982  fldccnfld 19471   freeLMod cfrlm 19812   unitVec cuvc 19843   LIndF clindf 19865  LIndSclinds 19866  0𝑝c0p 23117  Polycply 23628  coeffccoe 23630  𝔸caa 23757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6723  ax-inf2 8297  ax-cnex 9747  ax-resscn 9748  ax-1cn 9749  ax-icn 9750  ax-addcl 9751  ax-addrcl 9752  ax-mulcl 9753  ax-mulrcl 9754  ax-mulcom 9755  ax-addass 9756  ax-mulass 9757  ax-distr 9758  ax-i2m1 9759  ax-1ne0 9760  ax-1rid 9761  ax-rnegex 9762  ax-rrecex 9763  ax-cnre 9764  ax-pre-lttri 9765  ax-pre-lttrn 9766  ax-pre-ltadd 9767  ax-pre-mulgt0 9768  ax-pre-sup 9769  ax-addf 9770  ax-mulf 9771
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-iin 4356  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-se 4892  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-isom 5698  df-riota 6388  df-ov 6429  df-oprab 6430  df-mpt2 6431  df-of 6671  df-om 6834  df-1st 6934  df-2nd 6935  df-supp 7058  df-tpos 7114  df-wrecs 7169  df-recs 7231  df-rdg 7269  df-1o 7323  df-oadd 7327  df-er 7505  df-map 7622  df-pm 7623  df-ixp 7671  df-en 7718  df-dom 7719  df-sdom 7720  df-fin 7721  df-fsupp 8035  df-sup 8107  df-inf 8108  df-oi 8174  df-card 8524  df-pnf 9831  df-mnf 9832  df-xr 9833  df-ltxr 9834  df-le 9835  df-sub 10019  df-neg 10020  df-div 10434  df-nn 10776  df-2 10834  df-3 10835  df-4 10836  df-5 10837  df-6 10838  df-7 10839  df-8 10840  df-9 10841  df-n0 11048  df-z 11119  df-dec 11234  df-uz 11428  df-q 11531  df-rp 11575  df-fz 12066  df-fzo 12203  df-fl 12323  df-mod 12399  df-seq 12532  df-exp 12591  df-hash 12848  df-cj 13546  df-re 13547  df-im 13548  df-sqrt 13682  df-abs 13683  df-clim 13933  df-rlim 13934  df-sum 14134  df-struct 15581  df-ndx 15582  df-slot 15583  df-base 15584  df-sets 15585  df-ress 15586  df-plusg 15665  df-mulr 15666  df-starv 15667  df-sca 15668  df-vsca 15669  df-ip 15670  df-tset 15671  df-ple 15672  df-ds 15675  df-unif 15676  df-hom 15677  df-cco 15678  df-0g 15809  df-gsum 15810  df-prds 15815  df-pws 15817  df-mre 15961  df-mrc 15962  df-mri 15963  df-acs 15964  df-mgm 16957  df-sgrp 16999  df-mnd 17010  df-mhm 17050  df-submnd 17051  df-grp 17140  df-minusg 17141  df-sbg 17142  df-mulg 17256  df-subg 17306  df-ghm 17373  df-cntz 17465  df-cmn 17926  df-abl 17927  df-mgp 18220  df-ur 18232  df-ring 18279  df-cring 18280  df-oppr 18353  df-dvdsr 18371  df-unit 18372  df-invr 18402  df-dvr 18413  df-drng 18479  df-subrg 18508  df-lmod 18595  df-lss 18658  df-lsp 18697  df-lmhm 18747  df-lbs 18800  df-lvec 18828  df-sra 18897  df-rgmod 18898  df-nzr 18983  df-cnfld 19472  df-dsmm 19798  df-frlm 19813  df-uvc 19844  df-lindf 19867  df-linds 19868  df-0p 23118  df-ply 23632  df-coe 23634  df-dgr 23635  df-aa 23758
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator