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

Theorem matrcl 19979
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 3878 . 2 (𝑋𝐵 → ¬ 𝐵 = ∅)
2 matrcl.a . . . . 5 𝐴 = (𝑁 Mat 𝑅)
3 df-mat 19975 . . . . . 6 Mat = (𝑎 ∈ Fin, 𝑏 ∈ V ↦ ((𝑏 freeLMod (𝑎 × 𝑎)) sSet ⟨(.r‘ndx), (𝑏 maMul ⟨𝑎, 𝑎, 𝑎⟩)⟩))
43mpt2ndm0 6750 . . . . 5 (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (𝑁 Mat 𝑅) = ∅)
52, 4syl5eq 2655 . . . 4 (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐴 = ∅)
65fveq2d 6092 . . 3 (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (Base‘𝐴) = (Base‘∅))
7 matrcl.b . . 3 𝐵 = (Base‘𝐴)
8 base0 15686 . . 3 ∅ = (Base‘∅)
96, 7, 83eqtr4g 2668 . 2 (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐵 = ∅)
101, 9nsyl2 140 1 (𝑋𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382   = wceq 1474  wcel 1976  Vcvv 3172  c0 3873  cop 4130  cotp 4132   × cxp 5026  cfv 5790  (class class class)co 6527  Fincfn 7818  ndxcnx 15638   sSet csts 15639  Basecbs 15641  .rcmulr 15715   freeLMod cfrlm 19851   maMul cmmul 19950   Mat cmat 19974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-iota 5754  df-fun 5792  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-slot 15645  df-base 15646  df-mat 19975
This theorem is referenced by:  matbas2i  19989  matecl  19992  matplusg2  19994  matvsca2  19995  matplusgcell  20000  matsubgcell  20001  matinvgcell  20002  matvscacell  20003  matmulcell  20012  mattposcl  20020  mattposvs  20022  mattposm  20026  matgsumcl  20027  madetsumid  20028  madetsmelbas  20031  madetsmelbas2  20032  marrepval0  20128  marrepval  20129  marrepcl  20131  marepvval0  20133  marepvval  20134  marepvcl  20136  ma1repveval  20138  mulmarep1gsum1  20140  mulmarep1gsum2  20141  submabas  20145  submaval0  20147  submaval  20148  mdetleib2  20155  mdetf  20162  mdetrlin  20169  mdetrsca  20170  mdetralt  20175  mdetmul  20190  maduval  20205  maducoeval2  20207  maduf  20208  madutpos  20209  madugsum  20210  madurid  20211  madulid  20212  minmar1val0  20214  minmar1val  20215  marep01ma  20227  smadiadetlem0  20228  smadiadetlem1a  20230  smadiadetlem3  20235  smadiadetlem4  20236  smadiadet  20237  smadiadetglem2  20239  matinv  20244  matunit  20245  slesolvec  20246  slesolinv  20247  slesolinvbi  20248  slesolex  20249  cramerimplem2  20251  cramerimplem3  20252  cramerimp  20253  decpmatcl  20333  decpmataa0  20334  decpmatmul  20338  smatcl  29002  matunitlindflem2  32379  matunitlindf  32380
  Copyright terms: Public domain W3C validator