Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > matrcl | Structured version Visualization version GIF version |
Description: Reverse closure for the matrix algebra. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
Ref | Expression |
---|---|
matrcl.a | ⊢ 𝐴 = (𝑁 Mat 𝑅) |
matrcl.b | ⊢ 𝐵 = (Base‘𝐴) |
Ref | Expression |
---|---|
matrcl | ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | n0i 3920 | . 2 ⊢ (𝑋 ∈ 𝐵 → ¬ 𝐵 = ∅) | |
2 | matrcl.a | . . . . 5 ⊢ 𝐴 = (𝑁 Mat 𝑅) | |
3 | df-mat 20214 | . . . . . 6 ⊢ Mat = (𝑎 ∈ Fin, 𝑏 ∈ V ↦ ((𝑏 freeLMod (𝑎 × 𝑎)) sSet 〈(.r‘ndx), (𝑏 maMul 〈𝑎, 𝑎, 𝑎〉)〉)) | |
4 | 3 | mpt2ndm0 6875 | . . . . 5 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (𝑁 Mat 𝑅) = ∅) |
5 | 2, 4 | syl5eq 2668 | . . . 4 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐴 = ∅) |
6 | 5 | fveq2d 6195 | . . 3 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (Base‘𝐴) = (Base‘∅)) |
7 | matrcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐴) | |
8 | base0 15912 | . . 3 ⊢ ∅ = (Base‘∅) | |
9 | 6, 7, 8 | 3eqtr4g 2681 | . 2 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐵 = ∅) |
10 | 1, 9 | nsyl2 142 | 1 ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 Vcvv 3200 ∅c0 3915 〈cop 4183 〈cotp 4185 × cxp 5112 ‘cfv 5888 (class class class)co 6650 Fincfn 7955 ndxcnx 15854 sSet csts 15855 Basecbs 15857 .rcmulr 15942 freeLMod cfrlm 20090 maMul cmmul 20189 Mat cmat 20213 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-iota 5851 df-fun 5890 df-fv 5896 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-slot 15861 df-base 15863 df-mat 20214 |
This theorem is referenced by: matbas2i 20228 matecl 20231 matplusg2 20233 matvsca2 20234 matplusgcell 20239 matsubgcell 20240 matinvgcell 20241 matvscacell 20242 matmulcell 20251 mattposcl 20259 mattposvs 20261 mattposm 20265 matgsumcl 20266 madetsumid 20267 madetsmelbas 20270 madetsmelbas2 20271 marrepval0 20367 marrepval 20368 marrepcl 20370 marepvval0 20372 marepvval 20373 marepvcl 20375 ma1repveval 20377 mulmarep1gsum1 20379 mulmarep1gsum2 20380 submabas 20384 submaval0 20386 submaval 20387 mdetleib2 20394 mdetf 20401 mdetrlin 20408 mdetrsca 20409 mdetralt 20414 mdetmul 20429 maduval 20444 maducoeval2 20446 maduf 20447 madutpos 20448 madugsum 20449 madurid 20450 madulid 20451 minmar1val0 20453 minmar1val 20454 marep01ma 20466 smadiadetlem0 20467 smadiadetlem1a 20469 smadiadetlem3 20474 smadiadetlem4 20475 smadiadet 20476 smadiadetglem2 20478 matinv 20483 matunit 20484 slesolvec 20485 slesolinv 20486 slesolinvbi 20487 slesolex 20488 cramerimplem2 20490 cramerimplem3 20491 cramerimp 20492 decpmatcl 20572 decpmataa0 20573 decpmatmul 20577 smatcl 29868 matunitlindflem2 33406 matunitlindf 33407 |
Copyright terms: Public domain | W3C validator |