Metamath Proof Explorer

Theorem mat2pmatlin

Description: The transformation of matrices into polynomial matrices is "linear", analogous to lmhmlin . Since A and C have different scalar rings, T cannot be a left module homomorphism as defined in df-lmhm , see lmhmsca . (Contributed by AV, 13-Nov-2019) (Proof shortened by AV, 28-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 )
mat2pmatlin.k 
|- K = ( Base ` R )
mat2pmatlin.s 
|- S = ( algSc ` P )
mat2pmatlin.m 
|- .x. = ( .s ` A )
mat2pmatlin.n 
|- .X. = ( .s ` C )
Assertion mat2pmatlin 
|- ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( T ` ( X .x. Y ) ) = ( ( S ` X ) .X. ( T ` Y ) ) )

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 mat2pmatlin.k 
 |-  K = ( Base ` R )
8 mat2pmatlin.s 
 |-  S = ( algSc ` P )
9 mat2pmatlin.m 
 |-  .x. = ( .s ` A )
10 mat2pmatlin.n 
 |-  .X. = ( .s ` C )
11 simpr 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. CRing )
12 4 ply1assa 
 |-  ( R e. CRing -> P e. AssAlg )
13 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
14 8 13 asclrhm 
 |-  ( P e. AssAlg -> S e. ( ( Scalar ` P ) RingHom P ) )
15 11 12 14 3syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> S e. ( ( Scalar ` P ) RingHom P ) )
16 4 ply1sca 
 |-  ( R e. CRing -> R = ( Scalar ` P ) )
17 16 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R = ( Scalar ` P ) )
18 17 oveq1d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( R RingHom P ) = ( ( Scalar ` P ) RingHom P ) )
19 15 18 eleqtrrd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> S e. ( R RingHom P ) )
20 19 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> S e. ( R RingHom P ) )
21 20 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> S e. ( R RingHom P ) )
22 7 eleq2i 
 |-  ( X e. K <-> X e. ( Base ` R ) )
23 22 biimpi 
 |-  ( X e. K -> X e. ( Base ` R ) )
24 23 adantr 
 |-  ( ( X e. K /\ Y e. B ) -> X e. ( Base ` R ) )
25 24 ad2antlr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> X e. ( Base ` R ) )
26 eqid 
 |-  ( Base ` R ) = ( Base ` R )
27 simprl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
28 simpr 
 |-  ( ( i e. N /\ j e. N ) -> j e. N )
29 28 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
30 simplrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> Y e. B )
31 2 26 3 27 29 30 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( i Y j ) e. ( Base ` R ) )
32 eqid 
 |-  ( .r ` R ) = ( .r ` R )
33 eqid 
 |-  ( .r ` P ) = ( .r ` P )
34 26 32 33 rhmmul 
 |-  ( ( S e. ( R RingHom P ) /\ X e. ( Base ` R ) /\ ( i Y j ) e. ( Base ` R ) ) -> ( S ` ( X ( .r ` R ) ( i Y j ) ) ) = ( ( S ` X ) ( .r ` P ) ( S ` ( i Y j ) ) ) )
35 21 25 31 34 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( S ` ( X ( .r ` R ) ( i Y j ) ) ) = ( ( S ` X ) ( .r ` P ) ( S ` ( i Y j ) ) ) )
36 crngring 
 |-  ( R e. CRing -> R e. Ring )
37 36 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> R e. Ring )
38 37 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> R e. Ring )
39 simpr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( X e. K /\ Y e. B ) )
40 39 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( X e. K /\ Y e. B ) )
41 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( i e. N /\ j e. N ) )
42 2 3 7 9 32 matvscacell 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( X .x. Y ) j ) = ( X ( .r ` R ) ( i Y j ) ) )
43 38 40 41 42 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( i ( X .x. Y ) j ) = ( X ( .r ` R ) ( i Y j ) ) )
44 43 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( S ` ( i ( X .x. Y ) j ) ) = ( S ` ( X ( .r ` R ) ( i Y j ) ) ) )
45 36 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
46 simpr 
 |-  ( ( X e. K /\ Y e. B ) -> Y e. B )
