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

Theorem matrcl 20158
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 3902 . 2 (𝑋𝐵 → ¬ 𝐵 = ∅)
2 matrcl.a . . . . 5 𝐴 = (𝑁 Mat 𝑅)
3 df-mat 20154 . . . . . 6 Mat = (𝑎 ∈ Fin, 𝑏 ∈ V ↦ ((𝑏 freeLMod (𝑎 × 𝑎)) sSet ⟨(.r‘ndx), (𝑏 maMul ⟨𝑎, 𝑎, 𝑎⟩)⟩))
43mpt2ndm0 6840 . . . . 5 (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (𝑁 Mat 𝑅) = ∅)
52, 4syl5eq 2667 . . . 4 (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐴 = ∅)
65fveq2d 6162 . . 3 (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (Base‘𝐴) = (Base‘∅))
7 matrcl.b . . 3 𝐵 = (Base‘𝐴)
8 base0 15852 . . 3 ∅ = (Base‘∅)
96, 7, 83eqtr4g 2680 . 2 (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐵 = ∅)
101, 9nsyl2 142 1 (𝑋𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384   = wceq 1480  wcel 1987  Vcvv 3190  c0 3897  cop 4161  cotp 4163   × cxp 5082  cfv 5857  (class class class)co 6615  Fincfn 7915  ndxcnx 15797   sSet csts 15798  Basecbs 15800  .rcmulr 15882   freeLMod cfrlm 20030   maMul cmmul 20129   Mat cmat 20153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-opab 4684  df-mpt 4685  df-id 4999  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-iota 5820  df-fun 5859  df-fv 5865  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-slot 15804  df-base 15805  df-mat 20154
This theorem is referenced by:  matbas2i  20168  matecl  20171  matplusg2  20173  matvsca2  20174  matplusgcell  20179  matsubgcell  20180  matinvgcell  20181  matvscacell  20182  matmulcell  20191  mattposcl  20199  mattposvs  20201  mattposm  20205  matgsumcl  20206  madetsumid  20207  madetsmelbas  20210  madetsmelbas2  20211  marrepval0  20307  marrepval  20308  marrepcl  20310  marepvval0  20312  marepvval  20313  marepvcl  20315  ma1repveval  20317  mulmarep1gsum1  20319  mulmarep1gsum2  20320  submabas  20324  submaval0  20326  submaval  20327  mdetleib2  20334  mdetf  20341  mdetrlin  20348  mdetrsca  20349  mdetralt  20354  mdetmul  20369  maduval  20384  maducoeval2  20386  maduf  20387  madutpos  20388  madugsum  20389  madurid  20390  madulid  20391  minmar1val0  20393  minmar1val  20394  marep01ma  20406  smadiadetlem0  20407  smadiadetlem1a  20409  smadiadetlem3  20414  smadiadetlem4  20415  smadiadet  20416  smadiadetglem2  20418  matinv  20423  matunit  20424  slesolvec  20425  slesolinv  20426  slesolinvbi  20427  slesolex  20428  cramerimplem2  20430  cramerimplem3  20431  cramerimp  20432  decpmatcl  20512  decpmataa0  20513  decpmatmul  20517  smatcl  29692  matunitlindflem2  33077  matunitlindf  33078
  Copyright terms: Public domain W3C validator