Metamath Proof Explorer


Theorem mat2pmatf1

Description: The matrix transformation is a 1-1 function from the matrices to the polynomial matrices. (Contributed by AV, 28-Oct-2019) (Proof shortened by AV, 27-Nov-2019)

Ref Expression
Hypotheses mat2pmatbas.t
|- T = ( N matToPolyMat R )
mat2pmatbas.a
|- A = ( N Mat R )
mat2pmatbas.b
|- B = ( Base ` A )
mat2pmatbas.p
|- P = ( Poly1 ` R )
mat2pmatbas.c
|- C = ( N Mat P )
mat2pmatbas0.h
|- H = ( Base ` C )
Assertion mat2pmatf1
|- ( ( N e. Fin /\ R e. Ring ) -> T : B -1-1-> H )

Proof

Step Hyp Ref Expression
1 mat2pmatbas.t
 |-  T = ( N matToPolyMat R )
2 mat2pmatbas.a
 |-  A = ( N Mat R )
3 mat2pmatbas.b
 |-  B = ( Base ` A )
4 mat2pmatbas.p
 |-  P = ( Poly1 ` R )
5 mat2pmatbas.c
 |-  C = ( N Mat P )
6 mat2pmatbas0.h
 |-  H = ( Base ` C )
7 1 2 3 4 5 6 mat2pmatf
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : B --> H )
8 simpl
 |-  ( ( x e. B /\ y e. B ) -> x e. B )
9 8 anim2i
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ x e. B ) )
10 df-3an
 |-  ( ( N e. Fin /\ R e. Ring /\ x e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ x e. B ) )
11 9 10 sylibr
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( N e. Fin /\ R e. Ring /\ x e. B ) )
12 eqid
 |-  ( algSc ` P ) = ( algSc ` P )
13 1 2 3 4 12 mat2pmatvalel
 |-  ( ( ( N e. Fin /\ R e. Ring /\ x e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( T ` x ) j ) = ( ( algSc ` P ) ` ( i x j ) ) )
14 11 13 sylan
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( i ( T ` x ) j ) = ( ( algSc ` P ) ` ( i x j ) ) )
15 simpr
 |-  ( ( x e. B /\ y e. B ) -> y e. B )
16 15 anim2i
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ y e. B ) )
17 df-3an
 |-  ( ( N e. Fin /\ R e. Ring /\ y e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ y e. B ) )
18 16 17 sylibr
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( N e. Fin /\ R e. Ring /\ y e. B ) )
19 1 2 3 4 12 mat2pmatvalel
 |-  ( ( ( N e. Fin /\ R e. Ring /\ y e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( T ` y ) j ) = ( ( algSc ` P ) ` ( i y j ) ) )
20 18 19 sylan
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( i ( T ` y ) j ) = ( ( algSc ` P ) ` ( i y j ) ) )
21 14 20 eqeq12d
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( ( i ( T ` x ) j ) = ( i ( T ` y ) j ) <-> ( ( algSc ` P ) ` ( i x j ) ) = ( ( algSc ` P ) ` ( i y j ) ) ) )
22 eqid
 |-  ( Base ` R ) = ( Base ` R )
23 eqid
 |-  ( Base ` P ) = ( Base ` P )
24 4 12 22 23 ply1sclf1
 |-  ( R e. Ring -> ( algSc ` P ) : ( Base ` R ) -1-1-> ( Base ` P ) )
25 24 ad3antlr
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( algSc ` P ) : ( Base ` R ) -1-1-> ( Base ` P ) )
26 simprl
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
27 simprr
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
28 simplrl
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> x e. B )
29 2 22 3 26 27 28 matecld
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( i x j ) e. ( Base ` R ) )
30 simplrr
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> y e. B )
31 2 22 3 26 27 30 matecld
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( i y j ) e. ( Base ` R ) )
32 f1veqaeq
 |-  ( ( ( algSc ` P ) : ( Base ` R ) -1-1-> ( Base ` P ) /\ ( ( i x j ) e. ( Base ` R ) /\ ( i y j ) e. ( Base ` R ) ) ) -> ( ( ( algSc ` P ) ` ( i x j ) ) = ( ( algSc ` P ) ` ( i y j ) ) -> ( i x j ) = ( i y j ) ) )
33 25 29 31 32 syl12anc
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( ( ( algSc ` P ) ` ( i x j ) ) = ( ( algSc ` P ) ` ( i y j ) ) -> ( i x j ) = ( i y j ) ) )
34 21 33 sylbid
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( ( i ( T ` x ) j ) = ( i ( T ` y ) j ) -> ( i x j ) = ( i y j ) ) )
35 34 ralimdvva
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( A. i e. N A. j e. N ( i ( T ` x ) j ) = ( i ( T ` y ) j ) -> A. i e. N A. j e. N ( i x j ) = ( i y j ) ) )
36 1 2 3 4 5 6 mat2pmatbas0
 |-  ( ( N e. Fin /\ R e. Ring /\ x e. B ) -> ( T ` x ) e. H )
37 11 36 syl
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( T ` x ) e. H )
38 1 2 3 4 5 6 mat2pmatbas0
 |-  ( ( N e. Fin /\ R e. Ring /\ y e. B ) -> ( T ` y ) e. H )
39 18 38 syl
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( T ` y ) e. H )
40 5 6 eqmat
 |-  ( ( ( T ` x ) e. H /\ ( T ` y ) e. H ) -> ( ( T ` x ) = ( T ` y ) <-> A. i e. N A. j e. N ( i ( T ` x ) j ) = ( i ( T ` y ) j ) ) )
41 37 39 40 syl2anc
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( T ` x ) = ( T ` y ) <-> A. i e. N A. j e. N ( i ( T ` x ) j ) = ( i ( T ` y ) j ) ) )
42 2 3 eqmat
 |-  ( ( x e. B /\ y e. B ) -> ( x = y <-> A. i e. N A. j e. N ( i x j ) = ( i y j ) ) )
43 42 adantl
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( x = y <-> A. i e. N A. j e. N ( i x j ) = ( i y j ) ) )
44 35 41 43 3imtr4d
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( T ` x ) = ( T ` y ) -> x = y ) )
45 44 ralrimivva
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. x e. B A. y e. B ( ( T ` x ) = ( T ` y ) -> x = y ) )
46 dff13
 |-  ( T : B -1-1-> H <-> ( T : B --> H /\ A. x e. B A. y e. B ( ( T ` x ) = ( T ` y ) -> x = y ) ) )
47 7 45 46 sylanbrc
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : B -1-1-> H )