Metamath Proof Explorer

Theorem cpmatinvcl

Description: The set of all constant polynomial matrices over a ring R is closed under inversion. (Contributed by AV, 17-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

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

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 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
7 1 2 3 4 5 6 cpmatelimp2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( x e. S -> ( x e. ( Base ` C ) /\ A. i e. N A. j e. N E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) ) ) )
8 2 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
9 8 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R = ( Scalar ` P ) )
10 9 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ a e. ( Base ` R ) ) -> R = ( Scalar ` P ) )
11 10 eqcomd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ a e. ( Base ` R ) ) -> ( Scalar ` P ) = R )
12 11 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ a e. ( Base ` R ) ) -> ( invg ` ( Scalar ` P ) ) = ( invg ` R ) )
13 12 fveq1d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ a e. ( Base ` R ) ) -> ( ( invg ` ( Scalar ` P ) ) ` a ) = ( ( invg ` R ) ` a ) )
14 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
15 14 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Grp )
16 eqid 
 |-  ( invg ` R ) = ( invg ` R )
17 5 16 grpinvcl 
 |-  ( ( R e. Grp /\ a e. ( Base ` R ) ) -> ( ( invg ` R ) ` a ) e. ( Base ` R ) )
18 15 17 sylan 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ a e. ( Base ` R ) ) -> ( ( invg ` R ) ` a ) e. ( Base ` R ) )
19 13 18 eqeltrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ a e. ( Base ` R ) ) -> ( ( invg ` ( Scalar ` P ) ) ` a ) e. ( Base ` R ) )
20 19 ad5ant14 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) /\ a e. ( Base ` R ) ) /\ ( i x j ) = ( ( algSc ` P ) ` a ) ) -> ( ( invg ` ( Scalar ` P ) ) ` a ) e. ( Base ` R ) )
21 fveq2 
 |-  ( c = ( ( invg ` ( Scalar ` P ) ) ` a ) -> ( ( algSc ` P ) ` c ) = ( ( algSc ` P ) ` ( ( invg ` ( Scalar ` P ) ) ` a ) ) )
22 21 eqeq2d 
 |-  ( c = ( ( invg ` ( Scalar ` P ) ) ` a ) -> ( ( i ( ( invg ` C ) ` x ) j ) = ( ( algSc ` P ) ` c ) <-> ( i ( ( invg ` C ) ` x ) j ) = ( ( algSc ` P ) ` ( ( invg ` ( Scalar ` P ) ) ` a ) ) ) )
23 22 adantl 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) /\ a e. ( Base ` R ) ) /\ ( i x j ) = ( ( algSc ` P ) ` a ) ) /\ c = ( ( invg ` ( Scalar ` P ) ) ` a ) ) -> ( ( i ( ( invg ` C ) ` x ) j ) = ( ( algSc ` P ) ` c ) <-> ( i ( ( invg ` C ) ` x ) j ) = ( ( algSc ` P ) ` ( ( invg ` ( Scalar ` P ) ) ` a ) ) ) )
24 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
25 24 ad3antlr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) -> P e. Ring )
26 simplr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) -> x e. ( Base ` C ) )
27 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) -> ( i e. N /\ j e. N ) )
28 25 26 27 3jca 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) -> ( P e. Ring /\ x e. ( Base ` C ) /\ ( i e. N /\ j e. N ) ) )
29 28 ad2antrr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) /\ a e. ( Base ` R ) ) /\ ( i x j ) = ( ( algSc ` P ) ` a ) ) -> ( P e. Ring /\ x e. ( Base ` C ) /\ ( i e. N /\ j e. N ) ) )
30 eqid 
 |-  ( invg ` P ) = ( invg ` P )
31 eqid 
 |-  ( invg ` C ) = ( invg ` C )
32 3 4 30 31 matinvgcell 
 |-  ( ( P e. Ring /\ x e. ( Base ` C ) /\ ( i e. N /\ j e. N ) ) -> ( i ( ( invg ` C ) ` x ) j ) = ( ( invg ` P ) ` ( i x j ) ) )
33 29 32 syl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) /\ a e. ( Base ` R ) ) /\ ( i x j ) = ( ( algSc ` P ) ` a ) ) -> ( i ( ( invg ` C ) ` x ) j ) = ( ( invg ` P ) ` ( i x j ) ) )
34 fveq2 
 |-  ( ( i x j ) = ( ( algSc ` P ) ` a ) -> ( ( invg ` P ) ` ( i x j ) ) = ( ( invg ` P ) ` ( ( algSc ` P ) ` a ) ) )
35 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
36 25 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) /\ a e. ( Base ` R ) ) -> P e. Ring )
37 2 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
38 37 ad3antlr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) -> P e. LMod )
39 38 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) /\ a e. ( Base ` R ) ) -> P e. LMod )
40 6 35 36 39 asclghm 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) /\ a e. ( Base ` R ) ) -> ( algSc ` P ) e. ( ( Scalar ` P ) GrpHom P ) )
41 9 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
42 41 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( a e. ( Base ` R ) <-> a e. ( Base ` ( Scalar ` P ) ) ) )
43 42 biimpd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( a e. ( Base ` R ) -> a e. ( Base ` ( Scalar ` P ) ) ) )
44 43 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) -> ( a e. ( Base ` R ) -> a e. ( Base ` ( Scalar ` P ) ) ) )
45 44 imp 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) /\ a e. ( Base ` R ) ) -> a e. ( Base ` ( Scalar ` P ) ) )
46 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
47 eqid 
 |-  ( invg ` ( Scalar ` P ) ) = ( invg ` ( Scalar ` P ) )
