Metamath Proof Explorer

Theorem m2cpminvid2

Description: The transformation applied to the inverse transformation of a constant polynomial matrix over the ring R results in the matrix itself. (Contributed by AV, 12-Nov-2019) (Revised by AV, 14-Dec-2019)

Ref Expression
Hypotheses m2cpminvid2.s 
|- S = ( N ConstPolyMat R )
m2cpminvid2.i 
|- I = ( N cPolyMatToMat R )
m2cpminvid2.t 
|- T = ( N matToPolyMat R )
Assertion m2cpminvid2 
|- ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> ( T ` ( I ` M ) ) = M )

Proof

Step Hyp Ref Expression
1 m2cpminvid2.s 
 |-  S = ( N ConstPolyMat R )
2 m2cpminvid2.i 
 |-  I = ( N cPolyMatToMat R )
3 m2cpminvid2.t 
 |-  T = ( N matToPolyMat R )
4 2 1 cpm2mval 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> ( I ` M ) = ( x e. N , y e. N |-> ( ( coe1 ` ( x M y ) ) ` 0 ) ) )
5 4 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> ( T ` ( I ` M ) ) = ( T ` ( x e. N , y e. N |-> ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) )
6 simp1 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> N e. Fin )
7 simp2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> R e. Ring )
8 eqid 
 |-  ( N Mat R ) = ( N Mat R )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 eqid 
 |-  ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) )
11 eqid 
 |-  ( N Mat ( Poly1 ` R ) ) = ( N Mat ( Poly1 ` R ) )
12 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
13 eqid 
 |-  ( Base ` ( N Mat ( Poly1 ` R ) ) ) = ( Base ` ( N Mat ( Poly1 ` R ) ) )
14 simp2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ x e. N /\ y e. N ) -> x e. N )
15 simp3 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ x e. N /\ y e. N ) -> y e. N )
16 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
17 1 16 11 13 cpmatpmat 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> M e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) )
18 17 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ x e. N /\ y e. N ) -> M e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) )
19 11 12 13 14 15 18 matecld 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ x e. N /\ y e. N ) -> ( x M y ) e. ( Base ` ( Poly1 ` R ) ) )
20 0nn0 
 |-  0 e. NN0
21 eqid 
 |-  ( coe1 ` ( x M y ) ) = ( coe1 ` ( x M y ) )
22 21 12 16 9 coe1fvalcl 
 |-  ( ( ( x M y ) e. ( Base ` ( Poly1 ` R ) ) /\ 0 e. NN0 ) -> ( ( coe1 ` ( x M y ) ) ` 0 ) e. ( Base ` R ) )
23 19 20 22 sylancl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ x e. N /\ y e. N ) -> ( ( coe1 ` ( x M y ) ) ` 0 ) e. ( Base ` R ) )
24 8 9 10 6 7 23 matbas2d 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> ( x e. N , y e. N |-> ( ( coe1 ` ( x M y ) ) ` 0 ) ) e. ( Base ` ( N Mat R ) ) )
25 eqid 
 |-  ( algSc ` ( Poly1 ` R ) ) = ( algSc ` ( Poly1 ` R ) )
26 3 8 10 16 25 mat2pmatval 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( x e. N , y e. N |-> ( ( coe1 ` ( x M y ) ) ` 0 ) ) e. ( Base ` ( N Mat R ) ) ) -> ( T ` ( x e. N , y e. N |-> ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) = ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( i ( x e. N , y e. N |-> ( ( coe1 ` ( x M y ) ) ` 0 ) ) j ) ) ) )
27 6 7 24 26 syl3anc 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> ( T ` ( x e. N , y e. N |-> ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) = ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( i ( x e. N , y e. N |-> ( ( coe1 ` ( x M y ) ) ` 0 ) ) j ) ) ) )
28 eqidd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ i e. N /\ j e. N ) -> ( x e. N , y e. N |-> ( ( coe1 ` ( x M y ) ) ` 0 ) ) = ( x e. N , y e. N |-> ( ( coe1 ` ( x M y ) ) ` 0 ) ) )
29 oveq12 
 |-  ( ( x = i /\ y = j ) -> ( x M y ) = ( i M j ) )
30 29 fveq2d 
 |-  ( ( x = i /\ y = j ) -> ( coe1 ` ( x M y ) ) = ( coe1 ` ( i M j ) ) )
31 30 fveq1d 
 |-  ( ( x = i /\ y = j ) -> ( ( coe1 ` ( x M y ) ) ` 0 ) = ( ( coe1 ` ( i M j ) ) ` 0 ) )
32 31 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ i e. N /\ j e. N ) /\ ( x = i /\ y = j ) ) -> ( ( coe1 ` ( x M y ) ) ` 0 ) = ( ( coe1 ` ( i M j ) ) ` 0 ) )
33 simp2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ i e. N /\ j e. N ) -> i e. N )
34 simp3 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ i e. N /\ j e. N ) -> j e. N )
35 fvexd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i M j ) ) ` 0 ) e. _V )
36 28 32 33 34 35 ovmpod 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ i e. N /\ j e. N ) -> ( i ( x e. N , y e. N |-> ( ( coe1 ` ( x M y ) ) ` 0 ) ) j ) = ( ( coe1 ` ( i M j ) ) ` 0 ) )
37 36 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ i e. N /\ j e. N ) -> ( ( algSc ` ( Poly1 ` R ) ) ` ( i ( x e. N , y e. N |-> ( ( coe1 ` ( x M y ) ) ` 0 ) ) j ) ) = ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) )
38 37 mpoeq3dva 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( i ( x e. N , y e. N |-> ( ( coe1 ` ( x M y ) ) ` 0 ) ) j ) ) ) = ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) ) )
39 27 38 eqtrd 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> ( T ` ( x e. N , y e. N |-> ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) = ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) ) )
40 1 16 m2cpminvid2lem 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> A. n e. NN0 ( ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) )
41 simpl2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> R e. Ring )
42 simprl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> x e. N )
43 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> y e. N )
44 17 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> M e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) )
45 11 12 13 42 43 44 matecld 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> ( x M y ) e. ( Base ` ( Poly1 ` R ) ) )
46 45 20 22 sylancl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> ( ( coe1 ` ( x M y ) ) ` 0 ) e. ( Base ` R ) )
47 16 25 9 12 ply1sclcl 
 |-  ( ( R e. Ring /\ ( ( coe1 ` ( x M y ) ) ` 0 ) e. ( Base ` R ) ) -> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) e. ( Base ` ( Poly1 ` R ) ) )
48 41 46 47 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) e. ( Base ` ( Poly1 ` R ) ) )
49 eqid 
 |-  ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) = ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) )
50 16 12 49 21 ply1coe1eq 
 |-  ( ( R e. Ring /\ ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) e. ( Base ` ( Poly1 ` R ) ) /\ ( x M y ) e. ( Base ` ( Poly1 ` R ) ) ) -> ( A. n e. NN0 ( ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) <-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) = ( x M y ) ) )
51 50 bicomd 
 |-  ( ( R e. Ring /\ ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) e. ( Base ` ( Poly1 ` R ) ) /\ ( x M y ) e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) = ( x M y ) <-> A. n e. NN0 ( ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) ) )
52 41 48 45 51 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> ( ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) = ( x M y ) <-> A. n e. NN0 ( ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( x M y ) ) ` n ) ) )
53 40 52 mpbird 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) = ( x M y ) )
54 53 ralrimivva 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> A. x e. N A. y e. N ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) = ( x M y ) )
55 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ x e. N ) /\ y e. N ) -> ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) ) = ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) ) )
56 oveq12 
 |-  ( ( i = x /\ j = y ) -> ( i M j ) = ( x M y ) )
