pmatcoe1fsupp

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)

	Ref	Expression
Hypotheses	pmatcoe1fsupp.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	pmatcoe1fsupp.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pmatcoe1fsupp.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	pmatcoe1fsupp.0	⊢ 0 = ( 0_g ‘ 𝑅 )
Assertion	pmatcoe1fsupp	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ₀ ∀ 𝑥 ∈ ℕ₀ ( 𝑠 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		pmatcoe1fsupp.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
2		pmatcoe1fsupp.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pmatcoe1fsupp.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		pmatcoe1fsupp.0	⊢ 0 = ( 0_g ‘ 𝑅 )
5		ssrab2	⊢ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ⊆ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ )
6	5	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ⊆ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) )
7	6	olcd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ⊆ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∨ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ⊆ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ) )
8		inss	⊢ ( ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ⊆ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∨ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ⊆ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ) → ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ⊆ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) )
9	7 8	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ⊆ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) )
10		xpfi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑁 × 𝑁 ) ∈ Fin )
11	10	anidms	⊢ ( 𝑁 ∈ Fin → ( 𝑁 × 𝑁 ) ∈ Fin )
12		snfi	⊢ { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∈ Fin
13	12	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑢 ∈ ( 𝑁 × 𝑁 ) ) → { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∈ Fin )
14	13	ralrimiva	⊢ ( 𝑁 ∈ Fin → ∀ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∈ Fin )
15	11 14	jca	⊢ ( 𝑁 ∈ Fin → ( ( 𝑁 × 𝑁 ) ∈ Fin ∧ ∀ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∈ Fin ) )
16	15	3ad2ant1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 × 𝑁 ) ∈ Fin ∧ ∀ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∈ Fin ) )
17		iunfi	⊢ ( ( ( 𝑁 × 𝑁 ) ∈ Fin ∧ ∀ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∈ Fin ) → ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∈ Fin )
18		infi	⊢ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∈ Fin → ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∈ Fin )
19	16 17 18	3syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∈ Fin )
20		fvex	⊢ ( 0_g ‘ 𝑅 ) ∈ V
21	4 20	eqeltri	⊢ 0 ∈ V
22	21	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 0 ∈ V )
23		elin	⊢ ( 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ↔ ( 𝑤 ∈ ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∧ 𝑤 ∈ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) )
24		breq1	⊢ ( 𝑣 = 𝑤 → ( 𝑣 finSupp 0 ↔ 𝑤 finSupp 0 ) )
25	24	elrab	⊢ ( 𝑤 ∈ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ↔ ( 𝑤 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∧ 𝑤 finSupp 0 ) )
26	25	simprbi	⊢ ( 𝑤 ∈ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } → 𝑤 finSupp 0 )
27	23 26	simplbiim	⊢ ( 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) → 𝑤 finSupp 0 )
28	27	rgen	⊢ ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) 𝑤 finSupp 0
29	28	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) 𝑤 finSupp 0 )
30		fsuppmapnn0fiub0	⊢ ( ( ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ⊆ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∧ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∈ Fin ∧ 0 ∈ V ) → ( ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) 𝑤 finSupp 0 → ∃ 𝑠 ∈ ℕ₀ ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∀ 𝑧 ∈ ℕ₀ ( 𝑠 < 𝑧 → ( 𝑤 ‘ 𝑧 ) = 0 ) ) )
31	30	imp	⊢ ( ( ( ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ⊆ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∧ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∈ Fin ∧ 0 ∈ V ) ∧ ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) 𝑤 finSupp 0 ) → ∃ 𝑠 ∈ ℕ₀ ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∀ 𝑧 ∈ ℕ₀ ( 𝑠 < 𝑧 → ( 𝑤 ‘ 𝑧 ) = 0 ) )
32	9 19 22 29 31	syl31anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ₀ ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∀ 𝑧 ∈ ℕ₀ ( 𝑠 < 𝑧 → ( 𝑤 ‘ 𝑧 ) = 0 ) )
33		opelxpi	⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ⟨ 𝑖 , 𝑗 ⟩ ∈ ( 𝑁 × 𝑁 ) )
34		df-ov	⊢ ( 𝑖 𝑀 𝑗 ) = ( 𝑀 ‘ ⟨ 𝑖 , 𝑗 ⟩ )
35	34	fveq2i	⊢ ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) = ( coe₁ ‘ ( 𝑀 ‘ ⟨ 𝑖 , 𝑗 ⟩ ) )
36		fvex	⊢ ( coe₁ ‘ ( 𝑀 ‘ ⟨ 𝑖 , 𝑗 ⟩ ) ) ∈ V
37	36	snid	⊢ ( coe₁ ‘ ( 𝑀 ‘ ⟨ 𝑖 , 𝑗 ⟩ ) ) ∈ { ( coe₁ ‘ ( 𝑀 ‘ ⟨ 𝑖 , 𝑗 ⟩ ) ) }
38	35 37	eqeltri	⊢ ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ∈ { ( coe₁ ‘ ( 𝑀 ‘ ⟨ 𝑖 , 𝑗 ⟩ ) ) }
39	38	a1i	⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ∈ { ( coe₁ ‘ ( 𝑀 ‘ ⟨ 𝑖 , 𝑗 ⟩ ) ) } )
40		2fveq3	⊢ ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) = ( coe₁ ‘ ( 𝑀 ‘ ⟨ 𝑖 , 𝑗 ⟩ ) ) )
41	40	sneqd	⊢ ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } = { ( coe₁ ‘ ( 𝑀 ‘ ⟨ 𝑖 , 𝑗 ⟩ ) ) } )
42	41	eliuni	⊢ ( ( ⟨ 𝑖 , 𝑗 ⟩ ∈ ( 𝑁 × 𝑁 ) ∧ ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ∈ { ( coe₁ ‘ ( 𝑀 ‘ ⟨ 𝑖 , 𝑗 ⟩ ) ) } ) → ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ∈ ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } )
43	33 39 42	syl2anc	⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ∈ ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } )
44	43	adantl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ∈ ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } )
45		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
46		simprl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
47		simprr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
48	3	eleq2i	⊢ ( 𝑀 ∈ 𝐵 ↔ 𝑀 ∈ ( Base ‘ 𝐶 ) )
49	48	biimpi	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( Base ‘ 𝐶 ) )
50	49	3ad2ant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ ( Base ‘ 𝐶 ) )
51	50	ad3antrrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑀 ∈ ( Base ‘ 𝐶 ) )
52	51 3	eleqtrrdi	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑀 ∈ 𝐵 )
53	2 45 3 46 47 52	matecld	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
54		eqid	⊢ ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) = ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) )
55		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
56		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
57	54 45 1 55 56	coe1fsupp	⊢ ( ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑃 ) → ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ∈ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp ( 0_g ‘ 𝑅 ) } )
58	53 57	syl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ∈ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp ( 0_g ‘ 𝑅 ) } )
59	4	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 0 = ( 0_g ‘ 𝑅 ) )
60	59	breq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑣 finSupp 0 ↔ 𝑣 finSupp ( 0_g ‘ 𝑅 ) ) )
61	60	rabbidv	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } = { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp ( 0_g ‘ 𝑅 ) } )
62	61	eleq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ∈ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ↔ ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ∈ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp ( 0_g ‘ 𝑅 ) } ) )
63	62	ad3antrrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ∈ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ↔ ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ∈ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp ( 0_g ‘ 𝑅 ) } ) )
64	58 63	mpbird	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ∈ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } )
65	44 64	elind	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) )
66		simplr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑥 ∈ ℕ₀ )
67		fveq1	⊢ ( 𝑤 = ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) → ( 𝑤 ‘ 𝑧 ) = ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑧 ) )
68	67	eqeq1d	⊢ ( 𝑤 = ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) → ( ( 𝑤 ‘ 𝑧 ) = 0 ↔ ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑧 ) = 0 ) )
69	68	imbi2d	⊢ ( 𝑤 = ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) → ( ( 𝑠 < 𝑧 → ( 𝑤 ‘ 𝑧 ) = 0 ) ↔ ( 𝑠 < 𝑧 → ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑧 ) = 0 ) ) )
70		breq2	⊢ ( 𝑧 = 𝑥 → ( 𝑠 < 𝑧 ↔ 𝑠 < 𝑥 ) )
71		fveqeq2	⊢ ( 𝑧 = 𝑥 → ( ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑧 ) = 0 ↔ ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = 0 ) )
72	70 71	imbi12d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑠 < 𝑧 → ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑧 ) = 0 ) ↔ ( 𝑠 < 𝑥 → ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = 0 ) ) )
73	69 72	rspc2v	⊢ ( ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∧ 𝑥 ∈ ℕ₀ ) → ( ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∀ 𝑧 ∈ ℕ₀ ( 𝑠 < 𝑧 → ( 𝑤 ‘ 𝑧 ) = 0 ) → ( 𝑠 < 𝑥 → ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = 0 ) ) )
74	65 66 73	syl2anc	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∀ 𝑧 ∈ ℕ₀ ( 𝑠 < 𝑧 → ( 𝑤 ‘ 𝑧 ) = 0 ) → ( 𝑠 < 𝑥 → ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = 0 ) ) )
75	74	ex	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) → ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∀ 𝑧 ∈ ℕ₀ ( 𝑠 < 𝑧 → ( 𝑤 ‘ 𝑧 ) = 0 ) → ( 𝑠 < 𝑥 → ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = 0 ) ) ) )
76	75	com23	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ 𝑥 ∈ ℕ₀ ) → ( ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∀ 𝑧 ∈ ℕ₀ ( 𝑠 < 𝑧 → ( 𝑤 ‘ 𝑧 ) = 0 ) → ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑠 < 𝑥 → ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = 0 ) ) ) )
77	76	impancom	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∀ 𝑧 ∈ ℕ₀ ( 𝑠 < 𝑧 → ( 𝑤 ‘ 𝑧 ) = 0 ) ) → ( 𝑥 ∈ ℕ₀ → ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑠 < 𝑥 → ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = 0 ) ) ) )
78	77	imp	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∀ 𝑧 ∈ ℕ₀ ( 𝑠 < 𝑧 → ( 𝑤 ‘ 𝑧 ) = 0 ) ) ∧ 𝑥 ∈ ℕ₀ ) → ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑠 < 𝑥 → ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = 0 ) ) )
79	78	com23	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∀ 𝑧 ∈ ℕ₀ ( 𝑠 < 𝑧 → ( 𝑤 ‘ 𝑧 ) = 0 ) ) ∧ 𝑥 ∈ ℕ₀ ) → ( 𝑠 < 𝑥 → ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = 0 ) ) )
80	79	ralrimdvv	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∀ 𝑧 ∈ ℕ₀ ( 𝑠 < 𝑧 → ( 𝑤 ‘ 𝑧 ) = 0 ) ) ∧ 𝑥 ∈ ℕ₀ ) → ( 𝑠 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = 0 ) )
81	80	ralrimiva	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) ∧ ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∀ 𝑧 ∈ ℕ₀ ( 𝑠 < 𝑧 → ( 𝑤 ‘ 𝑧 ) = 0 ) ) → ∀ 𝑥 ∈ ℕ₀ ( 𝑠 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = 0 ) )
82	81	ex	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ₀ ) → ( ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∀ 𝑧 ∈ ℕ₀ ( 𝑠 < 𝑧 → ( 𝑤 ‘ 𝑧 ) = 0 ) → ∀ 𝑥 ∈ ℕ₀ ( 𝑠 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = 0 ) ) )
83	82	reximdva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ℕ₀ ∀ 𝑤 ∈ ( ∪ 𝑢 ∈ ( 𝑁 × 𝑁 ) { ( coe₁ ‘ ( 𝑀 ‘ 𝑢 ) ) } ∩ { 𝑣 ∈ ( ( Base ‘ 𝑅 ) ↑_m ℕ₀ ) ∣ 𝑣 finSupp 0 } ) ∀ 𝑧 ∈ ℕ₀ ( 𝑠 < 𝑧 → ( 𝑤 ‘ 𝑧 ) = 0 ) → ∃ 𝑠 ∈ ℕ₀ ∀ 𝑥 ∈ ℕ₀ ( 𝑠 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = 0 ) ) )
84	32 83	mpd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ₀ ∀ 𝑥 ∈ ℕ₀ ( 𝑠 < 𝑥 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑥 ) = 0 ) )

Metamath Proof Explorer

Theorem pmatcoe1fsupp

Proof