Theorem matrcl 22739

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 4288	. 2 ⊢ (𝑋 ∈ 𝐵 → ¬ 𝐵 = ∅)
2		matrcl.a	. . . . 5 ⊢ 𝐴 = (𝑁 Mat 𝑅)
3		df-mat 22735	. . . . . 6 ⊢ Mat = (𝑎 ∈ Fin, 𝑏 ∈ V ↦ ((𝑏 freeLMod (𝑎 × 𝑎)) sSet ⟨(.r‘ndx), (𝑏 maMul ⟨𝑎, 𝑎, 𝑎⟩)⟩))
4	3	mpondm0 7668	. . . . 5 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (𝑁 Mat 𝑅) = ∅)
5	2, 4	eqtrid 2810	. . . 4 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐴 = ∅)
6	5	fveq2d 6897	. . 3 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (Base‘𝐴) = (Base‘∅))
7		matrcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐴)
8		base0 17404	. . 3 ⊢ ∅ = (Base‘∅)
9	6, 7, 8	3eqtr4g 2823	. 2 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐵 = ∅)
10	1, 9	nsyl2 142	1 ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2146  Vcvv 3453  ∅c0 4280  ⟨cop 4837  ⟨cotp 4860   × cxp 5652  ‘cfv 6546  (class class class)co 7427  Fincfn 8984   sSet csts 17353  ndxcnx 17383  Basecbs 17399  ._rcmulr 17441   freeLMod cfrlm 22064   maMul cmmul 22717   Mat cmat 22734

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758  ax-cnex 11266  ax-1cn 11268  ax-addcl 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-pss 4016  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-iun 4955  df-br 5106  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5549  df-eprel 5554  df-po 5562  df-so 5563  df-fr 5607  df-we 5609  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6310  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-ov 7430  df-oprab 7431  df-mpo 7432  df-om 7885  df-2nd 8009  df-frecs 8310  df-wrecs 8341  df-recs 8390  df-rdg 8429  df-nn 12346  df-slot 17372  df-ndx 17384  df-base 17400  df-mat 22735

This theorem is used by:  matbas2i  22749  matecl  22752  matplusg2  22754  matvsca2  22755  matplusgcell  22760  matsubgcell  22761  matinvgcell  22762  matvscacell  22763  matmulcell  22772  mattposcl  22780  mattposvs  22782  mattposm  22786  matgsumcl  22787  madetsumid  22788  madetsmelbas  22791  madetsmelbas2  22792  marrepval0  22888  marrepval  22889  marrepcl  22891  marepvval0  22893  marepvval  22894  marepvcl  22896  ma1repveval  22898  mulmarep1gsum1  22900  mulmarep1gsum2  22901  submabas  22905  submaval0  22907  submaval  22908  mdetleib2  22915  mdetf  22922  mdetrlin  22929  mdetrsca  22930  mdetralt  22935  mdetmul  22950  maduval  22965  maducoeval2  22967  maduf  22968  madutpos  22969  madugsum  22970  madurid  22971  madulid  22972  minmar1val0  22974  minmar1val  22975  marep01ma  22987  smadiadetlem0  22988  smadiadetlem1a  22990  smadiadetlem3  22995  smadiadetlem4  22996  smadiadet  22997  smadiadetglem2  22999  matinv  23004  matunit  23005  matunitlindflem2  23007  matunitlindf  23008  slesolvec  23009  slesolinv  23010  slesolinvbi  23011  slesolex  23012  cramerimplem2  23014  cramerimplem3  23015  cramerimp  23016  decpmatcl  23097  decpmataa0  23098  decpmatmul  23102  smatcl  34487