cramerimplem3 - Metamath Proof Explorer

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

Theorem cramerimplem3 22650

Description: Lemma 3 for cramerimp 22651: 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	⊢ 𝐸 = (((1_r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼)
cramerimp.h	⊢ 𝐻 = ((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝐼)
cramerimp.x	⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)
cramerimp.d	⊢ 𝐷 = (𝑁 maDet 𝑅)
cramerimp.t	⊢ ⊗ = (._r‘𝑅)

**Assertion**
Ref	Expression
cramerimplem3	⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → ((𝐷‘𝑋) ⊗ (𝐷‘𝐸)) = (𝐷‘𝐻))

**Proof of Theorem cramerimplem3**
Step	Hyp	Ref	Expression
1		simpl 482	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → 𝑅 ∈ CRing)
2		cramerimp.a	. . . . . . . . . 10 ⊢ 𝐴 = (𝑁 Mat 𝑅)
3		cramerimp.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐴)
4	2, 3	matrcl 22377	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
5	4	simpld 494	. . . . . . . 8 ⊢ (𝑋 ∈ 𝐵 → 𝑁 ∈ Fin)
6	5	adantr 480	. . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → 𝑁 ∈ Fin)
7	1, 6	anim12ci 615	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing))
8	7	3adant3 1133	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing))
9		eqid 2737	. . . . . 6 ⊢ (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)
10	2, 9	matmulr 22403	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (._r‘𝐴))
11	8, 10	syl 17	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (._r‘𝐴))
12	11	oveqd 7384	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐸) = (𝑋(._r‘𝐴)𝐸))
13	12	fveq2d 6845	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝐷‘(𝑋(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐸)) = (𝐷‘(𝑋(._r‘𝐴)𝐸)))
14		cramerimp.v	. . . 4 ⊢ 𝑉 = ((Base‘𝑅) ↑_m 𝑁)
15		cramerimp.e	. . . 4 ⊢ 𝐸 = (((1_r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼)
16		cramerimp.h	. . . 4 ⊢ 𝐻 = ((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝐼)
17		cramerimp.x	. . . 4 ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)
18	2, 3, 14, 15, 16, 17, 9	cramerimplem2 22649	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐸) = 𝐻)
19	18	fveq2d 6845	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝐷‘(𝑋(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐸)) = (𝐷‘𝐻))
20		simp1l 1199	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑅 ∈ CRing)
21		simp2l 1201	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑋 ∈ 𝐵)
22		crngring 20226	. . . . . . . 8 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
23	22	adantr 480	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → 𝑅 ∈ Ring)
24	23, 6	anim12i 614	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin))
25	24	3adant3 1133	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin))
26		ne0i 4282	. . . . . . . 8 ⊢ (𝐼 ∈ 𝑁 → 𝑁 ≠ ∅)
27	22, 26	anim12ci 615	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → (𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring))
28	2, 3, 14, 17	slesolvec 22644	. . . . . . 7 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑋 · 𝑍) = 𝑌 → 𝑍 ∈ 𝑉))
29	27, 28	sylan 581	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑋 · 𝑍) = 𝑌 → 𝑍 ∈ 𝑉))
30	29	3impia 1118	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑍 ∈ 𝑉)
31		simp1r 1200	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝐼 ∈ 𝑁)
32		eqid 2737	. . . . . 6 ⊢ (1_r‘𝐴) = (1_r‘𝐴)
33	2, 3, 14, 32	ma1repvcl 22535	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁)) → (((1_r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) ∈ 𝐵)
34	25, 30, 31, 33	syl12anc 837	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (((1_r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) ∈ 𝐵)
35	15, 34	eqeltrid 2841	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝐸 ∈ 𝐵)
36		cramerimp.d	. . . 4 ⊢ 𝐷 = (𝑁 maDet 𝑅)
37		cramerimp.t	. . . 4 ⊢ ⊗ = (._r‘𝑅)
38		eqid 2737	. . . 4 ⊢ (._r‘𝐴) = (._r‘𝐴)
39	2, 3, 36, 37, 38	mdetmul 22588	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝐸 ∈ 𝐵) → (𝐷‘(𝑋(._r‘𝐴)𝐸)) = ((𝐷‘𝑋) ⊗ (𝐷‘𝐸)))
40	20, 21, 35, 39	syl3anc 1374	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝐷‘(𝑋(._r‘𝐴)𝐸)) = ((𝐷‘𝑋) ⊗ (𝐷‘𝐸)))
41	13, 19, 40	3eqtr3rd 2781	1 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → ((𝐷‘𝑋) ⊗ (𝐷‘𝐸)) = (𝐷‘𝐻))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 Vcvv 3430 ∅c0 4274 ⟨cop 4574 ⟨cotp 4576 ‘cfv 6499 (class class class)co 7367 ↑_m cmap 8773 Fincfn 8893 Basecbs 17179 ._rcmulr 17221 1_rcur 20162 Ringcrg 20214 CRingccrg 20215 maMul cmmul 22355 Mat cmat 22372 maVecMul cmvmul 22505 matRepV cmatrepV 22522 maDet cmdat 22549

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5308 ax-pr 5376 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-addf 11117 ax-mulf 11118

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-xor 1514 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-ot 4577 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6266 df-ord 6327 df-on 6328 df-lim 6329 df-suc 6330 df-iota 6455 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-of 7631 df-om 7818 df-1st 7942 df-2nd 7943 df-supp 8111 df-tpos 8176 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-2o 8406 df-er 8643 df-map 8775 df-pm 8776 df-ixp 8846 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-fsupp 9275 df-sup 9355 df-oi 9425 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-2 12244 df-3 12245 df-4 12246 df-5 12247 df-6 12248 df-7 12249 df-8 12250 df-9 12251 df-n0 12438 df-xnn0 12511 df-z 12525 df-dec 12645 df-uz 12789 df-rp 12943 df-fz 13462 df-fzo 13609 df-seq 13964 df-exp 14024 df-hash 14293 df-word 14476 df-lsw 14525 df-concat 14533 df-s1 14559 df-substr 14604 df-pfx 14634 df-splice 14712 df-reverse 14721 df-s2 14810 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-hom 17244 df-cco 17245 df-0g 17404 df-gsum 17405 df-prds 17410 df-pws 17412 df-mre 17548 df-mrc 17549 df-acs 17551 df-mgm 18608 df-sgrp 18687 df-mnd 18703 df-mhm 18751 df-submnd 18752 df-efmnd 18837 df-grp 18912 df-minusg 18913 df-sbg 18914 df-mulg 19044 df-subg 19099 df-ghm 19188 df-gim 19234 df-cntz 19292 df-oppg 19321 df-symg 19345 df-pmtr 19417 df-psgn 19466 df-evpm 19467 df-cmn 19757 df-abl 19758 df-mgp 20122 df-rng 20134 df-ur 20163 df-srg 20168 df-ring 20216 df-cring 20217 df-oppr 20317 df-dvdsr 20337 df-unit 20338 df-invr 20368 df-dvr 20381 df-rhm 20452 df-subrng 20523 df-subrg 20547 df-drng 20708 df-lmod 20857 df-lss 20927 df-sra 21168 df-rgmod 21169 df-cnfld 21353 df-zring 21427 df-zrh 21483 df-dsmm 21712 df-frlm 21727 df-mamu 22356 df-mat 22373 df-mvmul 22506 df-marepv 22524 df-mdet 22550

This theorem is referenced by: cramerimp 22651

W3C validator