48 46 47 30 ghminv 
 |-  ( ( ( algSc ` P ) e. ( ( Scalar ` P ) GrpHom P ) /\ a e. ( Base ` ( Scalar ` P ) ) ) -> ( ( algSc ` P ) ` ( ( invg ` ( Scalar ` P ) ) ` a ) ) = ( ( invg ` P ) ` ( ( algSc ` P ) ` a ) ) )
49 40 45 48 syl2anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) /\ a e. ( Base ` R ) ) -> ( ( algSc ` P ) ` ( ( invg ` ( Scalar ` P ) ) ` a ) ) = ( ( invg ` P ) ` ( ( algSc ` P ) ` a ) ) )
50 49 eqcomd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) /\ a e. ( Base ` R ) ) -> ( ( invg ` P ) ` ( ( algSc ` P ) ` a ) ) = ( ( algSc ` P ) ` ( ( invg ` ( Scalar ` P ) ) ` a ) ) )
51 34 50 sylan9eqr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) /\ a e. ( Base ` R ) ) /\ ( i x j ) = ( ( algSc ` P ) ` a ) ) -> ( ( invg ` P ) ` ( i x j ) ) = ( ( algSc ` P ) ` ( ( invg ` ( Scalar ` P ) ) ` a ) ) )
52 33 51 eqtrd 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) /\ a e. ( Base ` R ) ) /\ ( i x j ) = ( ( algSc ` P ) ` a ) ) -> ( i ( ( invg ` C ) ` x ) j ) = ( ( algSc ` P ) ` ( ( invg ` ( Scalar ` P ) ) ` a ) ) )
53 20 23 52 rspcedvd 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) /\ a e. ( Base ` R ) ) /\ ( i x j ) = ( ( algSc ` P ) ` a ) ) -> E. c e. ( Base ` R ) ( i ( ( invg ` C ) ` x ) j ) = ( ( algSc ` P ) ` c ) )
54 53 rexlimdva2 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) -> ( E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) -> E. c e. ( Base ` R ) ( i ( ( invg ` C ) ` x ) j ) = ( ( algSc ` P ) ` c ) ) )
55 54 ralimdvva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` C ) ) -> ( A. i e. N A. j e. N E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) -> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( ( invg ` C ) ` x ) j ) = ( ( algSc ` P ) ` c ) ) )
56 55 expimpd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( x e. ( Base ` C ) /\ A. i e. N A. j e. N E. a e. ( Base ` R ) ( i x j ) = ( ( algSc ` P ) ` a ) ) -> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( ( invg ` C ) ` x ) j ) = ( ( algSc ` P ) ` c ) ) )
57 7 56 syld 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( x e. S -> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( ( invg ` C ) ` x ) j ) = ( ( algSc ` P ) ` c ) ) )
58 57 imp 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) -> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( ( invg ` C ) ` x ) j ) = ( ( algSc ` P ) ` c ) )
59 simpll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) -> N e. Fin )
60 simplr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) -> R e. Ring )
61 2 3 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
62 ringgrp 
 |-  ( C e. Ring -> C e. Grp )
63 61 62 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Grp )
64 63 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) -> C e. Grp )
65 1 2 3 4 cpmatpmat 
 |-  ( ( N e. Fin /\ R e. Ring /\ x e. S ) -> x e. ( Base ` C ) )
66 65 3expa 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) -> x e. ( Base ` C ) )
67 4 31 grpinvcl 
 |-  ( ( C e. Grp /\ x e. ( Base ` C ) ) -> ( ( invg ` C ) ` x ) e. ( Base ` C ) )
68 64 66 67 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) -> ( ( invg ` C ) ` x ) e. ( Base ` C ) )
69 1 2 3 4 5 6 cpmatel2 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( ( invg ` C ) ` x ) e. ( Base ` C ) ) -> ( ( ( invg ` C ) ` x ) e. S <-> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( ( invg ` C ) ` x ) j ) = ( ( algSc ` P ) ` c ) ) )
70 59 60 68 69 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) -> ( ( ( invg ` C ) ` x ) e. S <-> A. i e. N A. j e. N E. c e. ( Base ` R ) ( i ( ( invg ` C ) ` x ) j ) = ( ( algSc ` P ) ` c ) ) )
71 58 70 mpbird 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) -> ( ( invg ` C ) ` x ) e. S )
72 71 ralrimiva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. x e. S ( ( invg ` C ) ` x ) e. S )