mdetero - Metamath Proof Explorer

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

Theorem mdetero 21311

Description: The determinant function is multilinear (additive and homogeneous for each row (matrices are given explicitly by their entries). Corollary 4.9 in [Lang] p. 515. (Contributed by SO, 16-Jul-2018.)

**Hypotheses**
Ref	Expression
mdetero.d	⊢ 𝐷 = (𝑁 maDet 𝑅)
mdetero.k	⊢ 𝐾 = (Base‘𝑅)
mdetero.p	⊢ + = (+_g‘𝑅)
mdetero.t	⊢ · = (._r‘𝑅)
mdetero.r	⊢ (𝜑 → 𝑅 ∈ CRing)
mdetero.n	⊢ (𝜑 → 𝑁 ∈ Fin)
mdetero.x	⊢ ((𝜑 ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐾)
mdetero.y	⊢ ((𝜑 ∧ 𝑗 ∈ 𝑁) → 𝑌 ∈ 𝐾)
mdetero.z	⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑍 ∈ 𝐾)
mdetero.w	⊢ (𝜑 → 𝑊 ∈ 𝐾)
mdetero.i	⊢ (𝜑 → 𝐼 ∈ 𝑁)
mdetero.j	⊢ (𝜑 → 𝐽 ∈ 𝑁)
mdetero.ij	⊢ (𝜑 → 𝐼 ≠ 𝐽)

**Assertion**
Ref	Expression
mdetero	⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + (𝑊 · 𝑌)), if(𝑖 = 𝐽, 𝑌, 𝑍)))) = (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑌, 𝑍)))))

Distinct variable groups: 𝜑,𝑖,𝑗 𝑖,𝐾,𝑗 𝑖,𝑁,𝑗 𝑖,𝐼,𝑗 𝑖,𝐽,𝑗 𝑖,𝑋 𝑖,𝑌 𝑖,𝑊,𝑗 · ,𝑖,𝑗 + ,𝑖,𝑗 Allowed substitution hints: 𝐷(𝑖,𝑗) 𝑅(𝑖,𝑗) 𝑋(𝑗) 𝑌(𝑗) 𝑍(𝑖,𝑗)

