Metamath Proof Explorer


Theorem cpmatel2

Description: Another property of a constant polynomial matrix. (Contributed by AV, 16-Nov-2019) (Proof shortened by AV, 27-Nov-2019)

Ref Expression
Hypotheses cpmat.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
cpmat.p 𝑃 = ( Poly1𝑅 )
cpmat.c 𝐶 = ( 𝑁 Mat 𝑃 )
cpmat.b 𝐵 = ( Base ‘ 𝐶 )
cpmatel2.k 𝐾 = ( Base ‘ 𝑅 )
cpmatel2.a 𝐴 = ( algSc ‘ 𝑃 )
Assertion cpmatel2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑀𝑆 ↔ ∀ 𝑖𝑁𝑗𝑁𝑘𝐾 ( 𝑖 𝑀 𝑗 ) = ( 𝐴𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 cpmat.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2 cpmat.p 𝑃 = ( Poly1𝑅 )
3 cpmat.c 𝐶 = ( 𝑁 Mat 𝑃 )
4 cpmat.b 𝐵 = ( Base ‘ 𝐶 )
5 cpmatel2.k 𝐾 = ( Base ‘ 𝑅 )
6 cpmatel2.a 𝐴 = ( algSc ‘ 𝑃 )
7 1 2 3 4 cpmatel ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑀𝑆 ↔ ∀ 𝑖𝑁𝑗𝑁𝑙 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑙 ) = ( 0g𝑅 ) ) )
8 simpl2 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑅 ∈ Ring )
9 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
10 simprl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑖𝑁 )
11 simprr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑗𝑁 )
12 simpl3 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑀𝐵 )
13 3 9 4 10 11 12 matecld ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
14 eqid ( 0g𝑅 ) = ( 0g𝑅 )
15 5 14 2 9 6 cply1coe0bi ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑃 ) ) → ( ∃ 𝑘𝐾 ( 𝑖 𝑀 𝑗 ) = ( 𝐴𝑘 ) ↔ ∀ 𝑙 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑙 ) = ( 0g𝑅 ) ) )
16 8 13 15 syl2anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( ∃ 𝑘𝐾 ( 𝑖 𝑀 𝑗 ) = ( 𝐴𝑘 ) ↔ ∀ 𝑙 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑙 ) = ( 0g𝑅 ) ) )
17 16 bicomd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( ∀ 𝑙 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑙 ) = ( 0g𝑅 ) ↔ ∃ 𝑘𝐾 ( 𝑖 𝑀 𝑗 ) = ( 𝐴𝑘 ) ) )
18 17 2ralbidva ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( ∀ 𝑖𝑁𝑗𝑁𝑙 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑙 ) = ( 0g𝑅 ) ↔ ∀ 𝑖𝑁𝑗𝑁𝑘𝐾 ( 𝑖 𝑀 𝑗 ) = ( 𝐴𝑘 ) ) )
19 7 18 bitrd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑀𝑆 ↔ ∀ 𝑖𝑁𝑗𝑁𝑘𝐾 ( 𝑖 𝑀 𝑗 ) = ( 𝐴𝑘 ) ) )