Metamath Proof Explorer

Theorem m2cpminvid

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

Ref Expression
Hypotheses m2cpminvid.i 
|- I = ( N cPolyMatToMat R )
m2cpminvid.a 
|- A = ( N Mat R )
m2cpminvid.k 
|- K = ( Base ` A )
m2cpminvid.t 
|- T = ( N matToPolyMat R )
Assertion m2cpminvid 
|- ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( I ` ( T ` M ) ) = M )

Proof

Step Hyp Ref Expression
1 m2cpminvid.i 
 |-  I = ( N cPolyMatToMat R )
2 m2cpminvid.a 
 |-  A = ( N Mat R )
3 m2cpminvid.k 
 |-  K = ( Base ` A )
4 m2cpminvid.t 
 |-  T = ( N matToPolyMat R )
5 eqid 
 |-  ( N ConstPolyMat R ) = ( N ConstPolyMat R )
6 5 4 2 3 m2cpm 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( T ` M ) e. ( N ConstPolyMat R ) )
7 1 5 cpm2mval 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( T ` M ) e. ( N ConstPolyMat R ) ) -> ( I ` ( T ` M ) ) = ( x e. N , y e. N |-> ( ( coe1 ` ( x ( T ` M ) y ) ) ` 0 ) ) )
8 6 7 syld3an3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( I ` ( T ` M ) ) = ( x e. N , y e. N |-> ( ( coe1 ` ( x ( T ` M ) y ) ) ` 0 ) ) )
9 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
10 eqid 
 |-  ( algSc ` ( Poly1 ` R ) ) = ( algSc ` ( Poly1 ` R ) )
11 4 2 3 9 10 mat2pmatvalel 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ ( x e. N /\ y e. N ) ) -> ( x ( T ` M ) y ) = ( ( algSc ` ( Poly1 ` R ) ) ` ( x M y ) ) )
12 11 3impb 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> ( x ( T ` M ) y ) = ( ( algSc ` ( Poly1 ` R ) ) ` ( x M y ) ) )
13 12 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> ( coe1 ` ( x ( T ` M ) y ) ) = ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( x M y ) ) ) )
14 13 fveq1d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> ( ( coe1 ` ( x ( T ` M ) y ) ) ` 0 ) = ( ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( x M y ) ) ) ` 0 ) )
15 simp12 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> R e. Ring )
16 eqid 
 |-  ( Base ` R ) = ( Base ` R )
17 simp2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> x e. N )
18 simp3 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> y e. N )
19 simp13 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> M e. K )
20 2 16 3 17 18 19 matecld 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> ( x M y ) e. ( Base ` R ) )
21 9 10 16 ply1sclid 
 |-  ( ( R e. Ring /\ ( x M y ) e. ( Base ` R ) ) -> ( x M y ) = ( ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( x M y ) ) ) ` 0 ) )
22 15 20 21 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> ( x M y ) = ( ( coe1 ` ( ( algSc ` ( Poly1 ` R ) ) ` ( x M y ) ) ) ` 0 ) )
23 14 22 eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ x e. N /\ y e. N ) -> ( ( coe1 ` ( x ( T ` M ) y ) ) ` 0 ) = ( x M y ) )
24 23 mpoeq3dva 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( x e. N , y e. N |-> ( ( coe1 ` ( x ( T ` M ) y ) ) ` 0 ) ) = ( x e. N , y e. N |-> ( x M y ) ) )
25 eqidd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ ( i e. N /\ j e. N ) ) -> ( x e. N , y e. N |-> ( x M y ) ) = ( x e. N , y e. N |-> ( x M y ) ) )
26 oveq12 
 |-  ( ( x = i /\ y = j ) -> ( x M y ) = ( i M j ) )
27 26 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ ( i e. N /\ j e. N ) ) /\ ( x = i /\ y = j ) ) -> ( x M y ) = ( i M j ) )
28 simprl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
29 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
30 ovexd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ ( i e. N /\ j e. N ) ) -> ( i M j ) e. _V )
31 25 27 28 29 30 ovmpod 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. K ) /\ ( i e. N /\ j e. N ) ) -> ( i ( x e. N , y e. N |-> ( x M y ) ) j ) = ( i M j ) )
32 31 ralrimivva 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> A. i e. N A. j e. N ( i ( x e. N , y e. N |-> ( x M y ) ) j ) = ( i M j ) )
33 simp1 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> N e. Fin )
34 simp2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> R e. Ring )
35 2 16 3 33 34 20 matbas2d 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( x e. N , y e. N |-> ( x M y ) ) e. K )
36 simp3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> M e. K )
37 2 3 eqmat 
 |-  ( ( ( x e. N , y e. N |-> ( x M y ) ) e. K /\ M e. K ) -> ( ( x e. N , y e. N |-> ( x M y ) ) = M <-> A. i e. N A. j e. N ( i ( x e. N , y e. N |-> ( x M y ) ) j ) = ( i M j ) ) )
38 35 36 37 syl2anc 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( ( x e. N , y e. N |-> ( x M y ) ) = M <-> A. i e. N A. j e. N ( i ( x e. N , y e. N |-> ( x M y ) ) j ) = ( i M j ) ) )
39 32 38 mpbird 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( x e. N , y e. N |-> ( x M y ) ) = M )
40 8 24 39 3eqtrd 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. K ) -> ( I ` ( T ` M ) ) = M )