Metamath Proof Explorer


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𝑅 ) ) ) )