Metamath Proof Explorer

Theorem pmatcollpwlem

Description: Lemma for pmatcollpw . (Contributed by AV, 26-Oct-2019) (Revised by AV, 4-Dec-2019)

Ref Expression
Hypotheses pmatcollpw.p 
|- P = ( Poly1 ` R )
pmatcollpw.c 
|- C = ( N Mat P )
pmatcollpw.b 
|- B = ( Base ` C )
pmatcollpw.m 
|- .* = ( .s ` C )
pmatcollpw.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
pmatcollpw.x 
|- X = ( var1 ` R )
pmatcollpw.t 
|- T = ( N matToPolyMat R )
Assertion pmatcollpwlem 
|- ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( ( a ( M decompPMat n ) b ) ( .s ` P ) ( n .^ X ) ) = ( a ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) b ) )

Proof

Step Hyp Ref Expression
1 pmatcollpw.p 
 |-  P = ( Poly1 ` R )
2 pmatcollpw.c 
 |-  C = ( N Mat P )
3 pmatcollpw.b 
 |-  B = ( Base ` C )
4 pmatcollpw.m 
 |-  .* = ( .s ` C )
5 pmatcollpw.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
6 pmatcollpw.x 
 |-  X = ( var1 ` R )
7 pmatcollpw.t 
 |-  T = ( N matToPolyMat R )
8 1 ply1assa 
 |-  ( R e. CRing -> P e. AssAlg )
9 8 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P e. AssAlg )
10 9 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> P e. AssAlg )
11 10 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> P e. AssAlg )
12 eqid 
 |-  ( N Mat R ) = ( N Mat R )
13 eqid 
 |-  ( Base ` R ) = ( Base ` R )
14 eqid 
 |-  ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) )
15 simp2 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> a e. N )
16 simp3 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> b e. N )
17 simp2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. CRing )
18 17 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> R e. CRing )
19 simp3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> M e. B )
20 19 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> M e. B )
21 simpr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> n e. NN0 )
22 1 2 3 12 14 decpmatcl 
 |-  ( ( R e. CRing /\ M e. B /\ n e. NN0 ) -> ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) )
23 18 20 21 22 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) )
24 23 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) )
25 12 13 14 15 16 24 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( a ( M decompPMat n ) b ) e. ( Base ` R ) )
26 crngring 
 |-  ( R e. CRing -> R e. Ring )
27 26 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
28 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
29 27 28 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R = ( Scalar ` P ) )
30 29 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Scalar ` P ) = R )
31 30 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
32 31 eleq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( a ( M decompPMat n ) b ) e. ( Base ` ( Scalar ` P ) ) <-> ( a ( M decompPMat n ) b ) e. ( Base ` R ) ) )
33 32 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( ( a ( M decompPMat n ) b ) e. ( Base ` ( Scalar ` P ) ) <-> ( a ( M decompPMat n ) b ) e. ( Base ` R ) ) )
34 33 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( ( a ( M decompPMat n ) b ) e. ( Base ` ( Scalar ` P ) ) <-> ( a ( M decompPMat n ) b ) e. ( Base ` R ) ) )
35 25 34 mpbird 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( a ( M decompPMat n ) b ) e. ( Base ` ( Scalar ` P ) ) )
36 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
37 eqid 
 |-  ( Base ` P ) = ( Base ` P )
38 1 6 36 5 37 ply1moncl 
 |-  ( ( R e. Ring /\ n e. NN0 ) -> ( n .^ X ) e. ( Base ` P ) )
39 27 38 sylan 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( n .^ X ) e. ( Base ` P ) )
40 39 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( n .^ X ) e. ( Base ` P ) )
41 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
42 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
43 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
44 eqid 
 |-  ( .r ` P ) = ( .r ` P )
45 eqid 
 |-  ( .s ` P ) = ( .s ` P )