**Proof of Theorem mdetero**
Step	Hyp	Ref	Expression
1		mdetero.d	. . 3 ⊢ 𝐷 = (𝑁 maDet 𝑅)
2		mdetero.k	. . 3 ⊢ 𝐾 = (Base‘𝑅)
3		mdetero.p	. . 3 ⊢ + = (+_g‘𝑅)
4		mdetero.r	. . 3 ⊢ (𝜑 → 𝑅 ∈ CRing)
5		mdetero.n	. . 3 ⊢ (𝜑 → 𝑁 ∈ Fin)
6		mdetero.x	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐾)
7	6	3adant2 1129	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐾)
8		crngring 19378	. . . . . 6 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
9	4, 8	syl 17	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Ring)
10	9	3ad2ant1 1131	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring)
11		mdetero.w	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ 𝐾)
12	11	3ad2ant1 1131	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑊 ∈ 𝐾)
13		mdetero.y	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑁) → 𝑌 ∈ 𝐾)
14	13	3adant2 1129	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑌 ∈ 𝐾)
15		mdetero.t	. . . . 5 ⊢ · = (._r‘𝑅)
16	2, 15	ringcl 19383	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑊 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾) → (𝑊 · 𝑌) ∈ 𝐾)
17	10, 12, 14, 16	syl3anc 1369	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑊 · 𝑌) ∈ 𝐾)
18		mdetero.z	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑍 ∈ 𝐾)
19	14, 18	ifcld 4467	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → if(𝑖 = 𝐽, 𝑌, 𝑍) ∈ 𝐾)
20		mdetero.i	. . 3 ⊢ (𝜑 → 𝐼 ∈ 𝑁)
21	1, 2, 3, 4, 5, 7, 17, 19, 20	mdetrlin2 21308	. 2 ⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + (𝑊 · 𝑌)), if(𝑖 = 𝐽, 𝑌, 𝑍)))) = ((𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑌, 𝑍)))) + (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑊 · 𝑌), if(𝑖 = 𝐽, 𝑌, 𝑍))))))
22	1, 2, 15, 4, 5, 14, 19, 11, 20	mdetrsca2 21305	. . . 4 ⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑊 · 𝑌), if(𝑖 = 𝐽, 𝑌, 𝑍)))) = (𝑊 · (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, if(𝑖 = 𝐽, 𝑌, 𝑍))))))
23		eqid 2759	. . . . . 6 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
24		mdetero.j	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ 𝑁)
25		mdetero.ij	. . . . . 6 ⊢ (𝜑 → 𝐼 ≠ 𝐽)
26	1, 2, 23, 4, 5, 13, 18, 20, 24, 25	mdetralt2 21310	. . . . 5 ⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, if(𝑖 = 𝐽, 𝑌, 𝑍)))) = (0_g‘𝑅))
27	26	oveq2d 7167	. . . 4 ⊢ (𝜑 → (𝑊 · (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, if(𝑖 = 𝐽, 𝑌, 𝑍))))) = (𝑊 · (0_g‘𝑅)))
28	2, 15, 23	ringrz 19410	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑊 ∈ 𝐾) → (𝑊 · (0_g‘𝑅)) = (0_g‘𝑅))
29	9, 11, 28	syl2anc 588	. . . 4 ⊢ (𝜑 → (𝑊 · (0_g‘𝑅)) = (0_g‘𝑅))
30	22, 27, 29	3eqtrd 2798	. . 3 ⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑊 · 𝑌), if(𝑖 = 𝐽, 𝑌, 𝑍)))) = (0_g‘𝑅))
31	30	oveq2d 7167	. 2 ⊢ (𝜑 → ((𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑌, 𝑍)))) + (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑊 · 𝑌), if(𝑖 = 𝐽, 𝑌, 𝑍))))) = ((𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑌, 𝑍)))) + (0_g‘𝑅)))
32		ringgrp 19371	. . . 4 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
33	9, 32	syl 17	. . 3 ⊢ (𝜑 → 𝑅 ∈ Grp)
34		eqid 2759	. . . . . 6 ⊢ (𝑁 Mat 𝑅) = (𝑁 Mat 𝑅)
35		eqid 2759	. . . . . 6 ⊢ (Base‘(𝑁 Mat 𝑅)) = (Base‘(𝑁 Mat 𝑅))
36	1, 34, 35, 2	mdetf 21296	. . . . 5 ⊢ (𝑅 ∈ CRing → 𝐷:(Base‘(𝑁 Mat 𝑅))⟶𝐾)
37	4, 36	syl 17	. . . 4 ⊢ (𝜑 → 𝐷:(Base‘(𝑁 Mat 𝑅))⟶𝐾)
38	7, 19	ifcld 4467	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑌, 𝑍)) ∈ 𝐾)
39	34, 2, 35, 5, 4, 38	matbas2d 21124	. . . 4 ⊢ (𝜑 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑌, 𝑍))) ∈ (Base‘(𝑁 Mat 𝑅)))
40	37, 39	ffvelrnd 6844	. . 3 ⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑌, 𝑍)))) ∈ 𝐾)
41	2, 3, 23	grprid 18202	. . 3 ⊢ ((𝑅 ∈ Grp ∧ (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑌, 𝑍)))) ∈ 𝐾) → ((𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑌, 𝑍)))) + (0_g‘𝑅)) = (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑌, 𝑍)))))
42	33, 40, 41	syl2anc 588	. 2 ⊢ (𝜑 → ((𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑌, 𝑍)))) + (0_g‘𝑅)) = (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑌, 𝑍)))))
43	21, 31, 42	3eqtrd 2798	1 ⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + (𝑊 · 𝑌)), if(𝑖 = 𝐽, 𝑌, 𝑍)))) = (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑌, 𝑍)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 ∧ w3a 1085 = wceq 1539 ∈ wcel 2112 ≠ wne 2952 ifcif 4421 ⟶wf 6332 ‘cfv 6336 (class class class)co 7151 ∈ cmpo 7153 Fincfn 8528 Basecbs 16542 +_gcplusg 16624 ._rcmulr 16625 0_gc0g 16772 Grpcgrp 18170 Ringcrg 19366 CRingccrg 19367 Mat cmat 21108 maDet cmdat 21285

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-rep 5157 ax-sep 5170 ax-nul 5177 ax-pow 5235 ax-pr 5299 ax-un 7460 ax-cnex 10632 ax-resscn 10633 ax-1cn 10634 ax-icn 10635 ax-addcl 10636 ax-addrcl 10637 ax-mulcl 10638 ax-mulrcl 10639 ax-mulcom 10640 ax-addass 10641 ax-mulass 10642 ax-distr 10643 ax-i2m1 10644 ax-1ne0 10645 ax-1rid 10646 ax-rnegex 10647 ax-rrecex 10648 ax-cnre 10649 ax-pre-lttri 10650 ax-pre-lttrn 10651 ax-pre-ltadd 10652 ax-pre-mulgt0 10653 ax-addf 10655 ax-mulf 10656

