Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pmattomply1ghm Structured version   Unicode version

Theorem pmattomply1ghm 31256
 Description: The transformation of matrices over polynomials into polynomials over matrices an additive group homomorphism. (Contributed by AV, 16-Oct-2019.)
Hypotheses
Ref Expression
pmattomply1.p Poly1
pmattomply1.c Mat
pmattomply1.b
pmattomply1.f coe1
pmattomply1.m
pmattomply1.e .gmulGrp
pmattomply1.x var1
pmattomply1.a Mat
pmattomply1.q Poly1
pmattomply1.l
pmattomply1.t g
Assertion
Ref Expression
pmattomply1ghm
Distinct variable groups:   ,,,,   ,,,   ,,,   ,   ,   ,   ,   ,   ,,,   ,,,,   ,,,   ,   ,   ,   ,   ,   ,   ,   ,,,   ,,,   ,
Allowed substitution hints:   ()   (,)   (,,,)   (,)   (,)   (,)

Proof of Theorem pmattomply1ghm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pmattomply1.b . 2
2 pmattomply1.l . 2
3 eqid 2450 . 2
4 eqid 2450 . 2
5 pmattomply1.p . . . . 5 Poly1
65ply1rng 17796 . . . 4
7 pmattomply1.c . . . . 5 Mat
87matrng 18426 . . . 4
96, 8sylan2 474 . . 3
10 rnggrp 16742 . . 3
119, 10syl 16 . 2
12 pmattomply1.a . . . . 5 Mat
1312matrng 18426 . . . 4
14 pmattomply1.q . . . . 5 Poly1
1514ply1rng 17796 . . . 4
1613, 15syl 16 . . 3
17 rnggrp 16742 . . 3
1816, 17syl 16 . 2
19 pmattomply1.f . . 3 coe1
20 pmattomply1.m . . 3
21 pmattomply1.e . . 3 .gmulGrp
22 pmattomply1.x . . 3 var1
23 pmattomply1.t . . 3 g
245, 7, 1, 19, 20, 21, 22, 12, 14, 2, 23pmattomply1f 31244 . 2
25 simplll 757 . . . . . . . . . 10
26 rngmnd 16746 . . . . . . . . . . . . . . 15
279, 26syl 16 . . . . . . . . . . . . . 14
2827anim1i 568 . . . . . . . . . . . . 13
29 3anass 969 . . . . . . . . . . . . 13
3028, 29sylibr 212 . . . . . . . . . . . 12
311, 3mndcl 15508 . . . . . . . . . . . 12
3230, 31syl 16 . . . . . . . . . . 11
3332adantr 465 . . . . . . . . . 10
34 simpr 461 . . . . . . . . . 10
35 oveq 6182 . . . . . . . . . . . . . . . 16
3635fveq2d 5779 . . . . . . . . . . . . . . 15 coe1 coe1
3736fveq1d 5777 . . . . . . . . . . . . . 14 coe1 coe1
3837mpt2eq3dv 6237 . . . . . . . . . . . . 13 coe1 coe1
39 fveq2 5775 . . . . . . . . . . . . . 14 coe1 coe1
4039mpt2eq3dv 6237 . . . . . . . . . . . . 13 coe1 coe1
4138, 40cbvmpt2v 6251 . . . . . . . . . . . 12 coe1 coe1
4219, 41eqtri 2478 . . . . . . . . . . 11 coe1
435, 7, 1, 42pmatcollpw1lem1 31209 . . . . . . . . . 10 coe1
4425, 33, 34, 43syl3anc 1219 . . . . . . . . 9 coe1
45 fvex 5785 . . . . . . . . . . . 12 coe1
4645a1i 11 . . . . . . . . . . 11 coe1
47 fvex 5785 . . . . . . . . . . . 12 coe1
4847a1i 11 . . . . . . . . . . 11 coe1
49 eqidd 2451 . . . . . . . . . . 11 coe1 coe1
50 eqidd 2451 . . . . . . . . . . 11 coe1 coe1
5125, 25, 46, 48, 49, 50offval22 6738 . . . . . . . . . 10 coe1 coe1 coe1 coe1
52 eqid 2450 . . . . . . . . . . . 12
53 eqid 2450 . . . . . . . . . . . 12
54 simpllr 758 . . . . . . . . . . . 12
55 simprl 755 . . . . . . . . . . . . . . . . . 18
56 simprr 756 . . . . . . . . . . . . . . . . . 18
571eleq2i 2526 . . . . . . . . . . . . . . . . . . . 20
5857biimpi 194 . . . . . . . . . . . . . . . . . . 19
5958ad2antlr 726 . . . . . . . . . . . . . . . . . 18
60 eqid 2450 . . . . . . . . . . . . . . . . . . 19
617, 60matecl 18421 . . . . . . . . . . . . . . . . . 18
6255, 56, 59, 61syl3anc 1219 . . . . . . . . . . . . . . . . 17
6362ex 434 . . . . . . . . . . . . . . . 16
6463adantrr 716 . . . . . . . . . . . . . . 15
6564adantr 465 . . . . . . . . . . . . . 14
66653impib 1186 . . . . . . . . . . . . 13
67343ad2ant1 1009 . . . . . . . . . . . . 13
68 eqid 2450 . . . . . . . . . . . . . 14 coe1 coe1
6968, 60, 5, 52coe1fvalcl 30958 . . . . . . . . . . . . 13 coe1
7066, 67, 69syl2anc 661 . . . . . . . . . . . 12 coe1
7112, 52, 53, 25, 54, 70matbas2d 18419 . . . . . . . . . . 11 coe1
72 simprl 755 . . . . . . . . . . . . . . . . . 18
73 simprr 756 . . . . . . . . . . . . . . . . . 18
741eleq2i 2526 . . . . . . . . . . . . . . . . . . . 20
7574biimpi 194 . . . . . . . . . . . . . . . . . . 19
7675ad2antlr 726 . . . . . . . . . . . . . . . . . 18
777, 60matecl 18421 . . . . . . . . . . . . . . . . . 18
7872, 73, 76, 77syl3anc 1219 . . . . . . . . . . . . . . . . 17
7978ex 434 . . . . . . . . . . . . . . . 16
8079adantrl 715 . . . . . . . . . . . . . . 15
8180adantr 465 . . . . . . . . . . . . . 14
82813impib 1186 . . . . . . . . . . . . 13
83 eqid 2450 . . . . . . . . . . . . . 14 coe1 coe1
8483, 60, 5, 52coe1fvalcl 30958 . . . . . . . . . . . . 13 coe1
8582, 67, 84syl2anc 661 . . . . . . . . . . . 12 coe1
8612, 52, 53, 25, 54, 85matbas2d 18419 . . . . . . . . . . 11 coe1
87 eqid 2450 . . . . . . . . . . . 12
88 eqid 2450 . . . . . . . . . . . 12
8912, 53, 87, 88matplusg2 18423 . . . . . . . . . . 11 coe1 coe1 coe1 coe1 coe1 coe1
9071, 86, 89syl2anc 661 . . . . . . . . . 10 coe1 coe1 coe1 coe1
91 simplr 754 . . . . . . . . . . . . . . . . 17
9291anim1i 568 . . . . . . . . . . . . . . . 16
93923impb 1184 . . . . . . . . . . . . . . 15
94 eqid 2450 . . . . . . . . . . . . . . . 16
957, 1, 3, 94matplusgcell 30991 . . . . . . . . . . . . . . 15
9693, 95syl 16 . . . . . . . . . . . . . 14
9796fveq2d 5779 . . . . . . . . . . . . 13 coe1 coe1
9897fveq1d 5777 . . . . . . . . . . . 12 coe1 coe1
99543ad2ant1 1009 . . . . . . . . . . . . 13
1005, 60, 94, 88coe1addfv 17812 . . . . . . . . . . . . 13 coe1 coe1 coe1
10199, 66, 82, 67, 100syl31anc 1222 . . . . . . . . . . . 12 coe1 coe1 coe1
10298, 101eqtrd 2490 . . . . . . . . . . 11 coe1 coe1 coe1
103102mpt2eq3dva 6235 . . . . . . . . . 10 coe1 coe1 coe1
10451, 90, 1033eqtr4rd 2501 . . . . . . . . 9 coe1 coe1 coe1
10514ply1sca 17801 . . . . . . . . . . . . 13 Scalar
10613, 105syl 16 . . . . . . . . . . . 12 Scalar
107106ad2antrr 725 . . . . . . . . . . 11 Scalar
108107fveq2d 5779 . . . . . . . . . 10 Scalar
109 simpl 457 . . . . . . . . . . . . . . 15
110 simpl 457 . . . . . . . . . . . . . . 15
111109, 110anim12i 566 . . . . . . . . . . . . . 14
112111anim1i 568 . . . . . . . . . . . . 13
113 df-3an 967 . . . . . . . . . . . . 13
114112, 113sylibr 212 . . . . . . . . . . . 12
1155, 7, 1, 42pmatcollpw1lem1 31209 . . . . . . . . . . . 12 coe1
116114, 115syl 16 . . . . . . . . . . 11 coe1
117116eqcomd 2457 . . . . . . . . . 10 coe1
118 simpr 461 . . . . . . . . . . . . . . 15
119109, 118anim12i 566 . . . . . . . . . . . . . 14
120119anim1i 568 . . . . . . . . . . . . 13
121 df-3an 967 . . . . . . . . . . . . 13
122120, 121sylibr 212 . . . . . . . . . . . 12
1235, 7, 1, 42pmatcollpw1lem1 31209 . . . . . . . . . . . 12 coe1
124122, 123syl 16 . . . . . . . . . . 11 coe1
125124eqcomd 2457 . . . . . . . . . 10 coe1
126108, 117, 125oveq123d 6197 . . . . . . . . 9 coe1 coe1 Scalar
12744, 104, 1263eqtrd 2494 . . . . . . . 8 Scalar
128127oveq1d 6191 . . . . . . 7 Scalar
12914ply1lmod 17800 . . . . . . . . . 10
13013, 129syl 16 . . . . . . . . 9
131130ad2antrr 725 . . . . . . . 8
132 simpll 753 . . . . . . . . . 10
133 simprl 755 . . . . . . . . . . 11
134133anim1i 568 . . . . . . . . . 10
1355, 7, 1, 42, 12, 53pmatcollpw1lem2 31210 . . . . . . . . . 10
136132, 134, 135syl2anc 661 . . . . . . . . 9
137106eqcomd 2457 . . . . . . . . . . 11 Scalar
138137ad2antrr 725 . . . . . . . . . 10 Scalar
139138fveq2d 5779 . . . . . . . . 9 Scalar
140136, 139eleqtrrd 2539 . . . . . . . 8 Scalar
141 simprr 756 . . . . . . . . . . 11
142141anim1i 568 . . . . . . . . . 10
1435, 7, 1, 42, 12, 53pmatcollpw1lem2 31210 . . . . . . . . . 10
144132, 142, 143syl2anc 661 . . . . . . . . 9
145144, 139eleqtrrd 2539 . . . . . . . 8 Scalar
146 eqid 2450 . . . . . . . . . . . 12 mulGrp mulGrp
147146rngmgp 16743 . . . . . . . . . . 11 mulGrp
14816, 147syl 16 . . . . . . . . . 10 mulGrp
149148ad2antrr 725 . . . . . . . . 9 mulGrp
15022, 14, 2vr1cl 17764 . . . . . . . . . . 11
15113, 150syl 16 . . . . . . . . . 10
152151ad2antrr 725 . . . . . . . . 9
153146, 2mgpbas 16688 . . . . . . . . . 10 mulGrp
154153, 21mulgnn0cl 15731 . . . . . . . . 9 mulGrp
155149, 34, 152, 154syl3anc 1219 . . . . . . . 8
156 eqid 2450 . . . . . . . . 9 Scalar Scalar
157 eqid 2450 . . . . . . . . 9 Scalar Scalar
158 eqid 2450 . . . . . . . . 9 Scalar Scalar
1592, 4, 156, 20, 157, 158lmodvsdir 17064 . . . . . . . 8 Scalar Scalar Scalar
160131, 140, 145, 155, 159syl13anc 1221 . . . . . . 7 Scalar
161128, 160eqtrd 2490 . . . . . 6
162161mpteq2dva 4462 . . . . 5
163162oveq2d 6192 . . . 4 g g
164 eqid 2450 . . . . 5
165 rngcmn 16767 . . . . . . 7 CMnd
16616, 165syl 16 . . . . . 6 CMnd
167166adantr 465 . . . . 5 CMnd
168 nn0ex 10672 . . . . . 6
169168a1i 11 . . . . 5
170110anim2i 569 . . . . . . 7
171 df-3an 967 . . . . . . 7
172170, 171sylibr 212 . . . . . 6
1735, 7, 1, 42, 20, 21, 22, 12, 14, 2pmattomply1ghmlem1 31239 . . . . . 6
174172, 173sylan 471 . . . . 5
175118anim2i 569 . . . . . . 7
176 df-3an 967 . . . . . . 7
177175, 176sylibr 212 . . . . . 6
1785, 7, 1, 42, 20, 21, 22, 12, 14, 2pmattomply1ghmlem1 31239 . . . . . 6
179177, 178sylan 471 . . . . 5
180 eqidd 2451 . . . . 5
181 eqidd 2451 . . . . 5
1825, 7, 1, 19, 20, 21, 22, 12, 14, 2pmattomply1ghmlem2 31240 . . . . . 6 finSupp
183172, 182syl 16 . . . . 5 finSupp
1845, 7, 1, 19, 20, 21, 22, 12, 14, 2pmattomply1ghmlem2 31240 . . . . . 6 finSupp
185177, 184syl 16 . . . . 5 finSupp
1862, 164, 4, 167, 169, 174, 179, 180, 181, 183, 185gsummptfsadd 16504 . . . 4 g g g
187163, 186eqtrd 2490 . . 3 g g g
1885, 7, 1, 19, 20, 21, 22, 12, 14, 2, 23pmattomply1 31242 . . . 4 g
18932, 188syl 16 . . 3 g
1905, 7, 1, 19, 20, 21, 22, 12, 14, 2, 23pmattomply1 31242 . . . . 5 g
1915, 7, 1, 19, 20, 21, 22, 12, 14, 2, 23pmattomply1 31242 . . . . 5 g
192190, 191oveqan12d 6195 . . . 4 g g
193192adantl 466 . . 3 g g
194187, 189, 1933eqtr4d 2500 . 2
1951, 2, 3, 4, 11, 18, 24, 194isghmd 15844 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   w3a 965   wceq 1370   wcel 1757  cvv 3054   class class class wbr 4376   cmpt 4434  cfv 5502  (class class class)co 6176   cmpt2 6178   cof 6404  cfn 7396   finSupp cfsupp 7707  cn0 10666  cbs 14262   cplusg 14326  Scalarcsca 14329  cvsca 14330  c0g 14466   g cgsu 14467  cmnd 15497  cgrp 15498  .gcmg 15502   cghm 15832  CMndccmn 16367  mulGrpcmgp 16682  crg 16737  clmod 17040  var1cv1 17725  Poly1cpl1 17726  coe1cco1 17727   Mat cmat 18375 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-rep 4487  ax-sep 4497  ax-nul 4505  ax-pow 4554  ax-pr 4615  ax-un 6458  ax-inf2 7934  ax-cnex 9425  ax-resscn 9426  ax-1cn 9427  ax-icn 9428  ax-addcl 9429  ax-addrcl 9430  ax-mulcl 9431  ax-mulrcl 9432  ax-mulcom 9433  ax-addass 9434  ax-mulass 9435  ax-distr 9436  ax-i2m1 9437  ax-1ne0 9438  ax-1rid 9439  ax-rnegex 9440  ax-rrecex 9441  ax-cnre 9442  ax-pre-lttri 9443  ax-pre-lttrn 9444  ax-pre-ltadd 9445  ax-pre-mulgt0 9446 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-nel 2644  df-ral 2797  df-rex 2798  df-reu 2799  df-rmo 2800  df-rab 2801  df-v 3056  df-sbc 3271  df-csb 3373  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-pss 3428  df-nul 3722  df-if 3876  df-pw 3946  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-ot 3970  df-uni 4176  df-int 4213  df-iun 4257  df-iin 4258  df-br 4377  df-opab 4435  df-mpt 4436  df-tr 4470  df-eprel 4716  df-id 4720  df-po 4725  df-so 4726  df-fr 4763  df-se 4764  df-we 4765  df-ord 4806  df-on 4807  df-lim 4808  df-suc 4809  df-xp 4930  df-rel 4931  df-cnv 4932  df-co 4933  df-dm 4934  df-rn 4935  df-res 4936  df-ima 4937  df-iota 5465  df-fun 5504  df-fn 5505  df-f 5506  df-f1 5507  df-fo 5508  df-f1o 5509  df-fv 5510  df-isom 5511  df-riota 6137  df-ov 6179  df-oprab 6180  df-mpt2 6181  df-of 6406  df-ofr 6407  df-om 6563  df-1st 6663  df-2nd 6664  df-supp 6777  df-recs 6918  df-rdg 6952  df-1o 7006  df-2o 7007  df-oadd 7010  df-er 7187  df-map 7302  df-pm 7303  df-ixp 7350  df-en 7397  df-dom 7398  df-sdom 7399  df-fin 7400  df-fsupp 7708  df-sup 7778  df-oi 7811  df-card 8196  df-pnf 9507  df-mnf 9508  df-xr 9509  df-ltxr 9510  df-le 9511  df-sub 9684  df-neg 9685  df-nn 10410  df-2 10467  df-3 10468  df-4 10469  df-5 10470  df-6 10471  df-7 10472  df-8 10473  df-9 10474  df-10 10475  df-n0 10667  df-z 10734  df-dec 10843  df-uz 10949  df-fz 11525  df-fzo 11636  df-seq 11894  df-hash 12191  df-struct 14264  df-ndx 14265  df-slot 14266  df-base 14267  df-sets 14268  df-ress 14269  df-plusg 14339  df-mulr 14340  df-sca 14342  df-vsca 14343  df-ip 14344  df-tset 14345  df-ple 14346  df-ds 14348  df-hom 14350  df-cco 14351  df-0g 14468  df-gsum 14469  df-prds 14474  df-pws 14476  df-mre 14612  df-mrc 14613  df-acs 14615  df-mnd 15503  df-mhm 15552  df-submnd 15553  df-grp 15633  df-minusg 15634  df-sbg 15635  df-mulg 15636  df-subg 15766  df-ghm 15833  df-cntz 15923  df-cmn 16369  df-abl 16370  df-mgp 16683  df-ur 16695  df-rng 16739  df-subrg 16955  df-lmod 17042  df-lss 17106  df-sra 17345  df-rgmod 17346  df-psr 17515  df-mvr 17516  df-mpl 17517  df-opsr 17519  df-psr1 17729  df-vr1 17730  df-ply1 17731  df-coe1 17732  df-dsmm 18252  df-frlm 18267  df-mamu 18376  df-mat 18377 This theorem is referenced by:  pmattomply1grpiso  31257  pmattomply1rhm  31262  pmat2matp  31265
 Copyright terms: Public domain W3C validator