MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mat2pmat1 Structured version   Visualization version   GIF version

Theorem mat2pmat1 21944
Description: The transformation of the identity matrix results in the identity polynomial matrix. (Contributed by AV, 29-Oct-2019.)
Hypotheses
Ref Expression
mat2pmatbas.t 𝑇 = (𝑁 matToPolyMat 𝑅)
mat2pmatbas.a 𝐴 = (𝑁 Mat 𝑅)
mat2pmatbas.b 𝐵 = (Base‘𝐴)
mat2pmatbas.p 𝑃 = (Poly1𝑅)
mat2pmatbas.c 𝐶 = (𝑁 Mat 𝑃)
mat2pmatbas0.h 𝐻 = (Base‘𝐶)
Assertion
Ref Expression
mat2pmat1 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑇‘(1r𝐴)) = (1r𝐶))

Proof of Theorem mat2pmat1
Dummy variables 𝑖 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 483 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑁 ∈ Fin)
2 simpr 485 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Ring)
3 mat2pmatbas.a . . . . . . . 8 𝐴 = (𝑁 Mat 𝑅)
43matring 21655 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
5 mat2pmatbas.b . . . . . . . 8 𝐵 = (Base‘𝐴)
6 eqid 2735 . . . . . . . 8 (1r𝐴) = (1r𝐴)
75, 6ringidcl 19866 . . . . . . 7 (𝐴 ∈ Ring → (1r𝐴) ∈ 𝐵)
84, 7syl 17 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (1r𝐴) ∈ 𝐵)
91, 2, 83jca 1127 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (1r𝐴) ∈ 𝐵))
10 mat2pmatbas.t . . . . . 6 𝑇 = (𝑁 matToPolyMat 𝑅)
11 mat2pmatbas.p . . . . . 6 𝑃 = (Poly1𝑅)
12 eqid 2735 . . . . . 6 (algSc‘𝑃) = (algSc‘𝑃)
1310, 3, 5, 11, 12mat2pmatvalel 21937 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (1r𝐴) ∈ 𝐵) ∧ (𝑖𝑁𝑗𝑁)) → (𝑖(𝑇‘(1r𝐴))𝑗) = ((algSc‘𝑃)‘(𝑖(1r𝐴)𝑗)))
149, 13sylan 580 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑖𝑁𝑗𝑁)) → (𝑖(𝑇‘(1r𝐴))𝑗) = ((algSc‘𝑃)‘(𝑖(1r𝐴)𝑗)))
15 fvif 6820 . . . . . 6 ((algSc‘𝑃)‘if(𝑖 = 𝑗, (1r𝑅), (0g𝑅))) = if(𝑖 = 𝑗, ((algSc‘𝑃)‘(1r𝑅)), ((algSc‘𝑃)‘(0g𝑅)))
16 eqid 2735 . . . . . . . . 9 (1r𝑅) = (1r𝑅)
17 eqid 2735 . . . . . . . . 9 (1r𝑃) = (1r𝑃)
1811, 12, 16, 17ply1scl1 21526 . . . . . . . 8 (𝑅 ∈ Ring → ((algSc‘𝑃)‘(1r𝑅)) = (1r𝑃))
1918ad2antlr 724 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑖𝑁𝑗𝑁)) → ((algSc‘𝑃)‘(1r𝑅)) = (1r𝑃))
20 eqid 2735 . . . . . . . . 9 (0g𝑅) = (0g𝑅)
21 eqid 2735 . . . . . . . . 9 (0g𝑃) = (0g𝑃)
2211, 12, 20, 21ply1scl0 21524 . . . . . . . 8 (𝑅 ∈ Ring → ((algSc‘𝑃)‘(0g𝑅)) = (0g𝑃))
2322ad2antlr 724 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑖𝑁𝑗𝑁)) → ((algSc‘𝑃)‘(0g𝑅)) = (0g𝑃))
2419, 23ifeq12d 4485 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑖𝑁𝑗𝑁)) → if(𝑖 = 𝑗, ((algSc‘𝑃)‘(1r𝑅)), ((algSc‘𝑃)‘(0g𝑅))) = if(𝑖 = 𝑗, (1r𝑃), (0g𝑃)))
2515, 24eqtrid 2787 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑖𝑁𝑗𝑁)) → ((algSc‘𝑃)‘if(𝑖 = 𝑗, (1r𝑅), (0g𝑅))) = if(𝑖 = 𝑗, (1r𝑃), (0g𝑃)))
261adantr 481 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑖𝑁𝑗𝑁)) → 𝑁 ∈ Fin)
272adantr 481 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑖𝑁𝑗𝑁)) → 𝑅 ∈ Ring)
28 simpl 483 . . . . . . . 8 ((𝑖𝑁𝑗𝑁) → 𝑖𝑁)
2928adantl 482 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑖𝑁𝑗𝑁)) → 𝑖𝑁)
30 simpr 485 . . . . . . . 8 ((𝑖𝑁𝑗𝑁) → 𝑗𝑁)
3130adantl 482 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑖𝑁𝑗𝑁)) → 𝑗𝑁)
323, 16, 20, 26, 27, 29, 31, 6mat1ov 21660 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑖𝑁𝑗𝑁)) → (𝑖(1r𝐴)𝑗) = if(𝑖 = 𝑗, (1r𝑅), (0g𝑅)))
3332fveq2d 6808 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑖𝑁𝑗𝑁)) → ((algSc‘𝑃)‘(𝑖(1r𝐴)𝑗)) = ((algSc‘𝑃)‘if(𝑖 = 𝑗, (1r𝑅), (0g𝑅))))
34 mat2pmatbas.c . . . . . 6 𝐶 = (𝑁 Mat 𝑃)
3511ply1ring 21482 . . . . . . 7 (𝑅 ∈ Ring → 𝑃 ∈ Ring)
3635ad2antlr 724 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑖𝑁𝑗𝑁)) → 𝑃 ∈ Ring)
37 eqid 2735 . . . . . 6 (1r𝐶) = (1r𝐶)
3834, 17, 21, 26, 36, 29, 31, 37mat1ov 21660 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑖𝑁𝑗𝑁)) → (𝑖(1r𝐶)𝑗) = if(𝑖 = 𝑗, (1r𝑃), (0g𝑃)))
3925, 33, 383eqtr4d 2785 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑖𝑁𝑗𝑁)) → ((algSc‘𝑃)‘(𝑖(1r𝐴)𝑗)) = (𝑖(1r𝐶)𝑗))
4014, 39eqtrd 2775 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑖𝑁𝑗𝑁)) → (𝑖(𝑇‘(1r𝐴))𝑗) = (𝑖(1r𝐶)𝑗))
4140ralrimivva 3192 . 2 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑖𝑁𝑗𝑁 (𝑖(𝑇‘(1r𝐴))𝑗) = (𝑖(1r𝐶)𝑗))
42 mat2pmatbas0.h . . . . 5 𝐻 = (Base‘𝐶)
4310, 3, 5, 11, 34, 42mat2pmatbas0 21939 . . . 4 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (1r𝐴) ∈ 𝐵) → (𝑇‘(1r𝐴)) ∈ 𝐻)
449, 43syl 17 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑇‘(1r𝐴)) ∈ 𝐻)
4511, 34pmatring 21904 . . . 4 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring)
4642, 37ringidcl 19866 . . . 4 (𝐶 ∈ Ring → (1r𝐶) ∈ 𝐻)
4745, 46syl 17 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (1r𝐶) ∈ 𝐻)
4834, 42eqmat 21636 . . 3 (((𝑇‘(1r𝐴)) ∈ 𝐻 ∧ (1r𝐶) ∈ 𝐻) → ((𝑇‘(1r𝐴)) = (1r𝐶) ↔ ∀𝑖𝑁𝑗𝑁 (𝑖(𝑇‘(1r𝐴))𝑗) = (𝑖(1r𝐶)𝑗)))
4944, 47, 48syl2anc 584 . 2 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑇‘(1r𝐴)) = (1r𝐶) ↔ ∀𝑖𝑁𝑗𝑁 (𝑖(𝑇‘(1r𝐴))𝑗) = (𝑖(1r𝐶)𝑗)))
5041, 49mpbird 256 1 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑇‘(1r𝐴)) = (1r𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1538  wcel 2103  wral 3060  ifcif 4464  cfv 6458  (class class class)co 7308  Fincfn 8769  Basecbs 16971  0gc0g 17209  1rcur 19796  Ringcrg 19842  algSccascl 21122  Poly1cpl1 21411   Mat cmat 21617   matToPolyMat cmat2pmat 21916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-8 2105  ax-9 2113  ax-10 2134  ax-11 2151  ax-12 2168  ax-ext 2706  ax-rep 5217  ax-sep 5231  ax-nul 5238  ax-pow 5296  ax-pr 5360  ax-un 7621  ax-cnex 10987  ax-resscn 10988  ax-1cn 10989  ax-icn 10990  ax-addcl 10991  ax-addrcl 10992  ax-mulcl 10993  ax-mulrcl 10994  ax-mulcom 10995  ax-addass 10996  ax-mulass 10997  ax-distr 10998  ax-i2m1 10999  ax-1ne0 11000  ax-1rid 11001  ax-rnegex 11002  ax-rrecex 11003  ax-cnre 11004  ax-pre-lttri 11005  ax-pre-lttrn 11006  ax-pre-ltadd 11007  ax-pre-mulgt0 11008
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1779  df-nf 1783  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2727  df-clel 2813  df-nfc 2885  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3339  df-reu 3340  df-rab 3357  df-v 3438  df-sbc 3721  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-ot 4573  df-uni 4844  df-int 4886  df-iun 4932  df-iin 4933  df-br 5081  df-opab 5143  df-mpt 5164  df-tr 5198  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-se 5556  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-isom 6467  df-riota 7265  df-ov 7311  df-oprab 7312  df-mpo 7313  df-of 7566  df-ofr 7567  df-om 7749  df-1st 7867  df-2nd 7868  df-supp 8013  df-frecs 8132  df-wrecs 8163  df-recs 8237  df-rdg 8276  df-1o 8332  df-er 8534  df-map 8653  df-pm 8654  df-ixp 8722  df-en 8770  df-dom 8771  df-sdom 8772  df-fin 8773  df-fsupp 9187  df-sup 9259  df-oi 9327  df-card 9755  df-pnf 11071  df-mnf 11072  df-xr 11073  df-ltxr 11074  df-le 11075  df-sub 11267  df-neg 11268  df-nn 12034  df-2 12096  df-3 12097  df-4 12098  df-5 12099  df-6 12100  df-7 12101  df-8 12102  df-9 12103  df-n0 12294  df-z 12380  df-dec 12498  df-uz 12643  df-fz 13300  df-fzo 13443  df-seq 13782  df-hash 14105  df-struct 16907  df-sets 16924  df-slot 16942  df-ndx 16954  df-base 16972  df-ress 17001  df-plusg 17034  df-mulr 17035  df-sca 17037  df-vsca 17038  df-ip 17039  df-tset 17040  df-ple 17041  df-ds 17043  df-hom 17045  df-cco 17046  df-0g 17211  df-gsum 17212  df-prds 17217  df-pws 17219  df-mre 17354  df-mrc 17355  df-acs 17357  df-mgm 18385  df-sgrp 18434  df-mnd 18445  df-mhm 18489  df-submnd 18490  df-grp 18639  df-minusg 18640  df-sbg 18641  df-mulg 18760  df-subg 18811  df-ghm 18891  df-cntz 18982  df-cmn 19447  df-abl 19448  df-mgp 19780  df-ur 19797  df-ring 19844  df-subrg 20085  df-lmod 20188  df-lss 20257  df-sra 20497  df-rgmod 20498  df-dsmm 21002  df-frlm 21017  df-ascl 21125  df-psr 21175  df-mpl 21177  df-opsr 21179  df-psr1 21414  df-ply1 21416  df-mamu 21596  df-mat 21618  df-mat2pmat 21919
This theorem is referenced by:  mat2pmatmhm  21945  idmatidpmat  21949
  Copyright terms: Public domain W3C validator