57 56 fveq2d 
 |-  ( ( i = x /\ j = y ) -> ( coe1 ` ( i M j ) ) = ( coe1 ` ( x M y ) ) )
58 57 fveq1d 
 |-  ( ( i = x /\ j = y ) -> ( ( coe1 ` ( i M j ) ) ` 0 ) = ( ( coe1 ` ( x M y ) ) ` 0 ) )
59 58 fveq2d 
 |-  ( ( i = x /\ j = y ) -> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) = ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) )
60 59 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ x e. N ) /\ y e. N ) /\ ( i = x /\ j = y ) ) -> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) = ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) )
61 simplr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ x e. N ) /\ y e. N ) -> x e. N )
62 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ x e. N ) /\ y e. N ) -> y e. N )
63 fvexd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ x e. N ) /\ y e. N ) -> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) e. _V )
64 55 60 61 62 63 ovmpod 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ x e. N ) /\ y e. N ) -> ( x ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) ) y ) = ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) )
65 64 eqeq1d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ x e. N ) /\ y e. N ) -> ( ( x ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) ) y ) = ( x M y ) <-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) = ( x M y ) ) )
66 65 anasss 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( x e. N /\ y e. N ) ) -> ( ( x ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) ) y ) = ( x M y ) <-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) = ( x M y ) ) )
67 66 2ralbidva 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> ( A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) ) y ) = ( x M y ) <-> A. x e. N A. y e. N ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( x M y ) ) ` 0 ) ) = ( x M y ) ) )
68 54 67 mpbird 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) ) y ) = ( x M y ) )
69 fvexd 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> ( Poly1 ` R ) e. _V )
70 7 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ i e. N /\ j e. N ) -> R e. Ring )
71 17 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ i e. N /\ j e. N ) -> M e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) )
72 11 12 13 33 34 71 matecld 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ i e. N /\ j e. N ) -> ( i M j ) e. ( Base ` ( Poly1 ` R ) ) )
73 eqid 
 |-  ( coe1 ` ( i M j ) ) = ( coe1 ` ( i M j ) )
74 73 12 16 9 coe1fvalcl 
 |-  ( ( ( i M j ) e. ( Base ` ( Poly1 ` R ) ) /\ 0 e. NN0 ) -> ( ( coe1 ` ( i M j ) ) ` 0 ) e. ( Base ` R ) )
75 72 20 74 sylancl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i M j ) ) ` 0 ) e. ( Base ` R ) )
76 16 25 9 12 ply1sclcl 
 |-  ( ( R e. Ring /\ ( ( coe1 ` ( i M j ) ) ` 0 ) e. ( Base ` R ) ) -> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) e. ( Base ` ( Poly1 ` R ) ) )
77 70 75 76 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ i e. N /\ j e. N ) -> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) e. ( Base ` ( Poly1 ` R ) ) )
78 11 12 13 6 69 77 matbas2d 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) ) e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) )
79 11 13 eqmat 
 |-  ( ( ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) ) e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) /\ M e. ( Base ` ( N Mat ( Poly1 ` R ) ) ) ) -> ( ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) ) = M <-> A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) ) y ) = ( x M y ) ) )
80 78 17 79 syl2anc 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> ( ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) ) = M <-> A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) ) y ) = ( x M y ) ) )
81 68 80 mpbird 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> ( i e. N , j e. N |-> ( ( algSc ` ( Poly1 ` R ) ) ` ( ( coe1 ` ( i M j ) ) ` 0 ) ) ) = M )
82 5 39 81 3eqtrd 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> ( T ` ( I ` M ) ) = M )