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 ) |