aacllem - Mathbox for David A. Wheeler

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

Theorem aacllem 42547

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	⊢ (𝜑 → 𝑁 ∈ ℕ₀)
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 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
3	2	nn0red 11352	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ)
4	3	ltp1d 10954	. . . . 5 ⊢ (𝜑 → 𝑁 < (𝑁 + 1))
5		peano2nn0 11333	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ₀)
6	2, 5	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ₀)
7	6	nn0red 11352	. . . . . 6 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
8	3, 7	ltnled 10184	. . . . 5 ⊢ (𝜑 → (𝑁 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑁))
9	4, 8	mpbid 222	. . . 4 ⊢ (𝜑 → ¬ (𝑁 + 1) ≤ 𝑁)
10		aacllem.3	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
11	10	3expa 1265	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
12		eqid 2622	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝑁) ↦ 𝐶) = (𝑛 ∈ (1...𝑁) ↦ 𝐶)
13	11, 12	fmptd 6385	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ)
14		qex 11800	. . . . . . . . . . 11 ⊢ ℚ ∈ V
15		ovex 6678	. . . . . . . . . . 11 ⊢ (1...𝑁) ∈ V
16	14, 15	elmap 7886	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑_𝑚 (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ 𝐶):(1...𝑁)⟶ℚ)
17	13, 16	sylibr 224	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑_𝑚 (1...𝑁)))
18		eqid 2622	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
19	17, 18	fmptd 6385	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑_𝑚 (1...𝑁)))
20		eqid 2622	. . . . . . . . . . . 12 ⊢ (ℂ_fld ↾_s ℚ) = (ℂ_fld ↾_s ℚ)
21	20	qdrng 25309	. . . . . . . . . . 11 ⊢ (ℂ_fld ↾_s ℚ) ∈ DivRing
22		drngring 18754	. . . . . . . . . . 11 ⊢ ((ℂ_fld ↾_s ℚ) ∈ DivRing → (ℂ_fld ↾_s ℚ) ∈ Ring)
23	21, 22	ax-mp 5	. . . . . . . . . 10 ⊢ (ℂ_fld ↾_s ℚ) ∈ Ring
24		fzfi 12771	. . . . . . . . . 10 ⊢ (1...𝑁) ∈ Fin
25		eqid 2622	. . . . . . . . . . 11 ⊢ ((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) = ((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))
26	25	frlmlmod 20093	. . . . . . . . . 10 ⊢ (((ℂ_fld ↾_s ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ∈ LMod)
27	23, 24, 26	mp2an 708	. . . . . . . . 9 ⊢ ((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ∈ LMod
28		fzfi 12771	. . . . . . . . 9 ⊢ (0...𝑁) ∈ Fin
29	20	qrngbas 25308	. . . . . . . . . . . 12 ⊢ ℚ = (Base‘(ℂ_fld ↾_s ℚ))
30	25, 29	frlmfibas 20105	. . . . . . . . . . 11 ⊢ (((ℂ_fld ↾_s ℚ) ∈ DivRing ∧ (1...𝑁) ∈ Fin) → (ℚ ↑_𝑚 (1...𝑁)) = (Base‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))))
31	21, 24, 30	mp2an 708	. . . . . . . . . 10 ⊢ (ℚ ↑_𝑚 (1...𝑁)) = (Base‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))
32	25	frlmsca 20097	. . . . . . . . . . 11 ⊢ (((ℂ_fld ↾_s ℚ) ∈ DivRing ∧ (1...𝑁) ∈ Fin) → (ℂ_fld ↾_s ℚ) = (Scalar‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))))
33	21, 24, 32	mp2an 708	. . . . . . . . . 10 ⊢ (ℂ_fld ↾_s ℚ) = (Scalar‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))
34		eqid 2622	. . . . . . . . . 10 ⊢ ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) = ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))
35	20	qrng0 25310	. . . . . . . . . . . 12 ⊢ 0 = (0_g‘(ℂ_fld ↾_s ℚ))
36	25, 35	frlm0 20098	. . . . . . . . . . 11 ⊢ (((ℂ_fld ↾_s ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((1...𝑁) × {0}) = (0_g‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))))
37	23, 24, 36	mp2an 708	. . . . . . . . . 10 ⊢ ((1...𝑁) × {0}) = (0_g‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))
38		eqid 2622	. . . . . . . . . . . 12 ⊢ ((ℂ_fld ↾_s ℚ) freeLMod (0...𝑁)) = ((ℂ_fld ↾_s ℚ) freeLMod (0...𝑁))
39	38, 29	frlmfibas 20105	. . . . . . . . . . 11 ⊢ (((ℂ_fld ↾_s ℚ) ∈ DivRing ∧ (0...𝑁) ∈ Fin) → (ℚ ↑_𝑚 (0...𝑁)) = (Base‘((ℂ_fld ↾_s ℚ) freeLMod (0...𝑁))))
40	21, 28, 39	mp2an 708	. . . . . . . . . 10 ⊢ (ℚ ↑_𝑚 (0...𝑁)) = (Base‘((ℂ_fld ↾_s ℚ) freeLMod (0...𝑁)))
41	31, 33, 34, 37, 35, 40	islindf4 20177	. . . . . . . . 9 ⊢ ((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (0...𝑁) ∈ Fin ∧ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑_𝑚 (1...𝑁))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑_𝑚 (0...𝑁))((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0}))))
42	27, 28, 41	mp3an12 1414	. . . . . . . 8 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑_𝑚 (1...𝑁)) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑_𝑚 (0...𝑁))((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0}))))
43	19, 42	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑_𝑚 (0...𝑁))((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0}))))
44		elmapi 7879	. . . . . . . . 9 ⊢ (𝑤 ∈ (ℚ ↑_𝑚 (0...𝑁)) → 𝑤:(0...𝑁)⟶ℚ)
45		fzfid 12772	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (0...𝑁) ∈ Fin)
46		fvexd 6203	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ V)
47	15	mptex 6486	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V
48	47	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ V)
49		simpr 477	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑤:(0...𝑁)⟶ℚ)
50	49	feqmptd 6249	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑤 = (𝑘 ∈ (0...𝑁) ↦ (𝑤‘𝑘)))
51		eqidd 2623	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
52	45, 46, 48, 50, 51	offval2 6914	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘)( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶))))
53		fzfid 12772	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
54		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ)
55	54	adantll 750	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ)
56	17	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) ∈ (ℚ ↑_𝑚 (1...𝑁)))
57		cnfldmul 19752	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ · = (._r‘ℂ_fld)
58	20, 57	ressmulr 16006	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℚ ∈ V → · = (._r‘(ℂ_fld ↾_s ℚ)))
59	14, 58	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ · = (._r‘(ℂ_fld ↾_s ℚ))
60	25, 31, 29, 53, 55, 56, 34, 59	frlmvscafval 20109	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘)( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (((1...𝑁) × {(𝑤‘𝑘)}) ∘_𝑓 · (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
61		fvexd 6203	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤‘𝑘) ∈ V)
62	11	adantllr 755	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℚ)
63		fconstmpt 5163	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1...𝑁) × {(𝑤‘𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤‘𝑘))
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((1...𝑁) × {(𝑤‘𝑘)}) = (𝑛 ∈ (1...𝑁) ↦ (𝑤‘𝑘)))
65		eqidd 2623	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ 𝐶) = (𝑛 ∈ (1...𝑁) ↦ 𝐶))
66	53, 61, 62, 64, 65	offval2 6914	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (((1...𝑁) × {(𝑤‘𝑘)}) ∘_𝑓 · (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))
67	60, 66	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘)( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))
68	67	mpteq2dva 4744	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘)( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))
69	52, 68	eqtrd 2656	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))
70	69	oveq2d 6666	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))))
71		fzfid 12772	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (1...𝑁) ∈ Fin)
72	23	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (ℂ_fld ↾_s ℚ) ∈ Ring)
73	55	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℚ)
74	11	an32s 846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℚ)
75	74	adantllr 755	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℚ)
76		qmulcl 11806	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑤‘𝑘) ∈ ℚ ∧ 𝐶 ∈ ℚ) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ)
77	73, 75, 76	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ)
78	77	an32s 846	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℚ)
79		eqid 2622	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))
80	78, 79	fmptd 6385	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
81	14, 15	elmap 7886	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑_𝑚 (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
82	80, 81	sylibr 224	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑_𝑚 (1...𝑁)))
83		eqid 2622	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))
84	15	mptex 6486	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ V
85	84	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) ∈ V)
86		snex 4908	. . . . . . . . . . . . . . . . . . 19 ⊢ {0} ∈ V
87	15, 86	xpex 6962	. . . . . . . . . . . . . . . . . 18 ⊢ ((1...𝑁) × {0}) ∈ V
88	87	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((1...𝑁) × {0}) ∈ V)
89	83, 45, 85, 88	fsuppmptdm 8286	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) finSupp ((1...𝑁) × {0}))
90	25, 31, 37, 71, 45, 72, 82, 89	frlmgsum 20111	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ ((ℂ_fld ↾_s ℚ) Σ_g (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))))
91		cnfldbas 19750	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ = (Base‘ℂ_fld)
92		cnfldadd 19751	. . . . . . . . . . . . . . . . . 18 ⊢ + = (+_g‘ℂ_fld)
93		cnfldex 19749	. . . . . . . . . . . . . . . . . . 19 ⊢ ℂ_fld ∈ V
94	93	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℂ_fld ∈ V)
95		fzfid 12772	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (0...𝑁) ∈ Fin)
96		qsscn 11799	. . . . . . . . . . . . . . . . . . 19 ⊢ ℚ ⊆ ℂ
97	96	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ℚ ⊆ ℂ)
98		eqid 2622	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)) = (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))
99	77, 98	fmptd 6385	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)):(0...𝑁)⟶ℚ)
100		0z 11388	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℤ
101		zq 11794	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℤ → 0 ∈ ℚ)
102	100, 101	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℚ
103	102	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 0 ∈ ℚ)
104		addid2 10219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℂ → (0 + 𝑥) = 𝑥)
105		addid1 10216	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℂ → (𝑥 + 0) = 𝑥)
106	104, 105	jca 554	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℂ → ((0 + 𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥))
107	106	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ ℂ) → ((0 + 𝑥) = 𝑥 ∧ (𝑥 + 0) = 𝑥))
108	91, 92, 20, 94, 95, 97, 99, 103, 107	gsumress 17276	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂ_fld Σ_g (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = ((ℂ_fld ↾_s ℚ) Σ_g (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))))
109		simplr 792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑤:(0...𝑁)⟶ℚ)
110		qcn 11802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤‘𝑘) ∈ ℚ → (𝑤‘𝑘) ∈ ℂ)
111	54, 110	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
112	109, 111	sylan 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
113		qcn 11802	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐶 ∈ ℚ → 𝐶 ∈ ℂ)
114	11, 113	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℂ)
115	114	an32s 846	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℂ)
116	115	adantllr 755	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → 𝐶 ∈ ℂ)
117	112, 116	mulcld 10060	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · 𝐶) ∈ ℂ)
118	95, 117	gsumfsum 19813	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (ℂ_fld Σ_g (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
119	108, 118	eqtr3d 2658	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((ℂ_fld ↾_s ℚ) Σ_g (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶))) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
120	119	mpteq2dva 4744	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ ((ℂ_fld ↾_s ℚ) Σ_g (𝑘 ∈ (0...𝑁) ↦ ((𝑤‘𝑘) · 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)))
121	70, 90, 120	3eqtrd 2660	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)))
122		qaddcl 11804	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ) → (𝑥 + 𝑦) ∈ ℚ)
123	122	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) ∈ ℚ)
124	97, 123, 95, 77, 103	fsumcllem 14463	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ ℚ)
125		eqid 2622	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) = (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
126	124, 125	fmptd 6385	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
127	14, 15	elmap 7886	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑_𝑚 (1...𝑁)) ↔ (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)):(1...𝑁)⟶ℚ)
128	126, 127	sylibr 224	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶)) ∈ (ℚ ↑_𝑚 (1...𝑁)))
129	121, 128	eqeltrd 2701	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) ∈ (ℚ ↑_𝑚 (1...𝑁)))
130		elmapi 7879	. . . . . . . . . . . . 13 ⊢ ((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) ∈ (ℚ ↑_𝑚 (1...𝑁)) → (((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))):(1...𝑁)⟶ℚ)
131		ffn 6045	. . . . . . . . . . . . 13 ⊢ ((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))):(1...𝑁)⟶ℚ → (((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁))
132	129, 130, 131	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁))
133		c0ex 10034	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
134		fnconstg 6093	. . . . . . . . . . . . 13 ⊢ (0 ∈ V → ((1...𝑁) × {0}) Fn (1...𝑁))
135	133, 134	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((1...𝑁) × {0}) Fn (1...𝑁)
136		nfcv 2764	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))
137		nfcv 2764	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛 Σ_g
138		nfcv 2764	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛𝑤
139		nfcv 2764	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))
140		nfcv 2764	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛(0...𝑁)
141		nfmpt1 4747	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑛(𝑛 ∈ (1...𝑁) ↦ 𝐶)
142	140, 141	nfmpt 4746	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
143	138, 139, 142	nfov 6676	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
144	136, 137, 143	nfov 6676	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛(((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))
145		nfcv 2764	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛((1...𝑁) × {0})
146	144, 145	eqfnfv2f 6315	. . . . . . . . . . . 12 ⊢ (((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) Fn (1...𝑁) ∧ ((1...𝑁) × {0}) Fn (1...𝑁)) → ((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
147	132, 135, 146	sylancl 694	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛)))
148	121	fveq1d 6193	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛))
149		sumex 14418	. . . . . . . . . . . . . . 15 ⊢ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ V
150	125	fvmpt2 6291	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (1...𝑁) ∧ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) ∈ V) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
151	149, 150	mpan2 707	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 ∈ (1...𝑁) ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
152	148, 151	sylan9eq 2676	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → ((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶))
153	133	fvconst2 6469	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {0})‘𝑛) = 0)
154	153	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {0})‘𝑛) = 0)
155	152, 154	eqeq12d 2637	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
156	155	ralbidva 2985	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (∀𝑛 ∈ (1...𝑁)((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))))‘𝑛) = (((1...𝑁) × {0})‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
157	147, 156	bitrd 268	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) ↔ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
158	157	imbi1d 331	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ (∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
159	44, 158	sylan2 491	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ (ℚ ↑_𝑚 (0...𝑁))) → (((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ (∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
160	159	ralbidva 2985	. . . . . . 7 ⊢ (𝜑 → (∀𝑤 ∈ (ℚ ↑_𝑚 (0...𝑁))((((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) Σ_g (𝑤 ∘_𝑓 ( ·_𝑠 ‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))(𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))) = ((1...𝑁) × {0}) → 𝑤 = ((0...𝑁) × {0})) ↔ ∀𝑤 ∈ (ℚ ↑_𝑚 (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
161	43, 160	bitrd 268	. . . . . 6 ⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ↔ ∀𝑤 ∈ (ℚ ↑_𝑚 (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0}))))
162		drngnzr 19262	. . . . . . . . 9 ⊢ ((ℂ_fld ↾_s ℚ) ∈ DivRing → (ℂ_fld ↾_s ℚ) ∈ NzRing)
163	21, 162	ax-mp 5	. . . . . . . 8 ⊢ (ℂ_fld ↾_s ℚ) ∈ NzRing
164	33	islindf3 20165	. . . . . . . 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...𝑁))))))
165	27, 163, 164	mp2an 708	. . . . . . 7 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))))
166	47, 18	dmmpti 6023	. . . . . . . . 9 ⊢ dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (0...𝑁)
167		f1eq2 6097	. . . . . . . . 9 ⊢ (dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) = (0...𝑁) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ↔ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V))
168	166, 167	ax-mp 5	. . . . . . . 8 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):dom (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))–1-1→V ↔ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V)
169	168	anbi1i 731	. . . . . . 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...𝑁)))))
170	165, 169	bitri 264	. . . . . 6 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) LIndF ((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ↔ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))))
171		con34b 306	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ (¬ 𝑤 = ((0...𝑁) × {0}) → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
172		df-nel 2898	. . . . . . . . . . 11 ⊢ (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬ 𝑤 ∈ {((0...𝑁) × {0})})
173		velsn 4193	. . . . . . . . . . 11 ⊢ (𝑤 ∈ {((0...𝑁) × {0})} ↔ 𝑤 = ((0...𝑁) × {0}))
174	172, 173	xchbinx 324	. . . . . . . . . 10 ⊢ (𝑤 ∉ {((0...𝑁) × {0})} ↔ ¬ 𝑤 = ((0...𝑁) × {0}))
175	174	imbi1i 339	. . . . . . . . 9 ⊢ ((𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ↔ (¬ 𝑤 = ((0...𝑁) × {0}) → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
176	171, 175	bitr4i 267	. . . . . . . 8 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ (𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
177	176	ralbii 2980	. . . . . . 7 ⊢ (∀𝑤 ∈ (ℚ ↑_𝑚 (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ∀𝑤 ∈ (ℚ ↑_𝑚 (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
178		raldifb 3750	. . . . . . 7 ⊢ (∀𝑤 ∈ (ℚ ↑_𝑚 (0...𝑁))(𝑤 ∉ {((0...𝑁) × {0})} → ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ↔ ∀𝑤 ∈ ((ℚ ↑_𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})}) ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
179		ralnex 2992	. . . . . . 7 ⊢ (∀𝑤 ∈ ((ℚ ↑_𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})}) ¬ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ↔ ¬ ∃𝑤 ∈ ((ℚ ↑_𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
180	177, 178, 179	3bitri 286	. . . . . 6 ⊢ (∀𝑤 ∈ (ℚ ↑_𝑚 (0...𝑁))(∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → 𝑤 = ((0...𝑁) × {0})) ↔ ¬ ∃𝑤 ∈ ((ℚ ↑_𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
181	161, 170, 180	3bitr3g 302	. . . . 5 ⊢ (𝜑 → (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))) ↔ ¬ ∃𝑤 ∈ ((ℚ ↑_𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
182		eqid 2622	. . . . . . . . . . . . 13 ⊢ (LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) = (LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))
183	31, 182	lssmre 18966	. . . . . . . . . . . 12 ⊢ (((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ∈ LMod → (LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑_𝑚 (1...𝑁))))
184	27, 183	ax-mp 5	. . . . . . . . . . 11 ⊢ (LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑_𝑚 (1...𝑁)))
185	184	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))) → (LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑_𝑚 (1...𝑁))))
186		eqid 2622	. . . . . . . . . . . 12 ⊢ (LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) = (LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))
187		eqid 2622	. . . . . . . . . . . 12 ⊢ (mrCls‘(LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))) = (mrCls‘(LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))))
188	182, 186, 187	mrclsp 18989	. . . . . . . . . . 11 ⊢ (((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ∈ LMod → (LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) = (mrCls‘(LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))))
189	27, 188	ax-mp 5	. . . . . . . . . 10 ⊢ (LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) = (mrCls‘(LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))))
190		eqid 2622	. . . . . . . . . 10 ⊢ (mrInd‘(LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))) = (mrInd‘(LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))))
191	33	islvec 19104	. . . . . . . . . . . . 13 ⊢ (((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ∈ LVec ↔ (((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂ_fld ↾_s ℚ) ∈ DivRing))
192	27, 21, 191	mpbir2an 955	. . . . . . . . . . . 12 ⊢ ((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ∈ LVec
193	182, 189, 31	lssacsex 19144	. . . . . . . . . . . . 13 ⊢ (((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ∈ LVec → ((LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) ∈ (ACS‘(ℚ ↑_𝑚 (1...𝑁))) ∧ ∀𝑧 ∈ 𝒫 (ℚ ↑_𝑚 (1...𝑁))∀𝑥 ∈ (ℚ ↑_𝑚 (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦}))))
194	193	simprd 479	. . . . . . . . . . . 12 ⊢ (((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ∈ LVec → ∀𝑧 ∈ 𝒫 (ℚ ↑_𝑚 (1...𝑁))∀𝑥 ∈ (ℚ ↑_𝑚 (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦})))
195	192, 194	ax-mp 5	. . . . . . . . . . 11 ⊢ ∀𝑧 ∈ 𝒫 (ℚ ↑_𝑚 (1...𝑁))∀𝑥 ∈ (ℚ ↑_𝑚 (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦}))
196	195	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))) → ∀𝑧 ∈ 𝒫 (ℚ ↑_𝑚 (1...𝑁))∀𝑥 ∈ (ℚ ↑_𝑚 (1...𝑁))∀𝑦 ∈ (((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑥})) ∖ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘𝑧))𝑥 ∈ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(𝑧 ∪ {𝑦})))
197		frn 6053	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)⟶(ℚ ↑_𝑚 (1...𝑁)) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ ↑_𝑚 (1...𝑁)))
198	19, 197	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ ↑_𝑚 (1...𝑁)))
199		dif0 3950	. . . . . . . . . . . 12 ⊢ ((ℚ ↑_𝑚 (1...𝑁)) ∖ ∅) = (ℚ ↑_𝑚 (1...𝑁))
200	198, 199	syl6sseqr 3652	. . . . . . . . . . 11 ⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((ℚ ↑_𝑚 (1...𝑁)) ∖ ∅))
201	200	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((ℚ ↑_𝑚 (1...𝑁)) ∖ ∅))
202		eqid 2622	. . . . . . . . . . . . . . 15 ⊢ ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) = ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁))
203	202, 25, 31	uvcff 20130	. . . . . . . . . . . . . 14 ⊢ (((ℂ_fld ↾_s ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑_𝑚 (1...𝑁)))
204	23, 24, 203	mp2an 708	. . . . . . . . . . . . 13 ⊢ ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑_𝑚 (1...𝑁))
205		frn 6053	. . . . . . . . . . . . 13 ⊢ (((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)):(1...𝑁)⟶(ℚ ↑_𝑚 (1...𝑁)) → ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ⊆ (ℚ ↑_𝑚 (1...𝑁)))
206	204, 205	ax-mp 5	. . . . . . . . . . . 12 ⊢ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ⊆ (ℚ ↑_𝑚 (1...𝑁))
207	206, 199	sseqtr4i 3638	. . . . . . . . . . 11 ⊢ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ⊆ ((ℚ ↑_𝑚 (1...𝑁)) ∖ ∅)
208	207	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))) → ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ⊆ ((ℚ ↑_𝑚 (1...𝑁)) ∖ ∅))
209		un0 3967	. . . . . . . . . . . . . 14 ⊢ (ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∪ ∅) = ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁))
210	209	fveq2i 6194	. . . . . . . . . . . . 13 ⊢ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∪ ∅)) = ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)))
211		eqid 2622	. . . . . . . . . . . . . . . 16 ⊢ (LBasis‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) = (LBasis‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))
212	25, 202, 211	frlmlbs 20136	. . . . . . . . . . . . . . 15 ⊢ (((ℂ_fld ↾_s ℚ) ∈ Ring ∧ (1...𝑁) ∈ Fin) → ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))))
213	23, 24, 212	mp2an 708	. . . . . . . . . . . . . 14 ⊢ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))
214	31, 211, 186	lbssp 19079	. . . . . . . . . . . . . 14 ⊢ (ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∈ (LBasis‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) → ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁))) = (ℚ ↑_𝑚 (1...𝑁)))
215	213, 214	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁))) = (ℚ ↑_𝑚 (1...𝑁))
216	210, 215	eqtri 2644	. . . . . . . . . . . 12 ⊢ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∪ ∅)) = (ℚ ↑_𝑚 (1...𝑁))
217	198, 216	syl6sseqr 3652	. . . . . . . . . . 11 ⊢ (𝜑 → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∪ ∅)))
218	217	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∪ ∅)))
219		un0 3967	. . . . . . . . . . 11 ⊢ (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) = ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))
220	27, 163	pm3.2i 471	. . . . . . . . . . . . . 14 ⊢ (((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)) ∈ LMod ∧ (ℂ_fld ↾_s ℚ) ∈ NzRing)
221	186, 33	lindsind2 20158	. . . . . . . . . . . . . 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...𝑁) ↦ 𝐶)) ∖ {𝑥})))
222	220, 221	mp3an1 1411	. . . . . . . . . . . . 13 ⊢ ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) ∧ 𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶))) → ¬ 𝑥 ∈ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
223	222	ralrimiva 2966	. . . . . . . . . . . 12 ⊢ (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) → ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥})))
224	189, 190	ismri2 16292	. . . . . . . . . . . . . 14 ⊢ (((LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) ∈ (Moore‘(ℚ ↑_𝑚 (1...𝑁))) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ⊆ (ℚ ↑_𝑚 (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))) ↔ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))))
225	184, 198, 224	sylancr 695	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))) ↔ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))))
226	225	biimpar 502	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∀𝑥 ∈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ¬ 𝑥 ∈ ((LSpan‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))‘(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∖ {𝑥}))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))))
227	223, 226	sylan2 491	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (mrInd‘(LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))))
228	219, 227	syl5eqel 2705	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))))
229		mptfi 8265	. . . . . . . . . . . . 13 ⊢ ((0...𝑁) ∈ Fin → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin)
230		rnfi 8249	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin)
231	28, 229, 230	mp2b 10	. . . . . . . . . . . 12 ⊢ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin
232	231	orci 405	. . . . . . . . . . 11 ⊢ (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin ∨ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∈ Fin)
233	232	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ Fin ∨ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∈ Fin))
234	185, 189, 190, 196, 201, 208, 218, 228, 233	mreexexd 16308	. . . . . . . . 9 ⊢ ((𝜑 ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))) → ∃𝑣 ∈ 𝒫 ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))))))
235	234	ex 450	. . . . . . . 8 ⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) → ∃𝑣 ∈ 𝒫 ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))))))
236		ovex 6678	. . . . . . . . . . . . 13 ⊢ ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∈ V
237	236	rnex 7100	. . . . . . . . . . . 12 ⊢ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∈ V
238		elpwi 4168	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ 𝒫 ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) → 𝑣 ⊆ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)))
239		ssdomg 8001	. . . . . . . . . . . 12 ⊢ (ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∈ V → (𝑣 ⊆ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) → 𝑣 ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁))))
240	237, 238, 239	mpsyl 68	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝒫 ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) → 𝑣 ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)))
241		endomtr 8014	. . . . . . . . . . . . . 14 ⊢ ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ 𝑣 ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁))) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)))
242	241	ancoms 469	. . . . . . . . . . . . 13 ⊢ ((𝑣 ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣) → ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)))
243		f1f1orn 6148	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1-onto→ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
244		ovex 6678	. . . . . . . . . . . . . . . . 17 ⊢ (0...𝑁) ∈ V
245	244	f1oen 7976	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1-onto→ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) → (0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
246	243, 245	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)))
247		endomtr 8014	. . . . . . . . . . . . . . . . 17 ⊢ (((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁))) → (0...𝑁) ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)))
248	202	uvcendim 20186	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℂ_fld ↾_s ℚ) ∈ NzRing ∧ (1...𝑁) ∈ Fin) → (1...𝑁) ≈ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)))
249	163, 24, 248	mp2an 708	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑁) ≈ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁))
250	249	ensymi 8006	. . . . . . . . . . . . . . . . . 18 ⊢ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)
251		domentr 8015	. . . . . . . . . . . . . . . . . . 19 ⊢ (((0...𝑁) ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∧ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (0...𝑁) ≼ (1...𝑁))
252		hashdom 13168	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((0...𝑁) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((#‘(0...𝑁)) ≤ (#‘(1...𝑁)) ↔ (0...𝑁) ≼ (1...𝑁)))
253	28, 24, 252	mp2an 708	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((#‘(0...𝑁)) ≤ (#‘(1...𝑁)) ↔ (0...𝑁) ≼ (1...𝑁))
254		hashfz0 13219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ₀ → (#‘(0...𝑁)) = (𝑁 + 1))
255	2, 254	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (#‘(0...𝑁)) = (𝑁 + 1))
256		hashfz1 13134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ₀ → (#‘(1...𝑁)) = 𝑁)
257	2, 256	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (#‘(1...𝑁)) = 𝑁)
258	255, 257	breq12d 4666	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((#‘(0...𝑁)) ≤ (#‘(1...𝑁)) ↔ (𝑁 + 1) ≤ 𝑁))
259	253, 258	syl5bbr 274	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((0...𝑁) ≼ (1...𝑁) ↔ (𝑁 + 1) ≤ 𝑁))
260	251, 259	syl5ib 234	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((0...𝑁) ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∧ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ≈ (1...𝑁)) → (𝑁 + 1) ≤ 𝑁))
261	250, 260	mpan2i 713	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((0...𝑁) ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁))
262	247, 261	syl5 34	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁))) → (𝑁 + 1) ≤ 𝑁))
263	262	expd 452	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((0...𝑁) ≈ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁)))
264	246, 263	syl5 34	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) → (𝑁 + 1) ≤ 𝑁)))
265	264	com23 86	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
266	242, 265	syl5 34	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑣 ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁)) ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
267	266	expdimp 453	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ≼ ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
268	240, 267	sylan2 491	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝒫 ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁))) → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
269	268	adantrd 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝒫 ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁))) → ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
270	269	rexlimdva 3031	. . . . . . . 8 ⊢ (𝜑 → (∃𝑣 ∈ 𝒫 ran ((ℂ_fld ↾_s ℚ) unitVec (1...𝑁))(ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ≈ 𝑣 ∧ (𝑣 ∪ ∅) ∈ (mrInd‘(LSubSp‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
271	235, 270	syld 47	. . . . . . 7 ⊢ (𝜑 → (ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) → ((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V → (𝑁 + 1) ≤ 𝑁)))
272	271	impd 447	. . . . . 6 ⊢ (𝜑 → ((ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁))) ∧ (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V) → (𝑁 + 1) ≤ 𝑁))
273	272	ancomsd 470	. . . . 5 ⊢ (𝜑 → (((𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)):(0...𝑁)–1-1→V ∧ ran (𝑘 ∈ (0...𝑁) ↦ (𝑛 ∈ (1...𝑁) ↦ 𝐶)) ∈ (LIndS‘((ℂ_fld ↾_s ℚ) freeLMod (1...𝑁)))) → (𝑁 + 1) ≤ 𝑁))
274	181, 273	sylbird 250	. . . 4 ⊢ (𝜑 → (¬ ∃𝑤 ∈ ((ℚ ↑_𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 → (𝑁 + 1) ≤ 𝑁))
275	9, 274	mt3d 140	. . 3 ⊢ (𝜑 → ∃𝑤 ∈ ((ℚ ↑_𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})})∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
276		eldifsn 4317	. . . . 5 ⊢ (𝑤 ∈ ((ℚ ↑_𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})}) ↔ (𝑤 ∈ (ℚ ↑_𝑚 (0...𝑁)) ∧ 𝑤 ≠ ((0...𝑁) × {0})))
277	44	anim1i 592	. . . . 5 ⊢ ((𝑤 ∈ (ℚ ↑_𝑚 (0...𝑁)) ∧ 𝑤 ≠ ((0...𝑁) × {0})) → (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})))
278	276, 277	sylbi 207	. . . 4 ⊢ (𝑤 ∈ ((ℚ ↑_𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})}) → (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})))
279	96	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ℚ ⊆ ℂ)
280	2	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → 𝑁 ∈ ℕ₀)
281	279, 280, 55	elplyd 23958	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ (Poly‘ℚ))
282	281	adantrr 753	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ (Poly‘ℚ))
283		uzdisj 12413	. . . . . . . . . . . . . . . . . 18 ⊢ ((0...((𝑁 + 1) − 1)) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅
284	2	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑁 ∈ ℂ)
285		pncan1 10454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
286	284, 285	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
287	286	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁))
288	287	ineq1d 3813	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∩ (ℤ_≥‘(𝑁 + 1))) = ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))))
289	283, 288	syl5eqr 2670	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∅ = ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))))
290	289	eqcomd 2628	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅)
291	133	fconst 6091	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℤ_≥‘(𝑁 + 1)) × {0}):(ℤ_≥‘(𝑁 + 1))⟶{0}
292		snssi 4339	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ ℚ → {0} ⊆ ℚ)
293	100, 101, 292	mp2b 10	. . . . . . . . . . . . . . . . . . 19 ⊢ {0} ⊆ ℚ
294	293, 96	sstri 3612	. . . . . . . . . . . . . . . . . 18 ⊢ {0} ⊆ ℂ
295		fss 6056	. . . . . . . . . . . . . . . . . 18 ⊢ ((((ℤ_≥‘(𝑁 + 1)) × {0}):(ℤ_≥‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℂ) → ((ℤ_≥‘(𝑁 + 1)) × {0}):(ℤ_≥‘(𝑁 + 1))⟶ℂ)
296	291, 294, 295	mp2an 708	. . . . . . . . . . . . . . . . 17 ⊢ ((ℤ_≥‘(𝑁 + 1)) × {0}):(ℤ_≥‘(𝑁 + 1))⟶ℂ
297		fun 6066	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑤:(0...𝑁)⟶ℚ ∧ ((ℤ_≥‘(𝑁 + 1)) × {0}):(ℤ_≥‘(𝑁 + 1))⟶ℂ) ∧ ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅) → (𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ_≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
298	296, 297	mpanl2 717	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅) → (𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ_≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
299	290, 298	sylan2 491	. . . . . . . . . . . . . . 15 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝜑) → (𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ_≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
300	299	ancoms 469	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ_≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ))
301		nn0uz 11722	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ₀ = (ℤ_≥‘0)
302	6, 301	syl6eleq 2711	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘0))
303		uzsplit 12412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘0) → (ℤ_≥‘0) = ((0...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))))
304	302, 303	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℤ_≥‘0) = ((0...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))))
305	301, 304	syl5eq 2668	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ℕ₀ = ((0...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))))
306	287	uneq1d 3766	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))) = ((0...𝑁) ∪ (ℤ_≥‘(𝑁 + 1))))
307	305, 306	eqtr2d 2657	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((0...𝑁) ∪ (ℤ_≥‘(𝑁 + 1))) = ℕ₀)
308		ssequn1 3783	. . . . . . . . . . . . . . . . . 18 ⊢ (ℚ ⊆ ℂ ↔ (ℚ ∪ ℂ) = ℂ)
309	96, 308	mpbi 220	. . . . . . . . . . . . . . . . 17 ⊢ (ℚ ∪ ℂ) = ℂ
310	309	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℚ ∪ ℂ) = ℂ)
311	307, 310	feq23d 6040	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ_≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ) ↔ (𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})):ℕ₀⟶ℂ))
312	311	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})):((0...𝑁) ∪ (ℤ_≥‘(𝑁 + 1)))⟶(ℚ ∪ ℂ) ↔ (𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})):ℕ₀⟶ℂ))
313	300, 312	mpbid 222	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})):ℕ₀⟶ℂ)
314		ffn 6045	. . . . . . . . . . . . . . . 16 ⊢ (𝑤:(0...𝑁)⟶ℚ → 𝑤 Fn (0...𝑁))
315		fnimadisj 6012	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅) → (𝑤 “ (ℤ_≥‘(𝑁 + 1))) = ∅)
316	314, 290, 315	syl2anr 495	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 “ (ℤ_≥‘(𝑁 + 1))) = ∅)
317	2	nn0zd 11480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℤ)
318	317	peano2zd 11485	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
319		uzid 11702	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 + 1) ∈ ℤ → (𝑁 + 1) ∈ (ℤ_≥‘(𝑁 + 1)))
320		ne0i 3921	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘(𝑁 + 1)) → (ℤ_≥‘(𝑁 + 1)) ≠ ∅)
321	318, 319, 320	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℤ_≥‘(𝑁 + 1)) ≠ ∅)
322		inidm 3822	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℤ_≥‘(𝑁 + 1)) ∩ (ℤ_≥‘(𝑁 + 1))) = (ℤ_≥‘(𝑁 + 1))
323	322	neeq1i 2858	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℤ_≥‘(𝑁 + 1)) ∩ (ℤ_≥‘(𝑁 + 1))) ≠ ∅ ↔ (ℤ_≥‘(𝑁 + 1)) ≠ ∅)
324	321, 323	sylibr 224	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((ℤ_≥‘(𝑁 + 1)) ∩ (ℤ_≥‘(𝑁 + 1))) ≠ ∅)
325		xpima2 5578	. . . . . . . . . . . . . . . . 17 ⊢ (((ℤ_≥‘(𝑁 + 1)) ∩ (ℤ_≥‘(𝑁 + 1))) ≠ ∅ → (((ℤ_≥‘(𝑁 + 1)) × {0}) “ (ℤ_≥‘(𝑁 + 1))) = {0})
326	324, 325	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((ℤ_≥‘(𝑁 + 1)) × {0}) “ (ℤ_≥‘(𝑁 + 1))) = {0})
327	326	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (((ℤ_≥‘(𝑁 + 1)) × {0}) “ (ℤ_≥‘(𝑁 + 1))) = {0})
328	316, 327	uneq12d 3768	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 “ (ℤ_≥‘(𝑁 + 1))) ∪ (((ℤ_≥‘(𝑁 + 1)) × {0}) “ (ℤ_≥‘(𝑁 + 1)))) = (∅ ∪ {0}))
329		imaundir 5546	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})) “ (ℤ_≥‘(𝑁 + 1))) = ((𝑤 “ (ℤ_≥‘(𝑁 + 1))) ∪ (((ℤ_≥‘(𝑁 + 1)) × {0}) “ (ℤ_≥‘(𝑁 + 1))))
330		uncom 3757	. . . . . . . . . . . . . . 15 ⊢ (∅ ∪ {0}) = ({0} ∪ ∅)
331		un0 3967	. . . . . . . . . . . . . . 15 ⊢ ({0} ∪ ∅) = {0}
332	330, 331	eqtr2i 2645	. . . . . . . . . . . . . 14 ⊢ {0} = (∅ ∪ {0})
333	328, 329, 332	3eqtr4g 2681	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})) “ (ℤ_≥‘(𝑁 + 1))) = {0})
334	290, 314	anim12ci 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅))
335		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ V → ((ℤ_≥‘(𝑁 + 1)) × {0}) Fn (ℤ_≥‘(𝑁 + 1)))
336	133, 335	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ_≥‘(𝑁 + 1)) × {0}) Fn (ℤ_≥‘(𝑁 + 1))
337		fvun1 6269	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 Fn (0...𝑁) ∧ ((ℤ_≥‘(𝑁 + 1)) × {0}) Fn (ℤ_≥‘(𝑁 + 1)) ∧ (((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅ ∧ 𝑘 ∈ (0...𝑁))) → ((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘))
338	336, 337	mp3an2 1412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 Fn (0...𝑁) ∧ (((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅ ∧ 𝑘 ∈ (0...𝑁))) → ((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘))
339	338	anassrs 680	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑤 Fn (0...𝑁) ∧ ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘))
340	334, 339	sylan 488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0}))‘𝑘) = (𝑤‘𝑘))
341	340	eqcomd 2628	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) = ((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0}))‘𝑘))
342	341	oveq1d 6665	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝑦↑𝑘)) = (((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘)))
343	342	sumeq2dv 14433	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘)))
344	343	mpteq2dv 4745	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0}))‘𝑘) · (𝑦↑𝑘))))
345	281, 280, 313, 333, 344	coeeq 23983	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) = (𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})))
346	345	reseq1d 5395	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)))
347		res0 5400	. . . . . . . . . . . . . 14 ⊢ (𝑤 ↾ ∅) = ∅
348	289	reseq2d 5396	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑤 ↾ ∅) = (𝑤 ↾ ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1)))))
349		res0 5400	. . . . . . . . . . . . . . 15 ⊢ (((ℤ_≥‘(𝑁 + 1)) × {0}) ↾ ∅) = ∅
350	289	reseq2d 5396	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((ℤ_≥‘(𝑁 + 1)) × {0}) ↾ ∅) = (((ℤ_≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1)))))
351	349, 350	syl5eqr 2670	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∅ = (((ℤ_≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1)))))
352	347, 348, 351	3eqtr3a 2680	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑤 ↾ ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1)))) = (((ℤ_≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1)))))
353		fss 6056	. . . . . . . . . . . . . . 15 ⊢ ((((ℤ_≥‘(𝑁 + 1)) × {0}):(ℤ_≥‘(𝑁 + 1))⟶{0} ∧ {0} ⊆ ℚ) → ((ℤ_≥‘(𝑁 + 1)) × {0}):(ℤ_≥‘(𝑁 + 1))⟶ℚ)
354	291, 293, 353	mp2an 708	. . . . . . . . . . . . . 14 ⊢ ((ℤ_≥‘(𝑁 + 1)) × {0}):(ℤ_≥‘(𝑁 + 1))⟶ℚ
355		fresaunres1 6077	. . . . . . . . . . . . . 14 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ ((ℤ_≥‘(𝑁 + 1)) × {0}):(ℤ_≥‘(𝑁 + 1))⟶ℚ ∧ (𝑤 ↾ ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1)))) = (((ℤ_≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))))) → ((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
356	354, 355	mp3an2 1412	. . . . . . . . . . . . 13 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ (𝑤 ↾ ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1)))) = (((ℤ_≥‘(𝑁 + 1)) × {0}) ↾ ((0...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))))) → ((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
357	352, 356	sylan2 491	. . . . . . . . . . . 12 ⊢ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝜑) → ((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
358	357	ancoms 469	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑤 ∪ ((ℤ_≥‘(𝑁 + 1)) × {0})) ↾ (0...𝑁)) = 𝑤)
359	346, 358	eqtrd 2656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤)
360		fveq2 6191	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0_𝑝 → (coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) = (coeff‘0_𝑝))
361	360	reseq1d 5395	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0_𝑝 → ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0_𝑝) ↾ (0...𝑁)))
362		eqtr2 2642	. . . . . . . . . . . 12 ⊢ ((((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0_𝑝) ↾ (0...𝑁))) → 𝑤 = ((coeff‘0_𝑝) ↾ (0...𝑁)))
363		coe0 24012	. . . . . . . . . . . . . 14 ⊢ (coeff‘0_𝑝) = (ℕ₀ × {0})
364	363	reseq1i 5392	. . . . . . . . . . . . 13 ⊢ ((coeff‘0_𝑝) ↾ (0...𝑁)) = ((ℕ₀ × {0}) ↾ (0...𝑁))
365		elfznn0 12433	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℕ₀)
366	365	ssriv 3607	. . . . . . . . . . . . . 14 ⊢ (0...𝑁) ⊆ ℕ₀
367		xpssres 5434	. . . . . . . . . . . . . 14 ⊢ ((0...𝑁) ⊆ ℕ₀ → ((ℕ₀ × {0}) ↾ (0...𝑁)) = ((0...𝑁) × {0}))
368	366, 367	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((ℕ₀ × {0}) ↾ (0...𝑁)) = ((0...𝑁) × {0})
369	364, 368	eqtri 2644	. . . . . . . . . . . 12 ⊢ ((coeff‘0_𝑝) ↾ (0...𝑁)) = ((0...𝑁) × {0})
370	362, 369	syl6eq 2672	. . . . . . . . . . 11 ⊢ ((((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 ∧ ((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0_𝑝) ↾ (0...𝑁))) → 𝑤 = ((0...𝑁) × {0}))
371	370	ex 450	. . . . . . . . . 10 ⊢ (((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = 𝑤 → (((coeff‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))) ↾ (0...𝑁)) = ((coeff‘0_𝑝) ↾ (0...𝑁)) → 𝑤 = ((0...𝑁) × {0})))
372	359, 361, 371	syl2im 40	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = 0_𝑝 → 𝑤 = ((0...𝑁) × {0})))
373	372	necon3d 2815	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → (𝑤 ≠ ((0...𝑁) × {0}) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠ 0_𝑝))
374	373	impr 649	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠ 0_𝑝)
375		eldifsn 4317	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖ {0_𝑝}) ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ (Poly‘ℚ) ∧ (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ≠ 0_𝑝))
376	282, 374, 375	sylanbrc 698	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0}))) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖ {0_𝑝}))
377	376	adantrr 753	. . . . 5 ⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖ {0_𝑝}))
378		oveq1 6657	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐴 → (𝑦↑𝑘) = (𝐴↑𝑘))
379	378	oveq2d 6666	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐴 → ((𝑤‘𝑘) · (𝑦↑𝑘)) = ((𝑤‘𝑘) · (𝐴↑𝑘)))
380	379	sumeq2sdv 14435	. . . . . . . . . 10 ⊢ (𝑦 = 𝐴 → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
381		eqid 2622	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))
382		sumex 14418	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) ∈ V
383	380, 381, 382	fvmpt 6282	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
384	1, 383	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
385	384	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)))
386	111	adantll 750	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
387		aacllem.2	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
388	387	adantlr 751	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
389	114, 388	mulcld 10060	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ)
390	389	adantllr 755	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝐶 · 𝑋) ∈ ℂ)
391	53, 386, 390	fsummulc2 14516	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)) = Σ𝑛 ∈ (1...𝑁)((𝑤‘𝑘) · (𝐶 · 𝑋)))
392		aacllem.4	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑𝑘) = Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋))
393	392	oveq2d 6666	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)))
394	393	adantlr 751	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = ((𝑤‘𝑘) · Σ𝑛 ∈ (1...𝑁)(𝐶 · 𝑋)))
395	386	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑤‘𝑘) ∈ ℂ)
396	114	adantllr 755	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ ℂ)
397		simpll 790	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → 𝜑)
398	397, 387	sylan 488	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
399	395, 396, 398	mulassd 10063	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((𝑤‘𝑘) · 𝐶) · 𝑋) = ((𝑤‘𝑘) · (𝐶 · 𝑋)))
400	399	sumeq2dv 14433	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)((𝑤‘𝑘) · (𝐶 · 𝑋)))
401	391, 394, 400	3eqtr4d 2666	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
402	401	sumeq2dv 14433	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑘 ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
403	111	ad2ant2lr 784	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (𝑤‘𝑘) ∈ ℂ)
404	114	anasss 679	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝐶 ∈ ℂ)
405	404	adantlr 751	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝐶 ∈ ℂ)
406	403, 405	mulcld 10060	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → ((𝑤‘𝑘) · 𝐶) ∈ ℂ)
407	387	ad2ant2rl 785	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → 𝑋 ∈ ℂ)
408	406, 407	mulcld 10060	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑛 ∈ (1...𝑁))) → (((𝑤‘𝑘) · 𝐶) · 𝑋) ∈ ℂ)
409	45, 71, 408	fsumcom 14507	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)Σ𝑛 ∈ (1...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
410	402, 409	eqtrd 2656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
411	410	adantrr 753	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
412		nfv 1843	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛𝜑
413		nfv 1843	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛 𝑤:(0...𝑁)⟶ℚ
414		nfra1 2941	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0
415	413, 414	nfan 1828	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛(𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
416	412, 415	nfan 1828	. . . . . . . . . . 11 ⊢ Ⅎ𝑛(𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0))
417		rspa 2930	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)
418	417	oveq1d 6665	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0 ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
419	418	adantll 750	. . . . . . . . . . . . . 14 ⊢ (((𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
420	419	adantll 750	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = (0 · 𝑋))
421	387	adantlr 751	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
422	95, 421, 117	fsummulc1 14517	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤:(0...𝑁)⟶ℚ) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
423	422	adantlrr 757	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋))
424	387	mul02d 10234	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0)
425	424	adantlr 751	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → (0 · 𝑋) = 0)
426	420, 423, 425	3eqtr3d 2664	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) ∧ 𝑛 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0)
427	426	ex 450	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → (𝑛 ∈ (1...𝑁) → Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0))
428	416, 427	ralrimi 2957	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = 0)
429	428	sumeq2d 14432	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)(((𝑤‘𝑘) · 𝐶) · 𝑋) = Σ𝑛 ∈ (1...𝑁)0)
430	411, 429	eqtrd 2656	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = Σ𝑛 ∈ (1...𝑁)0)
431	24	olci 406	. . . . . . . . 9 ⊢ ((1...𝑁) ⊆ (ℤ_≥‘𝐵) ∨ (1...𝑁) ∈ Fin)
432		sumz 14453	. . . . . . . . 9 ⊢ (((1...𝑁) ⊆ (ℤ_≥‘𝐵) ∨ (1...𝑁) ∈ Fin) → Σ𝑛 ∈ (1...𝑁)0 = 0)
433	431, 432	ax-mp 5	. . . . . . . 8 ⊢ Σ𝑛 ∈ (1...𝑁)0 = 0
434	430, 433	syl6eq 2672	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝐴↑𝑘)) = 0)
435	385, 434	eqtrd 2656	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤:(0...𝑁)⟶ℚ ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0)
436	435	adantrlr 759	. . . . 5 ⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0)
437		fveq1 6190	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) → (𝑥‘𝐴) = ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴))
438	437	eqeq1d 2624	. . . . . 6 ⊢ (𝑥 = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) → ((𝑥‘𝐴) = 0 ↔ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0))
439	438	rspcev 3309	. . . . 5 ⊢ (((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘))) ∈ ((Poly‘ℚ) ∖ {0_𝑝}) ∧ ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · (𝑦↑𝑘)))‘𝐴) = 0) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0_𝑝})(𝑥‘𝐴) = 0)
440	377, 436, 439	syl2anc 693	. . . 4 ⊢ ((𝜑 ∧ ((𝑤:(0...𝑁)⟶ℚ ∧ 𝑤 ≠ ((0...𝑁) × {0})) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0_𝑝})(𝑥‘𝐴) = 0)
441	278, 440	sylanr1 684	. . 3 ⊢ ((𝜑 ∧ (𝑤 ∈ ((ℚ ↑_𝑚 (0...𝑁)) ∖ {((0...𝑁) × {0})}) ∧ ∀𝑛 ∈ (1...𝑁)Σ𝑘 ∈ (0...𝑁)((𝑤‘𝑘) · 𝐶) = 0)) → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0_𝑝})(𝑥‘𝐴) = 0)
442	275, 441	rexlimddv 3035	. 2 ⊢ (𝜑 → ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0_𝑝})(𝑥‘𝐴) = 0)
443		elqaa 24077	. 2 ⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧ ∃𝑥 ∈ ((Poly‘ℚ) ∖ {0_𝑝})(𝑥‘𝐴) = 0))
444	1, 442, 443	sylanbrc 698	1 ⊢ (𝜑 → 𝐴 ∈ 𝔸)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∉ wnel 2897 ∀wral 2912 ∃wrex 2913 Vcvv 3200 ∖ cdif 3571 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 𝒫 cpw 4158 {csn 4177 class class class wbr 4653 ↦ cmpt 4729 × cxp 5112 dom cdm 5114 ran crn 5115 ↾ cres 5116 “ cima 5117 Fn wfn 5883 ⟶wf 5884 –1-1→wf1 5885 –1-1-onto→wf1o 5887 ‘cfv 5888 (class class class)co 6650 ∘_𝑓 cof 6895 ↑_𝑚 cmap 7857 ≈ cen 7952 ≼ cdom 7953 Fincfn 7955 ℂcc 9934 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 ≤ cle 10075 − cmin 10266 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ℚcq 11788 ...cfz 12326 ↑cexp 12860 #chash 13117 Σcsu 14416 Basecbs 15857 ↾_s cress 15858 ._rcmulr 15942 Scalarcsca 15944 ·_𝑠 cvsca 15945 0_gc0g 16100 Σ_g cgsu 16101 Moorecmre 16242 mrClscmrc 16243 mrIndcmri 16244 ACScacs 16245 Ringcrg 18547 DivRingcdr 18747 LModclmod 18863 LSubSpclss 18932 LSpanclspn 18971 LBasisclbs 19074 LVecclvec 19102 NzRingcnzr 19257 ℂ_fldccnfld 19746 freeLMod cfrlm 20090 unitVec cuvc 20121 LIndF clindf 20143 LIndSclinds 20144 0_𝑝c0p 23436 Polycply 23940 coeffccoe 23942 𝔸caa 24069

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-tpos 7352 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-xnn0 11364 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-rlim 14220 df-sum 14417 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-0g 16102 df-gsum 16103 df-prds 16108 df-pws 16110 df-mre 16246 df-mrc 16247 df-mri 16248 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-mhm 17335 df-submnd 17336 df-grp 17425 df-minusg 17426 df-sbg 17427 df-mulg 17541 df-subg 17591 df-ghm 17658 df-cntz 17750 df-cmn 18195 df-abl 18196 df-mgp 18490 df-ur 18502 df-ring 18549 df-cring 18550 df-oppr 18623 df-dvdsr 18641 df-unit 18642 df-invr 18672 df-dvr 18683 df-drng 18749 df-subrg 18778 df-lmod 18865 df-lss 18933 df-lsp 18972 df-lmhm 19022 df-lbs 19075 df-lvec 19103 df-sra 19172 df-rgmod 19173 df-nzr 19258 df-cnfld 19747 df-dsmm 20076 df-frlm 20091 df-uvc 20122 df-lindf 20145 df-linds 20146 df-0p 23437 df-ply 23944 df-coe 23946 df-dgr 23947 df-aa 24070

This theorem is referenced by: (None)

W3C validator