Theorem pmatcoe1fsupp 22050

Description: For a polynomial matrix there is an upper bound for the coefficients of all the polynomials being not 0. (Contributed by AV, 3-Oct-2019.) (Proof shortened by AV, 28-Nov-2019.)

Hypotheses

Ref	Expression
pmatcoe1fsupp.p	⊢ 𝑃 = (Poly1‘𝑅)
pmatcoe1fsupp.c	⊢ 𝐶 = (𝑁 Mat 𝑃)
pmatcoe1fsupp.b	⊢ 𝐵 = (Base‘𝐶)
pmatcoe1fsupp.0	⊢ 0 = (0g‘𝑅)

Assertion

Ref	Expression
pmatcoe1fsupp	⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 ))

Distinct variable groups:   𝐵,𝑖,𝑗,𝑠,𝑥   𝑖,𝑀,𝑗,𝑠,𝑥   𝑖,𝑁,𝑗,𝑠,𝑥   𝑅,𝑖,𝑗,𝑠,𝑥   0 ,𝑖,𝑗,𝑠,𝑥

Allowed substitution hints:   𝐶(𝑥,𝑖,𝑗,𝑠)   𝑃(𝑥,𝑖,𝑗,𝑠)

Proof of Theorem pmatcoe1fsupp

Dummy variables 𝑣 𝑢 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssrab2 4037	. . . . . 6 ⊢ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 } ⊆ ((Base‘𝑅) ↑m ℕ0)
2	1	a1i 11	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 } ⊆ ((Base‘𝑅) ↑m ℕ0))
3	2	olcd 872	. . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ⊆ ((Base‘𝑅) ↑m ℕ0) ∨ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 } ⊆ ((Base‘𝑅) ↑m ℕ0)))
4		inss 4198	. . . 4 ⊢ ((∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ⊆ ((Base‘𝑅) ↑m ℕ0) ∨ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 } ⊆ ((Base‘𝑅) ↑m ℕ0)) → (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 }) ⊆ ((Base‘𝑅) ↑m ℕ0))
5	3, 4	syl 17	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 }) ⊆ ((Base‘𝑅) ↑m ℕ0))
6		xpfi 9261	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑁 ∈ Fin) → (𝑁 × 𝑁) ∈ Fin)
7	6	anidms 567	. . . . . 6 ⊢ (𝑁 ∈ Fin → (𝑁 × 𝑁) ∈ Fin)
8		snfi 8988	. . . . . . . 8 ⊢ {(coe1‘(𝑀‘𝑢))} ∈ Fin
9	8	a1i 11	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑢 ∈ (𝑁 × 𝑁)) → {(coe1‘(𝑀‘𝑢))} ∈ Fin)
10	9	ralrimiva 3143	. . . . . 6 ⊢ (𝑁 ∈ Fin → ∀𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∈ Fin)
11	7, 10	jca 512	. . . . 5 ⊢ (𝑁 ∈ Fin → ((𝑁 × 𝑁) ∈ Fin ∧ ∀𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∈ Fin))
12	11	3ad2ant1 1133	. . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((𝑁 × 𝑁) ∈ Fin ∧ ∀𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∈ Fin))
13		iunfi 9284	. . . 4 ⊢ (((𝑁 × 𝑁) ∈ Fin ∧ ∀𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∈ Fin) → ∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∈ Fin)
14		infi 9212	. . . 4 ⊢ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∈ Fin → (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 }) ∈ Fin)
15	12, 13, 14	3syl 18	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 }) ∈ Fin)
16		pmatcoe1fsupp.0	. . . . 5 ⊢ 0 = (0g‘𝑅)
17		fvex 6855	. . . . 5 ⊢ (0g‘𝑅) ∈ V
18	16, 17	eqeltri 2834	. . . 4 ⊢ 0 ∈ V
19	18	a1i 11	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 0 ∈ V)
20		elin 3926	. . . . . 6 ⊢ (𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 }) ↔ (𝑤 ∈ ∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∧ 𝑤 ∈ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 }))
21		breq1 5108	. . . . . . . 8 ⊢ (𝑣 = 𝑤 → (𝑣 finSupp 0 ↔ 𝑤 finSupp 0 ))
22	21	elrab 3645	. . . . . . 7 ⊢ (𝑤 ∈ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 } ↔ (𝑤 ∈ ((Base‘𝑅) ↑m ℕ0) ∧ 𝑤 finSupp 0 ))
23	22	simprbi 497	. . . . . 6 ⊢ (𝑤 ∈ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 } → 𝑤 finSupp 0 )
24	20, 23	simplbiim 505	. . . . 5 ⊢ (𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 }) → 𝑤 finSupp 0 )
25	24	rgen 3066	. . . 4 ⊢ ∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })𝑤 finSupp 0
26	25	a1i 11	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })𝑤 finSupp 0 )
27		fsuppmapnn0fiub0 13898	. . . 4 ⊢ (((∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 }) ⊆ ((Base‘𝑅) ↑m ℕ0) ∧ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 }) ∈ Fin ∧ 0 ∈ V) → (∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })𝑤 finSupp 0 → ∃𝑠 ∈ ℕ0 ∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })∀𝑧 ∈ ℕ0 (𝑠 < 𝑧 → (𝑤‘𝑧) = 0 )))
28	27	imp 407	. . 3 ⊢ ((((∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 }) ⊆ ((Base‘𝑅) ↑m ℕ0) ∧ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 }) ∈ Fin ∧ 0 ∈ V) ∧ ∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })𝑤 finSupp 0 ) → ∃𝑠 ∈ ℕ0 ∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })∀𝑧 ∈ ℕ0 (𝑠 < 𝑧 → (𝑤‘𝑧) = 0 ))
29	5, 15, 19, 26, 28	syl31anc 1373	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })∀𝑧 ∈ ℕ0 (𝑠 < 𝑧 → (𝑤‘𝑧) = 0 ))
30		opelxpi 5670	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ⟨𝑖, 𝑗⟩ ∈ (𝑁 × 𝑁))
31		df-ov 7360	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖𝑀𝑗) = (𝑀‘⟨𝑖, 𝑗⟩)
32	31	fveq2i 6845	. . . . . . . . . . . . . . . . 17 ⊢ (coe1‘(𝑖𝑀𝑗)) = (coe1‘(𝑀‘⟨𝑖, 𝑗⟩))
33		fvex 6855	. . . . . . . . . . . . . . . . . 18 ⊢ (coe1‘(𝑀‘⟨𝑖, 𝑗⟩)) ∈ V
34	33	snid 4622	. . . . . . . . . . . . . . . . 17 ⊢ (coe1‘(𝑀‘⟨𝑖, 𝑗⟩)) ∈ {(coe1‘(𝑀‘⟨𝑖, 𝑗⟩))}
35	32, 34	eqeltri 2834	. . . . . . . . . . . . . . . 16 ⊢ (coe1‘(𝑖𝑀𝑗)) ∈ {(coe1‘(𝑀‘⟨𝑖, 𝑗⟩))}
36	35	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (coe1‘(𝑖𝑀𝑗)) ∈ {(coe1‘(𝑀‘⟨𝑖, 𝑗⟩))})
37		2fveq3 6847	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → (coe1‘(𝑀‘𝑢)) = (coe1‘(𝑀‘⟨𝑖, 𝑗⟩)))
38	37	sneqd 4598	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = ⟨𝑖, 𝑗⟩ → {(coe1‘(𝑀‘𝑢))} = {(coe1‘(𝑀‘⟨𝑖, 𝑗⟩))})
39	38	eliuni 4960	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑖, 𝑗⟩ ∈ (𝑁 × 𝑁) ∧ (coe1‘(𝑖𝑀𝑗)) ∈ {(coe1‘(𝑀‘⟨𝑖, 𝑗⟩))}) → (coe1‘(𝑖𝑀𝑗)) ∈ ∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))})
40	30, 36, 39	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (coe1‘(𝑖𝑀𝑗)) ∈ ∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))})
41	40	adantl 482	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (coe1‘(𝑖𝑀𝑗)) ∈ ∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))})
42		pmatcoe1fsupp.c	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = (𝑁 Mat 𝑃)
43		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝑃) = (Base‘𝑃)
44		pmatcoe1fsupp.b	. . . . . . . . . . . . . . . 16 ⊢ 𝐵 = (Base‘𝐶)
45		simprl 769	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑖 ∈ 𝑁)
46		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑗 ∈ 𝑁)
47	44	eleq2i 2829	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ 𝐵 ↔ 𝑀 ∈ (Base‘𝐶))
48	47	biimpi 215	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (Base‘𝐶))
49	48	3ad2ant3 1135	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ (Base‘𝐶))
50	49	ad3antrrr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑀 ∈ (Base‘𝐶))
51	50, 44	eleqtrrdi 2849	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑀 ∈ 𝐵)
52	42, 43, 44, 45, 46, 51	matecld 21775	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖𝑀𝑗) ∈ (Base‘𝑃))
53		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (coe1‘(𝑖𝑀𝑗)) = (coe1‘(𝑖𝑀𝑗))
54		pmatcoe1fsupp.p	. . . . . . . . . . . . . . . 16 ⊢ 𝑃 = (Poly1‘𝑅)
55		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (0g‘𝑅) = (0g‘𝑅)
56		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝑅) = (Base‘𝑅)
57	53, 43, 54, 55, 56	coe1fsupp 21585	. . . . . . . . . . . . . . 15 ⊢ ((𝑖𝑀𝑗) ∈ (Base‘𝑃) → (coe1‘(𝑖𝑀𝑗)) ∈ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp (0g‘𝑅)})
58	52, 57	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (coe1‘(𝑖𝑀𝑗)) ∈ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp (0g‘𝑅)})
59	16	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 0 = (0g‘𝑅))
60	59	breq2d 5117	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑣 finSupp 0 ↔ 𝑣 finSupp (0g‘𝑅)))
61	60	rabbidv 3415	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 } = {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp (0g‘𝑅)})
62	61	eleq2d 2823	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((coe1‘(𝑖𝑀𝑗)) ∈ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 } ↔ (coe1‘(𝑖𝑀𝑗)) ∈ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp (0g‘𝑅)}))
63	62	ad3antrrr 728	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((coe1‘(𝑖𝑀𝑗)) ∈ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 } ↔ (coe1‘(𝑖𝑀𝑗)) ∈ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp (0g‘𝑅)}))
64	58, 63	mpbird 256	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (coe1‘(𝑖𝑀𝑗)) ∈ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })
65	41, 64	elind 4154	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (coe1‘(𝑖𝑀𝑗)) ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 }))
66		simplr 767	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑥 ∈ ℕ0)
67		fveq1 6841	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (coe1‘(𝑖𝑀𝑗)) → (𝑤‘𝑧) = ((coe1‘(𝑖𝑀𝑗))‘𝑧))
68	67	eqeq1d 2738	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (coe1‘(𝑖𝑀𝑗)) → ((𝑤‘𝑧) = 0 ↔ ((coe1‘(𝑖𝑀𝑗))‘𝑧) = 0 ))
69	68	imbi2d 340	. . . . . . . . . . . . 13 ⊢ (𝑤 = (coe1‘(𝑖𝑀𝑗)) → ((𝑠 < 𝑧 → (𝑤‘𝑧) = 0 ) ↔ (𝑠 < 𝑧 → ((coe1‘(𝑖𝑀𝑗))‘𝑧) = 0 )))
70		breq2 5109	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → (𝑠 < 𝑧 ↔ 𝑠 < 𝑥))
71		fveqeq2 6851	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑥 → (((coe1‘(𝑖𝑀𝑗))‘𝑧) = 0 ↔ ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 ))
72	70, 71	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → ((𝑠 < 𝑧 → ((coe1‘(𝑖𝑀𝑗))‘𝑧) = 0 ) ↔ (𝑠 < 𝑥 → ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 )))
73	69, 72	rspc2v 3590	. . . . . . . . . . . 12 ⊢ (((coe1‘(𝑖𝑀𝑗)) ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 }) ∧ 𝑥 ∈ ℕ0) → (∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })∀𝑧 ∈ ℕ0 (𝑠 < 𝑧 → (𝑤‘𝑧) = 0 ) → (𝑠 < 𝑥 → ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 )))
74	65, 66, 73	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })∀𝑧 ∈ ℕ0 (𝑠 < 𝑧 → (𝑤‘𝑧) = 0 ) → (𝑠 < 𝑥 → ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 )))
75	74	ex 413	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })∀𝑧 ∈ ℕ0 (𝑠 < 𝑧 → (𝑤‘𝑧) = 0 ) → (𝑠 < 𝑥 → ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 ))))
76	75	com23 86	. . . . . . . . 9 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ 𝑥 ∈ ℕ0) → (∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })∀𝑧 ∈ ℕ0 (𝑠 < 𝑧 → (𝑤‘𝑧) = 0 ) → ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑠 < 𝑥 → ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 ))))
77	76	impancom 452	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ ∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })∀𝑧 ∈ ℕ0 (𝑠 < 𝑧 → (𝑤‘𝑧) = 0 )) → (𝑥 ∈ ℕ0 → ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑠 < 𝑥 → ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 ))))
78	77	imp 407	. . . . . . 7 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ ∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })∀𝑧 ∈ ℕ0 (𝑠 < 𝑧 → (𝑤‘𝑧) = 0 )) ∧ 𝑥 ∈ ℕ0) → ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑠 < 𝑥 → ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 )))
79	78	com23 86	. . . . . 6 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ ∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })∀𝑧 ∈ ℕ0 (𝑠 < 𝑧 → (𝑤‘𝑧) = 0 )) ∧ 𝑥 ∈ ℕ0) → (𝑠 < 𝑥 → ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 )))
80	79	ralrimdvv 3198	. . . . 5 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ ∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })∀𝑧 ∈ ℕ0 (𝑠 < 𝑧 → (𝑤‘𝑧) = 0 )) ∧ 𝑥 ∈ ℕ0) → (𝑠 < 𝑥 → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 ))
81	80	ralrimiva 3143	. . . 4 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) ∧ ∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })∀𝑧 ∈ ℕ0 (𝑠 < 𝑧 → (𝑤‘𝑧) = 0 )) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 ))
82	81	ex 413	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ0) → (∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })∀𝑧 ∈ ℕ0 (𝑠 < 𝑧 → (𝑤‘𝑧) = 0 ) → ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 )))
83	82	reximdva 3165	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (∃𝑠 ∈ ℕ0 ∀𝑤 ∈ (∪ 𝑢 ∈ (𝑁 × 𝑁){(coe1‘(𝑀‘𝑢))} ∩ {𝑣 ∈ ((Base‘𝑅) ↑m ℕ0) ∣ 𝑣 finSupp 0 })∀𝑧 ∈ ℕ0 (𝑠 < 𝑧 → (𝑤‘𝑧) = 0 ) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 )))
84	29, 83	mpd 15	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 ))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∀wral 3064  ∃wrex 3073  {crab 3407  Vcvv 3445   ∩ cin 3909   ⊆ wss 3910  {csn 4586  ⟨cop 4592  ∪ ciun 4954   class class class wbr 5105   × cxp 5631  ‘cfv 6496  (class class class)co 7357   ↑_m cmap 8765  Fincfn 8883   finSupp cfsupp 9305   < clt 11189  ℕ₀cn0 12413  Basecbs 17083  0_gc0g 17321  Ringcrg 19964  Poly₁cpl1 21548  coe₁cco1 21549   Mat cmat 21754

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-ot 4595  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-sup 9378  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-fz 13425  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-hom 17157  df-cco 17158  df-0g 17323  df-prds 17329  df-pws 17331  df-sra 20633  df-rgmod 20634  df-dsmm 21138  df-frlm 21153  df-psr 21311  df-mpl 21313  df-opsr 21315  df-psr1 21551  df-ply1 21553  df-coe1 21554  df-mat 21755

This theorem is referenced by:  decpmataa0  22117  decpmatmulsumfsupp  22122  pmatcollpw2lem  22126  pm2mpmhmlem1  22167