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 4298 | . 2 ⊢ (𝑋 ∈ 𝐵 → ¬ 𝐵 = ∅) | |
2 | matrcl.a | . . . . 5 ⊢ 𝐴 = (𝑁 Mat 𝑅) | |
3 | df-mat 21016 | . . . . . 6 ⊢ Mat = (𝑎 ∈ Fin, 𝑏 ∈ V ↦ ((𝑏 freeLMod (𝑎 × 𝑎)) sSet 〈(.r‘ndx), (𝑏 maMul 〈𝑎, 𝑎, 𝑎〉)〉)) | |
4 | 3 | mpondm0 7385 | . . . . 5 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (𝑁 Mat 𝑅) = ∅) |
5 | 2, 4 | syl5eq 2868 | . . . 4 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐴 = ∅) |
6 | 5 | fveq2d 6673 | . . 3 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (Base‘𝐴) = (Base‘∅)) |
7 | matrcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐴) | |
8 | base0 16535 | . . 3 ⊢ ∅ = (Base‘∅) | |
9 | 6, 7, 8 | 3eqtr4g 2881 | . 2 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐵 = ∅) |
10 | 1, 9 | nsyl2 143 | 1 ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 398 = wceq 1533 ∈ wcel 2110 Vcvv 3494 ∅c0 4290 〈cop 4572 〈cotp 4574 × cxp 5552 ‘cfv 6354 (class class class)co 7155 Fincfn 8508 ndxcnx 16479 sSet csts 16480 Basecbs 16482 .rcmulr 16565 freeLMod cfrlm 20889 maMul cmmul 20993 Mat cmat 21015 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5202 ax-nul 5209 ax-pow 5265 ax-pr 5329 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4567 df-pr 4569 df-op 4573 df-uni 4838 df-br 5066 df-opab 5128 df-mpt 5146 df-id 5459 df-xp 5560 df-rel 5561 df-cnv 5562 df-co 5563 df-dm 5564 df-iota 6313 df-fun 6356 df-fv 6362 df-ov 7158 df-oprab 7159 df-mpo 7160 df-slot 16486 df-base 16488 df-mat 21016 |
This theorem is referenced by: matbas2i 21030 matecl 21033 matplusg2 21035 matvsca2 21036 matplusgcell 21041 matsubgcell 21042 matinvgcell 21043 matvscacell 21044 matmulcell 21053 mattposcl 21061 mattposvs 21063 mattposm 21067 matgsumcl 21068 madetsumid 21069 madetsmelbas 21072 madetsmelbas2 21073 marrepval0 21169 marrepval 21170 marrepcl 21172 marepvval0 21174 marepvval 21175 marepvcl 21177 ma1repveval 21179 mulmarep1gsum1 21181 mulmarep1gsum2 21182 submabas 21186 submaval0 21188 submaval 21189 mdetleib2 21196 mdetf 21203 mdetrlin 21210 mdetrsca 21211 mdetralt 21216 mdetmul 21231 maduval 21246 maducoeval2 21248 maduf 21249 madutpos 21250 madugsum 21251 madurid 21252 madulid 21253 minmar1val0 21255 minmar1val 21256 marep01ma 21268 smadiadetlem0 21269 smadiadetlem1a 21271 smadiadetlem3 21276 smadiadetlem4 21277 smadiadet 21278 smadiadetglem2 21280 matinv 21285 matunit 21286 slesolvec 21287 slesolinv 21288 slesolinvbi 21289 slesolex 21290 cramerimplem2 21292 cramerimplem3 21293 cramerimp 21294 decpmatcl 21374 decpmataa0 21375 decpmatmul 21379 smatcl 31067 matunitlindflem2 34888 matunitlindf 34889 |
Copyright terms: Public domain | W3C validator |