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 birani 
 |-  ( ( X e. K /\ Y e. B ) -> X e. ( Base ` R ) )
24 23 ad2antlr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> X e. ( Base ` R ) )
25 eqid 
 |-  ( Base ` R ) = ( Base ` R )
26 simprl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
27 simpr 
 |-  ( ( i e. N /\ j e. N ) -> j e. N )
28 27 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
29 simplrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> Y e. B )
30 2 25 3 26 28 29 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 ) )
31 eqid 
 |-  ( .r ` R ) = ( .r ` R )
32 eqid 
 |-  ( .r ` P ) = ( .r ` P )
33 25 31 32 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 ) ) ) )
34 21 24 30 33 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 ) ) ) )
35 crngring 
 |-  ( R e. CRing -> R e. Ring )
36 35 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> R e. Ring )
37 36 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> R e. Ring )
38 simpr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( X e. K /\ Y e. B ) )
39 38 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 ) )
40 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 ) )
41 2 3 7 9 31 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 ) ) )
42 37 39 40 41 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 ) ) )
43 42 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 ) ) ) )
44 35 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
45 simpr 
 |-  ( ( X e. K /\ Y e. B ) -> Y e. B )
46 44 45 anim12i 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) )
47 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ Y e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ Y e. B ) )
48 46 47 sylibr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( N e. Fin /\ R e. Ring /\ Y e. B ) )
49 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 ) ) )
50 48 49 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 ) ) )
51 50 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 ) ) ) )
52 34 43 51 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 ) ) )
53 simpll 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> N e. Fin )
54 53 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> N e. Fin )
55 7 2 3 9 matvscl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. K /\ Y e. B ) ) -> ( X .x. Y ) e. B )
56 44 55 sylan 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( X .x. Y ) e. B )
57 56 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> ( X .x. Y ) e. B )
58 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 ) ) )
59 54 37 57 40 58 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 ) ) )
60 4 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
61 35 60 syl 
 |-  ( R e. CRing -> P e. Ring )
62 61 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> P e. Ring )
63 62 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) /\ ( i e. N /\ j e. N ) ) -> P e. Ring )
64 35 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. Ring )
65 simpl 
 |-  ( ( X e. K /\ Y e. B ) -> X e. K )
66 eqid 
 |-  ( Base ` P ) = ( Base ` P )
67 4 8 7 66 ply1sclcl 
 |-  ( ( R e. Ring /\ X e. K ) -> ( S ` X ) e. ( Base ` P ) )
68 64 65 67 syl2an 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( S ` X ) e. ( Base ` P ) )
69 1 2 3 4 5 6 mat2pmatbas0 
 |-  ( ( N e. Fin /\ R e. Ring /\ Y e. B ) -> ( T ` Y ) e. H )
70 48 69 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( T ` Y ) e. H )
71 68 70 jca 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( ( S ` X ) e. ( Base ` P ) /\ ( T ` Y ) e. H ) )
72 71 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 ) )
73 5 6 66 10 32 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 ) ) )
74 63 72 40 73 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 ) ) )
75 52 59 74 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 ) )
76 75 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 ) )
77 1 2 3 4 5 6 mat2pmatbas0 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( X .x. Y ) e. B ) -> ( T ` ( X .x. Y ) ) e. H )
78 53 36 56 77 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( T ` ( X .x. Y ) ) e. H )
79 66 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 )
80 53 62 71 79 syl21anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( ( S ` X ) .X. ( T ` Y ) ) e. H )
81 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 ) ) )
82 78 80 81 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 ) ) )
83 76 82 mpbird 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( X e. K /\ Y e. B ) ) -> ( T ` ( X .x. Y ) ) = ( ( S ` X ) .X. ( T ` Y ) ) )