![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cramer | Structured version Visualization version GIF version |
Description: Cramer's rule. According to Wikipedia "Cramer's rule", 21-Feb-2019, https://en.wikipedia.org/wiki/Cramer%27s_rule: "[Cramer's rule] ... expresses the [unique] solution [of a system of linear equations] in terms of the determinants of the (square) coefficient matrix and of matrices obtained from it by replacing one column by the column vector of right-hand sides of the equations." If it is assumed that a (unique) solution exists, it can be obtained by Cramer's rule (see also cramerimp 20999). On the other hand, if a vector can be constructed by Cramer's rule, it is a solution of the system of linear equations, so at least one solution exists. The uniqueness is ensured by considering only systems of linear equations whose matrix has a unit (of the underlying ring) as determinant, see matunit 20991 or slesolinv 20993. For fields as underlying rings, this requirement is equivalent to the determinant not being 0. Theorem 4.4 in [Lang] p. 513. This is Metamath 100 proof #97. (Contributed by Alexander van der Vekens, 21-Feb-2019.) (Revised by Alexander van der Vekens, 1-Mar-2019.) |
Ref | Expression |
---|---|
cramer.a | ⊢ 𝐴 = (𝑁 Mat 𝑅) |
cramer.b | ⊢ 𝐵 = (Base‘𝐴) |
cramer.v | ⊢ 𝑉 = ((Base‘𝑅) ↑𝑚 𝑁) |
cramer.d | ⊢ 𝐷 = (𝑁 maDet 𝑅) |
cramer.x | ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) |
cramer.q | ⊢ / = (/r‘𝑅) |
Ref | Expression |
---|---|
cramer | ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) ↔ (𝑋 · 𝑍) = 𝑌)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.22 452 | . . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) → (𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing)) | |
2 | cramer.a | . . . 4 ⊢ 𝐴 = (𝑁 Mat 𝑅) | |
3 | cramer.b | . . . 4 ⊢ 𝐵 = (Base‘𝐴) | |
4 | cramer.v | . . . 4 ⊢ 𝑉 = ((Base‘𝑅) ↑𝑚 𝑁) | |
5 | cramer.d | . . . 4 ⊢ 𝐷 = (𝑁 maDet 𝑅) | |
6 | cramer.x | . . . 4 ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) | |
7 | cramer.q | . . . 4 ⊢ / = (/r‘𝑅) | |
8 | 2, 3, 4, 5, 6, 7 | cramerlem3 21002 | . . 3 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)) |
9 | 1, 8 | syl3an1 1143 | . 2 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)) |
10 | simpl1l 1204 | . . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑅 ∈ CRing) | |
11 | simpl2 1172 | . . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) | |
12 | simpl3 1173 | . . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ (𝑋 · 𝑍) = 𝑌) → (𝐷‘𝑋) ∈ (Unit‘𝑅)) | |
13 | crngring 19031 | . . . . . . . 8 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | |
14 | 13 | anim1ci 606 | . . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) → (𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring)) |
15 | 14 | anim1i 605 | . . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉))) |
16 | 15 | 3adant3 1112 | . . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ((𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉))) |
17 | 2, 3, 4, 6 | slesolvec 20992 | . . . . . 6 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑋 · 𝑍) = 𝑌 → 𝑍 ∈ 𝑉)) |
18 | 17 | imp 398 | . . . . 5 ⊢ ((((𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑍 ∈ 𝑉) |
19 | 16, 18 | sylan 572 | . . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑍 ∈ 𝑉) |
20 | simpr 477 | . . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋 · 𝑍) = 𝑌) | |
21 | 2, 3, 4, 5, 6, 7 | cramerlem1 21000 | . . . 4 ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ ((𝐷‘𝑋) ∈ (Unit‘𝑅) ∧ 𝑍 ∈ 𝑉 ∧ (𝑋 · 𝑍) = 𝑌)) → 𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋)))) |
22 | 10, 11, 12, 19, 20, 21 | syl113anc 1362 | . . 3 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋)))) |
23 | 22 | ex 405 | . 2 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ((𝑋 · 𝑍) = 𝑌 → 𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))))) |
24 | 9, 23 | impbid 204 | 1 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) ↔ (𝑋 · 𝑍) = 𝑌)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∈ wcel 2050 ≠ wne 2967 ∅c0 4178 〈cop 4447 ↦ cmpt 5008 ‘cfv 6188 (class class class)co 6976 ↑𝑚 cmap 8206 Basecbs 16339 Ringcrg 19020 CRingccrg 19021 Unitcui 19112 /rcdvr 19155 Mat cmat 20720 maVecMul cmvmul 20853 matRepV cmatrepV 20870 maDet cmdat 20897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-rep 5049 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 ax-un 7279 ax-cnex 10391 ax-resscn 10392 ax-1cn 10393 ax-icn 10394 ax-addcl 10395 ax-addrcl 10396 ax-mulcl 10397 ax-mulrcl 10398 ax-mulcom 10399 ax-addass 10400 ax-mulass 10401 ax-distr 10402 ax-i2m1 10403 ax-1ne0 10404 ax-1rid 10405 ax-rnegex 10406 ax-rrecex 10407 ax-cnre 10408 ax-pre-lttri 10409 ax-pre-lttrn 10410 ax-pre-ltadd 10411 ax-pre-mulgt0 10412 ax-addf 10414 ax-mulf 10415 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-xor 1489 df-tru 1510 df-fal 1520 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-reu 3095 df-rmo 3096 df-rab 3097 df-v 3417 df-sbc 3682 df-csb 3787 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-pss 3845 df-nul 4179 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-tp 4446 df-op 4448 df-ot 4450 df-uni 4713 df-int 4750 df-iun 4794 df-iin 4795 df-br 4930 df-opab 4992 df-mpt 5009 df-tr 5031 df-id 5312 df-eprel 5317 df-po 5326 df-so 5327 df-fr 5366 df-se 5367 df-we 5368 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-pred 5986 df-ord 6032 df-on 6033 df-lim 6034 df-suc 6035 df-iota 6152 df-fun 6190 df-fn 6191 df-f 6192 df-f1 6193 df-fo 6194 df-f1o 6195 df-fv 6196 df-isom 6197 df-riota 6937 df-ov 6979 df-oprab 6980 df-mpo 6981 df-of 7227 df-om 7397 df-1st 7501 df-2nd 7502 df-supp 7634 df-tpos 7695 df-wrecs 7750 df-recs 7812 df-rdg 7850 df-1o 7905 df-2o 7906 df-oadd 7909 df-er 8089 df-map 8208 df-pm 8209 df-ixp 8260 df-en 8307 df-dom 8308 df-sdom 8309 df-fin 8310 df-fsupp 8629 df-sup 8701 df-oi 8769 df-card 9162 df-pnf 10476 df-mnf 10477 df-xr 10478 df-ltxr 10479 df-le 10480 df-sub 10672 df-neg 10673 df-div 11099 df-nn 11440 df-2 11503 df-3 11504 df-4 11505 df-5 11506 df-6 11507 df-7 11508 df-8 11509 df-9 11510 df-n0 11708 df-xnn0 11780 df-z 11794 df-dec 11912 df-uz 12059 df-rp 12205 df-fz 12709 df-fzo 12850 df-seq 13185 df-exp 13245 df-hash 13506 df-word 13673 df-lsw 13726 df-concat 13734 df-s1 13759 df-substr 13804 df-pfx 13853 df-splice 13960 df-reverse 13978 df-s2 14072 df-struct 16341 df-ndx 16342 df-slot 16343 df-base 16345 df-sets 16346 df-ress 16347 df-plusg 16434 df-mulr 16435 df-starv 16436 df-sca 16437 df-vsca 16438 df-ip 16439 df-tset 16440 df-ple 16441 df-ds 16443 df-unif 16444 df-hom 16445 df-cco 16446 df-0g 16571 df-gsum 16572 df-prds 16577 df-pws 16579 df-mre 16715 df-mrc 16716 df-acs 16718 df-mgm 17710 df-sgrp 17752 df-mnd 17763 df-mhm 17803 df-submnd 17804 df-grp 17894 df-minusg 17895 df-sbg 17896 df-mulg 18012 df-subg 18060 df-ghm 18127 df-gim 18170 df-cntz 18218 df-oppg 18245 df-symg 18267 df-pmtr 18331 df-psgn 18380 df-evpm 18381 df-cmn 18668 df-abl 18669 df-mgp 18963 df-ur 18975 df-srg 18979 df-ring 19022 df-cring 19023 df-oppr 19096 df-dvdsr 19114 df-unit 19115 df-invr 19145 df-dvr 19156 df-rnghom 19190 df-drng 19227 df-subrg 19256 df-lmod 19358 df-lss 19426 df-sra 19666 df-rgmod 19667 df-assa 19806 df-cnfld 20248 df-zring 20320 df-zrh 20353 df-dsmm 20578 df-frlm 20593 df-mamu 20697 df-mat 20721 df-mvmul 20854 df-marrep 20871 df-marepv 20872 df-subma 20890 df-mdet 20898 df-madu 20947 df-minmar1 20948 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |