Theorem cpmat 22210

Description: Value of the constructor of the set of all constant polynomial matrices, i.e. the set of all 𝑁 x 𝑁 matrices of polynomials over a ring 𝑅. (Contributed by AV, 15-Nov-2019.)

Hypotheses

Ref	Expression
cpmat.s	⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)
cpmat.p	⊢ 𝑃 = (Poly1‘𝑅)
cpmat.c	⊢ 𝐶 = (𝑁 Mat 𝑃)
cpmat.b	⊢ 𝐵 = (Base‘𝐶)

Assertion

Ref	Expression
cpmat	⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑆 = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)})

Distinct variable groups:   𝐵,𝑚   𝑖,𝑁,𝑗,𝑘,𝑚   𝑅,𝑖,𝑗,𝑘,𝑚

Allowed substitution hints:   𝐵(𝑖,𝑗,𝑘)   𝐶(𝑖,𝑗,𝑘,𝑚)   𝑃(𝑖,𝑗,𝑘,𝑚)   𝑆(𝑖,𝑗,𝑘,𝑚)   𝑉(𝑖,𝑗,𝑘,𝑚)

Proof of Theorem cpmat

Dummy variables 𝑛 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cpmat.s	. 2 ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)
2		df-cpmat 22207	. . . 4 ⊢ ConstPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)})
3	2	a1i 11	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → ConstPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)}))
4		simpl 483	. . . . . . . 8 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → 𝑛 = 𝑁)
5		fveq2 6891	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) = (Poly1‘𝑅))
6	5	adantl 482	. . . . . . . 8 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Poly1‘𝑟) = (Poly1‘𝑅))
7	4, 6	oveq12d 7426	. . . . . . 7 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑛 Mat (Poly1‘𝑟)) = (𝑁 Mat (Poly1‘𝑅)))
8	7	fveq2d 6895	. . . . . 6 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat (Poly1‘𝑟))) = (Base‘(𝑁 Mat (Poly1‘𝑅))))
9		cpmat.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐶)
10		cpmat.c	. . . . . . . . 9 ⊢ 𝐶 = (𝑁 Mat 𝑃)
11		cpmat.p	. . . . . . . . . 10 ⊢ 𝑃 = (Poly1‘𝑅)
12	11	oveq2i 7419	. . . . . . . . 9 ⊢ (𝑁 Mat 𝑃) = (𝑁 Mat (Poly1‘𝑅))
13	10, 12	eqtri 2760	. . . . . . . 8 ⊢ 𝐶 = (𝑁 Mat (Poly1‘𝑅))
14	13	fveq2i 6894	. . . . . . 7 ⊢ (Base‘𝐶) = (Base‘(𝑁 Mat (Poly1‘𝑅)))
15	9, 14	eqtri 2760	. . . . . 6 ⊢ 𝐵 = (Base‘(𝑁 Mat (Poly1‘𝑅)))
16	8, 15	eqtr4di 2790	. . . . 5 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat (Poly1‘𝑟))) = 𝐵)
17		fveq2 6891	. . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅))
18	17	adantl 482	. . . . . . . . 9 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (0g‘𝑟) = (0g‘𝑅))
19	18	eqeq2d 2743	. . . . . . . 8 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟) ↔ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)))
20	19	ralbidv 3177	. . . . . . 7 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟) ↔ ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)))
21	4, 20	raleqbidv 3342	. . . . . 6 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟) ↔ ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)))
22	4, 21	raleqbidv 3342	. . . . 5 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟) ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)))
23	16, 22	rabeqbidv 3449	. . . 4 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → {𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)} = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)})
24	23	adantl 482	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) ∧ (𝑛 = 𝑁 ∧ 𝑟 = 𝑅)) → {𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)} = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)})
25		simpl 483	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑁 ∈ Fin)
26		elex 3492	. . . 4 ⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V)
27	26	adantl 482	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑅 ∈ V)
28	9	fvexi 6905	. . . 4 ⊢ 𝐵 ∈ V
29		rabexg 5331	. . . 4 ⊢ (𝐵 ∈ V → {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)} ∈ V)
30	28, 29	mp1i 13	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)} ∈ V)
31	3, 24, 25, 27, 30	ovmpod 7559	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑁 ConstPolyMat 𝑅) = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)})
32	1, 31	eqtrid 2784	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑆 = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)})

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3061  {crab 3432  Vcvv 3474  ‘cfv 6543  (class class class)co 7408   ∈ cmpo 7410  Fincfn 8938  ℕcn 12211  Basecbs 17143  0_gc0g 17384  Poly₁cpl1 21700  coe₁cco1 21701   Mat cmat 21906   ConstPolyMat ccpmat 22204

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 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-cpmat 22207

This theorem is referenced by:  cpmatpmat  22211  cpmatel  22212  cpmatsubgpmat  22221