Metamath Proof Explorer

Theorem pm2mpf1

Description: The transformation of polynomial matrices into polynomials over matrices is a 1-1 function mapping polynomial matrices to polynomials over matrices. (Contributed by AV, 14-Oct-2019) (Revised by AV, 6-Dec-2019)

Ref Expression
Hypotheses pm2mpval.p 
|- P = ( Poly1 ` R )
pm2mpval.c 
|- C = ( N Mat P )
pm2mpval.b 
|- B = ( Base ` C )
pm2mpval.m 
|- .* = ( .s ` Q )
pm2mpval.e 
|- .^ = ( .g ` ( mulGrp ` Q ) )
pm2mpval.x 
|- X = ( var1 ` A )
pm2mpval.a 
|- A = ( N Mat R )
pm2mpval.q 
|- Q = ( Poly1 ` A )
pm2mpval.t 
|- T = ( N pMatToMatPoly R )
pm2mpcl.l 
|- L = ( Base ` Q )
Assertion pm2mpf1 
|- ( ( N e. Fin /\ R e. Ring ) -> T : B -1-1-> L )

Proof

Step Hyp Ref Expression
1 pm2mpval.p 
 |-  P = ( Poly1 ` R )
2 pm2mpval.c 
 |-  C = ( N Mat P )
3 pm2mpval.b 
 |-  B = ( Base ` C )
4 pm2mpval.m 
 |-  .* = ( .s ` Q )
5 pm2mpval.e 
 |-  .^ = ( .g ` ( mulGrp ` Q ) )
6 pm2mpval.x 
 |-  X = ( var1 ` A )
7 pm2mpval.a 
 |-  A = ( N Mat R )
8 pm2mpval.q 
 |-  Q = ( Poly1 ` A )
9 pm2mpval.t 
 |-  T = ( N pMatToMatPoly R )
10 pm2mpcl.l 
 |-  L = ( Base ` Q )
11 1 2 3 4 5 6 7 8 9 10 pm2mpf 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : B --> L )
12 7 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
13 12 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> A e. Ring )
14 1 2 3 4 5 6 7 8 9 10 pm2mpcl 
 |-  ( ( N e. Fin /\ R e. Ring /\ u e. B ) -> ( T ` u ) e. L )
15 14 3expa 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ u e. B ) -> ( T ` u ) e. L )
16 15 adantrr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> ( T ` u ) e. L )
17 1 2 3 4 5 6 7 8 9 10 pm2mpcl 
 |-  ( ( N e. Fin /\ R e. Ring /\ w e. B ) -> ( T ` w ) e. L )
