Theorem matrcl 22473

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1561   ∈ wcel 2143  Vcvv 3455  ∅c0 4286  ⟨cop 4589  ⟨cotp 4591   × cxp 5646  ‘cfv 6522  (class class class)co 7397  Fincfn 8928   sSet csts 17200  ndxcnx 17230  Basecbs 17246  ._rcmulr 17288   freeLMod cfrlm 21799   maMul cmmul 22451   Mat cmat 22468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7719  ax-cnex 11130  ax-1cn 11132  ax-addcl 11134

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-tr 5209  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6289  df-ord 6350  df-on 6351  df-lim 6352  df-suc 6353  df-iota 6478  df-fun 6524  df-fn 6525  df-f 6526  df-f1 6527  df-fo 6528  df-f1o 6529  df-fv 6530  df-ov 7400  df-oprab 7401  df-mpo 7402  df-om 7848  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8382  df-nn 12212  df-slot 17219  df-ndx 17231  df-base 17247  df-mat 22469

This theorem is referenced by:  matbas2i  22483  matecl  22486  matplusg2  22488  matvsca2  22489  matplusgcell  22494  matsubgcell  22495  matinvgcell  22496  matvscacell  22497  matmulcell  22506  mattposcl  22514  mattposvs  22516  mattposm  22520  matgsumcl  22521  madetsumid  22522  madetsmelbas  22525  madetsmelbas2  22526  marrepval0  22622  marrepval  22623  marrepcl  22625  marepvval0  22627  marepvval  22628  marepvcl  22630  ma1repveval  22632  mulmarep1gsum1  22634  mulmarep1gsum2  22635  submabas  22639  submaval0  22641  submaval  22642  mdetleib2  22649  mdetf  22656  mdetrlin  22663  mdetrsca  22664  mdetralt  22669  mdetmul  22684  maduval  22699  maducoeval2  22701  maduf  22702  madutpos  22703  madugsum  22704  madurid  22705  madulid  22706  minmar1val0  22708  minmar1val  22709  marep01ma  22721  smadiadetlem0  22722  smadiadetlem1a  22724  smadiadetlem3  22729  smadiadetlem4  22730  smadiadet  22731  smadiadetglem2  22733  matinv  22738  matunit  22739  slesolvec  22740  slesolinv  22741  slesolinvbi  22742  slesolex  22743  cramerimplem2  22745  cramerimplem3  22746  cramerimp  22747  decpmatcl  22828  decpmataa0  22829  decpmatmul  22833  smatcl  34100  matunitlindflem2  38117  matunitlindf  38118