Theorem aacllem 50883

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 12649	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ)
4	3	ltp1d 12228	. . . . 5 ⊢ (𝜑 → 𝑁 < (𝑁 + 1))
5		peano2nn0 12627	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
6	2, 5	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ0)
7	6	nn0red 12649	. . . . . 6 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
8	3, 7	ltnled 11438	. . . . 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 7107	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ)
13		qex 13069	. . . . . . . . . . 11 ⊢ ℚ ∈ V
14		ovex 7445	. . . . . . . . . . 11 ⊢ (1...𝑁) ∈ V
15	13, 14	elmap 8883	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ)
16	12, 15	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m (1...𝑁)))
17	16	fmpttd 7107	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑m (1...𝑁)))
18		eqid 2761	. . . . . . . . . . . 12 ⊢ (ℂfld ↾s ℚ) = (ℂfld ↾s ℚ)
19	18	qdrng 27929	. . . . . . . . . . 11 ⊢ (ℂfld ↾s ℚ) ∈ DivRing
20		drngring 20967	. . . . . . . . . . 11 ⊢ ((ℂfld ↾s ℚ) ∈ DivRing → (ℂfld ↾s ℚ) ∈ Ring)
21	19, 20	ax-mp 5	. . . . . . . . . 10 ⊢ (ℂfld ↾s ℚ) ∈ Ring
22		fzfi 14095	. . . . . . . . . 10 ⊢ (1...𝑁) ∈ Fin
23		eqid 2761	. . . . . . . . . . 11 ⊢ ((ℂfld ↾s ℚ) freeLMod (1...𝑁)) = ((ℂfld ↾s ℚ) freeLMod (1...𝑁))
24	23	frlmlmod 22035	. . . . . . . . . 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 14095	. . . . . . . . 9 ⊢ (0...𝑁) ∈ Fin
27	18	qrngbas 27928	. . . . . . . . . . . 12 ⊢ ℚ = (Base‘(ℂfld ↾s ℚ))
28	23, 27	frlmfibas 22048	. . . . . . . . . . 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 22039	. . . . . . . . . . 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 2761	. . . . . . . . . 10 ⊢ ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
33	18	qrng0 27930	. . . . . . . . . . . 12 ⊢ 0 = (0g‘(ℂfld ↾s ℚ))
34	23, 33	frlm0 22040	. . . . . . . . . . 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 2761	. . . . . . . . . . . 12 ⊢ ((ℂfld ↾s ℚ) freeLMod (0...𝑁)) = ((ℂfld ↾s ℚ) freeLMod (0...𝑁))
37	36, 27	frlmfibas 22048	. . . . . . . . . . 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 22124	. . . . . . . . 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 8853	. . . . . . . . 9 ⊢ (𝑤 ∈ (ℚ ↑m (0...𝑁)) → 𝑤:(0...𝑁)⟶ℚ)
43		fzfid 14096	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (0...𝑁) ∈ Fin)
44		fvexd 6892	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ V)
45	14	mptex 7221	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V
46	45	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V)
47		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑤:(0...𝑁)⟶ℚ)
48	47	feqmptd 6945	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑤 = (𝑘 ∈ (0...𝑁) ↦ (𝑤‘𝑘)))
49		eqidd 2762	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
50	43, 44, 46, 48, 49	offval2 7702	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘)( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶))))
51		fzfid 14096	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
52		ffvelcdm 7073	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ)
53	52	adantll 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ)
54	16	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑m (1...𝑁)))
55		cnfldmul 21666	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ · = (.r‘ℂfld)
56	18, 55	ressmulr 17458	. . . . . . . . . . . . . . . . . . . . 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 22052	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘)( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (((1...𝑁) × {(𝑤‘𝑘)}) ∘f · (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
59		fvexd 6892	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤‘𝑘) ∈ V)
60	11	adantllr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
61		fconstmpt 5713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1...𝑁) × {(𝑤‘𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤‘𝑘))
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((1...𝑁) × {(𝑤‘𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤‘𝑘)))
63		eqidd 2762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) = (𝑛 ∈ (1...𝑁) ↦ 𝐶))
64	51, 59, 60, 62, 63	offval2 7702	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (((1...𝑁) × {(𝑤‘𝑘)}) ∘f · (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))
65	58, 64	eqtrd 2796	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘)( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))
66	65	mpteq2dva 5198	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘)( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))
67	50, 66	eqtrd 2796	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))
68	67	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))))
69		fzfid 14096	. . . . . . . . . . . . . . . 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 13076	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤‘𝑘) ∈ ℚ ∧ 𝐶 ∈ ℚ) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ)
75	71, 73, 74	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ)
76	75	an32s 665	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ)
77	76	fmpttd 7107	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
78	13, 14	elmap 8883	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
79	77, 78	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)))
80		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))
81	14	mptex 7221	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ V
82	81	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ V)
83		snex 5397	. . . . . . . . . . . . . . . . . . 19 ⊢ {0} ∈ V
84	14, 83	xpex 7756	. . . . . . . . . . . . . . . . . 18 ⊢ ((1...𝑁) × {0}) ∈ V
85	84	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((1...𝑁) × {0}) ∈ V)
86	80, 43, 82, 85	fsuppmptdm 9352	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) finSupp ((1...𝑁) × {0}))
87	23, 29, 35, 69, 43, 70, 79, 86	frlmgsum 22058	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ ((ℂfld ↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))))
88		cnfldbas 21662	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ = (Base‘ℂfld)
89		cnfldadd 21664	. . . . . . . . . . . . . . . . . 18 ⊢ + = (+g‘ℂfld)
90		cnfldex 21661	. . . . . . . . . . . . . . . . . . 19 ⊢ ℂfld ∈ V
91	90	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℂfld ∈ V)
92		fzfid 14096	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (0...𝑁) ∈ Fin)
93		qsscn 13068	. . . . . . . . . . . . . . . . . . 19 ⊢ ℚ ⊆ ℂ
94	93	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℚ ⊆ ℂ)
95	75	fmpttd 7107	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(0...𝑁)⟶ℚ)
96		0z 12685	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℤ
97		zq 13062	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℤ → 0 ∈ ℚ)
98	96, 97	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℚ
99	98	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 0 ∈ ℚ)
100		addlid 11474	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℂ → (0 + 𝑥) = 𝑥)
101		addrid 11471	. . . . . . . . . . . . . . . . . . . 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 18851	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂfld Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = ((ℂfld ↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))
105		simplr 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑤:(0...𝑁)⟶ℚ)
106		qcn 13071	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤‘𝑘) ∈ ℚ → (𝑤‘𝑘) ∈ ℂ)
107	52, 106	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
108	105, 107	sylan 592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
109		qcn 13071	. . . . . . . . . . . . . . . . . . . . . 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 11310	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℂ)
114	92, 113	gsumfsum 21720	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂfld Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
115	104, 114	eqtr3d 2798	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((ℂfld ↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
116	115	mpteq2dva 5198	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ ((ℂfld ↾s ℚ) Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)))
117	68, 87, 116	3eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)))
118		qaddcl 13074	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ) → (𝑥 + 𝑦) ∈ ℚ)
119	118	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) ∈ ℚ)
120	94, 119, 92, 75, 99	fsumcllem 15878	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ ℚ)
121	120	fmpttd 7107	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
122	13, 14	elmap 8883	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
123	121, 122	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑m (1...𝑁)))
124	117, 123	eqeltrd 2861	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) ∈ (ℚ ↑m (1...𝑁)))
125		elmapi 8853	. . . . . . . . . . . . 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 6701	. . . . . . . . . . . . 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 11281	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
129		fnconstg 6762	. . . . . . . . . . . . 13 ⊢ (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
130	128, 129	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((1...𝑁) × {0}) Fn (1...𝑁)
131		nfcv 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛((ℂfld ↾s ℚ) freeLMod (1...𝑁))
132		nfcv 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛 Σg
133		nfcv 2923	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛𝑤
134		nfcv 2923	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
135		nfcv 2923	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛(0...𝑁)
136		nfmpt1 5204	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛(𝑛 ∈ (1...𝑁) ↦ 𝐶)
137	135, 136	nfmpt 5203	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
138	133, 134, 137	nfov 7442	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
139	131, 132, 138	nfov 7442	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛(((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))
140		nfcv 2923	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛((1...𝑁) × {0})
141	139, 140	eqfnfv2f 7025	. . . . . . . . . . . 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 6879	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛))
144		sumex 15835	. . . . . . . . . . . . . . 15 ⊢ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ V
145		eqid 2761	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
146	145	fvmpt2 6997	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (1...𝑁) ∧ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ V) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
147	144, 146	mpan2 704	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
148	143, 147	sylan9eq 2816	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
149	128	fvconst2 7202	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
150	149	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
151	148, 150	eqeq12d 2777	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((((ℂfld ↾s ℚ) freeLMod (1...𝑁)) Σg (𝑤 ∘f ( ·𝑠 ‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
152	151	ralbidva 3184	. . . . . . . . . . 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 3184	. . . . . . 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 20982	. . . . . . . . 9 ⊢ ((ℂfld ↾s ℚ) ∈ DivRing → (ℂfld ↾s ℚ) ∈ NzRing)
159	19, 158	ax-mp 5	. . . . . . . 8 ⊢ (ℂfld ↾s ℚ) ∈ NzRing
160	31	islindf3 22112	. . . . . . . 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 2761	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
163	45, 162	dmmpti 6675	. . . . . . . . 9 ⊢ dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (0...𝑁)
164		f1eq2 6766	. . . . . . . . 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 3063	. . . . . . . . . . 11 ⊢ (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬ 𝑤 ∈ {((0...𝑁) × {0})})
170		velsn 4600	. . . . . . . . . . 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 3109	. . . . . . 7 ⊢ (∀𝑤 ∈ (ℚ ↑m (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ∀𝑤 ∈ (ℚ ↑m (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
175		raldifb 4096	. . . . . . 7 ⊢ (∀𝑤 ∈ (ℚ ↑m (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ↔ ∀𝑤 ∈ ((ℚ ↑m (0...𝑁)) ∖ {((0...𝑁) × {0})}) ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
176		ralnex 3089	. . . . . . 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 2761	. . . . . . . . . . . . 13 ⊢ (LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = (LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
180	29, 179	lssmre 21221	. . . . . . . . . . . 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 2761	. . . . . . . . . . . 12 ⊢ (LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = (LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
184		eqid 2761	. . . . . . . . . . . 12 ⊢ (mrCls‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) = (mrCls‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
185	179, 183, 184	mrclsp 21244	. . . . . . . . . . 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 2761	. . . . . . . . . 10 ⊢ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) = (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))))
188	31	islvec 21359	. . . . . . . . . . . . 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 21402	. . . . . . . . . . . . 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 6710	. . . . . . . . . . . 12 ⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ ↑m (1...𝑁)))
195		dif0 4327	. . . . . . . . . . . 12 ⊢ ((ℚ ↑m (1...𝑁)) ∖ ∅) = (ℚ ↑m (1...𝑁))
196	194, 195	sseqtrrdi 3972	. . . . . . . . . . 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 2761	. . . . . . . . . . . . . . 15 ⊢ ((ℂfld ↾s ℚ) unitVec (1...𝑁)) = ((ℂfld ↾s ℚ) unitVec (1...𝑁))
199	198, 23, 29	uvcff 22077	. . . . . . . . . . . . . 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 6709	. . . . . . . . . . . . 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 3980	. . . . . . . . . . 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 4344	. . . . . . . . . . . . . 14 ⊢ (ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅) = ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))
206	205	fveq2i 6880	. . . . . . . . . . . . 13 ⊢ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅)) = ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
207		eqid 2761	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) = (LBasis‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))
208	23, 198, 207	frlmlbs 22083	. . . . . . . . . . . . . . 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 21334	. . . . . . . . . . . . . 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 2784	. . . . . . . . . . . 12 ⊢ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∪ ∅)) = (ℚ ↑m (1...𝑁))
213	194, 212	sseqtrrdi 3972	. . . . . . . . . . 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 4344	. . . . . . . . . . 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 22105	. . . . . . . . . . . . . 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 3155	. . . . . . . . . . . 12 ⊢ (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁))) → ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
220	186, 187	ismri2 17786	. . . . . . . . . . . . . 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 2865	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂfld ↾s ℚ) freeLMod (1...𝑁)))))
225		mptfi 9324	. . . . . . . . . . . . 13 ⊢ ((0...𝑁) ∈ Fin → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin)
226		rnfi 9313	. . . . . . . . . . . . 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 17802	. . . . . . . . 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 7445	. . . . . . . . . . . . 13 ⊢ ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V
233	232	rnex 7911	. . . . . . . . . . . 12 ⊢ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∈ V
234		elpwi 4564	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ 𝒫 ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) → 𝑣 ⊆ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
235		ssdomg 9011	. . . . . . . . . . . 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 9023	. . . . . . . . . . . . . 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 6828	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1-onto→ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
240		ovex 7445	. . . . . . . . . . . . . . . . 17 ⊢ (0...𝑁) ∈ V
241	240	f1oen 8983	. . . . . . . . . . . . . . . 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 9023	. . . . . . . . . . . . . . . . 17 ⊢ (((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁))) → (0...𝑁) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)))
244	198	uvcendim 22133	. . . . . . . . . . . . . . . . . . . 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 9015	. . . . . . . . . . . . . . . . . 18 ⊢ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)
247		domentr 9024	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0...𝑁) ≼ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ∧ ran ((ℂfld ↾s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (0...𝑁) ≼ (1...𝑁))
248		hashdom 14503	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((0...𝑁) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((♯‘(0...𝑁)) ≤ (♯‘(1...𝑁)) ↔ (0...𝑁) ≼ (1...𝑁)))
249	26, 22, 248	mp2an 705	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘(0...𝑁)) ≤ (♯‘(1...𝑁)) ↔ (0...𝑁) ≼ (1...𝑁))
250		hashfz0 14557	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ0 → (♯‘(0...𝑁)) = (𝑁 + 1))
251	2, 250	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘(0...𝑁)) = (𝑁 + 1))
252		hashfz1 14470	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
253	2, 252	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
254	251, 253	breq12d 5116	. . . . . . . . . . . . . . . . . . . 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 3164	. . . . . . . 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 4748	. . . . 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 26500	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ (Poly‘ℚ))
278	277	adantrr 730	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ (Poly‘ℚ))
279		uzdisj 13711	. . . . . . . . . . . . . . . . . 18 ⊢ ((0...((𝑁 + 1) − 1)) ∩ (ℤ≥‘(𝑁 + 1))) = ∅
280	2	nn0cnd 12650	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑁 ∈ ℂ)
281		pncan1 11721	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
282	280, 281	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
283	282	oveq2d 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁))
284	283	ineq1d 4165	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∩ (ℤ≥‘(𝑁 + 1))) = ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))))
285	279, 284	eqtr3id 2810	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∅ = ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))))
286	285	eqcomd 2767	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅)
287	128	fconst 6760	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶{0}
288		snssi 4746	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℚ → {0} ⊆ ℚ)
289	96, 97, 288	mp2b 10	. . . . . . . . . . . . . . . . . . 19 ⊢ {0} ⊆ ℚ
290	289, 93	sstri 3940	. . . . . . . . . . . . . . . . . 18 ⊢ {0} ⊆ ℂ
291		fss 6718	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℂ) → ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℂ)
292	287, 290, 291	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℂ
293		fun 6736	. . . . . . . . . . . . . . . . 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 12984	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ0 = (ℤ≥‘0)
298	6, 297	eleqtrdi 2871	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ≥‘0))
299		uzsplit 13710	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘0) → (ℤ≥‘0) = ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))))
300	298, 299	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℤ≥‘0) = ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))))
301	297, 300	eqtrid 2808	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ℕ0 = ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))))
302	283	uneq1d 4114	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))) = ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))))
303	301, 302	eqtr2d 2797	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))) = ℕ0)
304		ssequn1 4132	. . . . . . . . . . . . . . . . . 18 ⊢ (ℚ ⊆ ℂ ↔ (ℚ ∪ ℂ) = ℂ)
305	93, 304	mpbi 233	. . . . . . . . . . . . . . . . 17 ⊢ (ℚ ∪ ℂ) = ℂ
306	305	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℚ ∪ ℂ) = ℂ)
307	303, 306	feq23d 6696	. . . . . . . . . . . . . . 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 6701	. . . . . . . . . . . . . . . 16 ⊢ (𝑤:(0...𝑁)⟶ℚ → 𝑤 Fn (0...𝑁))
311		fnimadisj 6663	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅) → (𝑤 “ (ℤ≥‘(𝑁 + 1))) = ∅)
312	310, 286, 311	syl2anr 609	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 “ (ℤ≥‘(𝑁 + 1))) = ∅)
313	2	nn0zd 12699	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℤ)
314	313	peano2zd 12787	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
315		uzid 12961	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 + 1) ∈ ℤ → (𝑁 + 1) ∈ (ℤ≥‘(𝑁 + 1)))
316		ne0i 4287	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘(𝑁 + 1)) → (ℤ≥‘(𝑁 + 1)) ≠ ∅)
317	314, 315, 316	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℤ≥‘(𝑁 + 1)) ≠ ∅)
318		inidm 4172	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℤ≥‘(𝑁 + 1)) ∩ (ℤ≥‘(𝑁 + 1))) = (ℤ≥‘(𝑁 + 1))
319	318	neeq1i 3020	. . . . . . . . . . . . . . . . . 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 4116	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 “ (ℤ≥‘(𝑁 + 1))) ∪ (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1)))) = (∅ ∪ {0}))
325		imaundir 6140	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) “ (ℤ≥‘(𝑁 + 1))) = ((𝑤 “ (ℤ≥‘(𝑁 + 1))) ∪ (((ℤ≥‘(𝑁 + 1)) × {0}) “ (ℤ≥‘(𝑁 + 1))))
326		uncom 4105	. . . . . . . . . . . . . . 15 ⊢ (∅ ∪ {0}) = ({0} ∪ ∅)
327		un0 4344	. . . . . . . . . . . . . . 15 ⊢ ({0} ∪ ∅) = {0}
328	326, 327	eqtr2i 2785	. . . . . . . . . . . . . 14 ⊢ {0} = (∅ ∪ {0})
329	324, 325, 328	3eqtr4g 2821	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) “ (ℤ≥‘(𝑁 + 1))) = {0})
330	286, 310	anim12ci 626	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅))
331		fnconstg 6762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ V → ((ℤ≥‘(𝑁 + 1)) × {0}) Fn (ℤ≥‘(𝑁 + 1)))
332	128, 331	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ≥‘(𝑁 + 1)) × {0}) Fn (ℤ≥‘(𝑁 + 1))
333		fvun1 6968	. . . . . . . . . . . . . . . . . . . 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 2767	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) = ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘))
338	337	oveq1d 7427	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝑦↑𝑘)) = (((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘)))
339	338	sumeq2dv 15849	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘)))
340	339	mpteq2dv 5199	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘))))
341	277, 276, 309, 329, 340	coeeq 26526	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) = (𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})))
342	341	reseq1d 5969	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((𝑤 ∪ ((ℤ≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)))
343		res0 5974	. . . . . . . . . . . . . 14 ⊢ (𝑤 ↾ ∅) = ∅
344	285	reseq2d 5970	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑤 ↾ ∅) = (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))))
345		res0 5974	. . . . . . . . . . . . . . 15 ⊢ (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ∅) = ∅
346	285	reseq2d 5970	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ∅) = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))))
347	345, 346	eqtr3id 2810	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∅ = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))))
348	343, 344, 347	3eqtr3a 2820	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))) = (((ℤ≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ≥‘(𝑁 + 1)))))
349		fss 6718	. . . . . . . . . . . . . . 15 ⊢ ((((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℚ) → ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℚ)
350	287, 289, 349	mp2an 705	. . . . . . . . . . . . . 14 ⊢ ((ℤ≥‘(𝑁 + 1)) × {0}):(ℤ≥‘(𝑁 + 1))⟶ℚ
351		fresaunres1 6747	. . . . . . . . . . . . . 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 2796	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤)
356		fveq2 6877	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 → (coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) = (coeff‘0𝑝))
357	356	reseq1d 5969	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0𝑝 → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁)))
358		eqtr2 2782	. . . . . . . . . . . 12 ⊢ ((((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0𝑝) ↾ (0...𝑁))) → 𝑤 = ((coeff‘0𝑝) ↾ (0...𝑁)))
359		coe0 26555	. . . . . . . . . . . . . 14 ⊢ (coeff‘0𝑝) = (ℕ0 × {0})
360	359	reseq1i 5966	. . . . . . . . . . . . 13 ⊢ ((coeff‘0𝑝) ↾ (0...𝑁)) = ((ℕ0 × {0}) ↾ (0...𝑁))
361		elfznn0 13734	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℕ0)
362	361	ssriv 3935	. . . . . . . . . . . . . 14 ⊢ (0...𝑁) ⊆ ℕ0
363		xpssres 6009	. . . . . . . . . . . . . 14 ⊢ ((0...𝑁) ⊆ ℕ0 → ((ℕ0 × {0}) ↾ (0...𝑁)) = ((0...𝑁) × {0}))
364	362, 363	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((ℕ0 × {0}) ↾ (0...𝑁)) = ((0...𝑁) × {0})
365	360, 364	eqtri 2784	. . . . . . . . . . . 12 ⊢ ((coeff‘0𝑝) ↾ (0...𝑁)) = ((0...𝑁) × {0})
366	358, 365	eqtrdi 2812	. . . . . . . . . . 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 2977	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ≠ ((0...𝑁) × {0}) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠ 0𝑝))
370	369	impr 460	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠ 0𝑝)
371		eldifsn 4748	. . . . . . 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 7419	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐴 → (𝑦↑𝑘) = (𝐴↑𝑘))
375	374	oveq2d 7428	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐴 → ((𝑤‘𝑘) · (𝑦↑𝑘)) = ((𝑤‘𝑘) · (𝐴↑𝑘)))
376	375	sumeq2sdv 15850	. . . . . . . . . 10 ⊢ (𝑦 = 𝐴 → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
377		eqid 2761	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))
378		sumex 15835	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) ∈ V
379	376, 377, 378	fvmpt 6985	. . . . . . . . 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 11310	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ)
386	385	adantllr 732	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ)
387	51, 382, 386	fsummulc2 15930	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)) = Σ𝑛 ∈ (1...𝑁)((𝑤‘𝑘) · (𝐶 · 𝑋)))
388		aacllem.4	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑𝑘) = Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋))
389	388	oveq2d 7428	. . . . . . . . . . . . . 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 11313	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑤‘𝑘) · 𝐶) · 𝑋) = ((𝑤‘𝑘) · (𝐶 · 𝑋)))
396	395	sumeq2dv 15849	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)((𝑤‘𝑘) · (𝐶 · 𝑋)))
397	387, 390, 396	3eqtr4d 2806	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
398	397	sumeq2dv 15849	. . . . . . . . . . 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 11310	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → ((𝑤‘𝑘) · 𝐶) ∈ ℂ)
403	383	ad2ant2rl 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝑋 ∈ ℂ)
404	402, 403	mulcld 11310	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (((𝑤‘𝑘) · 𝐶) · 𝑋) ∈ ℂ)
405	43, 69, 404	fsumcom 15921	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
406	398, 405	eqtrd 2796	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
407	406	adantrr 730	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
408		nfv 1947	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛𝜑
409		nfv 1947	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛 𝑤:(0...𝑁)⟶ℚ
410		nfra1 3287	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0
411	409, 410	nfan 1932	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
412	408, 411	nfan 1932	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
413		rspa 3252	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
414	413	oveq1d 7427	. . . . . . . . . . . . . . 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 15931	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
419	418	adantlrr 734	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
420	383	mul02d 11489	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0)
421	420	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0)
422	416, 419, 421	3eqtr3d 2804	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0)
423	422	ex 418	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → (𝑛 ∈ (1...𝑁) → Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0))
424	412, 423	ralrimi 3261	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0)
425	424	sumeq2d 15848	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)0)
426	407, 425	eqtrd 2796	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)0)
427	22	olci 880	. . . . . . . . 9 ⊢ ((1...𝑁) ⊆ (ℤ≥‘𝐵) ∨ (1...𝑁) ∈ Fin)
428		sumz 15868	. . . . . . . . 9 ⊢ (((1...𝑁) ⊆ (ℤ≥‘𝐵) ∨ (1...𝑁) ∈ Fin) → Σ𝑛 ∈ (1...𝑁)0 = 0)
429	427, 428	ax-mp 5	. . . . . . . 8 ⊢ Σ𝑛 ∈ (1...𝑁)0 = 0
430	426, 429	eqtrdi 2812	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = 0)
431	381, 430	eqtrd 2796	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0)
432	431	adantrlr 736	. . . . 5 ⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0)
433		fveq1 6876	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) → (𝑥‘𝐴) = ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴))
434	433	eqeq1d 2763	. . . . . 6 ⊢ (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) → ((𝑥‘𝐴) = 0 ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0))
435	434	rspcev 3577	. . . . 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 3170	. 2 ⊢ (𝜑 → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑥‘𝐴) = 0)
439		elqaa 26627	. 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 1570   ∈ wcel 2145   ≠ wne 2956   ∉ wnel 3062  ∀wral 3077  ∃wrex 3087  Vcvv 3451   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  {csn 4584   class class class wbr 5103   ↦ cmpt 5186   × cxp 5649  dom cdm 5651  ran crn 5652   ↾ cres 5653   “ cima 5654   Fn wfn 6526  ⟶wf 6527  –1-1→wf1 6528  –1-1-onto→wf1o 6530  ‘cfv 6531  (class class class)co 7412   ∘_f cof 7680   ↑_m cmap 8831   ≈ cen 8954   ≼ cdom 8955  Fincfn 8957  ℂcc 11179  0cc0 11181  1c1 11182   + caddc 11184   · cmul 11186   < clt 11324   ≤ cle 11325   − cmin 11522  ℕ₀cn0 12587  ℤcz 12674  ℤ_≥cuz 12946  ℚcq 13056  ...cfz 13620  ↑cexp 14184  ♯chash 14454  Σcsu 15833  Basecbs 17367   ↾_s cress 17388  ._rcmulr 17409  Scalarcsca 17411   ·_𝑠 cvsca 17412  0_gc0g 17590   Σ_g cgsu 17591  Moorecmre 17732  mrClscmrc 17733  mrIndcmri 17734  ACScacs 17735  Ringcrg 20439  NzRingcnzr 20742  DivRingcdr 20960  LModclmod 21115  LSubSpclss 21186  LSpanclspn 21226  LBasisclbs 21329  LVecclvec 21357  ℂ_fldccnfld 21658   freeLMod cfrlm 22032   unitVec cuvc 22068   LIndF clindf 22090  LIndSclinds 22091  0_𝑝c0p 25970  Polycply 26482  coeffccoe 26484  𝔸caa 26619

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-inf2 9626  ax-cnex 11237  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-mulcom 11245  ax-addass 11246  ax-mulass 11247  ax-distr 11248  ax-i2m1 11249  ax-1ne0 11250  ax-1rid 11251  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254  ax-pre-lttri 11255  ax-pre-lttrn 11256  ax-pre-ltadd 11257  ax-pre-mulgt0 11258  ax-pre-sup 11259  ax-addf 11260  ax-mulf 11261

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-isom 6540  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7682  df-om 7867  df-1st 7990  df-2nd 7991  df-supp 8162  df-tpos 8227  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8460  df-2o 8461  df-oadd 8464  df-er 8701  df-map 8833  df-pm 8834  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fsupp 9338  df-sup 9418  df-inf 9419  df-oi 9488  df-card 10001  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11524  df-neg 11525  df-div 11955  df-nn 12317  df-2 12386  df-3 12387  df-4 12388  df-5 12389  df-6 12390  df-7 12391  df-8 12392  df-9 12393  df-n0 12588  df-xnn0 12661  df-z 12675  df-dec 12796  df-uz 12947  df-q 13057  df-rp 13102  df-fz 13621  df-fzo 13769  df-fl 13912  df-mod 13990  df-seq 14125  df-exp 14185  df-hash 14455  df-cj 15246  df-re 15247  df-im 15248  df-sqrt 15382  df-abs 15383  df-clim 15635  df-rlim 15636  df-sum 15834  df-struct 17305  df-sets 17322  df-slot 17340  df-ndx 17352  df-base 17368  df-ress 17389  df-plusg 17421  df-mulr 17422  df-starv 17423  df-sca 17424  df-vsca 17425  df-ip 17426  df-tset 17427  df-ple 17428  df-ds 17430  df-unif 17431  df-hom 17432  df-cco 17433  df-0g 17592  df-gsum 17593  df-prds 17598  df-pws 17600  df-mre 17736  df-mrc 17737  df-mri 17738  df-acs 17739  df-mgm 18796  df-sgrp 18888  df-mnd 18904  df-mhm 18958  df-submnd 18959  df-grp 19127  df-minusg 19128  df-sbg 19129  df-mulg 19258  df-subg 19313  df-ghm 19408  df-cntz 19511  df-cmn 19976  df-abl 19977  df-mgp 20341  df-rng 20355  df-ur 20388  df-ring 20441  df-cring 20442  df-oppr 20547  df-dvdsr 20567  df-unit 20568  df-invr 20598  df-dvr 20611  df-nzr 20743  df-subrng 20778  df-subrg 20802  df-drng 20962  df-lmod 21117  df-lss 21187  df-lsp 21227  df-lmhm 21277  df-lbs 21330  df-lvec 21358  df-sra 21428  df-rgmod 21429  df-cnfld 21659  df-dsmm 22018  df-frlm 22033  df-uvc 22069  df-lindf 22092  df-linds 22093  df-0p 25971  df-ply 26486  df-coe 26488  df-dgr 26489  df-aa 26620

This theorem is used by: (None)