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 ∧ 𝑀 ∈ 𝐵 ) → ( 𝑀 ∈ 𝑆 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∃ 𝑘 ∈ 𝐾 ( 𝑖 𝑀 𝑗 ) = ( 𝐴 ‘ 𝑘 ) ) )