18 17 3expia 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( w e. B -> ( T ` w ) e. L ) )
19 18 adantld 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( u e. B /\ w e. B ) -> ( T ` w ) e. L ) )
20 19 imp 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> ( T ` w ) e. L )
21 eqid 
 |-  ( coe1 ` ( T ` u ) ) = ( coe1 ` ( T ` u ) )
22 eqid 
 |-  ( coe1 ` ( T ` w ) ) = ( coe1 ` ( T ` w ) )
23 8 10 21 22 ply1coe1eq 
 |-  ( ( A e. Ring /\ ( T ` u ) e. L /\ ( T ` w ) e. L ) -> ( A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) <-> ( T ` u ) = ( T ` w ) ) )
24 23 bicomd 
 |-  ( ( A e. Ring /\ ( T ` u ) e. L /\ ( T ` w ) e. L ) -> ( ( T ` u ) = ( T ` w ) <-> A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) )
25 13 16 20 24 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> ( ( T ` u ) = ( T ` w ) <-> A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) )
26 simpll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> N e. Fin )
27 simplr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> R e. Ring )
28 simprl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> u e. B )
29 1 2 3 4 5 6 7 8 9 pm2mpfval 
 |-  ( ( N e. Fin /\ R e. Ring /\ u e. B ) -> ( T ` u ) = ( Q gsum ( k e. NN0 |-> ( ( u decompPMat k ) .* ( k .^ X ) ) ) ) )
30 26 27 28 29 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> ( T ` u ) = ( Q gsum ( k e. NN0 |-> ( ( u decompPMat k ) .* ( k .^ X ) ) ) ) )
31 30 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( T ` u ) = ( Q gsum ( k e. NN0 |-> ( ( u decompPMat k ) .* ( k .^ X ) ) ) ) )
32 31 fveq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( coe1 ` ( T ` u ) ) = ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( u decompPMat k ) .* ( k .^ X ) ) ) ) ) )
33 32 fveq1d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( u decompPMat k ) .* ( k .^ X ) ) ) ) ) ` n ) )
34 simplll 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( N e. Fin /\ R e. Ring ) )
35 28 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) -> u e. B )
36 35 anim1i 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( u e. B /\ n e. NN0 ) )
37 1 2 3 4 5 6 7 8 pm2mpf1lem 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ n e. NN0 ) ) -> ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( u decompPMat k ) .* ( k .^ X ) ) ) ) ) ` n ) = ( u decompPMat n ) )
38 34 36 37 syl2anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( u decompPMat k ) .* ( k .^ X ) ) ) ) ) ` n ) = ( u decompPMat n ) )
39 33 38 eqtrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( ( coe1 ` ( T ` u ) ) ` n ) = ( u decompPMat n ) )
40 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> w e. B )
41 1 2 3 4 5 6 7 8 9 pm2mpfval 
 |-  ( ( N e. Fin /\ R e. Ring /\ w e. B ) -> ( T ` w ) = ( Q gsum ( k e. NN0 |-> ( ( w decompPMat k ) .* ( k .^ X ) ) ) ) )
42 26 27 40 41 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> ( T ` w ) = ( Q gsum ( k e. NN0 |-> ( ( w decompPMat k ) .* ( k .^ X ) ) ) ) )
43 42 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> ( coe1 ` ( T ` w ) ) = ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( w decompPMat k ) .* ( k .^ X ) ) ) ) ) )
44 43 fveq1d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> ( ( coe1 ` ( T ` w ) ) ` n ) = ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( w decompPMat k ) .* ( k .^ X ) ) ) ) ) ` n ) )
45 44 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( ( coe1 ` ( T ` w ) ) ` n ) = ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( w decompPMat k ) .* ( k .^ X ) ) ) ) ) ` n ) )
46 40 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) -> w e. B )
47 46 anim1i 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( w e. B /\ n e. NN0 ) )
48 1 2 3 4 5 6 7 8 pm2mpf1lem 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( w e. B /\ n e. NN0 ) ) -> ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( w decompPMat k ) .* ( k .^ X ) ) ) ) ) ` n ) = ( w decompPMat n ) )
49 34 47 48 syl2anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( w decompPMat k ) .* ( k .^ X ) ) ) ) ) ` n ) = ( w decompPMat n ) )
50 45 49 eqtrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( ( coe1 ` ( T ` w ) ) ` n ) = ( w decompPMat n ) )
51 39 50 eqeq12d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) <-> ( u decompPMat n ) = ( w decompPMat n ) ) )
52 2 3 decpmatval 
 |-  ( ( u e. B /\ n e. NN0 ) -> ( u decompPMat n ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) )
53 28 52 sylan 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) -> ( u decompPMat n ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) )
54 2 3 decpmatval 
 |-  ( ( w e. B /\ n e. NN0 ) -> ( w decompPMat n ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) )
55 40 54 sylan 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) -> ( w decompPMat n ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) )
56 53 55 eqeq12d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) -> ( ( u decompPMat n ) = ( w decompPMat n ) <-> ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) ) )
57 eqid 
 |-  ( Base ` R ) = ( Base ` R )
58 eqid 
 |-  ( Base ` A ) = ( Base ` A )
59 simplll 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) -> N e. Fin )
60 simpllr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) -> R e. Ring )
61 eqid 
 |-  ( Base ` P ) = ( Base ` P )
62 simp2 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> i e. N )
63 simp3 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> j e. N )
64 3 eleq2i 
 |-  ( u e. B <-> u e. ( Base ` C ) )
65 64 biimpi 
 |-  ( u e. B -> u e. ( Base ` C ) )
66 65 adantr 
 |-  ( ( u e. B /\ w e. B ) -> u e. ( Base ` C ) )
