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

Theorem matrcl 20418
Description: Reverse closure for the matrix algebra. (Contributed by Stefan O'Rear, 5-Sep-2015.)
Hypotheses
Ref Expression
matrcl.a 𝐴 = (𝑁 Mat 𝑅)
matrcl.b 𝐵 = (Base‘𝐴)
Assertion
Ref Expression
matrcl (𝑋𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))

Proof of Theorem matrcl
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 n0i 4061 . 2 (𝑋𝐵 → ¬ 𝐵 = ∅)
2 matrcl.a . . . . 5 𝐴 = (𝑁 Mat 𝑅)
3 df-mat 20414 . . . . . 6 Mat = (𝑎 ∈ Fin, 𝑏 ∈ V ↦ ((𝑏 freeLMod (𝑎 × 𝑎)) sSet ⟨(.r‘ndx), (𝑏 maMul ⟨𝑎, 𝑎, 𝑎⟩)⟩))
43mpt2ndm0 7038 . . . . 5 (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (𝑁 Mat 𝑅) = ∅)
52, 4syl5eq 2804 . . . 4 (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐴 = ∅)
65fveq2d 6354 . . 3 (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (Base‘𝐴) = (Base‘∅))
7 matrcl.b . . 3 𝐵 = (Base‘𝐴)
8 base0 16112 . . 3 ∅ = (Base‘∅)
96, 7, 83eqtr4g 2817 . 2 (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐵 = ∅)
101, 9nsyl2 142 1 (𝑋𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383   = wceq 1630  wcel 2137  Vcvv 3338  c0 4056  cop 4325  cotp 4327   × cxp 5262  cfv 6047  (class class class)co 6811  Fincfn 8119  ndxcnx 16054   sSet csts 16055  Basecbs 16057  .rcmulr 16142   freeLMod cfrlm 20290   maMul cmmul 20389   Mat cmat 20413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ral 3053  df-rex 3054  df-rab 3057  df-v 3340  df-sbc 3575  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-sn 4320  df-pr 4322  df-op 4326  df-uni 4587  df-br 4803  df-opab 4863  df-mpt 4880  df-id 5172  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-iota 6010  df-fun 6049  df-fv 6055  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-slot 16061  df-base 16063  df-mat 20414
This theorem is referenced by:  matbas2i  20428  matecl  20431  matplusg2  20433  matvsca2  20434  matplusgcell  20439  matsubgcell  20440  matinvgcell  20441  matvscacell  20442  matmulcell  20451  mattposcl  20459  mattposvs  20461  mattposm  20465  matgsumcl  20466  madetsumid  20467  madetsmelbas  20470  madetsmelbas2  20471  marrepval0  20567  marrepval  20568  marrepcl  20570  marepvval0  20572  marepvval  20573  marepvcl  20575  ma1repveval  20577  mulmarep1gsum1  20579  mulmarep1gsum2  20580  submabas  20584  submaval0  20586  submaval  20587  mdetleib2  20594  mdetf  20601  mdetrlin  20608  mdetrsca  20609  mdetralt  20614  mdetmul  20629  maduval  20644  maducoeval2  20646  maduf  20647  madutpos  20648  madugsum  20649  madurid  20650  madulid  20651  minmar1val0  20653  minmar1val  20654  marep01ma  20666  smadiadetlem0  20667  smadiadetlem1a  20669  smadiadetlem3  20674  smadiadetlem4  20675  smadiadet  20676  smadiadetglem2  20678  matinv  20683  matunit  20684  slesolvec  20685  slesolinv  20686  slesolinvbi  20687  slesolex  20688  cramerimplem2  20690  cramerimplem3  20691  cramerimp  20692  decpmatcl  20772  decpmataa0  20773  decpmatmul  20777  smatcl  30175  matunitlindflem2  33717  matunitlindf  33718
  Copyright terms: Public domain W3C validator