This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3or 1086 df-3an 1087 df-xor 1504 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2902 df-ne 2953 df-nel 3057 df-ral 3076 df-rex 3077 df-reu 3078 df-rmo 3079 df-rab 3080 df-v 3412 df-sbc 3698 df-csb 3807 df-dif 3862 df-un 3864 df-in 3866 df-ss 3876 df-pss 3878 df-nul 4227 df-if 4422 df-pw 4497 df-sn 4524 df-pr 4526 df-tp 4528 df-op 4530 df-ot 4532 df-uni 4800 df-int 4840 df-iun 4886 df-iin 4887 df-br 5034 df-opab 5096 df-mpt 5114 df-tr 5140 df-id 5431 df-eprel 5436 df-po 5444 df-so 5445 df-fr 5484 df-se 5485 df-we 5486 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-pred 6127 df-ord 6173 df-on 6174 df-lim 6175 df-suc 6176 df-iota 6295 df-fun 6338 df-fn 6339 df-f 6340 df-f1 6341 df-fo 6342 df-f1o 6343 df-fv 6344 df-isom 6345 df-riota 7109 df-ov 7154 df-oprab 7155 df-mpo 7156 df-of 7406 df-om 7581 df-1st 7694 df-2nd 7695 df-supp 7837 df-tpos 7903 df-wrecs 7958 df-recs 8019 df-rdg 8057 df-1o 8113 df-2o 8114 df-er 8300 df-map 8419 df-pm 8420 df-ixp 8481 df-en 8529 df-dom 8530 df-sdom 8531 df-fin 8532 df-fsupp 8868 df-sup 8940 df-oi 9008 df-card 9402 df-pnf 10716 df-mnf 10717 df-xr 10718 df-ltxr 10719 df-le 10720 df-sub 10911 df-neg 10912 df-div 11337 df-nn 11676 df-2 11738 df-3 11739 df-4 11740 df-5 11741 df-6 11742 df-7 11743 df-8 11744 df-9 11745 df-n0 11936 df-xnn0 12008 df-z 12022 df-dec 12139 df-uz 12284 df-rp 12432 df-fz 12941 df-fzo 13084 df-seq 13420 df-exp 13481 df-hash 13742 df-word 13915 df-lsw 13963 df-concat 13971 df-s1 13998 df-substr 14051 df-pfx 14081 df-splice 14160 df-reverse 14169 df-s2 14258 df-struct 16544 df-ndx 16545 df-slot 16546 df-base 16548 df-sets 16549 df-ress 16550 df-plusg 16637 df-mulr 16638 df-starv 16639 df-sca 16640 df-vsca 16641 df-ip 16642 df-tset 16643 df-ple 16644 df-ds 16646 df-unif 16647 df-hom 16648 df-cco 16649 df-0g 16774 df-gsum 16775 df-prds 16780 df-pws 16782 df-mre 16916 df-mrc 16917 df-acs 16919 df-mgm 17919 df-sgrp 17968 df-mnd 17979 df-mhm 18023 df-submnd 18024 df-efmnd 18101 df-grp 18173 df-minusg 18174 df-mulg 18293 df-subg 18344 df-ghm 18424 df-gim 18467 df-cntz 18515 df-oppg 18542 df-symg 18564 df-pmtr 18638 df-psgn 18687 df-evpm 18688 df-cmn 18976 df-abl 18977 df-mgp 19309 df-ur 19321 df-ring 19368 df-cring 19369 df-oppr 19445 df-dvdsr 19463 df-unit 19464 df-invr 19494 df-dvr 19505 df-rnghom 19539 df-drng 19573 df-subrg 19602 df-sra 20013 df-rgmod 20014 df-cnfld 20168 df-zring 20240 df-zrh 20274 df-dsmm 20498 df-frlm 20513 df-mat 21109 df-mdet 21286

This theorem is referenced by: maducoeval2 21341 matunitlindflem1 35334

W3C validator