![]() |
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 22734). 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 22726 or slesolinv 22728. 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‘𝑅) ↑m 𝑁) |
cramer.d | ⊢ 𝐷 = (𝑁 maDet 𝑅) |
cramer.x | ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) |
cramer.q | ⊢ / = (/r‘𝑅) |
Ref | Expression |
---|---|
cramer | ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) ↔ (𝑋 · 𝑍) = 𝑌)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.22 459 | . . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) → (𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing)) | |
2 | cramer.a | . . . 4 ⊢ 𝐴 = (𝑁 Mat 𝑅) | |
3 | cramer.b | . . . 4 ⊢ 𝐵 = (Base‘𝐴) | |
4 | cramer.v | . . . 4 ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) | |
5 | cramer.d | . . . 4 ⊢ 𝐷 = (𝑁 maDet 𝑅) | |
6 | cramer.x | . . . 4 ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) | |
7 | cramer.q | . . . 4 ⊢ / = (/r‘𝑅) | |
8 | 2, 3, 4, 5, 6, 7 | cramerlem3 22737 | . . 3 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)) |
9 | 1, 8 | syl3an1 1163 | . 2 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)) |
10 | simpl1l 1224 | . . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑅 ∈ CRing) | |
11 | simpl2 1192 | . . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) | |
12 | simpl3 1193 | . . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ (𝑋 · 𝑍) = 𝑌) → (𝐷‘𝑋) ∈ (Unit‘𝑅)) | |
13 | crngring 20293 | . . . . . . . 8 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | |
14 | 13 | anim1ci 615 | . . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) → (𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring)) |
15 | 14 | anim1i 614 | . . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉))) |
16 | 15 | 3adant3 1132 | . . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ((𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉))) |
17 | 2, 3, 4, 6 | slesolvec 22727 | . . . . . 6 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑋 · 𝑍) = 𝑌 → 𝑍 ∈ 𝑉)) |
18 | 17 | imp 406 | . . . . 5 ⊢ ((((𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑍 ∈ 𝑉) |
19 | 16, 18 | sylan 579 | . . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑍 ∈ 𝑉) |
20 | simpr 484 | . . . 4 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋 · 𝑍) = 𝑌) | |
21 | 2, 3, 4, 5, 6, 7 | cramerlem1 22735 | . . . 4 ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ ((𝐷‘𝑋) ∈ (Unit‘𝑅) ∧ 𝑍 ∈ 𝑉 ∧ (𝑋 · 𝑍) = 𝑌)) → 𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋)))) |
22 | 10, 11, 12, 19, 20, 21 | syl113anc 1382 | . . 3 ⊢ ((((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋)))) |
23 | 22 | ex 412 | . 2 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ((𝑋 · 𝑍) = 𝑌 → 𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))))) |
24 | 9, 23 | impbid 212 | 1 ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) ↔ (𝑋 · 𝑍) = 𝑌)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 ∅c0 4353 〈cop 4655 ↦ cmpt 5251 ‘cfv 6577 (class class class)co 7452 ↑m cmap 8888 Basecbs 17279 Ringcrg 20281 CRingccrg 20282 Unitcui 20402 /rcdvr 20447 Mat cmat 22453 maVecMul cmvmul 22588 matRepV cmatrepV 22605 maDet cmdat 22632 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5305 ax-sep 5319 ax-nul 5326 ax-pow 5385 ax-pr 5449 ax-un 7774 ax-cnex 11244 ax-resscn 11245 ax-1cn 11246 ax-icn 11247 ax-addcl 11248 ax-addrcl 11249 ax-mulcl 11250 ax-mulrcl 11251 ax-mulcom 11252 ax-addass 11253 ax-mulass 11254 ax-distr 11255 ax-i2m1 11256 ax-1ne0 11257 ax-1rid 11258 ax-rnegex 11259 ax-rrecex 11260 ax-cnre 11261 ax-pre-lttri 11262 ax-pre-lttrn 11263 ax-pre-ltadd 11264 ax-pre-mulgt0 11265 ax-addf 11267 ax-mulf 11268 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-xor 1509 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3445 df-v 3491 df-sbc 3806 df-csb 3923 df-dif 3980 df-un 3982 df-in 3984 df-ss 3994 df-pss 3997 df-nul 4354 df-if 4550 df-pw 4625 df-sn 4650 df-pr 4652 df-tp 4654 df-op 4656 df-ot 4658 df-uni 4934 df-int 4973 df-iun 5019 df-iin 5020 df-br 5169 df-opab 5231 df-mpt 5252 df-tr 5286 df-id 5595 df-eprel 5601 df-po 5609 df-so 5610 df-fr 5654 df-se 5655 df-we 5656 df-xp 5708 df-rel 5709 df-cnv 5710 df-co 5711 df-dm 5712 df-rn 5713 df-res 5714 df-ima 5715 df-pred 6336 df-ord 6402 df-on 6403 df-lim 6404 df-suc 6405 df-iota 6529 df-fun 6579 df-fn 6580 df-f 6581 df-f1 6582 df-fo 6583 df-f1o 6584 df-fv 6585 df-isom 6586 df-riota 7408 df-ov 7455 df-oprab 7456 df-mpo 7457 df-of 7718 df-om 7908 df-1st 8034 df-2nd 8035 df-supp 8206 df-tpos 8271 df-frecs 8326 df-wrecs 8357 df-recs 8431 df-rdg 8470 df-1o 8526 df-2o 8527 df-er 8767 df-map 8890 df-pm 8891 df-ixp 8960 df-en 9008 df-dom 9009 df-sdom 9010 df-fin 9011 df-fsupp 9436 df-sup 9515 df-oi 9583 df-card 10012 df-pnf 11330 df-mnf 11331 df-xr 11332 df-ltxr 11333 df-le 11334 df-sub 11527 df-neg 11528 df-div 11954 df-nn 12300 df-2 12362 df-3 12363 df-4 12364 df-5 12365 df-6 12366 df-7 12367 df-8 12368 df-9 12369 df-n0 12560 df-xnn0 12633 df-z 12647 df-dec 12767 df-uz 12912 df-rp 13068 df-fz 13580 df-fzo 13724 df-seq 14071 df-exp 14131 df-hash 14398 df-word 14581 df-lsw 14629 df-concat 14637 df-s1 14662 df-substr 14707 df-pfx 14737 df-splice 14816 df-reverse 14825 df-s2 14915 df-struct 17215 df-sets 17232 df-slot 17250 df-ndx 17262 df-base 17280 df-ress 17309 df-plusg 17345 df-mulr 17346 df-starv 17347 df-sca 17348 df-vsca 17349 df-ip 17350 df-tset 17351 df-ple 17352 df-ds 17354 df-unif 17355 df-hom 17356 df-cco 17357 df-0g 17522 df-gsum 17523 df-prds 17528 df-pws 17530 df-mre 17665 df-mrc 17666 df-acs 17668 df-mgm 18699 df-sgrp 18778 df-mnd 18794 df-mhm 18839 df-submnd 18840 df-efmnd 18925 df-grp 18997 df-minusg 18998 df-sbg 18999 df-mulg 19129 df-subg 19184 df-ghm 19274 df-gim 19320 df-cntz 19378 df-oppg 19407 df-symg 19432 df-pmtr 19505 df-psgn 19554 df-evpm 19555 df-cmn 19845 df-abl 19846 df-mgp 20183 df-rng 20201 df-ur 20230 df-srg 20235 df-ring 20283 df-cring 20284 df-oppr 20381 df-dvdsr 20404 df-unit 20405 df-invr 20435 df-dvr 20448 df-rhm 20519 df-subrng 20593 df-subrg 20618 df-drng 20774 df-lmod 20903 df-lss 20974 df-sra 21216 df-rgmod 21217 df-cnfld 21409 df-zring 21502 df-zrh 21558 df-dsmm 21796 df-frlm 21811 df-assa 21917 df-mamu 22437 df-mat 22454 df-mvmul 22589 df-marrep 22606 df-marepv 22607 df-subma 22625 df-mdet 22633 df-madu 22682 df-minmar1 22683 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |