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 22964

Description: Lemma 3 for cramerimp 22965: 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 488	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → 𝑅 ∈ CRing)
2		cramerimp.a	. . . . . . . . . 10 ⊢ 𝐴 = (𝑁 Mat 𝑅)
3		cramerimp.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐴)
4	2, 3	matrcl 22688	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
5	4	simpld 500	. . . . . . . 8 ⊢ (𝑋 ∈ 𝐵 → 𝑁 ∈ Fin)
6	5	adantr 486	. . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → 𝑁 ∈ Fin)
7	1, 6	anim12ci 626	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing))
8	7	3adant3 1150	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing))
9		eqid 2760	. . . . . 6 ⊢ (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)
10	2, 9	matmulr 22714	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (._r‘𝐴))
11	8, 10	syl 18	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (._r‘𝐴))
12	11	oveqd 7425	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐸) = (𝑋(._r‘𝐴)𝐸))
13	12	fveq2d 6877	. 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 22963	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐸) = 𝐻)
19	18	fveq2d 6877	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝐷‘(𝑋(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐸)) = (𝐷‘𝐻))
20		simp1l 1216	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑅 ∈ CRing)
21		simp2l 1218	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑋 ∈ 𝐵)
22		crngring 20433	. . . . . . . 8 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
23	22	adantr 486	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → 𝑅 ∈ Ring)
24	23, 6	anim12i 625	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin))
25	24	3adant3 1150	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑅 ∈ Ring ∧ 𝑁 ∈ Fin))
26		ne0i 4286	. . . . . . . 8 ⊢ (𝐼 ∈ 𝑁 → 𝑁 ≠ ∅)
27	22, 26	anim12ci 626	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) → (𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring))
28	2, 3, 14, 17	slesolvec 22958	. . . . . . 7 ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑋 · 𝑍) = 𝑌 → 𝑍 ∈ 𝑉))
29	27, 28	sylan 592	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑋 · 𝑍) = 𝑌 → 𝑍 ∈ 𝑉))
30	29	3impia 1135	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝑍 ∈ 𝑉)
31		simp1r 1217	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝐼 ∈ 𝑁)
32		eqid 2760	. . . . . 6 ⊢ (1_r‘𝐴) = (1_r‘𝐴)
33	2, 3, 14, 32	ma1repvcl 22846	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝑍 ∈ 𝑉 ∧ 𝐼 ∈ 𝑁)) → (((1_r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) ∈ 𝐵)
34	25, 30, 31, 33	syl12anc 850	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (((1_r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) ∈ 𝐵)
35	15, 34	eqeltrid 2864	. . 3 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → 𝐸 ∈ 𝐵)
36		cramerimp.d	. . . 4 ⊢ 𝐷 = (𝑁 maDet 𝑅)
37		cramerimp.t	. . . 4 ⊢ ⊗ = (._r‘𝑅)
38		eqid 2760	. . . 4 ⊢ (._r‘𝐴) = (._r‘𝐴)
39	2, 3, 36, 37, 38	mdetmul 22899	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝐸 ∈ 𝐵) → (𝐷‘(𝑋(._r‘𝐴)𝐸)) = ((𝐷‘𝑋) ⊗ (𝐷‘𝐸)))
40	20, 21, 35, 39	syl3anc 1398	. 2 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝐷‘(𝑋(._r‘𝐴)𝐸)) = ((𝐷‘𝑋) ⊗ (𝐷‘𝐸)))
41	13, 19, 40	3eqtr3rd 2804	1 ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → ((𝐷‘𝑋) ⊗ (𝐷‘𝐸)) = (𝐷‘𝐻))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 Vcvv 3450 ∅c0 4278 ⟨cop 4589 ⟨cotp 4591 ‘cfv 6527 (class class class)co 7408 ↑_m cmap 8825 Fincfn 8951 Basecbs 17348 ._rcmulr 17390 1_rcur 20368 Ringcrg 20420 CRingccrg 20421 maMul cmmul 22666 Mat cmat 22683 maVecMul cmvmul 22816 matRepV cmatrepV 22833 maDet cmdat 22860

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7734 ax-cnex 11227 ax-resscn 11228 ax-1cn 11229 ax-icn 11230 ax-addcl 11231 ax-addrcl 11232 ax-mulcl 11233 ax-mulrcl 11234 ax-mulcom 11235 ax-addass 11236 ax-mulass 11237 ax-distr 11238 ax-i2m1 11239 ax-1ne0 11240 ax-1rid 11241 ax-rnegex 11242 ax-rrecex 11243 ax-cnre 11244 ax-pre-lttri 11245 ax-pre-lttrn 11246 ax-pre-ltadd 11247 ax-pre-mulgt0 11248 ax-addf 11250 ax-mulf 11251

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-xor 1542 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-ot 4592 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-se 5601 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6293 df-ord 6354 df-on 6355 df-lim 6356 df-suc 6357 df-iota 6483 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-isom 6536 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-of 7676 df-om 7861 df-1st 7984 df-2nd 7985 df-supp 8156 df-tpos 8221 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8454 df-2o 8455 df-er 8695 df-map 8827 df-pm 8828 df-ixp 8904 df-en 8952 df-dom 8953 df-sdom 8954 df-fin 8955 df-fsupp 9332 df-sup 9412 df-oi 9482 df-card 9991 df-pnf 11316 df-mnf 11317 df-xr 11318 df-ltxr 11319 df-le 11320 df-sub 11514 df-neg 11515 df-div 11943 df-nn 12305 df-2 12374 df-3 12375 df-4 12376 df-5 12377 df-6 12378 df-7 12379 df-8 12380 df-9 12381 df-n0 12576 df-xnn0 12649 df-z 12663 df-dec 12784 df-uz 12935 df-rp 13090 df-fz 13609 df-fzo 13757 df-seq 14113 df-exp 14173 df-hash 14442 df-word 14626 df-lsw 14675 df-concat 14683 df-s1 14710 df-substr 14756 df-pfx 14788 df-splice 14866 df-reverse 14875 df-s2 14966 df-struct 17286 df-sets 17303 df-slot 17321 df-ndx 17333 df-base 17349 df-ress 17370 df-plusg 17402 df-mulr 17403 df-starv 17404 df-sca 17405 df-vsca 17406 df-ip 17407 df-tset 17408 df-ple 17409 df-ds 17411 df-unif 17412 df-hom 17413 df-cco 17414 df-0g 17573 df-gsum 17574 df-prds 17579 df-pws 17581 df-mre 17717 df-mrc 17718 df-acs 17720 df-mgm 18777 df-sgrp 18869 df-mnd 18885 df-mhm 18939 df-submnd 18940 df-efmnd 19026 df-grp 19108 df-minusg 19109 df-sbg 19110 df-mulg 19239 df-subg 19294 df-ghm 19389 df-gim 19434 df-cntz 19492 df-oppg 19521 df-symg 19545 df-pmtr 19617 df-psgn 19666 df-evpm 19667 df-cmn 19957 df-abl 19958 df-mgp 20322 df-rng 20336 df-ur 20369 df-srg 20374 df-ring 20422 df-cring 20423 df-oppr 20528 df-dvdsr 20548 df-unit 20549 df-invr 20579 df-dvr 20592 df-rhm 20663 df-subrng 20759 df-subrg 20783 df-drng 20943 df-lmod 21098 df-lss 21168 df-sra 21409 df-rgmod 21410 df-cnfld 21640 df-zring 21714 df-zrh 21770 df-dsmm 21999 df-frlm 22014 df-mamu 22667 df-mat 22684 df-mvmul 22817 df-marepv 22835 df-mdet 22861

This theorem is used by: cramerimp 22965

W3C validator