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 20947 | . . . . . 6 ⊢ Mat = (𝑎 ∈ Fin, 𝑏 ∈ V ↦ ((𝑏 freeLMod (𝑎 × 𝑎)) sSet 〈(.r‘ndx), (𝑏 maMul 〈𝑎, 𝑎, 𝑎〉)〉)) | |
4 | 3 | mpondm0 7375 | . . . . 5 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (𝑁 Mat 𝑅) = ∅) |
5 | 2, 4 | syl5eq 2868 | . . . 4 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → 𝐴 = ∅) |
6 | 5 | fveq2d 6668 | . . 3 ⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (Base‘𝐴) = (Base‘∅)) |
7 | matrcl.b | . . 3 ⊢ 𝐵 = (Base‘𝐴) | |
8 | base0 16526 | . . 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 396 = wceq 1528 ∈ wcel 2105 Vcvv 3495 ∅c0 4290 〈cop 4565 〈cotp 4567 × cxp 5547 ‘cfv 6349 (class class class)co 7145 Fincfn 8498 ndxcnx 16470 sSet csts 16471 Basecbs 16473 .rcmulr 16556 freeLMod cfrlm 20820 maMul cmmul 20924 Mat cmat 20946 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 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 3497 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-br 5059 df-opab 5121 df-mpt 5139 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-iota 6308 df-fun 6351 df-fv 6357 df-ov 7148 df-oprab 7149 df-mpo 7150 df-slot 16477 df-base 16479 df-mat 20947 |
This theorem is referenced by: matbas2i 20961 matecl 20964 matplusg2 20966 matvsca2 20967 matplusgcell 20972 matsubgcell 20973 matinvgcell 20974 matvscacell 20975 matmulcell 20984 mattposcl 20992 mattposvs 20994 mattposm 20998 matgsumcl 20999 madetsumid 21000 madetsmelbas 21003 madetsmelbas2 21004 marrepval0 21100 marrepval 21101 marrepcl 21103 marepvval0 21105 marepvval 21106 marepvcl 21108 ma1repveval 21110 mulmarep1gsum1 21112 mulmarep1gsum2 21113 submabas 21117 submaval0 21119 submaval 21120 mdetleib2 21127 mdetf 21134 mdetrlin 21141 mdetrsca 21142 mdetralt 21147 mdetmul 21162 maduval 21177 maducoeval2 21179 maduf 21180 madutpos 21181 madugsum 21182 madurid 21183 madulid 21184 minmar1val0 21186 minmar1val 21187 marep01ma 21199 smadiadetlem0 21200 smadiadetlem1a 21202 smadiadetlem3 21207 smadiadetlem4 21208 smadiadet 21209 smadiadetglem2 21211 matinv 21216 matunit 21217 slesolvec 21218 slesolinv 21219 slesolinvbi 21220 slesolex 21221 cramerimplem2 21223 cramerimplem3 21224 cramerimp 21225 decpmatcl 21305 decpmataa0 21306 decpmatmul 21310 smatcl 30967 matunitlindflem2 34771 matunitlindf 34772 |
Copyright terms: Public domain | W3C validator |