47 45 46 anim12i 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) )
48 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ Y e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) )
49 47 48 sylibr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( N e. Fin /\ R e. Ring /\ Y e. B ) )
50 1 2 3 4 8 mat2pmatvalel 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ Y e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( T ` Y ) j ) = ( S ` ( i Y j ) ) )
51 49 50 sylan 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( i ( T ` Y ) j ) = ( S ` ( i Y j ) ) )
52 51 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( ( S ` X ) ( .r ` P ) ( i ( T ` Y ) j ) ) = ( ( S ` X ) ( .r ` P ) ( S ` ( i Y j ) ) ) )
53 35 44 52 3eqtr4d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( S ` ( i ( X .x. Y ) j ) ) = ( ( S ` X ) ( .r ` P ) ( i ( T ` Y ) j ) ) )
54 simpll 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> N e. Fin )
55 54 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> N e. Fin )
56 7 2 3 9 matvscl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. K /\ Y e. B ) ) -> ( X .x. Y ) e. B )
57 45 56 sylan 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( X .x. Y ) e. B )
58 57 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( X .x. Y ) e. B )
59 1 2 3 4 8 mat2pmatvalel 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ ( X .x. Y ) e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( T ` ( X .x. Y ) ) j ) = ( S ` ( i ( X .x. Y ) j ) ) )
60 55 38 58 41 59 syl31anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( i ( T ` ( X .x. Y ) ) j ) = ( S ` ( i ( X .x. Y ) j ) ) )
61 4 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
62 36 61 syl 
 |-  ( R e. CRing -> P e. Ring )
63 62 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> P e. Ring )
64 63 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> P e. Ring )
65 36 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. Ring )
66 simpl 
 |-  ( ( X e. K /\ Y e. B ) -> X e. K )
67 eqid 
 |-  ( Base ` P ) = ( Base ` P )
68 4 8 7 67 ply1sclcl 
 |-  ( ( R e. Ring /\ X e. K ) -> ( S ` X ) e. ( Base ` P ) )
69 65 66 68 syl2an 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( S ` X ) e. ( Base ` P ) )
70 1 2 3 4 5 6 mat2pmatbas0 
 |-  ( ( N e. Fin /\ R e. Ring /\ Y e. B ) -> ( T ` Y ) e. H )
71 49 70 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( T ` Y ) e. H )
72 69 71 jca 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( ( S ` X ) e. ( Base ` P ) /\ ( T ` Y ) e. H ) )
73 72 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( ( S ` X ) e. ( Base ` P ) /\ ( T ` Y ) e. H ) )
74 5 6 67 10 33 matvscacell 
 |-  ( ( P e. Ring /\ ( ( S ` X ) e. ( Base ` P ) /\ ( T ` Y ) e. H ) /\ ( i e. N /\ j e. N ) ) -> ( i ( ( S ` X ) .X. ( T ` Y ) ) j ) = ( ( S ` X ) ( .r ` P ) ( i ( T ` Y ) j ) ) )
75 64 73 41 74 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( i ( ( S ` X ) .X. ( T ` Y ) ) j ) = ( ( S ` X ) ( .r ` P ) ( i ( T ` Y ) j ) ) )
76 53 60 75 3eqtr4d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( i ( T ` ( X .x. Y ) ) j ) = ( i ( ( S ` X ) .X. ( T ` Y ) ) j ) )
77 76 ralrimivva 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> A. i e. N A. j e. N ( i ( T ` ( X .x. Y ) ) j ) = ( i ( ( S ` X ) .X. ( T ` Y ) ) j ) )
78 1 2 3 4 5 6 mat2pmatbas0 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( X .x. Y ) e. B ) -> ( T ` ( X .x. Y ) ) e. H )
79 54 37 57 78 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( T ` ( X .x. Y ) ) e. H )
80 67 5 6 10 matvscl 
 |-  ( ( ( N e. Fin /\ P e. Ring ) /\ ( ( S ` X ) e. ( Base ` P ) /\ ( T ` Y ) e. H ) ) -> ( ( S ` X ) .X. ( T ` Y ) ) e. H )
81 54 63 72 80 syl21anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( ( S ` X ) .X. ( T ` Y ) ) e. H )
82 5 6 eqmat 
 |-  ( ( ( T ` ( X .x. Y ) ) e. H /\ ( ( S ` X ) .X. ( T ` Y ) ) e. H ) -> ( ( T ` ( X .x. Y ) ) = ( ( S ` X ) .X. ( T ` Y ) ) <-> A. i e. N A. j e. N ( i ( T ` ( X .x. Y ) ) j ) = ( i ( ( S ` X ) .X. ( T ` Y ) ) j ) ) )
83 79 81 82 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( ( T ` ( X .x. Y ) ) = ( ( S ` X ) .X. ( T ` Y ) ) <-> A. i e. N A. j e. N ( i ( T ` ( X .x. Y ) ) j ) = ( i ( ( S ` X ) .X. ( T ` Y ) ) j ) ) )
84 77 83 mpbird 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( T ` ( X .x. Y ) ) = ( ( S ` X ) .X. ( T ` Y ) ) )