46 41 42 43 37 44 45 asclmul2 
 |-  ( ( P e. AssAlg /\ ( a ( M decompPMat n ) b ) e. ( Base ` ( Scalar ` P ) ) /\ ( n .^ X ) e. ( Base ` P ) ) -> ( ( n .^ X ) ( .r ` P ) ( ( algSc ` P ) ` ( a ( M decompPMat n ) b ) ) ) = ( ( a ( M decompPMat n ) b ) ( .s ` P ) ( n .^ X ) ) )
47 11 35 40 46 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( ( n .^ X ) ( .r ` P ) ( ( algSc ` P ) ` ( a ( M decompPMat n ) b ) ) ) = ( ( a ( M decompPMat n ) b ) ( .s ` P ) ( n .^ X ) ) )
48 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) )
49 oveq12 
 |-  ( ( i = a /\ j = b ) -> ( i ( M decompPMat n ) j ) = ( a ( M decompPMat n ) b ) )
50 49 fveq2d 
 |-  ( ( i = a /\ j = b ) -> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) = ( ( algSc ` P ) ` ( a ( M decompPMat n ) b ) ) )
51 50 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) /\ ( i = a /\ j = b ) ) -> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) = ( ( algSc ` P ) ` ( a ( M decompPMat n ) b ) ) )
52 fvexd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( ( algSc ` P ) ` ( a ( M decompPMat n ) b ) ) e. _V )
53 48 51 15 16 52 ovmpod 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( a ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) b ) = ( ( algSc ` P ) ` ( a ( M decompPMat n ) b ) ) )
54 53 eqcomd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( ( algSc ` P ) ` ( a ( M decompPMat n ) b ) ) = ( a ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) b ) )
55 54 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( ( n .^ X ) ( .r ` P ) ( ( algSc ` P ) ` ( a ( M decompPMat n ) b ) ) ) = ( ( n .^ X ) ( .r ` P ) ( a ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) b ) ) )
56 47 55 eqtr3d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( ( a ( M decompPMat n ) b ) ( .s ` P ) ( n .^ X ) ) = ( ( n .^ X ) ( .r ` P ) ( a ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) b ) ) )
57 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
58 26 57 syl 
 |-  ( R e. CRing -> P e. Ring )
59 58 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P e. Ring )
60 59 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> P e. Ring )
61 60 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> P e. Ring )
62 simpl1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> N e. Fin )
63 18 26 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> R e. Ring )
64 63 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> R e. Ring )
65 simp2 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> i e. N )
66 simp3 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> j e. N )
67 23 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) )
68 12 13 14 65 66 67 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> ( i ( M decompPMat n ) j ) e. ( Base ` R ) )
69 1 41 13 37 ply1sclcl 
 |-  ( ( R e. Ring /\ ( i ( M decompPMat n ) j ) e. ( Base ` R ) ) -> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) e. ( Base ` P ) )
70 64 68 69 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) e. ( Base ` P ) )
71 2 37 3 62 60 70 matbas2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) e. B )
72 39 71 jca 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( ( n .^ X ) e. ( Base ` P ) /\ ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) e. B ) )
73 72 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( ( n .^ X ) e. ( Base ` P ) /\ ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) e. B ) )
74 15 16 jca 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( a e. N /\ b e. N ) )
75 2 3 37 4 44 matvscacell 
 |-  ( ( P e. Ring /\ ( ( n .^ X ) e. ( Base ` P ) /\ ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) e. B ) /\ ( a e. N /\ b e. N ) ) -> ( a ( ( n .^ X ) .* ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) ) b ) = ( ( n .^ X ) ( .r ` P ) ( a ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) b ) ) )
76 61 73 74 75 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( a ( ( n .^ X ) .* ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) ) b ) = ( ( n .^ X ) ( .r ` P ) ( a ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) b ) ) )
77 27 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> R e. Ring )
78 7 12 14 1 41 mat2pmatval 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) ) -> ( T ` ( M decompPMat n ) ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) )
79 62 77 23 78 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( T ` ( M decompPMat n ) ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) )
80 79 eqcomd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) = ( T ` ( M decompPMat n ) ) )
81 80 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( ( n .^ X ) .* ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) ) = ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) )
82 81 oveqd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( a ( ( n .^ X ) .* ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) ) b ) = ( a ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) b ) )
83 82 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( a ( ( n .^ X ) .* ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( M decompPMat n ) j ) ) ) ) b ) = ( a ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) b ) )
84 56 76 83 3eqtr2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) /\ a e. N /\ b e. N ) -> ( ( a ( M decompPMat n ) b ) ( .s ` P ) ( n .^ X ) ) = ( a ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) b ) )