67 66 ad2antlr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) -> u e. ( Base ` C ) )
68 67 3ad2ant1 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> u e. ( Base ` C ) )
69 68 3 eleqtrrdi 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> u e. B )
70 2 61 3 62 63 69 matecld 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> ( i u j ) e. ( Base ` P ) )
71 simp1r 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> n e. NN0 )
72 eqid 
 |-  ( coe1 ` ( i u j ) ) = ( coe1 ` ( i u j ) )
73 72 61 1 57 coe1fvalcl 
 |-  ( ( ( i u j ) e. ( Base ` P ) /\ n e. NN0 ) -> ( ( coe1 ` ( i u j ) ) ` n ) e. ( Base ` R ) )
74 70 71 73 syl2anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i u j ) ) ` n ) e. ( Base ` R ) )
75 7 57 58 59 60 74 matbas2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) e. ( Base ` A ) )
76 3 eleq2i 
 |-  ( w e. B <-> w e. ( Base ` C ) )
77 76 biimpi 
 |-  ( w e. B -> w e. ( Base ` C ) )
78 77 ad2antll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> w e. ( Base ` C ) )
79 78 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) -> w e. ( Base ` C ) )
80 79 3ad2ant1 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> w e. ( Base ` C ) )
81 80 3 eleqtrrdi 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> w e. B )
82 2 61 3 62 63 81 matecld 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> ( i w j ) e. ( Base ` P ) )
83 eqid 
 |-  ( coe1 ` ( i w j ) ) = ( coe1 ` ( i w j ) )
84 83 61 1 57 coe1fvalcl 
 |-  ( ( ( i w j ) e. ( Base ` P ) /\ n e. NN0 ) -> ( ( coe1 ` ( i w j ) ) ` n ) e. ( Base ` R ) )
85 82 71 84 syl2anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i w j ) ) ` n ) e. ( Base ` R ) )
86 7 57 58 59 60 85 matbas2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) e. ( Base ` A ) )
87 7 58 eqmat 
 |-  ( ( ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) e. ( Base ` A ) /\ ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) e. ( Base ` A ) ) -> ( ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) <-> A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) = ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) ) )
88 75 86 87 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) -> ( ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) <-> A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) = ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) ) )
89 56 88 bitrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ n e. NN0 ) -> ( ( u decompPMat n ) = ( w decompPMat n ) <-> A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) = ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) ) )
90 89 adantlr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( ( u decompPMat n ) = ( w decompPMat n ) <-> A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) = ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) ) )
91 oveq1 
 |-  ( x = a -> ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) = ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) )
92 oveq1 
 |-  ( x = a -> ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) = ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) )
93 91 92 eqeq12d 
 |-  ( x = a -> ( ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) = ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) <-> ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) = ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) ) )
94 oveq2 
 |-  ( y = b -> ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) = ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) b ) )
95 oveq2 
 |-  ( y = b -> ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) = ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) b ) )
96 94 95 eqeq12d 
 |-  ( y = b -> ( ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) = ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) <-> ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) b ) = ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) b ) ) )
97 93 96 rspc2va 
 |-  ( ( ( a e. N /\ b e. N ) /\ A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) = ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) ) -> ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) b ) = ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) b ) )
98 eqidd 
 |-  ( ( ( ( a e. N /\ b e. N ) /\ ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) ) /\ n e. NN0 ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) )
99 oveq12 
 |-  ( ( i = a /\ j = b ) -> ( i u j ) = ( a u b ) )
100 99 fveq2d 
 |-  ( ( i = a /\ j = b ) -> ( coe1 ` ( i u j ) ) = ( coe1 ` ( a u b ) ) )
101 100 fveq1d 
 |-  ( ( i = a /\ j = b ) -> ( ( coe1 ` ( i u j ) ) ` n ) = ( ( coe1 ` ( a u b ) ) ` n ) )
102 101 adantl 
 |-  ( ( ( ( ( a e. N /\ b e. N ) /\ ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) ) /\ n e. NN0 ) /\ ( i = a /\ j = b ) ) -> ( ( coe1 ` ( i u j ) ) ` n ) = ( ( coe1 ` ( a u b ) ) ` n ) )
103 simplll 
 |-  ( ( ( ( a e. N /\ b e. N ) /\ ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) ) /\ n e. NN0 ) -> a e. N )
104 simpllr 
 |-  ( ( ( ( a e. N /\ b e. N ) /\ ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) ) /\ n e. NN0 ) -> b e. N )
105 fvexd 
 |-  ( ( ( ( a e. N /\ b e. N ) /\ ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) ) /\ n e. NN0 ) -> ( ( coe1 ` ( a u b ) ) ` n ) e. _V )
106 98 102 103 104 105 ovmpod 
 |-  ( ( ( ( a e. N /\ b e. N ) /\ ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) ) /\ n e. NN0 ) -> ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) b ) = ( ( coe1 ` ( a u b ) ) ` n ) )
107 eqidd 
 |-  ( ( ( ( a e. N /\ b e. N ) /\ ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) ) /\ n e. NN0 ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) )
108 oveq12 
 |-  ( ( i = a /\ j = b ) -> ( i w j ) = ( a w b ) )
109 108 fveq2d 
 |-  ( ( i = a /\ j = b ) -> ( coe1 ` ( i w j ) ) = ( coe1 ` ( a w b ) ) )
110 109 fveq1d 
 |-  ( ( i = a /\ j = b ) -> ( ( coe1 ` ( i w j ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) )
