Metamath Proof Explorer


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