Theorem aacllem 51107

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 12671	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ)
4	3	ltp1d 12250	. . . . 5 ⊢ (𝜑 → 𝑁 < (𝑁 + 1))
5		peano2nn0 12649	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
6	2, 5	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ0)
7	6	nn0red 12671	. . . . . 6 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
8	3, 7	ltnled 11460	. . . . 5 ⊢ (𝜑 → (𝑁 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑁))
9	4, 8	mpbid 235	. . . 4 ⊢ (𝜑 → ¬ (𝑁 + 1) ≤ 𝑁)
10		aacllem.3	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
11	10	3expa 1136	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
12	11	fmpttd 7115	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ)
13		qex 13091	. . . . . . . . . . 11 ⊢ ℚ ∈ V
14		ovex 7453	. . . . . . . . . . 11 ⊢ (1...𝑁) ∈ V
15	13, 14	elmap 8902	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ)
16	12, 15	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m (1...𝑁)))
17	16	fmpttd 7115	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑m (1...𝑁)))
18		eqid 2760	. . . . . . . . . . . 12 ⊢ (ℂfld ↾s ℚ) = (ℂfld ↾s ℚ)
19	18	qdrng 27952	. . . . . . . . . . 11 ⊢ (ℂfld ↾s ℚ) ∈ DivRing
20		drngring 20992	. . . . . . . . . . 11 ⊢ ((ℂfld ↾s ℚ) ∈ DivRing → (ℂfld ↾s ℚ) ∈ Ring)
21	19, 20	ax-mp 5	. . . . . . . . . 10 ⊢ (ℂfld ↾s ℚ) ∈ Ring
22		fzfi 14118	. . . . . . . . . 10 ⊢ (1...𝑁) ∈ Fin
23		eqid 2760	. . . . . . . . . . 11 ⊢ ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) = ((ℂfld ↾s ℚ) freeLMod (1...𝑁))
24	23	frlmlmod 22060	. . . . . . . . . 10 ⊢ (((ℂfld ↾s ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod)
25	21, 22, 24	mp2an 705	. . . . . . . . 9 ⊢ ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod
26		fzfi 14118	. . . . . . . . 9 ⊢ (0...𝑁) ∈ Fin
27	18	qrngbas 27951	. . . . . . . . . . . 12 ⊢ ℚ = (Base‘(ℂfld ↾s ℚ))
28	23, 27	frlmfibas 22073	. . . . . . . . . . 11 ⊢ (((ℂfld ↾s ℚ) ∈ DivRing ∧ (1...𝑁) ∈ Fin) → (ℚ ↑m (1...𝑁)) = (Base‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
29	19, 22, 28	mp2an 705	. . . . . . . . . 10 ⊢ (ℚ ↑m (1...𝑁)) = (Base‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
30	23	frlmsca 22064	. . . . . . . . . . 11 ⊢ (((ℂfld ↾s ℚ) ∈ DivRing ∧ (1...𝑁) ∈ Fin) → (ℂfld ↾s ℚ) = (Scalar‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
31	19, 22, 30	mp2an 705	. . . . . . . . . 10 ⊢ (ℂfld ↾s ℚ) = (Scalar‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
32		eqid 2760	. . . . . . . . . 10 ⊢ ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
33	18	qrng0 27953	. . . . . . . . . . . 12 ⊢ 0 = (0g‘(ℂfld ↾s ℚ))
34	23, 33	frlm0 22065	. . . . . . . . . . 11 ⊢ (((ℂfld ↾s ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((1...𝑁) × {0}) = (0g‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
35	21, 22, 34	mp2an 705	. . . . . . . . . 10 ⊢ ((1...𝑁) × {0}) = (0g‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
36		eqid 2760	. . . . . . . . . . . 12 ⊢ ((ℂfld ↾s ℚ) freeLMod (0...𝑁)) = ((ℂfld ↾s ℚ) freeLMod (0...𝑁))
37	36, 27	frlmfibas 22073	. . . . . . . . . . 11 ⊢ (((ℂfld ↾s ℚ) ∈ DivRing ∧ (0...𝑁) ∈ Fin) → (ℚ ↑m (0...𝑁)) = (Base‘((ℂfld ↾s ℚ) freeLMod (0...𝑁))))
38	19, 26, 37	mp2an 705	. . . . . . . . . 10 ⊢ (ℚ ↑m (0...𝑁)) = (Base‘((ℂfld ↾s ℚ) freeLMod (0...𝑁)))
39	29, 31, 32, 35, 33, 38	islindf4 22149	. . . . . . . . 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 1480	. . . . . . . 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 18	. . . . . . 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 8872	. . . . . . . . 9 ⊢ (𝑤 ∈ (ℚ ↑m (0...𝑁)) → 𝑤:(0...𝑁)⟶ℚ)
43		fzfid 14119	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (0...𝑁) ∈ Fin)
44		fvexd 6900	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ V)
45	14	mptex 7229	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V
46	45	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V)
47		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑤:(0...𝑁)⟶ℚ)
48	47	feqmptd 6953	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑤 = (𝑘 ∈ (0...𝑁) ↦ (𝑤‘𝑘)))
49		eqidd 2761	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
50	43, 44, 46, 48, 49	offval2 7713	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘)( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶))))
51		fzfid 14119	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
52		ffvelcdm 7081	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ)
53	52	adantll 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ)
54	16	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m (1...𝑁)))
55		cnfldmul 21691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ · = (.r‘ℂfld)
56	18, 55	ressmulr 17483	. . . . . . . . . . . . . . . . . . . . 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 22077	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘)( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (((1...𝑁) × {(𝑤‘𝑘)}) ∘f · (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
59		fvexd 6900	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤‘𝑘) ∈ V)
60	11	adantllr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
61		fconstmpt 5712	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1...𝑁) × {(𝑤‘𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤‘𝑘))
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((1...𝑁) × {(𝑤‘𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤‘𝑘)))
63		eqidd 2761	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) = (𝑛 ∈ (1...𝑁) ↦ 𝐶))
64	51, 59, 60, 62, 63	offval2 7713	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (((1...𝑁) × {(𝑤‘𝑘)}) ∘f · (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))
65	58, 64	eqtrd 2795	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘)( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))
66	65	mpteq2dva 5197	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘)( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))
67	50, 66	eqtrd 2795	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))
68	67	oveq2d 7436	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))))
69		fzfid 14119	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (1...𝑁) ∈ Fin)
70	21	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (ℂfld ↾s ℚ) ∈ Ring)
71	53	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ)
72	11	an32s 665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℚ)
73	72	adantllr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℚ)
74		qmulcl 13098	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤‘𝑘) ∈ ℚ ∧ 𝐶 ∈ ℚ) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ)
75	71, 73, 74	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ)
76	75	an32s 665	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ)
77	76	fmpttd 7115	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
78	13, 14	elmap 8902	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
79	77, 78	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)))
80		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))
81	14	mptex 7229	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ V
82	81	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ V)
83		snex 5396	. . . . . . . . . . . . . . . . . . 19 ⊢ {0} ∈ V
84	14, 83	xpex 7767	. . . . . . . . . . . . . . . . . 18 ⊢ ((1...𝑁) × {0}) ∈ V
85	84	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((1...𝑁) × {0}) ∈ V)
86	80, 43, 82, 85	fsuppmptdm 9371	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) finSupp ((1...𝑁) × {0}))
87	23, 29, 35, 69, 43, 70, 79, 86	frlmgsum 22083	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ ((ℂfld ↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))))
88		cnfldbas 21687	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ = (Base‘ℂfld)
89		cnfldadd 21689	. . . . . . . . . . . . . . . . . 18 ⊢ + = (+g‘ℂfld)
90		cnfldex 21686	. . . . . . . . . . . . . . . . . . 19 ⊢ ℂfld ∈ V
91	90	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℂfld ∈ V)
92		fzfid 14119	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (0...𝑁) ∈ Fin)
93		qsscn 13090	. . . . . . . . . . . . . . . . . . 19 ⊢ ℚ ⊆ ℂ
94	93	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℚ ⊆ ℂ)
95	75	fmpttd 7115	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(0...𝑁)⟶ℚ)
96		0z 12707	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℤ
97		zq 13084	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℤ → 0 ∈ ℚ)
98	96, 97	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℚ
99	98	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 0 ∈ ℚ)
100		addlid 11496	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℂ → (0 + 𝑥) = 𝑥)
101		addrid 11493	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℂ → (𝑥 + 0) = 𝑥)
102	100, 101	jca 521	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℂ → ((0 + 𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥))
103	102	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ ℂ) → ((0 + 𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥))
104	88, 89, 18, 91, 92, 94, 95, 99, 103	gsumress 18876	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂfld Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = ((ℂfld ↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))
105		simplr 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑤:(0...𝑁)⟶ℚ)
106		qcn 13093	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤‘𝑘) ∈ ℚ → (𝑤‘𝑘) ∈ ℂ)
107	52, 106	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
108	105, 107	sylan 592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
109		qcn 13093	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐶 ∈ ℚ → 𝐶 ∈ ℂ)
110	11, 109	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℂ)
111	110	an32s 665	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℂ)
112	111	adantllr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℂ)
113	108, 112	mulcld 11332	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℂ)
114	92, 113	gsumfsum 21745	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂfld Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
115	104, 114	eqtr3d 2797	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((ℂfld ↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
116	115	mpteq2dva 5197	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ ((ℂfld ↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)))
117	68, 87, 116	3eqtrd 2799	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)))
118		qaddcl 13096	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ) → (𝑥 + 𝑦) ∈ ℚ)
119	118	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) ∈ ℚ)
120	94, 119, 92, 75, 99	fsumcllem 15903	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ ℚ)
121	120	fmpttd 7115	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
122	13, 14	elmap 8902	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
123	121, 122	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)))
124	117, 123	eqeltrd 2860	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) ∈ (ℚ ↑m (1...𝑁)))
125		elmapi 8872	. . . . . . . . . . . . 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 6709	. . . . . . . . . . . . 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 19	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁))
128		c0ex 11303	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
129		fnconstg 6770	. . . . . . . . . . . . 13 ⊢ (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
130	128, 129	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((1...𝑁) × {0}) Fn (1...𝑁)
131		nfcv 2922	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛((ℂfld ↾s ℚ) freeLMod (1...𝑁))
132		nfcv 2922	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛 Σg
133		nfcv 2922	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛𝑤
134		nfcv 2922	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
135		nfcv 2922	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛(0...𝑁)
136		nfmpt1 5203	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛(𝑛 ∈ (1...𝑁) ↦ 𝐶)
137	135, 136	nfmpt 5202	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
138	133, 134, 137	nfov 7450	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
139	131, 132, 138	nfov 7450	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))
140		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛((1...𝑁) × {0})
141	139, 140	eqfnfv2f 7033	. . . . . . . . . . . 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 598	. . . . . . . . . . 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 6887	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛))
144		sumex 15860	. . . . . . . . . . . . . . 15 ⊢ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ V
145		eqid 2760	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
146	145	fvmpt2 7005	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (1...𝑁) ∧ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ V) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
147	144, 146	mpan2 704	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
148	143, 147	sylan9eq 2815	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
149	128	fvconst2 7210	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
150	149	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
151	148, 150	eqeq12d 2776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
152	151	ralbidva 3183	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (∀𝑛 ∈ (1...𝑁)((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
153	142, 152	bitrd 282	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
154	153	imbi1d 344	. . . . . . . . 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 605	. . . . . . . 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 3183	. . . . . . 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 282	. . . . . 6 ⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
158		drngnzr 21007	. . . . . . . . 9 ⊢ ((ℂfld ↾s ℚ) ∈ DivRing → (ℂfld ↾s ℚ) ∈ NzRing)
159	19, 158	ax-mp 5	. . . . . . . 8 ⊢ (ℂfld ↾s ℚ) ∈ NzRing
160	31	islindf3 22137	. . . . . . . 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 705	. . . . . . 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 2760	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
163	45, 162	dmmpti 6683	. . . . . . . . 9 ⊢ dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (0...𝑁)
164		f1eq2 6774	. . . . . . . . 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 636	. . . . . . 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 278	. . . . . 6 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
168		con34b 319	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ (¬ 𝑤 = ((0...𝑁) × {0}) → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
169		df-nel 3062	. . . . . . . . . . 11 ⊢ (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬ 𝑤 ∈ {((0...𝑁) × {0})})
170		velsn 4596	. . . . . . . . . . 11 ⊢ (𝑤 ∈ {((0...𝑁) × {0})} ↔ 𝑤 = ((0...𝑁) × {0}))
171	169, 170	xchbinx 337	. . . . . . . . . 10 ⊢ (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬ 𝑤 = ((0...𝑁) × {0}))
172	171	imbi1i 352	. . . . . . . . 9 ⊢ ((𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ↔ (¬ 𝑤 = ((0...𝑁) × {0}) → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
173	168, 172	bitr4i 281	. . . . . . . 8 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ (𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
174	173	ralbii 3108	. . . . . . 7 ⊢ (∀𝑤 ∈ (ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
175		raldifb 4085	. . . . . . 7 ⊢ (∀𝑤 ∈ (ℚ ↑m (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ↔ ∀𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
176		ralnex 3088	. . . . . . 7 ⊢ (∀𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ↔ ¬ ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
177	174, 175, 176	3bitri 300	. . . . . 6 ⊢ (∀𝑤 ∈ (ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ¬ ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
178	157, 167, 177	3bitr3g 316	. . . . 5 ⊢ (𝜑 → (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) ↔ ¬ ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
179		eqid 2760	. . . . . . . . . . . . 13 ⊢ (LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = (LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
180	29, 179	lssmre 21246	. . . . . . . . . . . 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 2760	. . . . . . . . . . . 12 ⊢ (LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = (LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
184		eqid 2760	. . . . . . . . . . . 12 ⊢ (mrCls‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) = (mrCls‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
185	179, 183, 184	mrclsp 21269	. . . . . . . . . . 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 2760	. . . . . . . . . 10 ⊢ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) = (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
188	31	islvec 21384	. . . . . . . . . . . . 13 ⊢ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LVec ↔ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂfld ↾s ℚ) ∈ DivRing))
189	25, 19, 188	mpbir2an 724	. . . . . . . . . . . 12 ⊢ ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LVec
190	179, 186, 29	lssacsex 21427	. . . . . . . . . . . . 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 501	. . . . . . . . . . . 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 6718	. . . . . . . . . . . 12 ⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ ↑m (1...𝑁)))
195		dif0 4326	. . . . . . . . . . . 12 ⊢ ((ℚ ↑m (1...𝑁)) ∖ ∅) = (ℚ ↑m (1...𝑁))
196	194, 195	sseqtrrdi 3949	. . . . . . . . . . 11 ⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((ℚ ↑m (1...𝑁)) ∖ ∅))
197	196	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((ℚ ↑m (1...𝑁)) ∖ ∅))
198		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ ((ℂfld ↾s ℚ) unitVec (1...𝑁)) = ((ℂfld ↾s ℚ) unitVec (1...𝑁))
199	198, 23, 29	uvcff 22102	. . . . . . . . . . . . . 14 ⊢ (((ℂfld ↾s ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((ℂfld ↾s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑m (1...𝑁)))
200	21, 22, 199	mp2an 705	. . . . . . . . . . . . 13 ⊢ ((ℂfld ↾s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑m (1...𝑁))
201		frn 6717	. . . . . . . . . . . . 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 3957	. . . . . . . . . . 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 4343	. . . . . . . . . . . . . 14 ⊢ (ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅) = ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))
206	205	fveq2i 6888	. . . . . . . . . . . . 13 ⊢ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅)) = ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
207		eqid 2760	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = (LBasis‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
208	23, 198, 207	frlmlbs 22108	. . . . . . . . . . . . . . 15 ⊢ (((ℂfld ↾s ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
209	21, 22, 208	mp2an 705	. . . . . . . . . . . . . 14 ⊢ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
210	29, 207, 183	lbssp 21359	. . . . . . . . . . . . . 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 2783	. . . . . . . . . . . 12 ⊢ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅)) = (ℚ ↑m (1...𝑁))
213	194, 212	sseqtrrdi 3949	. . . . . . . . . . 11 ⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅)))
214	213	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅)))
215		un0 4343	. . . . . . . . . . 11 ⊢ (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) = ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
216	25, 159	pm3.2i 476	. . . . . . . . . . . . . 14 ⊢ (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂfld ↾s ℚ) ∈ NzRing)
217	183, 31	lindsind2 22130	. . . . . . . . . . . . . 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 1477	. . . . . . . . . . . . 13 ⊢ ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∧ 𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) → ¬ 𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
219	218	ralrimiva 3154	. . . . . . . . . . . 12 ⊢ (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) → ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
220	186, 187	ismri2 17811	. . . . . . . . . . . . . 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 599	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) ↔ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))))
222	221	biimpar 483	. . . . . . . . . . . 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 605	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
224	215, 223	eqeltrid 2864	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
225		mptfi 9343	. . . . . . . . . . . . 13 ⊢ ((0...𝑁) ∈ Fin → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin)
226		rnfi 9332	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin)
227	26, 225, 226	mp2b 10	. . . . . . . . . . . 12 ⊢ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin
228	227	orci 879	. . . . . . . . . . 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 17827	. . . . . . . . 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 418	. . . . . . . 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 7453	. . . . . . . . . . . . 13 ⊢ ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V
233	232	rnex 7922	. . . . . . . . . . . 12 ⊢ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V
234		elpwi 4563	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → 𝑣 ⊆ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
235		ssdomg 9030	. . . . . . . . . . . 12 ⊢ (ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V → (𝑣 ⊆ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → 𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))))
236	233, 234, 235	mpsyl 69	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → 𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
237		endomtr 9042	. . . . . . . . . . . . . 14 ⊢ ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ 𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
238	237	ancoms 464	. . . . . . . . . . . . 13 ⊢ ((𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
239		f1f1orn 6836	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1-onto→ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
240		ovex 7453	. . . . . . . . . . . . . . . . 17 ⊢ (0...𝑁) ∈ V
241	240	f1oen 9002	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1-onto→ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) → (0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
242	239, 241	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
243		endomtr 9042	. . . . . . . . . . . . . . . . 17 ⊢ (((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → (0...𝑁) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
244	198	uvcendim 22158	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℂfld ↾s ℚ) ∈ NzRing ∧ (1...𝑁) ∈ Fin) → (1...𝑁) ≈ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
245	159, 22, 244	mp2an 705	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑁) ≈ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))
246	245	ensymi 9034	. . . . . . . . . . . . . . . . . 18 ⊢ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)
247		domentr 9043	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0...𝑁) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (0...𝑁) ≼ (1...𝑁))
248		hashdom 14526	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((0...𝑁) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((♯‘(0...𝑁)) ≤ (♯‘(1...𝑁)) ↔ (0...𝑁) ≼ (1...𝑁)))
249	26, 22, 248	mp2an 705	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘(0...𝑁)) ≤ (♯‘(1...𝑁)) ↔ (0...𝑁) ≼ (1...𝑁))
250		hashfz0 14580	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ0 → (♯‘(0...𝑁)) = (𝑁 + 1))
251	2, 250	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘(0...𝑁)) = (𝑁 + 1))
252		hashfz1 14493	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
253	2, 252	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
254	251, 253	breq12d 5115	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((♯‘(0...𝑁)) ≤ (♯‘(1...𝑁)) ↔ (𝑁 + 1) ≤ 𝑁))
255	249, 254	bitr3id 288	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((0...𝑁) ≼ (1...𝑁) ↔ (𝑁 + 1) ≤ 𝑁))
256	247, 255	imbitrid 247	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((0...𝑁) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (𝑁 + 1) ≤ 𝑁))
257	246, 256	mpan2i 710	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((0...𝑁) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁))
258	243, 257	syl5 35	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → (𝑁 + 1) ≤ 𝑁))
259	258	expd 421	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁)))
260	242, 259	syl5 35	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁)))
261	260	com23 87	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
262	238, 261	syl5 35	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
263	262	expdimp 458	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
264	236, 263	sylan2 605	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
265	264	adantrd 497	. . . . . . . . 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 3163	. . . . . . . 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 48	. . . . . . 7 ⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
268	267	impd 416	. . . . . 6 ⊢ (𝜑 → ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) ∧ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V) → (𝑁 + 1) ≤ 𝑁))
269	268	ancomsd 471	. . . . 5 ⊢ (𝜑 → (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → (𝑁 + 1) ≤ 𝑁))
270	178, 269	sylbird 263	. . . 4 ⊢ (𝜑 → (¬ ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → (𝑁 + 1) ≤ 𝑁))
271	9, 270	mt3d 149	. . 3 ⊢ (𝜑 → ∃𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
272		eldifsn 4744	. . . . 5 ⊢ (𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ↔ (𝑤 ∈ (ℚ ↑m (0...𝑁)) ∧ 𝑤 ≠ ((0...𝑁) × {0})))
273	42	anim1i 627	. . . . 5 ⊢ ((𝑤 ∈ (ℚ ↑m (0...𝑁)) ∧ 𝑤 ≠ ((0...𝑁) × {0})) → (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})))
274	272, 273	sylbi 220	. . . 4 ⊢ (𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) → (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})))
275	93	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ℚ ⊆ ℂ)
276	2	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑁 ∈ ℕ0)
277	275, 276, 53	elplyd 26525	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ (Poly‘ℚ))
278	277	adantrr 730	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ (Poly‘ℚ))
279		uzdisj 13734	. . . . . . . . . . . . . . . . . 18 ⊢ ((0...((𝑁 + 1) − 1)) ∩ (ℤ≥‘(𝑁 + 1))) = ∅
280	2	nn0cnd 12672	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑁 ∈ ℂ)
281		pncan1 11743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
282	280, 281	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
283	282	oveq2d 7436	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁))
284	283	ineq1d 4116	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∩ (ℤ≥‘(𝑁 + 1))) = ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))))
285	279, 284	eqtr3id 2809	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∅ = ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))))
286	285	eqcomd 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅)
287	128	fconst 6768	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶{0}
288		snssi 4742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℚ → {0} ⊆ ℚ)
289	96, 97, 288	mp2b 10	. . . . . . . . . . . . . . . . . . 19 ⊢ {0} ⊆ ℚ
290	289, 93	sstri 3917	. . . . . . . . . . . . . . . . . 18 ⊢ {0} ⊆ ℂ
291		fss 6726	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℂ) → ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℂ)
292	287, 290, 291	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℂ
293		fun 6744	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑤:(0...𝑁)⟶ℚ ∧ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℂ) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
294	292, 293	mpanl2 714	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
295	286, 294	sylan2 605	. . . . . . . . . . . . . . 15 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝜑) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
296	295	ancoms 464	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
297		nn0uz 13006	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ0 = (ℤ≥‘0)
298	6, 297	eleqtrdi 2870	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ≥‘0))
299		uzsplit 13733	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘0) → (ℤ≥‘0) = ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))))
300	298, 299	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℤ≥‘0) = ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))))
301	297, 300	eqtrid 2807	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ℕ0 = ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))))
302	283	uneq1d 4166	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))) = ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))))
303	301, 302	eqtr2d 2796	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))) = ℕ0)
304		ssequn1 4184	. . . . . . . . . . . . . . . . . 18 ⊢ (ℚ ⊆ ℂ ↔ (ℚ ∪ ℂ) = ℂ)
305	93, 304	mpbi 233	. . . . . . . . . . . . . . . . 17 ⊢ (ℚ ∪ ℂ) = ℂ
306	305	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℚ ∪ ℂ) = ℂ)
307	303, 306	feq23d 6704	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ) ↔ (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):ℕ0⟶ℂ))
308	307	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ) ↔ (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):ℕ0⟶ℂ))
309	296, 308	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})):ℕ0⟶ℂ)
310		ffn 6709	. . . . . . . . . . . . . . . 16 ⊢ (𝑤:(0...𝑁)⟶ℚ → 𝑤 Fn (0...𝑁))
311		fnimadisj 6671	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) → (𝑤 “ (ℤ≥‘(𝑁 + 1))) = ∅)
312	310, 286, 311	syl2anr 609	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 “ (ℤ≥‘(𝑁 + 1))) = ∅)
313	2	nn0zd 12721	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℤ)
314	313	peano2zd 12809	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
315		uzid 12983	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 + 1) ∈ ℤ → (𝑁 + 1) ∈ (ℤ≥‘(𝑁 + 1)))
316		ne0i 4286	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘(𝑁 + 1)) → (ℤ≥‘(𝑁 + 1)) ≠ ∅)
317	314, 315, 316	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℤ≥‘(𝑁 + 1)) ≠ ∅)
318		inidm 4123	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℤ≥‘(𝑁 + 1)) ∩ (ℤ≥‘(𝑁 + 1))) = (ℤ≥‘(𝑁 + 1))
319	318	neeq1i 3019	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℤ≥‘(𝑁 + 1)) ∩ (ℤ≥‘(𝑁 + 1))) ≠ ∅ ↔ (ℤ≥‘(𝑁 + 1)) ≠ ∅)
320	317, 319	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((ℤ≥‘(𝑁 + 1)) ∩ (ℤ≥‘(𝑁 + 1))) ≠ ∅)
321		xpima2 6175	. . . . . . . . . . . . . . . . 17 ⊢ (((ℤ≥‘(𝑁 + 1)) ∩ (ℤ≥‘(𝑁 + 1))) ≠ ∅ → (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1))) = {0})
322	320, 321	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1))) = {0})
323	322	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1))) = {0})
324	312, 323	uneq12d 4168	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 “ (ℤ≥‘(𝑁 + 1))) ∪ (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1)))) = (∅ ∪ {0}))
325		imaundir 6141	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) “ (ℤ≥‘(𝑁 + 1))) = ((𝑤 “ (ℤ≥‘(𝑁 + 1))) ∪ (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1))))
326		uncom 4157	. . . . . . . . . . . . . . 15 ⊢ (∅ ∪ {0}) = ({0} ∪ ∅)
327		un0 4343	. . . . . . . . . . . . . . 15 ⊢ ({0} ∪ ∅) = {0}
328	326, 327	eqtr2i 2784	. . . . . . . . . . . . . 14 ⊢ {0} = (∅ ∪ {0})
329	324, 325, 328	3eqtr4g 2820	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) “ (ℤ≥‘(𝑁 + 1))) = {0})
330	286, 310	anim12ci 626	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅))
331		fnconstg 6770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ V → ((ℤ≥‘(𝑁 + 1)) × {0}) Fn (ℤ≥‘(𝑁 + 1)))
332	128, 331	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ≥‘(𝑁 + 1)) × {0}) Fn (ℤ≥‘(𝑁 + 1))
333		fvun1 6976	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 Fn (0...𝑁) ∧ ((ℤ≥‘(𝑁 + 1)) × {0}) Fn (ℤ≥‘(𝑁 + 1)) ∧ (((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ ∧ 𝑘 ∈ (0...𝑁))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘))
334	332, 333	mp3an2 1478	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 Fn (0...𝑁) ∧ (((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ ∧ 𝑘 ∈ (0...𝑁))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘))
335	334	anassrs 473	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘))
336	330, 335	sylan 592	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘))
337	336	eqcomd 2766	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) = ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘))
338	337	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝑦↑𝑘)) = (((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘)))
339	338	sumeq2dv 15874	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘)))
340	339	mpteq2dv 5198	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘))))
341	277, 276, 309, 329, 340	coeeq 26551	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) = (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})))
342	341	reseq1d 5968	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)))
343		res0 5973	. . . . . . . . . . . . . 14 ⊢ (𝑤 ↾ ∅) = ∅
344	285	reseq2d 5969	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑤 ↾ ∅) = (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))))
345		res0 5973	. . . . . . . . . . . . . . 15 ⊢ (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ∅) = ∅
346	285	reseq2d 5969	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ∅) = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))))
347	345, 346	eqtr3id 2809	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∅ = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))))
348	343, 344, 347	3eqtr3a 2819	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))))
349		fss 6726	. . . . . . . . . . . . . . 15 ⊢ ((((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℚ) → ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℚ)
350	287, 289, 349	mp2an 705	. . . . . . . . . . . . . 14 ⊢ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℚ
351		fresaunres1 6755	. . . . . . . . . . . . . 14 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℚ ∧ (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
352	350, 351	mp3an2 1478	. . . . . . . . . . . . 13 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))))) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
353	348, 352	sylan2 605	. . . . . . . . . . . 12 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝜑) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
354	353	ancoms 464	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
355	342, 354	eqtrd 2795	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤)
356		fveq2 6885	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 → (coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) = (coeff‘0𝑝))
357	356	reseq1d 5968	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁)))
358		eqtr2 2781	. . . . . . . . . . . 12 ⊢ ((((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁))) → 𝑤 = ((coeff‘0𝑝) ↾ (0...𝑁)))
359		coe0 26580	. . . . . . . . . . . . . 14 ⊢ (coeff‘0𝑝) = (ℕ0 × {0})
360	359	reseq1i 5965	. . . . . . . . . . . . 13 ⊢ ((coeff‘0𝑝) ↾ (0...𝑁)) = ((ℕ0 × {0}) ↾ (0...𝑁))
361		elfznn0 13757	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℕ0)
362	361	ssriv 3912	. . . . . . . . . . . . . 14 ⊢ (0...𝑁) ⊆ ℕ0
363		xpssres 6006	. . . . . . . . . . . . . 14 ⊢ ((0...𝑁) ⊆ ℕ0 → ((ℕ0 × {0}) ↾ (0...𝑁)) = ((0...𝑁) × {0}))
364	362, 363	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((ℕ0 × {0}) ↾ (0...𝑁)) = ((0...𝑁) × {0})
365	360, 364	eqtri 2783	. . . . . . . . . . . 12 ⊢ ((coeff‘0𝑝) ↾ (0...𝑁)) = ((0...𝑁) × {0})
366	358, 365	eqtrdi 2811	. . . . . . . . . . 11 ⊢ ((((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁))) → 𝑤 = ((0...𝑁) × {0}))
367	366	ex 418	. . . . . . . . . 10 ⊢ (((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 → (((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁)) → 𝑤 = ((0...𝑁) × {0})))
368	355, 357, 367	syl2im 41	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 → 𝑤 = ((0...𝑁) × {0})))
369	368	necon3d 2976	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ≠ ((0...𝑁) × {0}) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠ 0𝑝))
370	369	impr 460	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠ 0𝑝)
371		eldifsn 4744	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}) ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ (Poly‘ℚ) ∧ (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠ 0𝑝))
372	278, 370, 371	sylanbrc 595	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}))
373	372	adantrr 730	. . . . 5 ⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}))
374		oveq1 7427	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐴 → (𝑦↑𝑘) = (𝐴↑𝑘))
375	374	oveq2d 7436	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐴 → ((𝑤‘𝑘) · (𝑦↑𝑘)) = ((𝑤‘𝑘) · (𝐴↑𝑘)))
376	375	sumeq2sdv 15875	. . . . . . . . . 10 ⊢ (𝑦 = 𝐴 → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
377		eqid 2760	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))
378		sumex 15860	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) ∈ V
379	376, 377, 378	fvmpt 6993	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
380	1, 379	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
381	380	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
382	107	adantll 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
383		aacllem.2	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
384	383	adantlr 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
385	110, 384	mulcld 11332	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ)
386	385	adantllr 732	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ)
387	51, 382, 386	fsummulc2 15955	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)) = Σ𝑛 ∈ (1...𝑁)((𝑤‘𝑘) · (𝐶 · 𝑋)))
388		aacllem.4	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑𝑘) = Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋))
389	388	oveq2d 7436	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)))
390	389	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)))
391	382	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
392	110	adantllr 732	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℂ)
393		simpll 779	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → 𝜑)
394	393, 383	sylan 592	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
395	391, 392, 394	mulassd 11335	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑤‘𝑘) · 𝐶) · 𝑋) = ((𝑤‘𝑘) · (𝐶 · 𝑋)))
396	395	sumeq2dv 15874	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)((𝑤‘𝑘) · (𝐶 · 𝑋)))
397	387, 390, 396	3eqtr4d 2805	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
398	397	sumeq2dv 15874	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑘 ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
399	107	ad2ant2lr 761	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (𝑤‘𝑘) ∈ ℂ)
400	110	anasss 472	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝐶 ∈ ℂ)
401	400	adantlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝐶 ∈ ℂ)
402	399, 401	mulcld 11332	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → ((𝑤‘𝑘) · 𝐶) ∈ ℂ)
403	383	ad2ant2rl 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝑋 ∈ ℂ)
404	402, 403	mulcld 11332	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (((𝑤‘𝑘) · 𝐶) · 𝑋) ∈ ℂ)
405	43, 69, 404	fsumcom 15946	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
406	398, 405	eqtrd 2795	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
407	406	adantrr 730	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
408		nfv 1946	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛𝜑
409		nfv 1946	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛 𝑤:(0...𝑁)⟶ℚ
410		nfra1 3286	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0
411	409, 410	nfan 1931	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
412	408, 411	nfan 1931	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
413		rspa 3251	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
414	413	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
415	414	adantll 727	. . . . . . . . . . . . . 14 ⊢ (((𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
416	415	adantll 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
417	383	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
418	92, 417, 113	fsummulc1 15956	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
419	418	adantlrr 734	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
420	383	mul02d 11511	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0)
421	420	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0)
422	416, 419, 421	3eqtr3d 2803	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0)
423	422	ex 418	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → (𝑛 ∈ (1...𝑁) → Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0))
424	412, 423	ralrimi 3260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0)
425	424	sumeq2d 15873	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)0)
426	407, 425	eqtrd 2795	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)0)
427	22	olci 880	. . . . . . . . 9 ⊢ ((1...𝑁) ⊆ (ℤ≥‘𝐵) ∨ (1...𝑁) ∈ Fin)
428		sumz 15893	. . . . . . . . 9 ⊢ (((1...𝑁) ⊆ (ℤ≥‘𝐵) ∨ (1...𝑁) ∈ Fin) → Σ𝑛 ∈ (1...𝑁)0 = 0)
429	427, 428	ax-mp 5	. . . . . . . 8 ⊢ Σ𝑛 ∈ (1...𝑁)0 = 0
430	426, 429	eqtrdi 2811	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = 0)
431	381, 430	eqtrd 2795	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0)
432	431	adantrlr 736	. . . . 5 ⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0)
433		fveq1 6884	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) → (𝑥‘𝐴) = ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴))
434	433	eqeq1d 2762	. . . . . 6 ⊢ (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) → ((𝑥‘𝐴) = 0 ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0))
435	434	rspcev 3576	. . . . 5 ⊢ (((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖ {0𝑝}) ∧ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0)
436	373, 432, 435	syl2anc 596	. . . 4 ⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0)
437	274, 436	sylanr1 695	. . 3 ⊢ ((𝜑 ∧ (𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0)
438	271, 437	rexlimddv 3169	. 2 ⊢ (𝜑 → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0)
439		elqaa 26650	. 2 ⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧ ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0))
440	1, 438, 439	sylanbrc 595	1 ⊢ (𝜑 → 𝐴 ∈ 𝔸)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144   ≠ wne 2955   ∉ wnel 3061  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ⊆ wss 3895   ∖ cdif 4045   ∩ cin 4089   ∪ cun 4149  ∅c0 4278  𝒫 cpw 4556  {csn 4584   class class class wbr 5102   ↦ cmpt 5185   × cxp 5648  dom cdm 5650  ran crn 5651   ↾ cres 5652   “ cima 5653   Fn wfn 6533  ⟶wf 6534  –1-1→wf1 6535  –1-1-onto→wf1o 6537  ‘cfv 6538  (class class class)co 7420   ∘_f cof 7691   ↑_m cmap 8850   ≈ cen 8973   ≼ cdom 8974  Fincfn 8976  ℂcc 11201  0cc0 11203  1c1 11204   + caddc 11206   · cmul 11208   < clt 11346   ≤ cle 11347   − cmin 11544  ℕ₀cn0 12609  ℤcz 12696  ℤ_≥cuz 12968  ℚcq 13078  ...cfz 13642  ↑cexp 14207  ♯chash 14477  Σcsu 15858  Basecbs 17392   ↾_s cress 17413  ._rcmulr 17434  Scalarcsca 17436   ·_𝑠 cvsca 17437  0_gc0g 17615   Σ_g cgsu 17616  Moorecmre 17757  mrClscmrc 17758  mrIndcmri 17759  ACScacs 17760  Ringcrg 20464  NzRingcnzr 20767  DivRingcdr 20985  LModclmod 21140  LSubSpclss 21211  LSpanclspn 21251  LBasisclbs 21354  LVecclvec 21382  ℂ_fldccnfld 21683   freeLMod cfrlm 22057   unitVec cuvc 22093   LIndF clindf 22115  LIndSclinds 22116  0_𝑝c0p 25995  Polycply 26507  coeffccoe 26509  𝔸caa 26642

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-inf2 9645  ax-cnex 11259  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-addrcl 11264  ax-mulcl 11265  ax-mulrcl 11266  ax-mulcom 11267  ax-addass 11268  ax-mulass 11269  ax-distr 11270  ax-i2m1 11271  ax-1ne0 11272  ax-1rid 11273  ax-rnegex 11274  ax-rrecex 11275  ax-cnre 11276  ax-pre-lttri 11277  ax-pre-lttrn 11278  ax-pre-ltadd 11279  ax-pre-mulgt0 11280  ax-pre-sup 11281  ax-addf 11282  ax-mulf 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-of 7693  df-om 7878  df-1st 8001  df-2nd 8002  df-supp 8180  df-tpos 8246  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-1o 8479  df-2o 8480  df-oadd 8483  df-er 8720  df-map 8852  df-pm 8853  df-ixp 8929  df-en 8977  df-dom 8978  df-sdom 8979  df-fin 8980  df-fsupp 9357  df-sup 9437  df-inf 9438  df-oi 9507  df-card 10023  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351  df-le 11352  df-sub 11546  df-neg 11547  df-div 11977  df-nn 12339  df-2 12408  df-3 12409  df-4 12410  df-5 12411  df-6 12412  df-7 12413  df-8 12414  df-9 12415  df-n0 12610  df-xnn0 12683  df-z 12697  df-dec 12818  df-uz 12969  df-q 13079  df-rp 13124  df-fz 13643  df-fzo 13792  df-fl 13935  df-mod 14013  df-seq 14148  df-exp 14208  df-hash 14478  df-cj 15271  df-re 15272  df-im 15273  df-sqrt 15407  df-abs 15408  df-clim 15660  df-rlim 15661  df-sum 15859  df-struct 17330  df-sets 17347  df-slot 17365  df-ndx 17377  df-base 17393  df-ress 17414  df-plusg 17446  df-mulr 17447  df-starv 17448  df-sca 17449  df-vsca 17450  df-ip 17451  df-tset 17452  df-ple 17453  df-ds 17455  df-unif 17456  df-hom 17457  df-cco 17458  df-0g 17617  df-gsum 17618  df-prds 17623  df-pws 17625  df-mre 17761  df-mrc 17762  df-mri 17763  df-acs 17764  df-mgm 18821  df-sgrp 18913  df-mnd 18929  df-mhm 18983  df-submnd 18984  df-grp 19152  df-minusg 19153  df-sbg 19154  df-mulg 19283  df-subg 19338  df-ghm 19433  df-cntz 19536  df-cmn 20001  df-abl 20002  df-mgp 20366  df-rng 20380  df-ur 20413  df-ring 20466  df-cring 20467  df-oppr 20572  df-dvdsr 20592  df-unit 20593  df-invr 20623  df-dvr 20636  df-nzr 20768  df-subrng 20803  df-subrg 20827  df-drng 20987  df-lmod 21142  df-lss 21212  df-lsp 21252  df-lmhm 21302  df-lbs 21355  df-lvec 21383  df-sra 21453  df-rgmod 21454  df-cnfld 21684  df-dsmm 22043  df-frlm 22058  df-uvc 22094  df-lindf 22117  df-linds 22118  df-0p 25996  df-ply 26511  df-coe 26513  df-dgr 26514  df-aa 26643

This theorem is used by: (None)