Theorem cpmatel

Description: Property of a constant polynomial matrix. (Contributed by AV, 15-Nov-2019)

	Ref	Expression
Hypotheses	cpmat.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
	cpmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	cpmat.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	cpmat.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	cpmatel	⊢ ( ( 𝑁 ∈ 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	1 2 3 4	cpmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑆 = { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) } )
6	5	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) → 𝑆 = { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) } )
7	6	eleq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) → ( 𝑀 ∈ 𝑆 ↔ 𝑀 ∈ { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) } ) )
8		oveq	⊢ ( 𝑚 = 𝑀 → ( 𝑖 𝑚 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
9	8	fveq2d	⊢ ( 𝑚 = 𝑀 → ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) )
10	9	fveq1d	⊢ ( 𝑚 = 𝑀 → ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) )
11	10	eqeq1d	⊢ ( 𝑚 = 𝑀 → ( ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) ↔ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) ) )
12	11	ralbidv	⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) ↔ ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) ) )
13	12	2ralbidv	⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) ) )
14	13	elrab	⊢ ( 𝑀 ∈ { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) } ↔ ( 𝑀 ∈ 𝐵 ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) ) )
15	7 14	bitrdi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) → ( 𝑀 ∈ 𝑆 ↔ ( 𝑀 ∈ 𝐵 ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) ) ) )
16	15	3anibar	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) → ( 𝑀 ∈ 𝑆 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) ) )