Theorem matrcl 22395

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.

Step	Hyp	Ref	Expression
1		n0i 4268	. 2 ⊢ (𝑋 ∈ 𝐵 → ¬ 𝐵 = ∅)
2		matrcl.a	. . . . 5 ⊢ 𝐴 = (𝑁 Mat 𝑅)
3		df-mat 22391	. . . . . 6 ⊢ Mat = (𝑎 ∈ Fin, 𝑏 ∈ V ↦ ((𝑏 freeLMod (𝑎 × 𝑎)) sSet ⟨(.r‘ndx), (𝑏 maMul ⟨𝑎, 𝑎, 𝑎⟩)⟩))
4	3	mpondm0 7596	. . . . 5 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (𝑁 Mat 𝑅) = ∅)
5	2, 4	eqtrid 2786	. . . 4 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐴 = ∅)
6	5	fveq2d 6831	. . 3 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (Base‘𝐴) = (Base‘∅))
7		matrcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐴)
8		base0 17175	. . 3 ⊢ ∅ = (Base‘∅)
9	6, 7, 8	3eqtr4g 2799	. 2 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐵 = ∅)
10	1, 9	nsyl2 141	1 ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  Vcvv 3431  ∅c0 4261  ⟨cop 4561  ⟨cotp 4563   × cxp 5616  ‘cfv 6485  (class class class)co 7356  Fincfn 8883   sSet csts 17124  ndxcnx 17154  Basecbs 17170  ._rcmulr 17212   freeLMod cfrlm 21721   maMul cmmul 22373   Mat cmat 22390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-1cn 11087  ax-addcl 11089

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12166  df-slot 17143  df-ndx 17155  df-base 17171  df-mat 22391

This theorem is referenced by:  matbas2i  22405  matecl  22408  matplusg2  22410  matvsca2  22411  matplusgcell  22416  matsubgcell  22417  matinvgcell  22418  matvscacell  22419  matmulcell  22428  mattposcl  22436  mattposvs  22438  mattposm  22442  matgsumcl  22443  madetsumid  22444  madetsmelbas  22447  madetsmelbas2  22448  marrepval0  22544  marrepval  22545  marrepcl  22547  marepvval0  22549  marepvval  22550  marepvcl  22552  ma1repveval  22554  mulmarep1gsum1  22556  mulmarep1gsum2  22557  submabas  22561  submaval0  22563  submaval  22564  mdetleib2  22571  mdetf  22578  mdetrlin  22585  mdetrsca  22586  mdetralt  22591  mdetmul  22606  maduval  22621  maducoeval2  22623  maduf  22624  madutpos  22625  madugsum  22626  madurid  22627  madulid  22628  minmar1val0  22630  minmar1val  22631  marep01ma  22643  smadiadetlem0  22644  smadiadetlem1a  22646  smadiadetlem3  22651  smadiadetlem4  22652  smadiadet  22653  smadiadetglem2  22655  matinv  22660  matunit  22661  slesolvec  22662  slesolinv  22663  slesolinvbi  22664  slesolex  22665  cramerimplem2  22667  cramerimplem3  22668  cramerimp  22669  decpmatcl  22750  decpmataa0  22751  decpmatmul  22755  smatcl  33986  matunitlindflem2  37984  matunitlindf  37985