MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cramerimplem3 Structured version   Visualization version   GIF version

Theorem cramerimplem3 21613
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.)
Hypotheses
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𝑅)
Assertion
Ref Expression
cramerimplem3 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → ((𝐷𝑋) (𝐷𝐸)) = (𝐷𝐻))

Proof of Theorem cramerimplem3
StepHypRef Expression
1 simpl 486 . . . . . . 7 ((𝑅 ∈ CRing ∧ 𝐼𝑁) → 𝑅 ∈ CRing)
2 cramerimp.a . . . . . . . . . 10 𝐴 = (𝑁 Mat 𝑅)
3 cramerimp.b . . . . . . . . . 10 𝐵 = (Base‘𝐴)
42, 3matrcl 21340 . . . . . . . . 9 (𝑋𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
54simpld 498 . . . . . . . 8 (𝑋𝐵𝑁 ∈ Fin)
65adantr 484 . . . . . . 7 ((𝑋𝐵𝑌𝑉) → 𝑁 ∈ Fin)
71, 6anim12ci 617 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing))
873adant3 1134 . . . . 5 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing))
9 eqid 2739 . . . . . 6 (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)
102, 9matmulr 21366 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (.r𝐴))
118, 10syl 17 . . . 4 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (.r𝐴))
1211oveqd 7251 . . 3 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐸) = (𝑋(.r𝐴)𝐸))
1312fveq2d 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 ⟨𝑁, 𝑁⟩)
182, 3, 14, 15, 16, 17, 9cramerimplem2 21612 . . 3 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐸) = 𝐻)
1918fveq2d 6742 . 2 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝐷‘(𝑋(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐸)) = (𝐷𝐻))
20 simp1l 1199 . . 3 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑅 ∈ CRing)
21 simp2l 1201 . . 3 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑋𝐵)
22 crngring 19606 . . . . . . . 8 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
2322adantr 484 . . . . . . 7 ((𝑅 ∈ CRing ∧ 𝐼𝑁) → 𝑅 ∈ Ring)
2423, 6anim12i 616 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉)) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin))
25243adant3 1134 . . . . 5 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin))
26 ne0i 4265 . . . . . . . 8 (𝐼𝑁𝑁 ≠ ∅)
2722, 26anim12ci 617 . . . . . . 7 ((𝑅 ∈ CRing ∧ 𝐼𝑁) → (𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring))
282, 3, 14, 17slesolvec 21607 . . . . . . 7 (((𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) ∧ (𝑋𝐵𝑌𝑉)) → ((𝑋 · 𝑍) = 𝑌𝑍𝑉))
2927, 28sylan 583 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉)) → ((𝑋 · 𝑍) = 𝑌𝑍𝑉))
30293impia 1119 . . . . 5 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑍𝑉)
31 simp1r 1200 . . . . 5 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝐼𝑁)
32 eqid 2739 . . . . . 6 (1r𝐴) = (1r𝐴)
332, 3, 14, 32ma1repvcl 21498 . . . . 5 (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝑍𝑉𝐼𝑁)) → (((1r𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) ∈ 𝐵)
3425, 30, 31, 33syl12anc 837 . . . 4 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (((1r𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) ∈ 𝐵)
3515, 34eqeltrid 2844 . . 3 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝐸𝐵)
36 cramerimp.d . . . 4 𝐷 = (𝑁 maDet 𝑅)
37 cramerimp.t . . . 4 = (.r𝑅)
38 eqid 2739 . . . 4 (.r𝐴) = (.r𝐴)
392, 3, 36, 37, 38mdetmul 21551 . . 3 ((𝑅 ∈ CRing ∧ 𝑋𝐵𝐸𝐵) → (𝐷‘(𝑋(.r𝐴)𝐸)) = ((𝐷𝑋) (𝐷𝐸)))
4020, 21, 35, 39syl3anc 1373 . 2 (((𝑅 ∈ CRing ∧ 𝐼𝑁) ∧ (𝑋𝐵𝑌𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝐷‘(𝑋(.r𝐴)𝐸)) = ((𝐷𝑋) (𝐷𝐸)))
4113, 19, 403eqtr3rd 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