Theorem aacllem 49613

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.

Step	Hyp	Ref	Expression
1		aacllem.0	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		aacllem.1	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
3	2	nn0red 12561	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ)
4	3	ltp1d 12170	. . . . 5 ⊢ (𝜑 → 𝑁 < (𝑁 + 1))
5		peano2nn0 12539	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
6	2, 5	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ0)
7	6	nn0red 12561	. . . . . 6 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
8	3, 7	ltnled 11380	. . . . 5 ⊢ (𝜑 → (𝑁 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑁))
9	4, 8	mpbid 232	. . . 4 ⊢ (𝜑 → ¬ (𝑁 + 1) ≤ 𝑁)
10		aacllem.3	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
11	10	3expa 1118	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
12	11	fmpttd 7104	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ)
13		qex 12975	. . . . . . . . . . 11 ⊢ ℚ ∈ V
14		ovex 7436	. . . . . . . . . . 11 ⊢ (1...𝑁) ∈ V
15	13, 14	elmap 8883	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ)
16	12, 15	sylibr 234	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m (1...𝑁)))
17	16	fmpttd 7104	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑m (1...𝑁)))
18		eqid 2735	. . . . . . . . . . . 12 ⊢ (ℂfld ↾s ℚ) = (ℂfld ↾s ℚ)
19	18	qdrng 27581	. . . . . . . . . . 11 ⊢ (ℂfld ↾s ℚ) ∈ DivRing
20		drngring 20694	. . . . . . . . . . 11 ⊢ ((ℂfld ↾s ℚ) ∈ DivRing → (ℂfld ↾s ℚ) ∈ Ring)
21	19, 20	ax-mp 5	. . . . . . . . . 10 ⊢ (ℂfld ↾s ℚ) ∈ Ring
22		fzfi 13988	. . . . . . . . . 10 ⊢ (1...𝑁) ∈ Fin
23		eqid 2735	. . . . . . . . . . 11 ⊢ ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) = ((ℂfld ↾s ℚ) freeLMod (1...𝑁))
24	23	frlmlmod 21707	. . . . . . . . . 10 ⊢ (((ℂfld ↾s ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod)
25	21, 22, 24	mp2an 692	. . . . . . . . 9 ⊢ ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod
26		fzfi 13988	. . . . . . . . 9 ⊢ (0...𝑁) ∈ Fin
27	18	qrngbas 27580	. . . . . . . . . . . 12 ⊢ ℚ = (Base‘(ℂfld ↾s ℚ))
28	23, 27	frlmfibas 21720	. . . . . . . . . . 11 ⊢ (((ℂfld ↾s ℚ) ∈ DivRing ∧ (1...𝑁) ∈ Fin) → (ℚ ↑m (1...𝑁)) = (Base‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
29	19, 22, 28	mp2an 692	. . . . . . . . . 10 ⊢ (ℚ ↑m (1...𝑁)) = (Base‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
30	23	frlmsca 21711	. . . . . . . . . . 11 ⊢ (((ℂfld ↾s ℚ) ∈ DivRing ∧ (1...𝑁) ∈ Fin) → (ℂfld ↾s ℚ) = (Scalar‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
31	19, 22, 30	mp2an 692	. . . . . . . . . 10 ⊢ (ℂfld ↾s ℚ) = (Scalar‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
32		eqid 2735	. . . . . . . . . 10 ⊢ ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
33	18	qrng0 27582	. . . . . . . . . . . 12 ⊢ 0 = (0g‘(ℂfld ↾s ℚ))
34	23, 33	frlm0 21712	. . . . . . . . . . 11 ⊢ (((ℂfld ↾s ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((1...𝑁) × {0}) = (0g‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
35	21, 22, 34	mp2an 692	. . . . . . . . . 10 ⊢ ((1...𝑁) × {0}) = (0g‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
36		eqid 2735	. . . . . . . . . . . 12 ⊢ ((ℂfld ↾s ℚ) freeLMod (0...𝑁)) = ((ℂfld ↾s ℚ) freeLMod (0...𝑁))
37	36, 27	frlmfibas 21720	. . . . . . . . . . 11 ⊢ (((ℂfld ↾s ℚ) ∈ DivRing ∧ (0...𝑁) ∈ Fin) → (ℚ ↑m (0...𝑁)) = (Base‘((ℂfld ↾s ℚ) freeLMod (0...𝑁))))
38	19, 26, 37	mp2an 692	. . . . . . . . . 10 ⊢ (ℚ ↑m (0...𝑁)) = (Base‘((ℂfld ↾s ℚ) freeLMod (0...𝑁)))
39	29, 31, 32, 35, 33, 38	islindf4 21796	. . . . . . . . 9 ⊢ ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (0...𝑁) ∈ Fin ∧ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑m (1...𝑁))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0}))))
40	25, 26, 39	mp3an12 1453	. . . . . . . 8 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑m (1...𝑁)) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0}))))
41	17, 40	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0}))))
42		elmapi 8861	. . . . . . . . 9 ⊢ (𝑤 ∈ (ℚ ↑m (0...𝑁)) → 𝑤:(0...𝑁)⟶ℚ)
43		fzfid 13989	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (0...𝑁) ∈ Fin)
44		fvexd 6890	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ V)
45	14	mptex 7214	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V
46	45	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V)
47		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑤:(0...𝑁)⟶ℚ)
48	47	feqmptd 6946	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑤 = (𝑘 ∈ (0...𝑁) ↦ (𝑤‘𝑘)))
49		eqidd 2736	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
50	43, 44, 46, 48, 49	offval2 7689	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘)( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶))))
51		fzfid 13989	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
52		ffvelcdm 7070	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ)
53	52	adantll 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ)
54	16	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m (1...𝑁)))
55		cnfldmul 21321	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ · = (.r‘ℂfld)
56	18, 55	ressmulr 17319	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℚ ∈ V → · = (.r‘(ℂfld ↾s ℚ)))
57	13, 56	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ · = (.r‘(ℂfld ↾s ℚ))
58	23, 29, 27, 51, 53, 54, 32, 57	frlmvscafval 21724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘)( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (((1...𝑁) × {(𝑤‘𝑘)}) ∘f · (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
59		fvexd 6890	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤‘𝑘) ∈ V)
60	11	adantllr 719	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
61		fconstmpt 5716	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1...𝑁) × {(𝑤‘𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤‘𝑘))
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((1...𝑁) × {(𝑤‘𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤‘𝑘)))
63		eqidd 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) = (𝑛 ∈ (1...𝑁) ↦ 𝐶))
64	51, 59, 60, 62, 63	offval2 7689	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (((1...𝑁) × {(𝑤‘𝑘)}) ∘f · (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))
65	58, 64	eqtrd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘)( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))
66	65	mpteq2dva 5214	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘)( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))
67	50, 66	eqtrd 2770	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))
68	67	oveq2d 7419	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))))
69		fzfid 13989	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (1...𝑁) ∈ Fin)
70	21	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (ℂfld ↾s ℚ) ∈ Ring)
71	53	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ)
72	11	an32s 652	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℚ)
73	72	adantllr 719	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℚ)
74		qmulcl 12981	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤‘𝑘) ∈ ℚ ∧ 𝐶 ∈ ℚ) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ)
75	71, 73, 74	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ)
76	75	an32s 652	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ)
77	76	fmpttd 7104	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
78	13, 14	elmap 8883	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
79	77, 78	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)))
80		eqid 2735	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))
81	14	mptex 7214	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ V
82	81	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ V)
83		snex 5406	. . . . . . . . . . . . . . . . . . 19 ⊢ {0} ∈ V
84	14, 83	xpex 7745	. . . . . . . . . . . . . . . . . 18 ⊢ ((1...𝑁) × {0}) ∈ V
85	84	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((1...𝑁) × {0}) ∈ V)
86	80, 43, 82, 85	fsuppmptdm 9386	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) finSupp ((1...𝑁) × {0}))
87	23, 29, 35, 69, 43, 70, 79, 86	frlmgsum 21730	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ ((ℂfld ↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))))
88		cnfldbas 21317	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ = (Base‘ℂfld)
89		cnfldadd 21319	. . . . . . . . . . . . . . . . . 18 ⊢ + = (+g‘ℂfld)
90		cnfldex 21316	. . . . . . . . . . . . . . . . . . 19 ⊢ ℂfld ∈ V
91	90	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℂfld ∈ V)
92		fzfid 13989	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (0...𝑁) ∈ Fin)
93		qsscn 12974	. . . . . . . . . . . . . . . . . . 19 ⊢ ℚ ⊆ ℂ
94	93	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℚ ⊆ ℂ)
95	75	fmpttd 7104	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(0...𝑁)⟶ℚ)
96		0z 12597	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℤ
97		zq 12968	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℤ → 0 ∈ ℚ)
98	96, 97	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℚ
99	98	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 0 ∈ ℚ)
100		addlid 11416	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℂ → (0 + 𝑥) = 𝑥)
101		addrid 11413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℂ → (𝑥 + 0) = 𝑥)
102	100, 101	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℂ → ((0 + 𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥))
103	102	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ ℂ) → ((0 + 𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥))
104	88, 89, 18, 91, 92, 94, 95, 99, 103	gsumress 18658	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂfld Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = ((ℂfld ↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))
105		simplr 768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑤:(0...𝑁)⟶ℚ)
106		qcn 12977	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤‘𝑘) ∈ ℚ → (𝑤‘𝑘) ∈ ℂ)
107	52, 106	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
108	105, 107	sylan 580	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
109		qcn 12977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐶 ∈ ℚ → 𝐶 ∈ ℂ)
110	11, 109	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℂ)
111	110	an32s 652	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℂ)
112	111	adantllr 719	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℂ)
113	108, 112	mulcld 11253	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℂ)
114	92, 113	gsumfsum 21400	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂfld Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
115	104, 114	eqtr3d 2772	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((ℂfld ↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
116	115	mpteq2dva 5214	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ ((ℂfld ↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)))
117	68, 87, 116	3eqtrd 2774	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)))
118		qaddcl 12979	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ) → (𝑥 + 𝑦) ∈ ℚ)
119	118	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) ∈ ℚ)
120	94, 119, 92, 75, 99	fsumcllem 15746	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ ℚ)
121	120	fmpttd 7104	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
122	13, 14	elmap 8883	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
123	121, 122	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)))
124	117, 123	eqeltrd 2834	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) ∈ (ℚ ↑m (1...𝑁)))
125		elmapi 8861	. . . . . . . . . . . . 13 ⊢ ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) ∈ (ℚ ↑m (1...𝑁)) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))):(1...𝑁)⟶ℚ)
126		ffn 6705	. . . . . . . . . . . . 13 ⊢ ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))):(1...𝑁)⟶ℚ → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁))
127	124, 125, 126	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁))
128		c0ex 11227	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
129		fnconstg 6765	. . . . . . . . . . . . 13 ⊢ (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
130	128, 129	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((1...𝑁) × {0}) Fn (1...𝑁)
131		nfcv 2898	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛((ℂfld ↾s ℚ) freeLMod (1...𝑁))
132		nfcv 2898	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛 Σg
133		nfcv 2898	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛𝑤
134		nfcv 2898	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
135		nfcv 2898	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛(0...𝑁)
136		nfmpt1 5220	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛(𝑛 ∈ (1...𝑁) ↦ 𝐶)
137	135, 136	nfmpt 5219	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
138	133, 134, 137	nfov 7433	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
139	131, 132, 138	nfov 7433	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))
140		nfcv 2898	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛((1...𝑁) × {0})
141	139, 140	eqfnfv2f 7024	. . . . . . . . . . . 12 ⊢ (((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁) ∧ ((1...𝑁) × {0}) Fn (1...𝑁)) → ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
142	127, 130, 141	sylancl 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
143	117	fveq1d 6877	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛))
144		sumex 15702	. . . . . . . . . . . . . . 15 ⊢ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ V
145		eqid 2735	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
146	145	fvmpt2 6996	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (1...𝑁) ∧ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ V) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
147	144, 146	mpan2 691	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
148	143, 147	sylan9eq 2790	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
149	128	fvconst2 7195	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
150	149	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
151	148, 150	eqeq12d 2751	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
152	151	ralbidva 3161	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (∀𝑛 ∈ (1...𝑁)((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
153	142, 152	bitrd 279	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
154	153	imbi1d 341	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ (∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
155	42, 154	sylan2 593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (ℚ ↑m (0...𝑁))) → (((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ (∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
156	155	ralbidva 3161	. . . . . . 7 ⊢ (𝜑 → (∀𝑤 ∈ (ℚ ↑m (0...𝑁))((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
157	41, 156	bitrd 279	. . . . . 6 ⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
158		drngnzr 20706	. . . . . . . . 9 ⊢ ((ℂfld ↾s ℚ) ∈ DivRing → (ℂfld ↾s ℚ) ∈ NzRing)
159	19, 158	ax-mp 5	. . . . . . . 8 ⊢ (ℂfld ↾s ℚ) ∈ NzRing
160	31	islindf3 21784	. . . . . . . 8 ⊢ ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂfld ↾s ℚ) ∈ NzRing) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))))
161	25, 159, 160	mp2an 692	. . . . . . 7 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
162		eqid 2735	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
163	45, 162	dmmpti 6681	. . . . . . . . 9 ⊢ dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (0...𝑁)
164		f1eq2 6769	. . . . . . . . 9 ⊢ (dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (0...𝑁) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ↔ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V))
165	163, 164	ax-mp 5	. . . . . . . 8 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ↔ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V)
166	165	anbi1i 624	. . . . . . 7 ⊢ (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
167	161, 166	bitri 275	. . . . . 6 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
168		con34b 316	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ (¬ 𝑤 = ((0...𝑁) × {0}) → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
169		df-nel 3037	. . . . . . . . . . 11 ⊢ (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬ 𝑤 ∈ {((0...𝑁) × {0})})
170		velsn 4617	. . . . . . . . . . 11 ⊢ (𝑤 ∈ {((0...𝑁) × {0})} ↔ 𝑤 = ((0...𝑁) × {0}))
171	169, 170	xchbinx 334	. . . . . . . . . 10 ⊢ (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬ 𝑤 = ((0...𝑁) × {0}))
172	171	imbi1i 349	. . . . . . . . 9 ⊢ ((𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ↔ (¬ 𝑤 = ((0...𝑁) × {0}) → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
173	168, 172	bitr4i 278	. . . . . . . 8 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ (𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
174	173	ralbii 3082	. . . . . . 7 ⊢ (∀𝑤 ∈ (ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
175		raldifb 4124	. . . . . . 7 ⊢ (∀𝑤 ∈ (ℚ ↑m (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ↔ ∀𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
176		ralnex 3062	. . . . . . 7 ⊢ (∀𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ↔ ¬ ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
177	174, 175, 176	3bitri 297	. . . . . 6 ⊢ (∀𝑤 ∈ (ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ¬ ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
178	157, 167, 177	3bitr3g 313	. . . . 5 ⊢ (𝜑 → (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) ↔ ¬ ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
179		eqid 2735	. . . . . . . . . . . . 13 ⊢ (LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = (LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
180	29, 179	lssmre 20921	. . . . . . . . . . . 12 ⊢ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod → (LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑m (1...𝑁))))
181	25, 180	ax-mp 5	. . . . . . . . . . 11 ⊢ (LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑m (1...𝑁)))
182	181	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → (LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑m (1...𝑁))))
183		eqid 2735	. . . . . . . . . . . 12 ⊢ (LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = (LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
184		eqid 2735	. . . . . . . . . . . 12 ⊢ (mrCls‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) = (mrCls‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
185	179, 183, 184	mrclsp 20944	. . . . . . . . . . 11 ⊢ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod → (LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = (mrCls‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
186	25, 185	ax-mp 5	. . . . . . . . . 10 ⊢ (LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = (mrCls‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
187		eqid 2735	. . . . . . . . . 10 ⊢ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) = (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
188	31	islvec 21060	. . . . . . . . . . . . 13 ⊢ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LVec ↔ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂfld ↾s ℚ) ∈ DivRing))
189	25, 19, 188	mpbir2an 711	. . . . . . . . . . . 12 ⊢ ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LVec
190	179, 186, 29	lssacsex 21103	. . . . . . . . . . . . 13 ⊢ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LVec → ((LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∈ (ACS‘(ℚ ↑m (1...𝑁))) ∧ ∀𝑧 ∈ 𝒫 (ℚ ↑m (1...𝑁))∀𝑥 ∈ (ℚ ↑m (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦}))))
191	190	simprd 495	. . . . . . . . . . . 12 ⊢ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LVec → ∀𝑧 ∈ 𝒫 (ℚ ↑m (1...𝑁))∀𝑥 ∈ (ℚ ↑m (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦})))
192	189, 191	ax-mp 5	. . . . . . . . . . 11 ⊢ ∀𝑧 ∈ 𝒫 (ℚ ↑m (1...𝑁))∀𝑥 ∈ (ℚ ↑m (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦}))
193	192	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → ∀𝑧 ∈ 𝒫 (ℚ ↑m (1...𝑁))∀𝑥 ∈ (ℚ ↑m (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦})))
194	17	frnd 6713	. . . . . . . . . . . 12 ⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ ↑m (1...𝑁)))
195		dif0 4353	. . . . . . . . . . . 12 ⊢ ((ℚ ↑m (1...𝑁)) ∖ ∅) = (ℚ ↑m (1...𝑁))
196	194, 195	sseqtrrdi 4000	. . . . . . . . . . 11 ⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((ℚ ↑m (1...𝑁)) ∖ ∅))
197	196	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((ℚ ↑m (1...𝑁)) ∖ ∅))
198		eqid 2735	. . . . . . . . . . . . . . 15 ⊢ ((ℂfld ↾s ℚ) unitVec (1...𝑁)) = ((ℂfld ↾s ℚ) unitVec (1...𝑁))
199	198, 23, 29	uvcff 21749	. . . . . . . . . . . . . 14 ⊢ (((ℂfld ↾s ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((ℂfld ↾s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑m (1...𝑁)))
200	21, 22, 199	mp2an 692	. . . . . . . . . . . . 13 ⊢ ((ℂfld ↾s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑m (1...𝑁))
201		frn 6712	. . . . . . . . . . . . 13 ⊢ (((ℂfld ↾s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑m (1...𝑁)) → ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ⊆ (ℚ ↑m (1...𝑁)))
202	200, 201	ax-mp 5	. . . . . . . . . . . 12 ⊢ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ⊆ (ℚ ↑m (1...𝑁))
203	202, 195	sseqtrri 4008	. . . . . . . . . . 11 ⊢ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ⊆ ((ℚ ↑m (1...𝑁)) ∖ ∅)
204	203	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ⊆ ((ℚ ↑m (1...𝑁)) ∖ ∅))
205		un0 4369	. . . . . . . . . . . . . 14 ⊢ (ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅) = ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))
206	205	fveq2i 6878	. . . . . . . . . . . . 13 ⊢ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅)) = ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
207		eqid 2735	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = (LBasis‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
208	23, 198, 207	frlmlbs 21755	. . . . . . . . . . . . . . 15 ⊢ (((ℂfld ↾s ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
209	21, 22, 208	mp2an 692	. . . . . . . . . . . . . 14 ⊢ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
210	29, 207, 183	lbssp 21035	. . . . . . . . . . . . . 14 ⊢ (ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) → ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) = (ℚ ↑m (1...𝑁)))
211	209, 210	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) = (ℚ ↑m (1...𝑁))
212	206, 211	eqtri 2758	. . . . . . . . . . . 12 ⊢ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅)) = (ℚ ↑m (1...𝑁))
213	194, 212	sseqtrrdi 4000	. . . . . . . . . . 11 ⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅)))
214	213	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅)))
215		un0 4369	. . . . . . . . . . 11 ⊢ (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) = ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
216	25, 159	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂfld ↾s ℚ) ∈ NzRing)
217	183, 31	lindsind2 21777	. . . . . . . . . . . . . 14 ⊢ (((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂfld ↾s ℚ) ∈ NzRing) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∧ 𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) → ¬ 𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
218	216, 217	mp3an1 1450	. . . . . . . . . . . . 13 ⊢ ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∧ 𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) → ¬ 𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
219	218	ralrimiva 3132	. . . . . . . . . . . 12 ⊢ (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) → ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
220	186, 187	ismri2 17642	. . . . . . . . . . . . . 14 ⊢ (((LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑m (1...𝑁))) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ ↑m (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) ↔ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))))
221	181, 194, 220	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) ↔ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))))
222	221	biimpar 477	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
223	219, 222	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
224	215, 223	eqeltrid 2838	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
225		mptfi 9361	. . . . . . . . . . . . 13 ⊢ ((0...𝑁) ∈ Fin → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin)
226		rnfi 9350	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin)
227	26, 225, 226	mp2b 10	. . . . . . . . . . . 12 ⊢ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin
228	227	orci 865	. . . . . . . . . . 11 ⊢ (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin ∨ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ Fin)
229	228	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin ∨ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ Fin))
230	182, 186, 187, 193, 197, 204, 214, 224, 229	mreexexd 17658	. . . . . . . . 9 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → ∃𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))))
231	230	ex 412	. . . . . . . 8 ⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) → ∃𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))))
232		ovex 7436	. . . . . . . . . . . . 13 ⊢ ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V
233	232	rnex 7904	. . . . . . . . . . . 12 ⊢ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V
234		elpwi 4582	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → 𝑣 ⊆ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
235		ssdomg 9012	. . . . . . . . . . . 12 ⊢ (ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V → (𝑣 ⊆ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → 𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))))
236	233, 234, 235	mpsyl 68	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → 𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
237		endomtr 9024	. . . . . . . . . . . . . 14 ⊢ ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ 𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
238	237	ancoms 458	. . . . . . . . . . . . 13 ⊢ ((𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
239		f1f1orn 6828	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1-onto→ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
240		ovex 7436	. . . . . . . . . . . . . . . . 17 ⊢ (0...𝑁) ∈ V
241	240	f1oen 8985	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1-onto→ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) → (0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
242	239, 241	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
243		endomtr 9024	. . . . . . . . . . . . . . . . 17 ⊢ (((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → (0...𝑁) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
244	198	uvcendim 21805	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℂfld ↾s ℚ) ∈ NzRing ∧ (1...𝑁) ∈ Fin) → (1...𝑁) ≈ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
245	159, 22, 244	mp2an 692	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑁) ≈ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))
246	245	ensymi 9016	. . . . . . . . . . . . . . . . . 18 ⊢ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)
247		domentr 9025	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0...𝑁) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (0...𝑁) ≼ (1...𝑁))
248		hashdom 14395	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((0...𝑁) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((♯‘(0...𝑁)) ≤ (♯‘(1...𝑁)) ↔ (0...𝑁) ≼ (1...𝑁)))
249	26, 22, 248	mp2an 692	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘(0...𝑁)) ≤ (♯‘(1...𝑁)) ↔ (0...𝑁) ≼ (1...𝑁))
250		hashfz0 14448	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ0 → (♯‘(0...𝑁)) = (𝑁 + 1))
251	2, 250	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘(0...𝑁)) = (𝑁 + 1))
252		hashfz1 14362	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
253	2, 252	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
254	251, 253	breq12d 5132	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((♯‘(0...𝑁)) ≤ (♯‘(1...𝑁)) ↔ (𝑁 + 1) ≤ 𝑁))
255	249, 254	bitr3id 285	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((0...𝑁) ≼ (1...𝑁) ↔ (𝑁 + 1) ≤ 𝑁))
256	247, 255	imbitrid 244	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((0...𝑁) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (𝑁 + 1) ≤ 𝑁))
257	246, 256	mpan2i 697	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((0...𝑁) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁))
258	243, 257	syl5 34	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → (𝑁 + 1) ≤ 𝑁))
259	258	expd 415	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁)))
260	242, 259	syl5 34	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁)))
261	260	com23 86	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
262	238, 261	syl5 34	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
263	262	expdimp 452	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
264	236, 263	sylan2 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
265	264	adantrd 491	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
266	265	rexlimdva 3141	. . . . . . . 8 ⊢ (𝜑 → (∃𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
267	231, 266	syld 47	. . . . . . 7 ⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
268	267	impd 410	. . . . . 6 ⊢ (𝜑 → ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∧ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V) → (𝑁 + 1) ≤ 𝑁))
269	268	ancomsd 465	. . . . 5 ⊢ (𝜑 → (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → (𝑁 + 1) ≤ 𝑁))
270	178, 269	sylbird 260	. . . 4 ⊢ (𝜑 → (¬ ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → (𝑁 + 1) ≤ 𝑁))
271	9, 270	mt3d 148	. . 3 ⊢ (𝜑 → ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
272		eldifsn 4762	. . . . 5 ⊢ (𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ↔ (𝑤 ∈ (ℚ ↑m (0...𝑁)) ∧ 𝑤 ≠ ((0...𝑁) × {0})))
273	42	anim1i 615	. . . . 5 ⊢ ((𝑤 ∈ (ℚ ↑m (0...𝑁)) ∧ 𝑤 ≠ ((0...𝑁) × {0})) → (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})))
274	272, 273	sylbi 217	. . . 4 ⊢ (𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) → (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})))
275	93	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ℚ ⊆ ℂ)
276	2	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑁 ∈ ℕ0)
277	275, 276, 53	elplyd 26157	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ (Poly‘ℚ))
278	277	adantrr 717	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ (Poly‘ℚ))
279		uzdisj 13612	. . . . . . . . . . . . . . . . . 18 ⊢ ((0...((𝑁 + 1) − 1)) ∩ (ℤ≥‘(𝑁 + 1))) = ∅
280	2	nn0cnd 12562	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑁 ∈ ℂ)
281		pncan1 11659	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
282	280, 281	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
283	282	oveq2d 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁))
284	283	ineq1d 4194	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∩ (ℤ≥‘(𝑁 + 1))) = ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))))
285	279, 284	eqtr3id 2784	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∅ = ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))))
286	285	eqcomd 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅)
287	128	fconst 6763	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶{0}
288		snssi 4784	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℚ → {0} ⊆ ℚ)
289	96, 97, 288	mp2b 10	. . . . . . . . . . . . . . . . . . 19 ⊢ {0} ⊆ ℚ
290	289, 93	sstri 3968	. . . . . . . . . . . . . . . . . 18 ⊢ {0} ⊆ ℂ
291		fss 6721	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℂ) → ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℂ)
292	287, 290, 291	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℂ
293		fun 6739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑤:(0...𝑁)⟶ℚ ∧ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℂ) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
294	292, 293	mpanl2 701	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
295	286, 294	sylan2 593	. . . . . . . . . . . . . . 15 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝜑) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
296	295	ancoms 458	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
297		nn0uz 12892	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ0 = (ℤ≥‘0)
298	6, 297	eleqtrdi 2844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ≥‘0))
299		uzsplit 13611	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘0) → (ℤ≥‘0) = ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))))
300	298, 299	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℤ≥‘0) = ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))))
301	297, 300	eqtrid 2782	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ℕ0 = ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))))
302	283	uneq1d 4142	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))) = ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))))
303	301, 302	eqtr2d 2771	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))) = ℕ0)
304		ssequn1 4161	. . . . . . . . . . . . . . . . . 18 ⊢ (ℚ ⊆ ℂ ↔ (ℚ ∪ ℂ) = ℂ)
305	93, 304	mpbi 230	. . . . . . . . . . . . . . . . 17 ⊢ (ℚ ∪ ℂ) = ℂ
306	305	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℚ ∪ ℂ) = ℂ)
307	303, 306	feq23d 6700	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ) ↔ (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):ℕ0⟶ℂ))
308	307	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ) ↔ (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):ℕ0⟶ℂ))
309	296, 308	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):ℕ0⟶ℂ)
310		ffn 6705	. . . . . . . . . . . . . . . 16 ⊢ (𝑤:(0...𝑁)⟶ℚ → 𝑤 Fn (0...𝑁))
311		fnimadisj 6669	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) → (𝑤 “ (ℤ≥‘(𝑁 + 1))) = ∅)
312	310, 286, 311	syl2anr 597	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 “ (ℤ≥‘(𝑁 + 1))) = ∅)
313	2	nn0zd 12612	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℤ)
314	313	peano2zd 12698	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
315		uzid 12865	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 + 1) ∈ ℤ → (𝑁 + 1) ∈ (ℤ≥‘(𝑁 + 1)))
316		ne0i 4316	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘(𝑁 + 1)) → (ℤ≥‘(𝑁 + 1)) ≠ ∅)
317	314, 315, 316	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℤ≥‘(𝑁 + 1)) ≠ ∅)
318		inidm 4202	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℤ≥‘(𝑁 + 1)) ∩ (ℤ≥‘(𝑁 + 1))) = (ℤ≥‘(𝑁 + 1))
319	318	neeq1i 2996	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℤ≥‘(𝑁 + 1)) ∩ (ℤ≥‘(𝑁 + 1))) ≠ ∅ ↔ (ℤ≥‘(𝑁 + 1)) ≠ ∅)
320	317, 319	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((ℤ≥‘(𝑁 + 1)) ∩ (ℤ≥‘(𝑁 + 1))) ≠ ∅)
321		xpima2 6173	. . . . . . . . . . . . . . . . 17 ⊢ (((ℤ≥‘(𝑁 + 1)) ∩ (ℤ≥‘(𝑁 + 1))) ≠ ∅ → (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1))) = {0})
322	320, 321	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1))) = {0})
323	322	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1))) = {0})
324	312, 323	uneq12d 4144	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 “ (ℤ≥‘(𝑁 + 1))) ∪ (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1)))) = (∅ ∪ {0}))
325		imaundir 6139	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) “ (ℤ≥‘(𝑁 + 1))) = ((𝑤 “ (ℤ≥‘(𝑁 + 1))) ∪ (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1))))
326		uncom 4133	. . . . . . . . . . . . . . 15 ⊢ (∅ ∪ {0}) = ({0} ∪ ∅)
327		un0 4369	. . . . . . . . . . . . . . 15 ⊢ ({0} ∪ ∅) = {0}
328	326, 327	eqtr2i 2759	. . . . . . . . . . . . . 14 ⊢ {0} = (∅ ∪ {0})
329	324, 325, 328	3eqtr4g 2795	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) “ (ℤ≥‘(𝑁 + 1))) = {0})
330	286, 310	anim12ci 614	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅))
331		fnconstg 6765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ V → ((ℤ≥‘(𝑁 + 1)) × {0}) Fn (ℤ≥‘(𝑁 + 1)))
332	128, 331	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ≥‘(𝑁 + 1)) × {0}) Fn (ℤ≥‘(𝑁 + 1))
333		fvun1 6969	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 Fn (0...𝑁) ∧ ((ℤ≥‘(𝑁 + 1)) × {0}) Fn (ℤ≥‘(𝑁 + 1)) ∧ (((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ ∧ 𝑘 ∈ (0...𝑁))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘))
334	332, 333	mp3an2 1451	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 Fn (0...𝑁) ∧ (((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ ∧ 𝑘 ∈ (0...𝑁))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘))
335	334	anassrs 467	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘))
336	330, 335	sylan 580	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘))
337	336	eqcomd 2741	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) = ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘))
338	337	oveq1d 7418	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝑦↑𝑘)) = (((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘)))
339	338	sumeq2dv 15716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘)))
340	339	mpteq2dv 5215	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘))))
341	277, 276, 309, 329, 340	coeeq 26182	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) = (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})))
342	341	reseq1d 5965	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)))
343		res0 5970	. . . . . . . . . . . . . 14 ⊢ (𝑤 ↾ ∅) = ∅
344	285	reseq2d 5966	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑤 ↾ ∅) = (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))))
345		res0 5970	. . . . . . . . . . . . . . 15 ⊢ (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ∅) = ∅
346	285	reseq2d 5966	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ∅) = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))))
347	345, 346	eqtr3id 2784	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∅ = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))))
348	343, 344, 347	3eqtr3a 2794	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))))
349		fss 6721	. . . . . . . . . . . . . . 15 ⊢ ((((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℚ) → ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℚ)
350	287, 289, 349	mp2an 692	. . . . . . . . . . . . . 14 ⊢ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℚ
351		fresaunres1 6750	. . . . . . . . . . . . . 14 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℚ ∧ (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
352	350, 351	mp3an2 1451	. . . . . . . . . . . . 13 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
353	348, 352	sylan2 593	. . . . . . . . . . . 12 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝜑) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
354	353	ancoms 458	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
355	342, 354	eqtrd 2770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤)
356		fveq2 6875	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 → (coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) = (coeff‘0𝑝))
357	356	reseq1d 5965	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁)))
358		eqtr2 2756	. . . . . . . . . . . 12 ⊢ ((((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁))) → 𝑤 = ((coeff‘0𝑝) ↾ (0...𝑁)))
359		coe0 26211	. . . . . . . . . . . . . 14 ⊢ (coeff‘0𝑝) = (ℕ0 × {0})
360	359	reseq1i 5962	. . . . . . . . . . . . 13 ⊢ ((coeff‘0𝑝) ↾ (0...𝑁)) = ((ℕ0 × {0}) ↾ (0...𝑁))
361		elfznn0 13635	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℕ0)
362	361	ssriv 3962	. . . . . . . . . . . . . 14 ⊢ (0...𝑁) ⊆ ℕ0
363		xpssres 6005	. . . . . . . . . . . . . 14 ⊢ ((0...𝑁) ⊆ ℕ0 → ((ℕ0 × {0}) ↾ (0...𝑁)) = ((0...𝑁) × {0}))
364	362, 363	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((ℕ0 × {0}) ↾ (0...𝑁)) = ((0...𝑁) × {0})
365	360, 364	eqtri 2758	. . . . . . . . . . . 12 ⊢ ((coeff‘0𝑝) ↾ (0...𝑁)) = ((0...𝑁) × {0})
366	358, 365	eqtrdi 2786	. . . . . . . . . . 11 ⊢ ((((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁))) → 𝑤 = ((0...𝑁) × {0}))
367	366	ex 412	. . . . . . . . . 10 ⊢ (((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 → (((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁)) → 𝑤 = ((0...𝑁) × {0})))
368	355, 357, 367	syl2im 40	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 → 𝑤 = ((0...𝑁) × {0})))
369	368	necon3d 2953	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ≠ ((0...𝑁) × {0}) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠ 0𝑝))
370	369	impr 454	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠ 0𝑝)
371		eldifsn 4762	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}) ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ (Poly‘ℚ) ∧ (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠ 0𝑝))
372	278, 370, 371	sylanbrc 583	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}))
373	372	adantrr 717	. . . . 5 ⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}))
374		oveq1 7410	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐴 → (𝑦↑𝑘) = (𝐴↑𝑘))
375	374	oveq2d 7419	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐴 → ((𝑤‘𝑘) · (𝑦↑𝑘)) = ((𝑤‘𝑘) · (𝐴↑𝑘)))
376	375	sumeq2sdv 15717	. . . . . . . . . 10 ⊢ (𝑦 = 𝐴 → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
377		eqid 2735	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))
378		sumex 15702	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) ∈ V
379	376, 377, 378	fvmpt 6985	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
380	1, 379	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
381	380	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
382	107	adantll 714	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
383		aacllem.2	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
384	383	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
385	110, 384	mulcld 11253	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ)
386	385	adantllr 719	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ)
387	51, 382, 386	fsummulc2 15798	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)) = Σ𝑛 ∈ (1...𝑁)((𝑤‘𝑘) · (𝐶 · 𝑋)))
388		aacllem.4	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑𝑘) = Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋))
389	388	oveq2d 7419	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)))
390	389	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)))
391	382	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
392	110	adantllr 719	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℂ)
393		simpll 766	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → 𝜑)
394	393, 383	sylan 580	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
395	391, 392, 394	mulassd 11256	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑤‘𝑘) · 𝐶) · 𝑋) = ((𝑤‘𝑘) · (𝐶 · 𝑋)))
396	395	sumeq2dv 15716	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)((𝑤‘𝑘) · (𝐶 · 𝑋)))
397	387, 390, 396	3eqtr4d 2780	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
398	397	sumeq2dv 15716	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑘 ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
399	107	ad2ant2lr 748	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (𝑤‘𝑘) ∈ ℂ)
400	110	anasss 466	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝐶 ∈ ℂ)
401	400	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝐶 ∈ ℂ)
402	399, 401	mulcld 11253	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → ((𝑤‘𝑘) · 𝐶) ∈ ℂ)
403	383	ad2ant2rl 749	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝑋 ∈ ℂ)
404	402, 403	mulcld 11253	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (((𝑤‘𝑘) · 𝐶) · 𝑋) ∈ ℂ)
405	43, 69, 404	fsumcom 15789	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
406	398, 405	eqtrd 2770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
407	406	adantrr 717	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
408		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛𝜑
409		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛 𝑤:(0...𝑁)⟶ℚ
410		nfra1 3266	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0
411	409, 410	nfan 1899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
412	408, 411	nfan 1899	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
413		rspa 3231	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
414	413	oveq1d 7418	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
415	414	adantll 714	. . . . . . . . . . . . . 14 ⊢ (((𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
416	415	adantll 714	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
417	383	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
418	92, 417, 113	fsummulc1 15799	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
419	418	adantlrr 721	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
420	383	mul02d 11431	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0)
421	420	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0)
422	416, 419, 421	3eqtr3d 2778	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0)
423	422	ex 412	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → (𝑛 ∈ (1...𝑁) → Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0))
424	412, 423	ralrimi 3240	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0)
425	424	sumeq2d 15715	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)0)
426	407, 425	eqtrd 2770	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)0)
427	22	olci 866	. . . . . . . . 9 ⊢ ((1...𝑁) ⊆ (ℤ≥‘𝐵) ∨ (1...𝑁) ∈ Fin)
428		sumz 15736	. . . . . . . . 9 ⊢ (((1...𝑁) ⊆ (ℤ≥‘𝐵) ∨ (1...𝑁) ∈ Fin) → Σ𝑛 ∈ (1...𝑁)0 = 0)
429	427, 428	ax-mp 5	. . . . . . . 8 ⊢ Σ𝑛 ∈ (1...𝑁)0 = 0
430	426, 429	eqtrdi 2786	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = 0)
431	381, 430	eqtrd 2770	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0)
432	431	adantrlr 723	. . . . 5 ⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0)
433		fveq1 6874	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) → (𝑥‘𝐴) = ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴))
434	433	eqeq1d 2737	. . . . . 6 ⊢ (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) → ((𝑥‘𝐴) = 0 ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0))
435	434	rspcev 3601	. . . . 5 ⊢ (((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}) ∧ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0)
436	373, 432, 435	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0)
437	274, 436	sylanr1 682	. . 3 ⊢ ((𝜑 ∧ (𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0)
438	271, 437	rexlimddv 3147	. 2 ⊢ (𝜑 → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0)
439		elqaa 26280	. 2 ⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧ ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0))
440	1, 438, 439	sylanbrc 583	1 ⊢ (𝜑 → 𝐴 ∈ 𝔸)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108   ≠ wne 2932   ∉ wnel 3036  ∀wral 3051  ∃wrex 3060  Vcvv 3459   ∖ cdif 3923   ∪ cun 3924   ∩ cin 3925   ⊆ wss 3926  ∅c0 4308  𝒫 cpw 4575  {csn 4601   class class class wbr 5119   ↦ cmpt 5201   × cxp 5652  dom cdm 5654  ran crn 5655   ↾ cres 5656   “ cima 5657   Fn wfn 6525  ⟶wf 6526  –1-1→wf1 6527  –1-1-onto→wf1o 6529  ‘cfv 6530  (class class class)co 7403   ∘_f cof 7667   ↑_m cmap 8838   ≈ cen 8954   ≼ cdom 8955  Fincfn 8957  ℂcc 11125  0cc0 11127  1c1 11128   + caddc 11130   · cmul 11132   < clt 11267   ≤ cle 11268   − cmin 11464  ℕ₀cn0 12499  ℤcz 12586  ℤ_≥cuz 12850  ℚcq 12962  ...cfz 13522  ↑cexp 14077  ♯chash 14346  Σcsu 15700  Basecbs 17226   ↾_s cress 17249  ._rcmulr 17270  Scalarcsca 17272   ·_𝑠 cvsca 17273  0_gc0g 17451   Σ_g cgsu 17452  Moorecmre 17592  mrClscmrc 17593  mrIndcmri 17594  ACScacs 17595  Ringcrg 20191  NzRingcnzr 20470  DivRingcdr 20687  LModclmod 20815  LSubSpclss 20886  LSpanclspn 20926  LBasisclbs 21030  LVecclvec 21058  ℂ_fldccnfld 21313   freeLMod cfrlm 21704   unitVec cuvc 21740   LIndF clindf 21762  LIndSclinds 21763  0_𝑝c0p 25620  Polycply 26139  coeffccoe 26141  𝔸caa 26272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-inf2 9653  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204  ax-pre-sup 11205  ax-addf 11206  ax-mulf 11207

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-tp 4606  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-iin 4970  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-se 5607  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-isom 6539  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-of 7669  df-om 7860  df-1st 7986  df-2nd 7987  df-supp 8158  df-tpos 8223  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-2o 8479  df-oadd 8482  df-er 8717  df-map 8840  df-pm 8841  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fsupp 9372  df-sup 9452  df-inf 9453  df-oi 9522  df-card 9951  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-div 11893  df-nn 12239  df-2 12301  df-3 12302  df-4 12303  df-5 12304  df-6 12305  df-7 12306  df-8 12307  df-9 12308  df-n0 12500  df-xnn0 12573  df-z 12587  df-dec 12707  df-uz 12851  df-q 12963  df-rp 13007  df-fz 13523  df-fzo 13670  df-fl 13807  df-mod 13885  df-seq 14018  df-exp 14078  df-hash 14347  df-cj 15116  df-re 15117  df-im 15118  df-sqrt 15252  df-abs 15253  df-clim 15502  df-rlim 15503  df-sum 15701  df-struct 17164  df-sets 17181  df-slot 17199  df-ndx 17211  df-base 17227  df-ress 17250  df-plusg 17282  df-mulr 17283  df-starv 17284  df-sca 17285  df-vsca 17286  df-ip 17287  df-tset 17288  df-ple 17289  df-ds 17291  df-unif 17292  df-hom 17293  df-cco 17294  df-0g 17453  df-gsum 17454  df-prds 17459  df-pws 17461  df-mre 17596  df-mrc 17597  df-mri 17598  df-acs 17599  df-mgm 18616  df-sgrp 18695  df-mnd 18711  df-mhm 18759  df-submnd 18760  df-grp 18917  df-minusg 18918  df-sbg 18919  df-mulg 19049  df-subg 19104  df-ghm 19194  df-cntz 19298  df-cmn 19761  df-abl 19762  df-mgp 20099  df-rng 20111  df-ur 20140  df-ring 20193  df-cring 20194  df-oppr 20295  df-dvdsr 20315  df-unit 20316  df-invr 20346  df-dvr 20359  df-nzr 20471  df-subrng 20504  df-subrg 20528  df-drng 20689  df-lmod 20817  df-lss 20887  df-lsp 20927  df-lmhm 20978  df-lbs 21031  df-lvec 21059  df-sra 21129  df-rgmod 21130  df-cnfld 21314  df-dsmm 21690  df-frlm 21705  df-uvc 21741  df-lindf 21764  df-linds 21765  df-0p 25621  df-ply 26143  df-coe 26145  df-dgr 26146  df-aa 26273

This theorem is referenced by: (None)