Metamath Proof Explorer

Theorem cpmatsubgpmat

Description: The set of all constant polynomial matrices over a ring R is an additive subgroup of the ring of all polynomial matrices over the ring R . (Contributed by AV, 15-Nov-2019)

Ref Expression
Hypotheses cpmatsrngpmat.s
`|- S = ( N ConstPolyMat R )`
cpmatsrngpmat.p
`|- P = ( Poly1 ` R )`
cpmatsrngpmat.c
`|- C = ( N Mat P )`
Assertion cpmatsubgpmat
`|- ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubGrp ` C ) )`

Proof

Step Hyp Ref Expression
1 cpmatsrngpmat.s
` |-  S = ( N ConstPolyMat R )`
2 cpmatsrngpmat.p
` |-  P = ( Poly1 ` R )`
3 cpmatsrngpmat.c
` |-  C = ( N Mat P )`
4 eqid
` |-  ( Base ` C ) = ( Base ` C )`
5 1 2 3 4 cpmat
` |-  ( ( N e. Fin /\ R e. Ring ) -> S = { m e. ( Base ` C ) | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } )`
6 ssrab2
` |-  { m e. ( Base ` C ) | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } C_ ( Base ` C )`
7 5 6 eqsstrdi
` |-  ( ( N e. Fin /\ R e. Ring ) -> S C_ ( Base ` C ) )`
8 1 2 3 1elcpmat
` |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` C ) e. S )`
9 8 ne0d
` |-  ( ( N e. Fin /\ R e. Ring ) -> S =/= (/) )`
10 1 2 3 cpmatacl
` |-  ( ( N e. Fin /\ R e. Ring ) -> A. x e. S A. y e. S ( x ( +g ` C ) y ) e. S )`
11 1 2 3 cpmatinvcl
` |-  ( ( N e. Fin /\ R e. Ring ) -> A. x e. S ( ( invg ` C ) ` x ) e. S )`
12 r19.26
` |-  ( A. x e. S ( A. y e. S ( x ( +g ` C ) y ) e. S /\ ( ( invg ` C ) ` x ) e. S ) <-> ( A. x e. S A. y e. S ( x ( +g ` C ) y ) e. S /\ A. x e. S ( ( invg ` C ) ` x ) e. S ) )`
13 10 11 12 sylanbrc
` |-  ( ( N e. Fin /\ R e. Ring ) -> A. x e. S ( A. y e. S ( x ( +g ` C ) y ) e. S /\ ( ( invg ` C ) ` x ) e. S ) )`
14 2 3 pmatring
` |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )`
15 ringgrp
` |-  ( C e. Ring -> C e. Grp )`
16 eqid
` |-  ( +g ` C ) = ( +g ` C )`
17 eqid
` |-  ( invg ` C ) = ( invg ` C )`
18 4 16 17 issubg2
` |-  ( C e. Grp -> ( S e. ( SubGrp ` C ) <-> ( S C_ ( Base ` C ) /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x ( +g ` C ) y ) e. S /\ ( ( invg ` C ) ` x ) e. S ) ) ) )`
19 14 15 18 3syl
` |-  ( ( N e. Fin /\ R e. Ring ) -> ( S e. ( SubGrp ` C ) <-> ( S C_ ( Base ` C ) /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x ( +g ` C ) y ) e. S /\ ( ( invg ` C ) ` x ) e. S ) ) ) )`
20 7 9 13 19 mpbir3and
` |-  ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubGrp ` C ) )`