Theorem cpmatelimp

Description: Implication of a set being a constant polynomial matrix. (Contributed by AV, 18-Nov-2019)

	Ref	Expression
Hypotheses	cpmat.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
	cpmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	cpmat.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	cpmat.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	cpmatelimp	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ 𝑆 → ( 𝑀 ∈ 𝐵 ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( 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	cpmatpmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → 𝑀 ∈ 𝐵 )
6	5	3expa	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀 ∈ 𝑆 ) → 𝑀 ∈ 𝐵 )
7	1 2 3 4	cpmatel	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑀 ∈ 𝑆 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) ) )
8	7	3expa	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑀 ∈ 𝑆 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) ) )
9	8	biimpd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑀 ∈ 𝑆 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) ) )
10	9	impancom	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀 ∈ 𝑆 ) → ( 𝑀 ∈ 𝐵 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) ) )
11	6 10	jcai	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀 ∈ 𝑆 ) → ( 𝑀 ∈ 𝐵 ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) ) )
12	11	ex	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ 𝑆 → ( 𝑀 ∈ 𝐵 ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) ) ) )