Theorem cpmat

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

	Ref	Expression
Hypotheses	cpmat.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
	cpmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	cpmat.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	cpmat.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	cpmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑆 = { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) } )

Proof

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