![]() |
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 4249 | . 2 ⊢ (𝑋 ∈ 𝐵 → ¬ 𝐵 = ∅) | |
2 | matrcl.a | . . . . 5 ⊢ 𝐴 = (𝑁 Mat 𝑅) | |
3 | df-mat 21013 | . . . . . 6 ⊢ Mat = (𝑎 ∈ Fin, 𝑏 ∈ V ↦ ((𝑏 freeLMod (𝑎 × 𝑎)) sSet 〈(.r‘ndx), (𝑏 maMul 〈𝑎, 𝑎, 𝑎〉)〉)) | |
4 | 3 | mpondm0 7366 | . . . . 5 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (𝑁 Mat 𝑅) = ∅) |
5 | 2, 4 | syl5eq 2845 | . . . 4 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐴 = ∅) |
6 | 5 | fveq2d 6649 | . . 3 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (Base‘𝐴) = (Base‘∅)) |
7 | matrcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐴) | |
8 | base0 16528 | . . 3 ⊢ ∅ = (Base‘∅) | |
9 | 6, 7, 8 | 3eqtr4g 2858 | . 2 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐵 = ∅) |
10 | 1, 9 | nsyl2 143 | 1 ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 = wceq 1538 ∈ wcel 2111 Vcvv 3441 ∅c0 4243 〈cop 4531 〈cotp 4533 × cxp 5517 ‘cfv 6324 (class class class)co 7135 Fincfn 8492 ndxcnx 16472 sSet csts 16473 Basecbs 16475 .rcmulr 16558 freeLMod cfrlm 20435 maMul cmmul 20990 Mat cmat 21012 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-iota 6283 df-fun 6326 df-fv 6332 df-ov 7138 df-oprab 7139 df-mpo 7140 df-slot 16479 df-base 16481 df-mat 21013 |
This theorem is referenced by: matbas2i 21027 matecl 21030 matplusg2 21032 matvsca2 21033 matplusgcell 21038 matsubgcell 21039 matinvgcell 21040 matvscacell 21041 matmulcell 21050 mattposcl 21058 mattposvs 21060 mattposm 21064 matgsumcl 21065 madetsumid 21066 madetsmelbas 21069 madetsmelbas2 21070 marrepval0 21166 marrepval 21167 marrepcl 21169 marepvval0 21171 marepvval 21172 marepvcl 21174 ma1repveval 21176 mulmarep1gsum1 21178 mulmarep1gsum2 21179 submabas 21183 submaval0 21185 submaval 21186 mdetleib2 21193 mdetf 21200 mdetrlin 21207 mdetrsca 21208 mdetralt 21213 mdetmul 21228 maduval 21243 maducoeval2 21245 maduf 21246 madutpos 21247 madugsum 21248 madurid 21249 madulid 21250 minmar1val0 21252 minmar1val 21253 marep01ma 21265 smadiadetlem0 21266 smadiadetlem1a 21268 smadiadetlem3 21273 smadiadetlem4 21274 smadiadet 21275 smadiadetglem2 21277 matinv 21282 matunit 21283 slesolvec 21284 slesolinv 21285 slesolinvbi 21286 slesolex 21287 cramerimplem2 21289 cramerimplem3 21290 cramerimp 21291 decpmatcl 21372 decpmataa0 21373 decpmatmul 21377 smatcl 31155 matunitlindflem2 35054 matunitlindf 35055 |
Copyright terms: Public domain | W3C validator |