111 110 adantl 
 |-  ( ( ( ( ( a e. N /\ b e. N ) /\ ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) ) /\ n e. NN0 ) /\ ( i = a /\ j = b ) ) -> ( ( coe1 ` ( i w j ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) )
112 fvexd 
 |-  ( ( ( ( a e. N /\ b e. N ) /\ ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) ) /\ n e. NN0 ) -> ( ( coe1 ` ( a w b ) ) ` n ) e. _V )
113 107 111 103 104 112 ovmpod 
 |-  ( ( ( ( a e. N /\ b e. N ) /\ ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) ) /\ n e. NN0 ) -> ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) b ) = ( ( coe1 ` ( a w b ) ) ` n ) )
114 106 113 eqeq12d 
 |-  ( ( ( ( a e. N /\ b e. N ) /\ ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) ) /\ n e. NN0 ) -> ( ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) b ) = ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) b ) <-> ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) ) )
115 114 biimpd 
 |-  ( ( ( ( a e. N /\ b e. N ) /\ ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) ) /\ n e. NN0 ) -> ( ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) b ) = ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) b ) -> ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) ) )
116 115 exp31 
 |-  ( ( a e. N /\ b e. N ) -> ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> ( n e. NN0 -> ( ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) b ) = ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) b ) -> ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) ) ) ) )
117 116 com14 
 |-  ( ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) b ) = ( a ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) b ) -> ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> ( n e. NN0 -> ( ( a e. N /\ b e. N ) -> ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) ) ) ) )
118 97 117 syl 
 |-  ( ( ( a e. N /\ b e. N ) /\ A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) = ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) ) -> ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> ( n e. NN0 -> ( ( a e. N /\ b e. N ) -> ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) ) ) ) )
119 118 ex 
 |-  ( ( a e. N /\ b e. N ) -> ( A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) = ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) -> ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> ( n e. NN0 -> ( ( a e. N /\ b e. N ) -> ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) ) ) ) ) )
120 119 com25 
 |-  ( ( a e. N /\ b e. N ) -> ( ( a e. N /\ b e. N ) -> ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> ( n e. NN0 -> ( A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) = ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) -> ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) ) ) ) ) )
121 120 pm2.43i 
 |-  ( ( a e. N /\ b e. N ) -> ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> ( n e. NN0 -> ( A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) = ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) -> ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) ) ) ) )
122 121 impcom 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) -> ( n e. NN0 -> ( A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) = ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) -> ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) ) ) )
123 122 imp 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( A. x e. N A. y e. N ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i u j ) ) ` n ) ) y ) = ( x ( i e. N , j e. N |-> ( ( coe1 ` ( i w j ) ) ` n ) ) y ) -> ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) ) )
124 90 123 sylbid 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( ( u decompPMat n ) = ( w decompPMat n ) -> ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) ) )
125 51 124 sylbid 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) /\ n e. NN0 ) -> ( ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) -> ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) ) )
126 125 ralimdva 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ ( a e. N /\ b e. N ) ) -> ( A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) -> A. n e. NN0 ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) ) )
127 126 impancom 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) -> ( ( a e. N /\ b e. N ) -> A. n e. NN0 ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) ) )
128 127 imp 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) /\ ( a e. N /\ b e. N ) ) -> A. n e. NN0 ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) )
129 27 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) /\ ( a e. N /\ b e. N ) ) -> R e. Ring )
130 simprl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) /\ ( a e. N /\ b e. N ) ) -> a e. N )
131 simprr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) /\ ( a e. N /\ b e. N ) ) -> b e. N )
132 66 ad2antlr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) -> u e. ( Base ` C ) )
133 132 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) /\ ( a e. N /\ b e. N ) ) -> u e. ( Base ` C ) )
134 133 3 eleqtrrdi 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) /\ ( a e. N /\ b e. N ) ) -> u e. B )
135 2 61 3 130 131 134 matecld 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) /\ ( a e. N /\ b e. N ) ) -> ( a u b ) e. ( Base ` P ) )
136 78 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) /\ ( a e. N /\ b e. N ) ) -> w e. ( Base ` C ) )
137 136 3 eleqtrrdi 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) /\ ( a e. N /\ b e. N ) ) -> w e. B )
138 2 61 3 130 131 137 matecld 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) /\ ( a e. N /\ b e. N ) ) -> ( a w b ) e. ( Base ` P ) )
139 eqid 
 |-  ( coe1 ` ( a u b ) ) = ( coe1 ` ( a u b ) )
140 eqid 
 |-  ( coe1 ` ( a w b ) ) = ( coe1 ` ( a w b ) )
141 1 61 139 140 ply1coe1eq 
 |-  ( ( R e. Ring /\ ( a u b ) e. ( Base ` P ) /\ ( a w b ) e. ( Base ` P ) ) -> ( A. n e. NN0 ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) <-> ( a u b ) = ( a w b ) ) )
142 141 bicomd 
 |-  ( ( R e. Ring /\ ( a u b ) e. ( Base ` P ) /\ ( a w b ) e. ( Base ` P ) ) -> ( ( a u b ) = ( a w b ) <-> A. n e. NN0 ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) ) )
143 129 135 138 142 syl3anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) /\ ( a e. N /\ b e. N ) ) -> ( ( a u b ) = ( a w b ) <-> A. n e. NN0 ( ( coe1 ` ( a u b ) ) ` n ) = ( ( coe1 ` ( a w b ) ) ` n ) ) )
144 128 143 mpbird 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) /\ ( a e. N /\ b e. N ) ) -> ( a u b ) = ( a w b ) )
145 144 ralrimivva 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) -> A. a e. N A. b e. N ( a u b ) = ( a w b ) )
146 2 3 eqmat 
 |-  ( ( u e. B /\ w e. B ) -> ( u = w <-> A. a e. N A. b e. N ( a u b ) = ( a w b ) ) )
147 146 ad2antlr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) -> ( u = w <-> A. a e. N A. b e. N ( a u b ) = ( a w b ) ) )
148 145 147 mpbird 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) /\ A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) ) -> u = w )
149 148 ex 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> ( A. n e. NN0 ( ( coe1 ` ( T ` u ) ) ` n ) = ( ( coe1 ` ( T ` w ) ) ` n ) -> u = w ) )
150 25 149 sylbid 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( u e. B /\ w e. B ) ) -> ( ( T ` u ) = ( T ` w ) -> u = w ) )
151 150 ralrimivva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. u e. B A. w e. B ( ( T ` u ) = ( T ` w ) -> u = w ) )
152 dff13 
 |-  ( T : B -1-1-> L <-> ( T : B --> L /\ A. u e. B A. w e. B ( ( T ` u ) = ( T ` w ) -> u = w ) ) )
153 11 151 152 sylanbrc 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : B -1-1-> L )