Metamath Proof Explorer

Theorem cpmatmcl

Description: The set of all constant polynomial matrices over a ring R is closed under multiplication. (Contributed by AV, 18-Nov-2019)

Ref Expression
Hypotheses cpmatsrngpmat.s ⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
cpmatsrngpmat.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
cpmatsrngpmat.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
Assertion cpmatmcl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 cpmatsrngpmat.s ⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2 cpmatsrngpmat.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 cpmatsrngpmat.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
4 1 2 3 cpmatmcllem ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) )
5 2 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
6 5 ad4antlr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑃 ∈ Ring )
7 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
8 1 2 3 7 cpmatpmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
9 8 3expa ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
10 1 2 3 7 cpmatpmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
11 10 3expa ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
12 9 11 anim12dan ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) )
13 12 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑖 ∈ 𝑁 ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) )
14 13 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) )
15 simpr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑖 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
16 15 anim1i ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) )
17 eqid ⊢ ( .r ‘ 𝐶 ) = ( .r ‘ 𝐶 )
18 3 7 17 matmulcell ⊢ ( ( 𝑃 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) = ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) )
19 6 14 16 18 syl3anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) = ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) )
20 19 fveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) )
21 20 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑐 ∈ ℕ ) → ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) )
22 21 fveq1d ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑐 ∈ ℕ ) → ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑐 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) )
23 22 eqeq1d ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) ∧ 𝑐 ∈ ℕ ) → ( ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ↔ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
24 23 ralbidva ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ↔ ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
25 24 ralbidva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑖 ∈ 𝑁 ) → ( ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ↔ ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
26 25 ralbidva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
27 4 26 mpbird ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) )
28 simpl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑁 ∈ Fin )
29 28 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑁 ∈ Fin )
30 simpr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
31 30 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑅 ∈ Ring )
32 2 3 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
33 32 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝐶 ∈ Ring )
34 simpl ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
35 34 anim2i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) )
36 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) )
37 35 36 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆 ) )
38 37 8 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
39 simpr ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑆 )
40 39 anim2i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑦 ∈ 𝑆 ) )
41 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑆 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑦 ∈ 𝑆 ) )
42 40 41 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑆 ) )
43 42 10 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
44 7 17 ringcl ⊢ ( ( 𝐶 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
45 33 38 43 44 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
46 1 2 3 7 cpmatel ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝑆 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
47 29 31 45 46 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝑆 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
48 27 47 mpbird ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝑆 )
49 48 ralrimivva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝑆 )