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 )