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 47238
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 12474 . . . . . 6 (𝜑𝑁 ∈ ℝ)
43ltp1d 12085 . . . . 5 (𝜑𝑁 < (𝑁 + 1))
5 peano2nn0 12453 . . . . . . . 8 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
62, 5syl 17 . . . . . . 7 (𝜑 → (𝑁 + 1) ∈ ℕ0)
76nn0red 12474 . . . . . 6 (𝜑 → (𝑁 + 1) ∈ ℝ)
83, 7ltnled 11302 . . . . 5 (𝜑 → (𝑁 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑁))
94, 8mpbid 231 . . . 4 (𝜑 → ¬ (𝑁 + 1) ≤ 𝑁)
10 aacllem.3 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
11103expa 1118 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
1211fmpttd 7063 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ)
13 qex 12886 . . . . . . . . . . 11 ℚ ∈ V
14 ovex 7390 . . . . . . . . . . 11 (1...𝑁) ∈ V
1513, 14elmap 8809 . . . . . . . . . 10 ((𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ)
1612, 15sylibr 233 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m (1...𝑁)))
1716fmpttd 7063 . . . . . . . 8 (𝜑 → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑m (1...𝑁)))
18 eqid 2736 . . . . . . . . . . . 12 (ℂflds ℚ) = (ℂflds ℚ)
1918qdrng 26968 . . . . . . . . . . 11 (ℂflds ℚ) ∈ DivRing
20 drngring 20192 . . . . . . . . . . 11 ((ℂflds ℚ) ∈ DivRing → (ℂflds ℚ) ∈ Ring)
2119, 20ax-mp 5 . . . . . . . . . 10 (ℂflds ℚ) ∈ Ring
22 fzfi 13877 . . . . . . . . . 10 (1...𝑁) ∈ Fin
23 eqid 2736 . . . . . . . . . . 11 ((ℂflds ℚ) freeLMod (1...𝑁)) = ((ℂflds ℚ) freeLMod (1...𝑁))
2423frlmlmod 21155 . . . . . . . . . 10 (((ℂflds ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod)
2521, 22, 24mp2an 690 . . . . . . . . 9 ((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod
26 fzfi 13877 . . . . . . . . 9 (0...𝑁) ∈ Fin
2718qrngbas 26967 . . . . . . . . . . . 12 ℚ = (Base‘(ℂflds ℚ))
2823, 27frlmfibas 21168 . . . . . . . . . . 11 (((ℂflds ℚ) ∈ DivRing ∧ (1...𝑁) ∈ Fin) → (ℚ ↑m (1...𝑁)) = (Base‘((ℂflds ℚ) freeLMod (1...𝑁))))
2919, 22, 28mp2an 690 . . . . . . . . . 10 (ℚ ↑m (1...𝑁)) = (Base‘((ℂflds ℚ) freeLMod (1...𝑁)))
3023frlmsca 21159 . . . . . . . . . . 11 (((ℂflds ℚ) ∈ DivRing ∧ (1...𝑁) ∈ Fin) → (ℂflds ℚ) = (Scalar‘((ℂflds ℚ) freeLMod (1...𝑁))))
3119, 22, 30mp2an 690 . . . . . . . . . 10 (ℂflds ℚ) = (Scalar‘((ℂflds ℚ) freeLMod (1...𝑁)))
32 eqid 2736 . . . . . . . . . 10 ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁))) = ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))
3318qrng0 26969 . . . . . . . . . . . 12 0 = (0g‘(ℂflds ℚ))
3423, 33frlm0 21160 . . . . . . . . . . 11 (((ℂflds ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((1...𝑁) × {0}) = (0g‘((ℂflds ℚ) freeLMod (1...𝑁))))
3521, 22, 34mp2an 690 . . . . . . . . . 10 ((1...𝑁) × {0}) = (0g‘((ℂflds ℚ) freeLMod (1...𝑁)))
36 eqid 2736 . . . . . . . . . . . 12 ((ℂflds ℚ) freeLMod (0...𝑁)) = ((ℂflds ℚ) freeLMod (0...𝑁))
3736, 27frlmfibas 21168 . . . . . . . . . . 11 (((ℂflds ℚ) ∈ DivRing ∧ (0...𝑁) ∈ Fin) → (ℚ ↑m (0...𝑁)) = (Base‘((ℂflds ℚ) freeLMod (0...𝑁))))
3819, 26, 37mp2an 690 . . . . . . . . . 10 (ℚ ↑m (0...𝑁)) = (Base‘((ℂflds ℚ) freeLMod (0...𝑁)))
3929, 31, 32, 35, 33, 38islindf4 21244 . . . . . . . . 9 ((((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (0...𝑁) ∈ Fin ∧ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑m (1...𝑁))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂflds ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0}))))
4025, 26, 39mp3an12 1451 . . . . . . . 8 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑m (1...𝑁)) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂflds ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0}))))
4117, 40syl 17 . . . . . . 7 (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂflds ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0}))))
42 elmapi 8787 . . . . . . . . 9 (𝑤 ∈ (ℚ ↑m (0...𝑁)) → 𝑤:(0...𝑁)⟶ℚ)
43 fzfid 13878 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (0...𝑁) ∈ Fin)
44 fvexd 6857 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤𝑘) ∈ V)
4514mptex 7173 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V
4645a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V)
47 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤:(0...𝑁)⟶ℚ) → 𝑤:(0...𝑁)⟶ℚ)
4847feqmptd 6910 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤:(0...𝑁)⟶ℚ) → 𝑤 = (𝑘 ∈ (0...𝑁) ↦ (𝑤𝑘)))
49 eqidd 2737 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
5043, 44, 46, 48, 49offval2 7637 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘)( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶))))
51 fzfid 13878 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
52 ffvelcdm 7032 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤𝑘) ∈ ℚ)
5352adantll 712 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤𝑘) ∈ ℚ)
5416adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m (1...𝑁)))
55 cnfldmul 20802 . . . . . . . . . . . . . . . . . . . . . 22 · = (.r‘ℂfld)
5618, 55ressmulr 17188 . . . . . . . . . . . . . . . . . . . . 21 (ℚ ∈ V → · = (.r‘(ℂflds ℚ)))
5713, 56ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 · = (.r‘(ℂflds ℚ))
5823, 29, 27, 51, 53, 54, 32, 57frlmvscafval 21172 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤𝑘)( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (((1...𝑁) × {(𝑤𝑘)}) ∘f · (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
59 fvexd 6857 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤𝑘) ∈ V)
6011adantllr 717 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
61 fconstmpt 5694 . . . . . . . . . . . . . . . . . . . . 21 ((1...𝑁) × {(𝑤𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤𝑘))
6261a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((1...𝑁) × {(𝑤𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤𝑘)))
63 eqidd 2737 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) = (𝑛 ∈ (1...𝑁) ↦ 𝐶))
6451, 59, 60, 62, 63offval2 7637 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (((1...𝑁) × {(𝑤𝑘)}) ∘f · (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)))
6558, 64eqtrd 2776 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤𝑘)( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)))
6665mpteq2dva 5205 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘)( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶))))
6750, 66eqtrd 2776 . . . . . . . . . . . . . . . 16 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶))))
6867oveq2d 7373 . . . . . . . . . . . . . . 15 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)))))
69 fzfid 13878 . . . . . . . . . . . . . . . 16 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (1...𝑁) ∈ Fin)
7021a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (ℂflds ℚ) ∈ Ring)
7153adantlr 713 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤𝑘) ∈ ℚ)
7211an32s 650 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℚ)
7372adantllr 717 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℚ)
74 qmulcl 12892 . . . . . . . . . . . . . . . . . . . 20 (((𝑤𝑘) ∈ ℚ ∧ 𝐶 ∈ ℚ) → ((𝑤𝑘) · 𝐶) ∈ ℚ)
7571, 73, 74syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤𝑘) · 𝐶) ∈ ℚ)
7675an32s 650 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑤𝑘) · 𝐶) ∈ ℚ)
7776fmpttd 7063 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
7813, 14elmap 8809 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
7977, 78sylibr 233 . . . . . . . . . . . . . . . 16 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)))
80 eqid 2736 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)))
8114mptex 7173 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)) ∈ V
8281a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)) ∈ V)
83 snex 5388 . . . . . . . . . . . . . . . . . . 19 {0} ∈ V
8414, 83xpex 7687 . . . . . . . . . . . . . . . . . 18 ((1...𝑁) × {0}) ∈ V
8584a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((1...𝑁) × {0}) ∈ V)
8680, 43, 82, 85fsuppmptdm 9316 . . . . . . . . . . . . . . . 16 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶))) finSupp ((1...𝑁) × {0}))
8723, 29, 35, 69, 43, 70, 79, 86frlmgsum 21178 . . . . . . . . . . . . . . 15 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ ((ℂflds ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘) · 𝐶)))))
88 cnfldbas 20800 . . . . . . . . . . . . . . . . . 18 ℂ = (Base‘ℂfld)
89 cnfldadd 20801 . . . . . . . . . . . . . . . . . 18 + = (+g‘ℂfld)
90 cnfldex 20799 . . . . . . . . . . . . . . . . . . 19 fld ∈ V
9190a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℂfld ∈ V)
92 fzfid 13878 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (0...𝑁) ∈ Fin)
93 qsscn 12885 . . . . . . . . . . . . . . . . . . 19 ℚ ⊆ ℂ
9493a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℚ ⊆ ℂ)
9575fmpttd 7063 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘) · 𝐶)):(0...𝑁)⟶ℚ)
96 0z 12510 . . . . . . . . . . . . . . . . . . . 20 0 ∈ ℤ
97 zq 12879 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℤ → 0 ∈ ℚ)
9896, 97ax-mp 5 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℚ
9998a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 0 ∈ ℚ)
100 addid2 11338 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℂ → (0 + 𝑥) = 𝑥)
101 addid1 11335 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℂ → (𝑥 + 0) = 𝑥)
102100, 101jca 512 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ → ((0 + 𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥))
103102adantl 482 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ ℂ) → ((0 + 𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥))
10488, 89, 18, 91, 92, 94, 95, 99, 103gsumress 18537 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂfld Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘) · 𝐶))) = ((ℂflds ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘) · 𝐶))))
105 simplr 767 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑤:(0...𝑁)⟶ℚ)
106 qcn 12888 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤𝑘) ∈ ℚ → (𝑤𝑘) ∈ ℂ)
10752, 106syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤𝑘) ∈ ℂ)
108105, 107sylan 580 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤𝑘) ∈ ℂ)
109 qcn 12888 . . . . . . . . . . . . . . . . . . . . . 22 (𝐶 ∈ ℚ → 𝐶 ∈ ℂ)
11011, 109syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℂ)
111110an32s 650 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℂ)
112111adantllr 717 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℂ)
113108, 112mulcld 11175 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤𝑘) · 𝐶) ∈ ℂ)
11492, 113gsumfsum 20864 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂfld Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))
115104, 114eqtr3d 2778 . . . . . . . . . . . . . . . 16 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((ℂflds ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))
116115mpteq2dva 5205 . . . . . . . . . . . . . . 15 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ ((ℂflds ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶)))
11768, 87, 1163eqtrd 2780 . . . . . . . . . . . . . 14 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶)))
118 qaddcl 12890 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ) → (𝑥 + 𝑦) ∈ ℚ)
119118adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) ∈ ℚ)
12094, 119, 92, 75, 99fsumcllem 15617 . . . . . . . . . . . . . . . 16 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) ∈ ℚ)
121120fmpttd 7063 . . . . . . . . . . . . . . 15 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
12213, 14elmap 8809 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
123121, 122sylibr 233 . . . . . . . . . . . . . 14 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)))
124117, 123eqeltrd 2838 . . . . . . . . . . . . 13 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) ∈ (ℚ ↑m (1...𝑁)))
125 elmapi 8787 . . . . . . . . . . . . 13 ((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) ∈ (ℚ ↑m (1...𝑁)) → (((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))):(1...𝑁)⟶ℚ)
126 ffn 6668 . . . . . . . . . . . . 13 ((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))):(1...𝑁)⟶ℚ → (((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁))
127124, 125, 1263syl 18 . . . . . . . . . . . 12 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁))
128 c0ex 11149 . . . . . . . . . . . . 13 0 ∈ V
129 fnconstg 6730 . . . . . . . . . . . . 13 (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
130128, 129ax-mp 5 . . . . . . . . . . . 12 ((1...𝑁) × {0}) Fn (1...𝑁)
131 nfcv 2907 . . . . . . . . . . . . . 14 𝑛((ℂflds ℚ) freeLMod (1...𝑁))
132 nfcv 2907 . . . . . . . . . . . . . 14 𝑛 Σg
133 nfcv 2907 . . . . . . . . . . . . . . 15 𝑛𝑤
134 nfcv 2907 . . . . . . . . . . . . . . 15 𝑛f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))
135 nfcv 2907 . . . . . . . . . . . . . . . 16 𝑛(0...𝑁)
136 nfmpt1 5213 . . . . . . . . . . . . . . . 16 𝑛(𝑛 ∈ (1...𝑁) ↦ 𝐶)
137135, 136nfmpt 5212 . . . . . . . . . . . . . . 15 𝑛(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
138133, 134, 137nfov 7387 . . . . . . . . . . . . . 14 𝑛(𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
139131, 132, 138nfov 7387 . . . . . . . . . . . . 13 𝑛(((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))
140 nfcv 2907 . . . . . . . . . . . . 13 𝑛((1...𝑁) × {0})
141139, 140eqfnfv2f 6986 . . . . . . . . . . . 12 (((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁) ∧ ((1...𝑁) × {0}) Fn (1...𝑁)) → ((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
142127, 130, 141sylancl 586 . . . . . . . . . . 11 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
143117fveq1d 6844 . . . . . . . . . . . . . 14 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))‘𝑛))
144 sumex 15572 . . . . . . . . . . . . . . 15 Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) ∈ V
145 eqid 2736 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))
146145fvmpt2 6959 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ∧ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) ∈ V) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))
147144, 146mpan2 689 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))
148143, 147sylan9eq 2796 . . . . . . . . . . . . 13 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶))
149128fvconst2 7153 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
150149adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
151148, 150eqeq12d 2752 . . . . . . . . . . . 12 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
152151ralbidva 3172 . . . . . . . . . . 11 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (∀𝑛 ∈ (1...𝑁)((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
153142, 152bitrd 278 . . . . . . . . . 10 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
154153imbi1d 341 . . . . . . . . 9 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ (∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
15542, 154sylan2 593 . . . . . . . 8 ((𝜑𝑤 ∈ (ℚ ↑m (0...𝑁))) → (((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ (∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
156155ralbidva 3172 . . . . . . 7 (𝜑 → (∀𝑤 ∈ (ℚ ↑m (0...𝑁))((((ℂflds ℚ) freeLMod (1...𝑁)) Σg (𝑤f ( ·𝑠 ‘((ℂflds ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
15741, 156bitrd 278 . . . . . 6 (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂflds ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
158 drngnzr 20732 . . . . . . . . 9 ((ℂflds ℚ) ∈ DivRing → (ℂflds ℚ) ∈ NzRing)
15919, 158ax-mp 5 . . . . . . . 8 (ℂflds ℚ) ∈ NzRing
16031islindf3 21232 . . . . . . . 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...𝑁))))))
16125, 159, 160mp2an 690 . . . . . . 7 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂflds ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))))
162 eqid 2736 . . . . . . . . . 10 (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
16345, 162dmmpti 6645 . . . . . . . . 9 dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (0...𝑁)
164 f1eq2 6734 . . . . . . . . 9 (dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (0...𝑁) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ↔ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V))
165163, 164ax-mp 5 . . . . . . . 8 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ↔ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V)
166165anbi1i 624 . . . . . . 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...𝑁)))))
167161, 166bitri 274 . . . . . 6 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂflds ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))))
168 con34b 315 . . . . . . . . 9 ((∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ (¬ 𝑤 = ((0...𝑁) × {0}) → ¬ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
169 df-nel 3050 . . . . . . . . . . 11 (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬ 𝑤 ∈ {((0...𝑁) × {0})})
170 velsn 4602 . . . . . . . . . . 11 (𝑤 ∈ {((0...𝑁) × {0})} ↔ 𝑤 = ((0...𝑁) × {0}))
171169, 170xchbinx 333 . . . . . . . . . 10 (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬ 𝑤 = ((0...𝑁) × {0}))
172171imbi1i 349 . . . . . . . . 9 ((𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0) ↔ (¬ 𝑤 = ((0...𝑁) × {0}) → ¬ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
173168, 172bitr4i 277 . . . . . . . 8 ((∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ (𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
174173ralbii 3096 . . . . . . 7 (∀𝑤 ∈ (ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
175 raldifb 4104 . . . . . . 7 (∀𝑤 ∈ (ℚ ↑m (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0) ↔ ∀𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ¬ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)
176 ralnex 3075 . . . . . . 7 (∀𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ¬ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 ↔ ¬ ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)
177174, 175, 1763bitri 296 . . . . . 6 (∀𝑤 ∈ (ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ¬ ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)
178157, 167, 1773bitr3g 312 . . . . 5 (𝜑 → (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) ↔ ¬ ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
179 eqid 2736 . . . . . . . . . . . . 13 (LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))) = (LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))
18029, 179lssmre 20427 . . . . . . . . . . . 12 (((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod → (LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑m (1...𝑁))))
18125, 180ax-mp 5 . . . . . . . . . . 11 (LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑m (1...𝑁)))
182181a1i 11 . . . . . . . . . 10 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → (LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑m (1...𝑁))))
183 eqid 2736 . . . . . . . . . . . 12 (LSpan‘((ℂflds ℚ) freeLMod (1...𝑁))) = (LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))
184 eqid 2736 . . . . . . . . . . . 12 (mrCls‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))) = (mrCls‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))))
185179, 183, 184mrclsp 20450 . . . . . . . . . . 11 (((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod → (LSpan‘((ℂflds ℚ) freeLMod (1...𝑁))) = (mrCls‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))))
18625, 185ax-mp 5 . . . . . . . . . 10 (LSpan‘((ℂflds ℚ) freeLMod (1...𝑁))) = (mrCls‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))))
187 eqid 2736 . . . . . . . . . 10 (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))) = (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))))
18831islvec 20565 . . . . . . . . . . . . 13 (((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LVec ↔ (((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂflds ℚ) ∈ DivRing))
18925, 19, 188mpbir2an 709 . . . . . . . . . . . 12 ((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LVec
190179, 186, 29lssacsex 20605 . . . . . . . . . . . . 13 (((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LVec → ((LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))) ∈ (ACS‘(ℚ ↑m (1...𝑁))) ∧ ∀𝑧 ∈ 𝒫 (ℚ ↑m (1...𝑁))∀𝑥 ∈ (ℚ ↑m (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦}))))
191190simprd 496 . . . . . . . . . . . 12 (((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LVec → ∀𝑧 ∈ 𝒫 (ℚ ↑m (1...𝑁))∀𝑥 ∈ (ℚ ↑m (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦})))
192189, 191ax-mp 5 . . . . . . . . . . 11 𝑧 ∈ 𝒫 (ℚ ↑m (1...𝑁))∀𝑥 ∈ (ℚ ↑m (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦}))
193192a1i 11 . . . . . . . . . 10 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → ∀𝑧 ∈ 𝒫 (ℚ ↑m (1...𝑁))∀𝑥 ∈ (ℚ ↑m (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦})))
19417frnd 6676 . . . . . . . . . . . 12 (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ ↑m (1...𝑁)))
195 dif0 4332 . . . . . . . . . . . 12 ((ℚ ↑m (1...𝑁)) ∖ ∅) = (ℚ ↑m (1...𝑁))
196194, 195sseqtrrdi 3995 . . . . . . . . . . 11 (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((ℚ ↑m (1...𝑁)) ∖ ∅))
197196adantr 481 . . . . . . . . . 10 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((ℚ ↑m (1...𝑁)) ∖ ∅))
198 eqid 2736 . . . . . . . . . . . . . . 15 ((ℂflds ℚ) unitVec (1...𝑁)) = ((ℂflds ℚ) unitVec (1...𝑁))
199198, 23, 29uvcff 21197 . . . . . . . . . . . . . 14 (((ℂflds ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((ℂflds ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑m (1...𝑁)))
20021, 22, 199mp2an 690 . . . . . . . . . . . . 13 ((ℂflds ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑m (1...𝑁))
201 frn 6675 . . . . . . . . . . . . 13 (((ℂflds ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑m (1...𝑁)) → ran ((ℂflds ℚ) unitVec (1...𝑁)) ⊆ (ℚ ↑m (1...𝑁)))
202200, 201ax-mp 5 . . . . . . . . . . . 12 ran ((ℂflds ℚ) unitVec (1...𝑁)) ⊆ (ℚ ↑m (1...𝑁))
203202, 195sseqtrri 3981 . . . . . . . . . . 11 ran ((ℂflds ℚ) unitVec (1...𝑁)) ⊆ ((ℚ ↑m (1...𝑁)) ∖ ∅)
204203a1i 11 . . . . . . . . . 10 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → ran ((ℂflds ℚ) unitVec (1...𝑁)) ⊆ ((ℚ ↑m (1...𝑁)) ∖ ∅))
205 un0 4350 . . . . . . . . . . . . . 14 (ran ((ℂflds ℚ) unitVec (1...𝑁)) ∪ ∅) = ran ((ℂflds ℚ) unitVec (1...𝑁))
206205fveq2i 6845 . . . . . . . . . . . . 13 ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran ((ℂflds ℚ) unitVec (1...𝑁)) ∪ ∅)) = ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘ran ((ℂflds ℚ) unitVec (1...𝑁)))
207 eqid 2736 . . . . . . . . . . . . . . . 16 (LBasis‘((ℂflds ℚ) freeLMod (1...𝑁))) = (LBasis‘((ℂflds ℚ) freeLMod (1...𝑁)))
20823, 198, 207frlmlbs 21203 . . . . . . . . . . . . . . 15 (((ℂflds ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ran ((ℂflds ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂflds ℚ) freeLMod (1...𝑁))))
20921, 22, 208mp2an 690 . . . . . . . . . . . . . 14 ran ((ℂflds ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂflds ℚ) freeLMod (1...𝑁)))
21029, 207, 183lbssp 20540 . . . . . . . . . . . . . 14 (ran ((ℂflds ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂflds ℚ) freeLMod (1...𝑁))) → ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘ran ((ℂflds ℚ) unitVec (1...𝑁))) = (ℚ ↑m (1...𝑁)))
211209, 210ax-mp 5 . . . . . . . . . . . . 13 ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘ran ((ℂflds ℚ) unitVec (1...𝑁))) = (ℚ ↑m (1...𝑁))
212206, 211eqtri 2764 . . . . . . . . . . . 12 ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran ((ℂflds ℚ) unitVec (1...𝑁)) ∪ ∅)) = (ℚ ↑m (1...𝑁))
213194, 212sseqtrrdi 3995 . . . . . . . . . . 11 (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran ((ℂflds ℚ) unitVec (1...𝑁)) ∪ ∅)))
214213adantr 481 . . . . . . . . . 10 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran ((ℂflds ℚ) unitVec (1...𝑁)) ∪ ∅)))
215 un0 4350 . . . . . . . . . . 11 (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) = ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
21625, 159pm3.2i 471 . . . . . . . . . . . . . 14 (((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂflds ℚ) ∈ NzRing)
217183, 31lindsind2 21225 . . . . . . . . . . . . . 14 (((((ℂflds ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂflds ℚ) ∈ NzRing) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁))) ∧ 𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) → ¬ 𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
218216, 217mp3an1 1448 . . . . . . . . . . . . 13 ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁))) ∧ 𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) → ¬ 𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
219218ralrimiva 3143 . . . . . . . . . . . 12 (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁))) → ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
220186, 187ismri2 17512 . . . . . . . . . . . . . 14 (((LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑m (1...𝑁))) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ ↑m (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))) ↔ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))))
221181, 194, 220sylancr 587 . . . . . . . . . . . . 13 (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))) ↔ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))))
222221biimpar 478 . . . . . . . . . . . 12 ((𝜑 ∧ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂflds ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))))
223219, 222sylan2 593 . . . . . . . . . . 11 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))))
224215, 223eqeltrid 2842 . . . . . . . . . 10 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))))
225 mptfi 9295 . . . . . . . . . . . . 13 ((0...𝑁) ∈ Fin → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin)
226 rnfi 9279 . . . . . . . . . . . . 13 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin)
22726, 225, 226mp2b 10 . . . . . . . . . . . 12 ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin
228227orci 863 . . . . . . . . . . 11 (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin ∨ ran ((ℂflds ℚ) unitVec (1...𝑁)) ∈ Fin)
229228a1i 11 . . . . . . . . . 10 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin ∨ ran ((ℂflds ℚ) unitVec (1...𝑁)) ∈ Fin))
230182, 186, 187, 193, 197, 204, 214, 224, 229mreexexd 17528 . . . . . . . . 9 ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → ∃𝑣 ∈ 𝒫 ran ((ℂflds ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))))))
231230ex 413 . . . . . . . 8 (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁))) → ∃𝑣 ∈ 𝒫 ran ((ℂflds ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁)))))))
232 ovex 7390 . . . . . . . . . . . . 13 ((ℂflds ℚ) unitVec (1...𝑁)) ∈ V
233232rnex 7849 . . . . . . . . . . . 12 ran ((ℂflds ℚ) unitVec (1...𝑁)) ∈ V
234 elpwi 4567 . . . . . . . . . . . 12 (𝑣 ∈ 𝒫 ran ((ℂflds ℚ) unitVec (1...𝑁)) → 𝑣 ⊆ ran ((ℂflds ℚ) unitVec (1...𝑁)))
235 ssdomg 8940 . . . . . . . . . . . 12 (ran ((ℂflds ℚ) unitVec (1...𝑁)) ∈ V → (𝑣 ⊆ ran ((ℂflds ℚ) unitVec (1...𝑁)) → 𝑣 ≼ ran ((ℂflds ℚ) unitVec (1...𝑁))))
236233, 234, 235mpsyl 68 . . . . . . . . . . 11 (𝑣 ∈ 𝒫 ran ((ℂflds ℚ) unitVec (1...𝑁)) → 𝑣 ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)))
237 endomtr 8952 . . . . . . . . . . . . . 14 ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣𝑣 ≼ ran ((ℂflds ℚ) unitVec (1...𝑁))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)))
238237ancoms 459 . . . . . . . . . . . . 13 ((𝑣 ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)))
239 f1f1orn 6795 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1-onto→ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
240 ovex 7390 . . . . . . . . . . . . . . . . 17 (0...𝑁) ∈ V
241240f1oen 8913 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1-onto→ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) → (0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
242239, 241syl 17 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
243 endomtr 8952 . . . . . . . . . . . . . . . . 17 (((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁))) → (0...𝑁) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)))
244198uvcendim 21253 . . . . . . . . . . . . . . . . . . . 20 (((ℂflds ℚ) ∈ NzRing ∧ (1...𝑁) ∈ Fin) → (1...𝑁) ≈ ran ((ℂflds ℚ) unitVec (1...𝑁)))
245159, 22, 244mp2an 690 . . . . . . . . . . . . . . . . . . 19 (1...𝑁) ≈ ran ((ℂflds ℚ) unitVec (1...𝑁))
246245ensymi 8944 . . . . . . . . . . . . . . . . . 18 ran ((ℂflds ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)
247 domentr 8953 . . . . . . . . . . . . . . . . . . 19 (((0...𝑁) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)) ∧ ran ((ℂflds ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (0...𝑁) ≼ (1...𝑁))
248 hashdom 14279 . . . . . . . . . . . . . . . . . . . . 21 (((0...𝑁) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((♯‘(0...𝑁)) ≤ (♯‘(1...𝑁)) ↔ (0...𝑁) ≼ (1...𝑁)))
24926, 22, 248mp2an 690 . . . . . . . . . . . . . . . . . . . 20 ((♯‘(0...𝑁)) ≤ (♯‘(1...𝑁)) ↔ (0...𝑁) ≼ (1...𝑁))
250 hashfz0 14332 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ0 → (♯‘(0...𝑁)) = (𝑁 + 1))
2512, 250syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (♯‘(0...𝑁)) = (𝑁 + 1))
252 hashfz1 14246 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
2532, 252syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (♯‘(1...𝑁)) = 𝑁)
254251, 253breq12d 5118 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((♯‘(0...𝑁)) ≤ (♯‘(1...𝑁)) ↔ (𝑁 + 1) ≤ 𝑁))
255249, 254bitr3id 284 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((0...𝑁) ≼ (1...𝑁) ↔ (𝑁 + 1) ≤ 𝑁))
256247, 255imbitrid 243 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((0...𝑁) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)) ∧ ran ((ℂflds ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (𝑁 + 1) ≤ 𝑁))
257246, 256mpan2i 695 . . . . . . . . . . . . . . . . 17 (𝜑 → ((0...𝑁) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁))
258243, 257syl5 34 . . . . . . . . . . . . . . . 16 (𝜑 → (((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁))) → (𝑁 + 1) ≤ 𝑁))
259258expd 416 . . . . . . . . . . . . . . 15 (𝜑 → ((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁)))
260242, 259syl5 34 . . . . . . . . . . . . . 14 (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁)))
261260com23 86 . . . . . . . . . . . . 13 (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
262238, 261syl5 34 . . . . . . . . . . . 12 (𝜑 → ((𝑣 ≼ ran ((ℂflds ℚ) unitVec (1...𝑁)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
263262expdimp 453 . . . . . . . . . . 11 ((𝜑𝑣 ≼ ran ((ℂflds ℚ) unitVec (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
264236, 263sylan2 593 . . . . . . . . . 10 ((𝜑𝑣 ∈ 𝒫 ran ((ℂflds ℚ) unitVec (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
265264adantrd 492 . . . . . . . . 9 ((𝜑𝑣 ∈ 𝒫 ran ((ℂflds ℚ) unitVec (1...𝑁))) → ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
266265rexlimdva 3152 . . . . . . . 8 (𝜑 → (∃𝑣 ∈ 𝒫 ran ((ℂflds ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂflds ℚ) freeLMod (1...𝑁))))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
267231, 266syld 47 . . . . . . 7 (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
268267impd 411 . . . . . 6 (𝜑 → ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁))) ∧ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V) → (𝑁 + 1) ≤ 𝑁))
269268ancomsd 466 . . . . 5 (𝜑 → (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂflds ℚ) freeLMod (1...𝑁)))) → (𝑁 + 1) ≤ 𝑁))
270178, 269sylbird 259 . . . 4 (𝜑 → (¬ ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 → (𝑁 + 1) ≤ 𝑁))
2719, 270mt3d 148 . . 3 (𝜑 → ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)
272 eldifsn 4747 . . . . 5 (𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ↔ (𝑤 ∈ (ℚ ↑m (0...𝑁)) ∧ 𝑤 ≠ ((0...𝑁) × {0})))
27342anim1i 615 . . . . 5 ((𝑤 ∈ (ℚ ↑m (0...𝑁)) ∧ 𝑤 ≠ ((0...𝑁) × {0})) → (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})))
274272, 273sylbi 216 . . . 4 (𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) → (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})))
27593a1i 11 . . . . . . . . 9 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ℚ ⊆ ℂ)
2762adantr 481 . . . . . . . . 9 ((𝜑𝑤:(0...𝑁)⟶ℚ) → 𝑁 ∈ ℕ0)
277275, 276, 53elplyd 25563 . . . . . . . 8 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ∈ (Poly‘ℚ))
278277adantrr 715 . . . . . . 7 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ∈ (Poly‘ℚ))
279 uzdisj 13514 . . . . . . . . . . . . . . . . . 18 ((0...((𝑁 + 1) − 1)) ∩ (ℤ‘(𝑁 + 1))) = ∅
2802nn0cnd 12475 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑁 ∈ ℂ)
281 pncan1 11579 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
282280, 281syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
283282oveq2d 7373 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁))
284283ineq1d 4171 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((0...((𝑁 + 1) − 1)) ∩ (ℤ‘(𝑁 + 1))) = ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))))
285279, 284eqtr3id 2790 . . . . . . . . . . . . . . . . 17 (𝜑 → ∅ = ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))))
286285eqcomd 2742 . . . . . . . . . . . . . . . 16 (𝜑 → ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅)
287128fconst 6728 . . . . . . . . . . . . . . . . . 18 ((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶{0}
288 snssi 4768 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℚ → {0} ⊆ ℚ)
28996, 97, 288mp2b 10 . . . . . . . . . . . . . . . . . . 19 {0} ⊆ ℚ
290289, 93sstri 3953 . . . . . . . . . . . . . . . . . 18 {0} ⊆ ℂ
291 fss 6685 . . . . . . . . . . . . . . . . . 18 ((((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℂ) → ((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶ℂ)
292287, 290, 291mp2an 690 . . . . . . . . . . . . . . . . 17 ((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶ℂ
293 fun 6704 . . . . . . . . . . . . . . . . 17 (((𝑤:(0...𝑁)⟶ℚ ∧ ((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶ℂ) ∧ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅) → (𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
294292, 293mpanl2 699 . . . . . . . . . . . . . . . 16 ((𝑤:(0...𝑁)⟶ℚ ∧ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅) → (𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
295286, 294sylan2 593 . . . . . . . . . . . . . . 15 ((𝑤:(0...𝑁)⟶ℚ ∧ 𝜑) → (𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
296295ancoms 459 . . . . . . . . . . . . . 14 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
297 nn0uz 12805 . . . . . . . . . . . . . . . . . 18 0 = (ℤ‘0)
2986, 297eleqtrdi 2848 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 + 1) ∈ (ℤ‘0))
299 uzsplit 13513 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ (ℤ‘0) → (ℤ‘0) = ((0...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))))
300298, 299syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℤ‘0) = ((0...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))))
301297, 300eqtrid 2788 . . . . . . . . . . . . . . . . 17 (𝜑 → ℕ0 = ((0...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))))
302283uneq1d 4122 . . . . . . . . . . . . . . . . 17 (𝜑 → ((0...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))) = ((0...𝑁) ∪ (ℤ‘(𝑁 + 1))))
303301, 302eqtr2d 2777 . . . . . . . . . . . . . . . 16 (𝜑 → ((0...𝑁) ∪ (ℤ‘(𝑁 + 1))) = ℕ0)
304 ssequn1 4140 . . . . . . . . . . . . . . . . . 18 (ℚ ⊆ ℂ ↔ (ℚ ∪ ℂ) = ℂ)
30593, 304mpbi 229 . . . . . . . . . . . . . . . . 17 (ℚ ∪ ℂ) = ℂ
306305a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (ℚ ∪ ℂ) = ℂ)
307303, 306feq23d 6663 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ‘(𝑁 + 1)))⟶(ℚ ∪ ℂ) ↔ (𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):ℕ0⟶ℂ))
308307adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ‘(𝑁 + 1)))⟶(ℚ ∪ ℂ) ↔ (𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):ℕ0⟶ℂ))
309296, 308mpbid 231 . . . . . . . . . . . . 13 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})):ℕ0⟶ℂ)
310 ffn 6668 . . . . . . . . . . . . . . . 16 (𝑤:(0...𝑁)⟶ℚ → 𝑤 Fn (0...𝑁))
311 fnimadisj 6633 . . . . . . . . . . . . . . . 16 ((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅) → (𝑤 “ (ℤ‘(𝑁 + 1))) = ∅)
312310, 286, 311syl2anr 597 . . . . . . . . . . . . . . 15 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑤 “ (ℤ‘(𝑁 + 1))) = ∅)
3132nn0zd 12525 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℤ)
314313peano2zd 12610 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 + 1) ∈ ℤ)
315 uzid 12778 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ ℤ → (𝑁 + 1) ∈ (ℤ‘(𝑁 + 1)))
316 ne0i 4294 . . . . . . . . . . . . . . . . . . 19 ((𝑁 + 1) ∈ (ℤ‘(𝑁 + 1)) → (ℤ‘(𝑁 + 1)) ≠ ∅)
317314, 315, 3163syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℤ‘(𝑁 + 1)) ≠ ∅)
318 inidm 4178 . . . . . . . . . . . . . . . . . . 19 ((ℤ‘(𝑁 + 1)) ∩ (ℤ‘(𝑁 + 1))) = (ℤ‘(𝑁 + 1))
319318neeq1i 3008 . . . . . . . . . . . . . . . . . 18 (((ℤ‘(𝑁 + 1)) ∩ (ℤ‘(𝑁 + 1))) ≠ ∅ ↔ (ℤ‘(𝑁 + 1)) ≠ ∅)
320317, 319sylibr 233 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℤ‘(𝑁 + 1)) ∩ (ℤ‘(𝑁 + 1))) ≠ ∅)
321 xpima2 6136 . . . . . . . . . . . . . . . . 17 (((ℤ‘(𝑁 + 1)) ∩ (ℤ‘(𝑁 + 1))) ≠ ∅ → (((ℤ‘(𝑁 + 1)) × {0}) “ (ℤ‘(𝑁 + 1))) = {0})
322320, 321syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (((ℤ‘(𝑁 + 1)) × {0}) “ (ℤ‘(𝑁 + 1))) = {0})
323322adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (((ℤ‘(𝑁 + 1)) × {0}) “ (ℤ‘(𝑁 + 1))) = {0})
324312, 323uneq12d 4124 . . . . . . . . . . . . . 14 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((𝑤 “ (ℤ‘(𝑁 + 1))) ∪ (((ℤ‘(𝑁 + 1)) × {0}) “ (ℤ‘(𝑁 + 1)))) = (∅ ∪ {0}))
325 imaundir 6103 . . . . . . . . . . . . . 14 ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})) “ (ℤ‘(𝑁 + 1))) = ((𝑤 “ (ℤ‘(𝑁 + 1))) ∪ (((ℤ‘(𝑁 + 1)) × {0}) “ (ℤ‘(𝑁 + 1))))
326 uncom 4113 . . . . . . . . . . . . . . 15 (∅ ∪ {0}) = ({0} ∪ ∅)
327 un0 4350 . . . . . . . . . . . . . . 15 ({0} ∪ ∅) = {0}
328326, 327eqtr2i 2765 . . . . . . . . . . . . . 14 {0} = (∅ ∪ {0})
329324, 325, 3283eqtr4g 2801 . . . . . . . . . . . . 13 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})) “ (ℤ‘(𝑁 + 1))) = {0})
330286, 310anim12ci 614 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅))
331 fnconstg 6730 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V → ((ℤ‘(𝑁 + 1)) × {0}) Fn (ℤ‘(𝑁 + 1)))
332128, 331ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((ℤ‘(𝑁 + 1)) × {0}) Fn (ℤ‘(𝑁 + 1))
333 fvun1 6932 . . . . . . . . . . . . . . . . . . . 20 ((𝑤 Fn (0...𝑁) ∧ ((ℤ‘(𝑁 + 1)) × {0}) Fn (ℤ‘(𝑁 + 1)) ∧ (((0...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅ ∧ 𝑘 ∈ (0...𝑁))) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤𝑘))
334332, 333mp3an2 1449 . . . . . . . . . . . . . . . . . . 19 ((𝑤 Fn (0...𝑁) ∧ (((0...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅ ∧ 𝑘 ∈ (0...𝑁))) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤𝑘))
335334anassrs 468 . . . . . . . . . . . . . . . . . 18 (((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤𝑘))
336330, 335sylan 580 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤𝑘))
337336eqcomd 2742 . . . . . . . . . . . . . . . 16 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤𝑘) = ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0}))‘𝑘))
338337oveq1d 7372 . . . . . . . . . . . . . . 15 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤𝑘) · (𝑦𝑘)) = (((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦𝑘)))
339338sumeq2dv 15588 . . . . . . . . . . . . . 14 ((𝜑𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)) = Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦𝑘)))
340339mpteq2dv 5207 . . . . . . . . . . . . 13 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦𝑘))))
341277, 276, 309, 329, 340coeeq 25588 . . . . . . . . . . . 12 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) = (𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})))
342341reseq1d 5936 . . . . . . . . . . 11 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)))
343 res0 5941 . . . . . . . . . . . . . 14 (𝑤 ↾ ∅) = ∅
344285reseq2d 5937 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ↾ ∅) = (𝑤 ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1)))))
345 res0 5941 . . . . . . . . . . . . . . 15 (((ℤ‘(𝑁 + 1)) × {0}) ↾ ∅) = ∅
346285reseq2d 5937 . . . . . . . . . . . . . . 15 (𝜑 → (((ℤ‘(𝑁 + 1)) × {0}) ↾ ∅) = (((ℤ‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1)))))
347345, 346eqtr3id 2790 . . . . . . . . . . . . . 14 (𝜑 → ∅ = (((ℤ‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1)))))
348343, 344, 3473eqtr3a 2800 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1)))) = (((ℤ‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1)))))
349 fss 6685 . . . . . . . . . . . . . . 15 ((((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℚ) → ((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶ℚ)
350287, 289, 349mp2an 690 . . . . . . . . . . . . . 14 ((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶ℚ
351 fresaunres1 6715 . . . . . . . . . . . . . 14 ((𝑤:(0...𝑁)⟶ℚ ∧ ((ℤ‘(𝑁 + 1)) × {0}):(ℤ‘(𝑁 + 1))⟶ℚ ∧ (𝑤 ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1)))) = (((ℤ‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))))) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
352350, 351mp3an2 1449 . . . . . . . . . . . . 13 ((𝑤:(0...𝑁)⟶ℚ ∧ (𝑤 ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1)))) = (((ℤ‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ‘(𝑁 + 1))))) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
353348, 352sylan2 593 . . . . . . . . . . . 12 ((𝑤:(0...𝑁)⟶ℚ ∧ 𝜑) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
354353ancoms 459 . . . . . . . . . . 11 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
355342, 354eqtrd 2776 . . . . . . . . . 10 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = 𝑤)
356 fveq2 6842 . . . . . . . . . . 11 ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) = 0𝑝 → (coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) = (coeff‘0𝑝))
357356reseq1d 5936 . . . . . . . . . 10 ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) = 0𝑝 → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁)))
358 eqtr2 2760 . . . . . . . . . . . 12 ((((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁))) → 𝑤 = ((coeff‘0𝑝) ↾ (0...𝑁)))
359 coe0 25617 . . . . . . . . . . . . . 14 (coeff‘0𝑝) = (ℕ0 × {0})
360359reseq1i 5933 . . . . . . . . . . . . 13 ((coeff‘0𝑝) ↾ (0...𝑁)) = ((ℕ0 × {0}) ↾ (0...𝑁))
361 elfznn0 13534 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℕ0)
362361ssriv 3948 . . . . . . . . . . . . . 14 (0...𝑁) ⊆ ℕ0
363 xpssres 5974 . . . . . . . . . . . . . 14 ((0...𝑁) ⊆ ℕ0 → ((ℕ0 × {0}) ↾ (0...𝑁)) = ((0...𝑁) × {0}))
364362, 363ax-mp 5 . . . . . . . . . . . . 13 ((ℕ0 × {0}) ↾ (0...𝑁)) = ((0...𝑁) × {0})
365360, 364eqtri 2764 . . . . . . . . . . . 12 ((coeff‘0𝑝) ↾ (0...𝑁)) = ((0...𝑁) × {0})
366358, 365eqtrdi 2792 . . . . . . . . . . 11 ((((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁))) → 𝑤 = ((0...𝑁) × {0}))
367366ex 413 . . . . . . . . . 10 (((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = 𝑤 → (((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁)) → 𝑤 = ((0...𝑁) × {0})))
368355, 357, 367syl2im 40 . . . . . . . . 9 ((𝜑𝑤:(0...𝑁)⟶ℚ) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) = 0𝑝𝑤 = ((0...𝑁) × {0})))
369368necon3d 2964 . . . . . . . 8 ((𝜑𝑤:(0...𝑁)⟶ℚ) → (𝑤 ≠ ((0...𝑁) × {0}) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ≠ 0𝑝))
370369impr 455 . . . . . . 7 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ≠ 0𝑝)
371 eldifsn 4747 . . . . . . 7 ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}) ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ∈ (Poly‘ℚ) ∧ (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ≠ 0𝑝))
372278, 370, 371sylanbrc 583 . . . . . 6 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}))
373372adantrr 715 . . . . 5 ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}))
374 oveq1 7364 . . . . . . . . . . . 12 (𝑦 = 𝐴 → (𝑦𝑘) = (𝐴𝑘))
375374oveq2d 7373 . . . . . . . . . . 11 (𝑦 = 𝐴 → ((𝑤𝑘) · (𝑦𝑘)) = ((𝑤𝑘) · (𝐴𝑘)))
376375sumeq2sdv 15589 . . . . . . . . . 10 (𝑦 = 𝐴 → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)))
377 eqid 2736 . . . . . . . . . 10 (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))
378 sumex 15572 . . . . . . . . . 10 Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)) ∈ V
379376, 377, 378fvmpt 6948 . . . . . . . . 9 (𝐴 ∈ ℂ → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)))
3801, 379syl 17 . . . . . . . 8 (𝜑 → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)))
381380adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)))
382107adantll 712 . . . . . . . . . . . . . 14 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤𝑘) ∈ ℂ)
383 aacllem.2 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
384383adantlr 713 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
385110, 384mulcld 11175 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ)
386385adantllr 717 . . . . . . . . . . . . . 14 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ)
38751, 382, 386fsummulc2 15669 . . . . . . . . . . . . 13 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)) = Σ𝑛 ∈ (1...𝑁)((𝑤𝑘) · (𝐶 · 𝑋)))
388 aacllem.4 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → (𝐴𝑘) = Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋))
389388oveq2d 7373 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝑁)) → ((𝑤𝑘) · (𝐴𝑘)) = ((𝑤𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)))
390389adantlr 713 . . . . . . . . . . . . 13 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤𝑘) · (𝐴𝑘)) = ((𝑤𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)))
391382adantr 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤𝑘) ∈ ℂ)
392110adantllr 717 . . . . . . . . . . . . . . 15 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℂ)
393 simpll 765 . . . . . . . . . . . . . . . 16 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → 𝜑)
394393, 383sylan 580 . . . . . . . . . . . . . . 15 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
395391, 392, 394mulassd 11178 . . . . . . . . . . . . . 14 ((((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑤𝑘) · 𝐶) · 𝑋) = ((𝑤𝑘) · (𝐶 · 𝑋)))
396395sumeq2dv 15588 . . . . . . . . . . . . 13 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)((𝑤𝑘) · (𝐶 · 𝑋)))
397387, 390, 3963eqtr4d 2786 . . . . . . . . . . . 12 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤𝑘) · (𝐴𝑘)) = Σ𝑛 ∈ (1...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋))
398397sumeq2dv 15588 . . . . . . . . . . 11 ((𝜑𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)) = Σ𝑘 ∈ (0...𝑁𝑛 ∈ (1...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋))
399107ad2ant2lr 746 . . . . . . . . . . . . . 14 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (𝑤𝑘) ∈ ℂ)
400110anasss 467 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝐶 ∈ ℂ)
401400adantlr 713 . . . . . . . . . . . . . 14 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝐶 ∈ ℂ)
402399, 401mulcld 11175 . . . . . . . . . . . . 13 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → ((𝑤𝑘) · 𝐶) ∈ ℂ)
403383ad2ant2rl 747 . . . . . . . . . . . . 13 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝑋 ∈ ℂ)
404402, 403mulcld 11175 . . . . . . . . . . . 12 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (((𝑤𝑘) · 𝐶) · 𝑋) ∈ ℂ)
40543, 69, 404fsumcom 15660 . . . . . . . . . . 11 ((𝜑𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁𝑛 ∈ (1...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋))
406398, 405eqtrd 2776 . . . . . . . . . 10 ((𝜑𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)) = Σ𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋))
407406adantrr 715 . . . . . . . . 9 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)) = Σ𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋))
408 nfv 1917 . . . . . . . . . . . 12 𝑛𝜑
409 nfv 1917 . . . . . . . . . . . . 13 𝑛 𝑤:(0...𝑁)⟶ℚ
410 nfra1 3267 . . . . . . . . . . . . 13 𝑛𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0
411409, 410nfan 1902 . . . . . . . . . . . 12 𝑛(𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)
412408, 411nfan 1902 . . . . . . . . . . 11 𝑛(𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0))
413 rspa 3231 . . . . . . . . . . . . . . . 16 ((∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)
414413oveq1d 7372 . . . . . . . . . . . . . . 15 ((∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
415414adantll 712 . . . . . . . . . . . . . 14 (((𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
416415adantll 712 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
417383adantlr 713 . . . . . . . . . . . . . . 15 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
41892, 417, 113fsummulc1 15670 . . . . . . . . . . . . . 14 (((𝜑𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋))
419418adantlrr 719 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋))
420383mul02d 11353 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0)
421420adantlr 713 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0)
422416, 419, 4213eqtr3d 2784 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋) = 0)
423422ex 413 . . . . . . . . . . 11 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → (𝑛 ∈ (1...𝑁) → Σ𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋) = 0))
424412, 423ralrimi 3240 . . . . . . . . . 10 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋) = 0)
425424sumeq2d 15587 . . . . . . . . 9 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → Σ𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)(((𝑤𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)0)
426407, 425eqtrd 2776 . . . . . . . 8 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)) = Σ𝑛 ∈ (1...𝑁)0)
42722olci 864 . . . . . . . . 9 ((1...𝑁) ⊆ (ℤ𝐵) ∨ (1...𝑁) ∈ Fin)
428 sumz 15607 . . . . . . . . 9 (((1...𝑁) ⊆ (ℤ𝐵) ∨ (1...𝑁) ∈ Fin) → Σ𝑛 ∈ (1...𝑁)0 = 0)
429427, 428ax-mp 5 . . . . . . . 8 Σ𝑛 ∈ (1...𝑁)0 = 0
430426, 429eqtrdi 2792 . . . . . . 7 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝐴𝑘)) = 0)
431381, 430eqtrd 2776 . . . . . 6 ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))‘𝐴) = 0)
432431adantrlr 721 . . . . 5 ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))‘𝐴) = 0)
433 fveq1 6841 . . . . . . 7 (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) → (𝑥𝐴) = ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))‘𝐴))
434433eqeq1d 2738 . . . . . 6 (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) → ((𝑥𝐴) = 0 ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))‘𝐴) = 0))
435434rspcev 3581 . . . . 5 (((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}) ∧ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤𝑘) · (𝑦𝑘)))‘𝐴) = 0) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥𝐴) = 0)
436373, 432, 435syl2anc 584 . . . 4 ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥𝐴) = 0)
437274, 436sylanr1 680 . . 3 ((𝜑 ∧ (𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ∧ ∀𝑛 ∈ (1...𝑁𝑘 ∈ (0...𝑁)((𝑤𝑘) · 𝐶) = 0)) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥𝐴) = 0)
438271, 437rexlimddv 3158 . 2 (𝜑 → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥𝐴) = 0)
439 elqaa 25682 . 2 (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧ ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥𝐴) = 0))
4401, 438, 439sylanbrc 583 1 (𝜑𝐴 ∈ 𝔸)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wnel 3049  wral 3064  wrex 3073  Vcvv 3445  cdif 3907  cun 3908  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560  {csn 4586   class class class wbr 5105  cmpt 5188   × cxp 5631  dom cdm 5633  ran crn 5634  cres 5635  cima 5636   Fn wfn 6491  wf 6492  1-1wf1 6493  1-1-ontowf1o 6495  cfv 6496  (class class class)co 7357  f cof 7615  m cmap 8765  cen 8880  cdom 8881  Fincfn 8883  cc 11049  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189  cle 11190  cmin 11385  0cn0 12413  cz 12499  cuz 12763  cq 12873  ...cfz 13424  cexp 13967  chash 14230  Σcsu 15570  Basecbs 17083  s cress 17112  .rcmulr 17134  Scalarcsca 17136   ·𝑠 cvsca 17137  0gc0g 17321   Σg cgsu 17322  Moorecmre 17462  mrClscmrc 17463  mrIndcmri 17464  ACScacs 17465  Ringcrg 19964  DivRingcdr 20185  LModclmod 20322  LSubSpclss 20392  LSpanclspn 20432  LBasisclbs 20535  LVecclvec 20563  NzRingcnzr 20727  fldccnfld 20796   freeLMod cfrlm 21152   unitVec cuvc 21188   LIndF clindf 21210  LIndSclinds 21211  0𝑝c0p 25033  Polycply 25545  coeffccoe 25547  𝔸caa 25674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-tpos 8157  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-xnn0 12486  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-rlim 15371  df-sum 15571  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-0g 17323  df-gsum 17324  df-prds 17329  df-pws 17331  df-mre 17466  df-mrc 17467  df-mri 17468  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-mhm 18601  df-submnd 18602  df-grp 18751  df-minusg 18752  df-sbg 18753  df-mulg 18873  df-subg 18925  df-ghm 19006  df-cntz 19097  df-cmn 19564  df-abl 19565  df-mgp 19897  df-ur 19914  df-ring 19966  df-cring 19967  df-oppr 20049  df-dvdsr 20070  df-unit 20071  df-invr 20101  df-dvr 20112  df-drng 20187  df-subrg 20220  df-lmod 20324  df-lss 20393  df-lsp 20433  df-lmhm 20483  df-lbs 20536  df-lvec 20564  df-sra 20633  df-rgmod 20634  df-nzr 20728  df-cnfld 20797  df-dsmm 21138  df-frlm 21153  df-uvc 21189  df-lindf 21212  df-linds 21213  df-0p 25034  df-ply 25549  df-coe 25551  df-dgr 25552  df-aa 25675
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator