Theorem matrcl 21097

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 4228	. 2 ⊢ (𝑋 ∈ 𝐵 → ¬ 𝐵 = ∅)
2		matrcl.a	. . . . 5 ⊢ 𝐴 = (𝑁 Mat 𝑅)
3		df-mat 21093	. . . . . 6 ⊢ Mat = (𝑎 ∈ Fin, 𝑏 ∈ V ↦ ((𝑏 freeLMod (𝑎 × 𝑎)) sSet ⟨(.r‘ndx), (𝑏 maMul ⟨𝑎, 𝑎, 𝑎⟩)⟩))
4	3	mpondm0 7375	. . . . 5 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (𝑁 Mat 𝑅) = ∅)
5	2, 4	syl5eq 2806	. . . 4 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐴 = ∅)
6	5	fveq2d 6655	. . 3 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (Base‘𝐴) = (Base‘∅))
7		matrcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐴)
8		base0 16579	. . 3 ⊢ ∅ = (Base‘∅)
9	6, 7, 8	3eqtr4g 2819	. 2 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐵 = ∅)
10	1, 9	nsyl2 143	1 ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1539   ∈ wcel 2112  Vcvv 3407  ∅c0 4221  ⟨cop 4521  ⟨cotp 4523   × cxp 5515  ‘cfv 6328  (class class class)co 7143  Fincfn 8520  ndxcnx 16523   sSet csts 16524  Basecbs 16526  ._rcmulr 16609   freeLMod cfrlm 20496   maMul cmmul 21070   Mat cmat 21092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5162  ax-nul 5169  ax-pr 5291

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-ral 3073  df-rex 3074  df-v 3409  df-sbc 3694  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-nul 4222  df-if 4414  df-sn 4516  df-pr 4518  df-op 4522  df-uni 4792  df-br 5026  df-opab 5088  df-mpt 5106  df-id 5423  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-iota 6287  df-fun 6330  df-fv 6336  df-ov 7146  df-oprab 7147  df-mpo 7148  df-slot 16530  df-base 16532  df-mat 21093

This theorem is referenced by:  matbas2i  21107  matecl  21110  matplusg2  21112  matvsca2  21113  matplusgcell  21118  matsubgcell  21119  matinvgcell  21120  matvscacell  21121  matmulcell  21130  mattposcl  21138  mattposvs  21140  mattposm  21144  matgsumcl  21145  madetsumid  21146  madetsmelbas  21149  madetsmelbas2  21150  marrepval0  21246  marrepval  21247  marrepcl  21249  marepvval0  21251  marepvval  21252  marepvcl  21254  ma1repveval  21256  mulmarep1gsum1  21258  mulmarep1gsum2  21259  submabas  21263  submaval0  21265  submaval  21266  mdetleib2  21273  mdetf  21280  mdetrlin  21287  mdetrsca  21288  mdetralt  21293  mdetmul  21308  maduval  21323  maducoeval2  21325  maduf  21326  madutpos  21327  madugsum  21328  madurid  21329  madulid  21330  minmar1val0  21332  minmar1val  21333  marep01ma  21345  smadiadetlem0  21346  smadiadetlem1a  21348  smadiadetlem3  21353  smadiadetlem4  21354  smadiadet  21355  smadiadetglem2  21357  matinv  21362  matunit  21363  slesolvec  21364  slesolinv  21365  slesolinvbi  21366  slesolex  21367  cramerimplem2  21369  cramerimplem3  21370  cramerimp  21371  decpmatcl  21452  decpmataa0  21453  decpmatmul  21457  smatcl  31258  matunitlindflem2  35319  matunitlindf  35320