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 22821

Description: Lemma 3 for cramerimp 22822: 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 487	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → 𝑅 ∈ CRing)
2		cramerimp.a	. . . . . . . . . 10 ⊢ 𝐴 = (𝑁 Mat 𝑅)
3		cramerimp.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐴)
4	2, 3	matrcl 22548	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
5	4	simpld 499	. . . . . . . 8 ⊢ (𝑋 ∈ 𝐵 → 𝑁 ∈ Fin)
6	5	adantr 485	. . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → 𝑁 ∈ Fin)
7	1, 6	anim12ci 625	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing))
8	7	3adant3 1148	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing))
9		eqid 2761	. . . . . 6 ⊢ (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)
10	2, 9	matmulr 22574	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (._r‘𝐴))
11	8, 10	syl 18	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (._r‘𝐴))
12	11	oveqd 7427	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐸) = (𝑋(._r‘𝐴)𝐸))
13	12	fveq2d 6885	. 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 22820	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐸) = 𝐻)
19	18	fveq2d 6885	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝐷‘(𝑋(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐸)) = (𝐷‘𝐻))
20		simp1l 1214	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑅 ∈ CRing)
21		simp2l 1216	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑋 ∈ 𝐵)
22		crngring 20326	. . . . . . . 8 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
23	22	adantr 485	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → 𝑅 ∈ Ring)
24	23, 6	anim12i 624	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin))
25	24	3adant3 1148	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin))
26		ne0i 4293	. . . . . . . 8 ⊢ (𝐼 ∈ 𝑁 → 𝑁 ≠ ∅)
27	22, 26	anim12ci 625	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → (𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring))
28	2, 3, 14, 17	slesolvec 22815	. . . . . . 7 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑋 · 𝑍) = 𝑌 → 𝑍 ∈ 𝑉))
29	27, 28	sylan 591	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑋 · 𝑍) = 𝑌 → 𝑍 ∈ 𝑉))
30	29	3impia 1133	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑍 ∈ 𝑉)
31		simp1r 1215	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝐼 ∈ 𝑁)
32		eqid 2761	. . . . . 6 ⊢ (1_r‘𝐴) = (1_r‘𝐴)
33	2, 3, 14, 32	ma1repvcl 22706	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁)) → (((1_r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) ∈ 𝐵)
34	25, 30, 31, 33	syl12anc 849	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (((1_r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) ∈ 𝐵)
35	15, 34	eqeltrid 2865	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝐸 ∈ 𝐵)
36		cramerimp.d	. . . 4 ⊢ 𝐷 = (𝑁 maDet 𝑅)
37		cramerimp.t	. . . 4 ⊢ ⊗ = (._r‘𝑅)
38		eqid 2761	. . . 4 ⊢ (._r‘𝐴) = (._r‘𝐴)
39	2, 3, 36, 37, 38	mdetmul 22759	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝐸 ∈ 𝐵) → (𝐷‘(𝑋(._r‘𝐴)𝐸)) = ((𝐷‘𝑋) ⊗ (𝐷‘𝐸)))
40	20, 21, 35, 39	syl3anc 1396	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝐷‘(𝑋(._r‘𝐴)𝐸)) = ((𝐷‘𝑋) ⊗ (𝐷‘𝐸)))
41	13, 19, 40	3eqtr3rd 2805	1 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → ((𝐷‘𝑋) ⊗ (𝐷‘𝐸)) = (𝐷‘𝐻))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 ∧ w3a 1101 = wceq 1568 ∈ wcel 2141 ≠ wne 2956 Vcvv 3453 ∅c0 4285 ⟨cop 4594 ⟨cotp 4596 ‘cfv 6536 (class class class)co 7410 ↑_m cmap 8823 Fincfn 8942 Basecbs 17268 ._rcmulr 17310 1_rcur 20262 Ringcrg 20314 CRingccrg 20315 maMul cmmul 22526 Mat cmat 22543 maVecMul cmvmul 22676 matRepV cmatrepV 22693 maDet cmdat 22720

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176 ax-addf 11178 ax-mulf 11179

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-xor 1540 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-ot 4597 df-uni 4872 df-int 4912 df-iun 4957 df-iin 4958 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-om 7862 df-1st 7985 df-2nd 7986 df-supp 8156 df-tpos 8221 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-er 8693 df-map 8825 df-pm 8826 df-ixp 8895 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-fsupp 9321 df-sup 9401 df-oi 9471 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-div 11871 df-nn 12233 df-2 12302 df-3 12303 df-4 12304 df-5 12305 df-6 12306 df-7 12307 df-8 12308 df-9 12309 df-n0 12504 df-xnn0 12577 df-z 12591 df-dec 12711 df-uz 12862 df-rp 13016 df-fz 13535 df-fzo 13682 df-seq 14037 df-exp 14097 df-hash 14366 df-word 14550 df-lsw 14599 df-concat 14607 df-s1 14633 df-substr 14678 df-pfx 14708 df-splice 14786 df-reverse 14795 df-s2 14884 df-struct 17206 df-sets 17223 df-slot 17241 df-ndx 17253 df-base 17269 df-ress 17290 df-plusg 17322 df-mulr 17323 df-starv 17324 df-sca 17325 df-vsca 17326 df-ip 17327 df-tset 17328 df-ple 17329 df-ds 17331 df-unif 17332 df-hom 17333 df-cco 17334 df-0g 17493 df-gsum 17494 df-prds 17499 df-pws 17501 df-mre 17637 df-mrc 17638 df-acs 17640 df-mgm 18697 df-sgrp 18776 df-mnd 18792 df-mhm 18840 df-submnd 18841 df-efmnd 18927 df-grp 19002 df-minusg 19003 df-sbg 19004 df-mulg 19133 df-subg 19188 df-ghm 19283 df-gim 19328 df-cntz 19386 df-oppg 19415 df-symg 19439 df-pmtr 19511 df-psgn 19560 df-evpm 19561 df-cmn 19851 df-abl 19852 df-mgp 20216 df-rng 20230 df-ur 20263 df-srg 20268 df-ring 20316 df-cring 20317 df-oppr 20418 df-dvdsr 20438 df-unit 20439 df-invr 20469 df-dvr 20482 df-rhm 20553 df-subrng 20630 df-subrg 20654 df-drng 20814 df-lmod 20962 df-lss 21032 df-sra 21273 df-rgmod 21274 df-cnfld 21502 df-zring 21576 df-zrh 21632 df-dsmm 21861 df-frlm 21876 df-mamu 22527 df-mat 22544 df-mvmul 22677 df-marepv 22695 df-mdet 22721

This theorem is referenced by: cramerimp 22822

W3C validator