Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cramerimplem3 | Structured version Visualization version GIF version |
Description: Lemma 3 for cramerimp 21614: The determinant of the matrix of a system of linear equations multiplied with the determinant of the identity matrix with the ith column replaced by the solution vector of the system of linear equations equals the determinant of the matrix of the system of linear equations with the ith column replaced by the right-hand side vector of the system of linear equations. (Contributed by AV, 19-Feb-2019.) (Revised by AV, 1-Mar-2019.) |
Ref | Expression |
---|---|
cramerimp.a | ⊢ 𝐴 = (𝑁 Mat 𝑅) |
cramerimp.b | ⊢ 𝐵 = (Base‘𝐴) |
cramerimp.v | ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) |
cramerimp.e | ⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) |
cramerimp.h | ⊢ 𝐻 = ((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝐼) |
cramerimp.x | ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) |
cramerimp.d | ⊢ 𝐷 = (𝑁 maDet 𝑅) |
cramerimp.t | ⊢ ⊗ = (.r‘𝑅) |
Ref | Expression |
---|---|
cramerimplem3 | ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → ((𝐷‘𝑋) ⊗ (𝐷‘𝐸)) = (𝐷‘𝐻)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 486 | . . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → 𝑅 ∈ CRing) | |
2 | cramerimp.a | . . . . . . . . . 10 ⊢ 𝐴 = (𝑁 Mat 𝑅) | |
3 | cramerimp.b | . . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐴) | |
4 | 2, 3 | matrcl 21340 | . . . . . . . . 9 ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
5 | 4 | simpld 498 | . . . . . . . 8 ⊢ (𝑋 ∈ 𝐵 → 𝑁 ∈ Fin) |
6 | 5 | adantr 484 | . . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → 𝑁 ∈ Fin) |
7 | 1, 6 | anim12ci 617 | . . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) |
8 | 7 | 3adant3 1134 | . . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) |
9 | eqid 2739 | . . . . . 6 ⊢ (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) | |
10 | 2, 9 | matmulr 21366 | . . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (.r‘𝐴)) |
11 | 8, 10 | syl 17 | . . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) = (.r‘𝐴)) |
12 | 11 | oveqd 7251 | . . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐸) = (𝑋(.r‘𝐴)𝐸)) |
13 | 12 | fveq2d 6742 | . 2 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝐷‘(𝑋(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐸)) = (𝐷‘(𝑋(.r‘𝐴)𝐸))) |
14 | cramerimp.v | . . . 4 ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) | |
15 | cramerimp.e | . . . 4 ⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) | |
16 | cramerimp.h | . . . 4 ⊢ 𝐻 = ((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝐼) | |
17 | cramerimp.x | . . . 4 ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) | |
18 | 2, 3, 14, 15, 16, 17, 9 | cramerimplem2 21612 | . . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐸) = 𝐻) |
19 | 18 | fveq2d 6742 | . 2 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝐷‘(𝑋(𝑅 maMul 〈𝑁, 𝑁, 𝑁〉)𝐸)) = (𝐷‘𝐻)) |
20 | simp1l 1199 | . . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑅 ∈ CRing) | |
21 | simp2l 1201 | . . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑋 ∈ 𝐵) | |
22 | crngring 19606 | . . . . . . . 8 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | |
23 | 22 | adantr 484 | . . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → 𝑅 ∈ Ring) |
24 | 23, 6 | anim12i 616 | . . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin)) |
25 | 24 | 3adant3 1134 | . . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin)) |
26 | ne0i 4265 | . . . . . . . 8 ⊢ (𝐼 ∈ 𝑁 → 𝑁 ≠ ∅) | |
27 | 22, 26 | anim12ci 617 | . . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → (𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring)) |
28 | 2, 3, 14, 17 | slesolvec 21607 | . . . . . . 7 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑋 · 𝑍) = 𝑌 → 𝑍 ∈ 𝑉)) |
29 | 27, 28 | sylan 583 | . . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑋 · 𝑍) = 𝑌 → 𝑍 ∈ 𝑉)) |
30 | 29 | 3impia 1119 | . . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑍 ∈ 𝑉) |
31 | simp1r 1200 | . . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝐼 ∈ 𝑁) | |
32 | eqid 2739 | . . . . . 6 ⊢ (1r‘𝐴) = (1r‘𝐴) | |
33 | 2, 3, 14, 32 | ma1repvcl 21498 | . . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁)) → (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) ∈ 𝐵) |
34 | 25, 30, 31, 33 | syl12anc 837 | . . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) ∈ 𝐵) |
35 | 15, 34 | eqeltrid 2844 | . . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝐸 ∈ 𝐵) |
36 | cramerimp.d | . . . 4 ⊢ 𝐷 = (𝑁 maDet 𝑅) | |
37 | cramerimp.t | . . . 4 ⊢ ⊗ = (.r‘𝑅) | |
38 | eqid 2739 | . . . 4 ⊢ (.r‘𝐴) = (.r‘𝐴) | |
39 | 2, 3, 36, 37, 38 | mdetmul 21551 | . . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝐸 ∈ 𝐵) → (𝐷‘(𝑋(.r‘𝐴)𝐸)) = ((𝐷‘𝑋) ⊗ (𝐷‘𝐸))) |
40 | 20, 21, 35, 39 | syl3anc 1373 | . 2 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝐷‘(𝑋(.r‘𝐴)𝐸)) = ((𝐷‘𝑋) ⊗ (𝐷‘𝐸))) |
41 | 13, 19, 40 | 3eqtr3rd 2788 | 1 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → ((𝐷‘𝑋) ⊗ (𝐷‘𝐸)) = (𝐷‘𝐻)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∈ wcel 2112 ≠ wne 2943 Vcvv 3423 ∅c0 4253 〈cop 4563 〈cotp 4565 ‘cfv 6400 (class class class)co 7234 ↑m cmap 8531 Fincfn 8649 Basecbs 16792 .rcmulr 16835 1rcur 19548 Ringcrg 19594 CRingccrg 19595 maMul cmmul 21313 Mat cmat 21335 maVecMul cmvmul 21468 matRepV cmatrepV 21485 maDet cmdat 21512 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-rep 5195 ax-sep 5208 ax-nul 5215 ax-pow 5274 ax-pr 5338 ax-un 7544 ax-cnex 10814 ax-resscn 10815 ax-1cn 10816 ax-icn 10817 ax-addcl 10818 ax-addrcl 10819 ax-mulcl 10820 ax-mulrcl 10821 ax-mulcom 10822 ax-addass 10823 ax-mulass 10824 ax-distr 10825 ax-i2m1 10826 ax-1ne0 10827 ax-1rid 10828 ax-rnegex 10829 ax-rrecex 10830 ax-cnre 10831 ax-pre-lttri 10832 ax-pre-lttrn 10833 ax-pre-ltadd 10834 ax-pre-mulgt0 10835 ax-addf 10837 ax-mulf 10838 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-xor 1508 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3425 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4456 df-pw 4531 df-sn 4558 df-pr 4560 df-tp 4562 df-op 4564 df-ot 4566 df-uni 4836 df-int 4876 df-iun 4922 df-iin 4923 df-br 5070 df-opab 5132 df-mpt 5152 df-tr 5178 df-id 5471 df-eprel 5477 df-po 5485 df-so 5486 df-fr 5526 df-se 5527 df-we 5528 df-xp 5574 df-rel 5575 df-cnv 5576 df-co 5577 df-dm 5578 df-rn 5579 df-res 5580 df-ima 5581 df-pred 6178 df-ord 6236 df-on 6237 df-lim 6238 df-suc 6239 df-iota 6358 df-fun 6402 df-fn 6403 df-f 6404 df-f1 6405 df-fo 6406 df-f1o 6407 df-fv 6408 df-isom 6409 df-riota 7191 df-ov 7237 df-oprab 7238 df-mpo 7239 df-of 7490 df-om 7666 df-1st 7782 df-2nd 7783 df-supp 7927 df-tpos 7991 df-wrecs 8070 df-recs 8131 df-rdg 8169 df-1o 8225 df-2o 8226 df-er 8414 df-map 8533 df-pm 8534 df-ixp 8602 df-en 8650 df-dom 8651 df-sdom 8652 df-fin 8653 df-fsupp 9015 df-sup 9087 df-oi 9155 df-card 9584 df-pnf 10898 df-mnf 10899 df-xr 10900 df-ltxr 10901 df-le 10902 df-sub 11093 df-neg 11094 df-div 11519 df-nn 11860 df-2 11922 df-3 11923 df-4 11924 df-5 11925 df-6 11926 df-7 11927 df-8 11928 df-9 11929 df-n0 12120 df-xnn0 12192 df-z 12206 df-dec 12323 df-uz 12468 df-rp 12616 df-fz 13125 df-fzo 13268 df-seq 13606 df-exp 13667 df-hash 13929 df-word 14102 df-lsw 14150 df-concat 14158 df-s1 14185 df-substr 14238 df-pfx 14268 df-splice 14347 df-reverse 14356 df-s2 14445 df-struct 16732 df-sets 16749 df-slot 16767 df-ndx 16777 df-base 16793 df-ress 16817 df-plusg 16847 df-mulr 16848 df-starv 16849 df-sca 16850 df-vsca 16851 df-ip 16852 df-tset 16853 df-ple 16854 df-ds 16856 df-unif 16857 df-hom 16858 df-cco 16859 df-0g 16978 df-gsum 16979 df-prds 16984 df-pws 16986 df-mre 17121 df-mrc 17122 df-acs 17124 df-mgm 18146 df-sgrp 18195 df-mnd 18206 df-mhm 18250 df-submnd 18251 df-efmnd 18328 df-grp 18400 df-minusg 18401 df-sbg 18402 df-mulg 18521 df-subg 18572 df-ghm 18652 df-gim 18695 df-cntz 18743 df-oppg 18770 df-symg 18792 df-pmtr 18866 df-psgn 18915 df-evpm 18916 df-cmn 19204 df-abl 19205 df-mgp 19537 df-ur 19549 df-srg 19553 df-ring 19596 df-cring 19597 df-oppr 19673 df-dvdsr 19691 df-unit 19692 df-invr 19722 df-dvr 19733 df-rnghom 19767 df-drng 19801 df-subrg 19830 df-lmod 19933 df-lss 20001 df-sra 20241 df-rgmod 20242 df-cnfld 20396 df-zring 20468 df-zrh 20502 df-dsmm 20726 df-frlm 20741 df-mamu 21314 df-mat 21336 df-mvmul 21469 df-marepv 21487 df-mdet 21513 |
This theorem is referenced by: cramerimp 21614 |
Copyright terms: Public domain | W3C validator |