mdetf - Metamath Proof Explorer

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

Theorem mdetf 20724

Description: Functionality of the determinant, see also definition in [Lang] p. 513. (Contributed by Stefan O'Rear, 9-Jul-2018.) (Proof shortened by AV, 23-Jul-2019.)

**Hypotheses**
Ref	Expression
mdetf.d	⊢ 𝐷 = (𝑁 maDet 𝑅)
mdetf.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
mdetf.b	⊢ 𝐵 = (Base‘𝐴)
mdetf.k	⊢ 𝐾 = (Base‘𝑅)

**Assertion**
Ref	Expression
mdetf	⊢ (𝑅 ∈ CRing → 𝐷:𝐵⟶𝐾)

Proof of Theorem mdetf Dummy variables 𝑝 𝑐 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mdetf.k	. . 3 ⊢ 𝐾 = (Base‘𝑅)
2		crngring 18871	. . . . 5 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
3	2	adantr 473	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → 𝑅 ∈ Ring)
4		ringcmn 18894	. . . 4 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
5	3, 4	syl 17	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → 𝑅 ∈ CMnd)
6		mdetf.a	. . . . . . 7 ⊢ 𝐴 = (𝑁 Mat 𝑅)
7		mdetf.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐴)
8	6, 7	matrcl 20540	. . . . . 6 ⊢ (𝑚 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
9	8	adantl 474	. . . . 5 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
10	9	simpld 489	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → 𝑁 ∈ Fin)
11		eqid 2797	. . . . 5 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
12		eqid 2797	. . . . 5 ⊢ (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
13	11, 12	symgbasfi 18115	. . . 4 ⊢ (𝑁 ∈ Fin → (Base‘(SymGrp‘𝑁)) ∈ Fin)
14	10, 13	syl 17	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → (Base‘(SymGrp‘𝑁)) ∈ Fin)
15	2	ad2antrr 718	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring)
16		zrhpsgnmhm 20248	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
17	3, 10, 16	syl2anc 580	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
18		eqid 2797	. . . . . . . . 9 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
19	18, 1	mgpbas 18808	. . . . . . . 8 ⊢ 𝐾 = (Base‘(mulGrp‘𝑅))
20	12, 19	mhmf 17652	. . . . . . 7 ⊢ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾)
21	17, 20	syl 17	. . . . . 6 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾)
22	21	ffvelrnda 6583	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾)
23	18	crngmgp 18868	. . . . . . 7 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
24	23	ad2antrr 718	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd)
25	10	adantr 473	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 ∈ Fin)
26	6, 1, 7	matbas2i 20550	. . . . . . . . . 10 ⊢ (𝑚 ∈ 𝐵 → 𝑚 ∈ (𝐾 ↑_𝑚 (𝑁 × 𝑁)))
27	26	ad3antlr 723	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑚 ∈ (𝐾 ↑_𝑚 (𝑁 × 𝑁)))
28		elmapi 8115	. . . . . . . . 9 ⊢ (𝑚 ∈ (𝐾 ↑_𝑚 (𝑁 × 𝑁)) → 𝑚:(𝑁 × 𝑁)⟶𝐾)
29	27, 28	syl 17	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑚:(𝑁 × 𝑁)⟶𝐾)
30	11, 12	symgbasf 18113	. . . . . . . . . 10 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) → 𝑝:𝑁⟶𝑁)
31	30	adantl 474	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁⟶𝑁)
32	31	ffvelrnda 6583	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → (𝑝‘𝑐) ∈ 𝑁)
33		simpr 478	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑐 ∈ 𝑁)
34	29, 32, 33	fovrnd 7038	. . . . . . 7 ⊢ ((((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐)𝑚𝑐) ∈ 𝐾)
35	34	ralrimiva 3145	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑐 ∈ 𝑁 ((𝑝‘𝑐)𝑚𝑐) ∈ 𝐾)
36	19, 24, 25, 35	gsummptcl 18678	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σ_g (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑚𝑐))) ∈ 𝐾)
37		eqid 2797	. . . . . 6 ⊢ (._r‘𝑅) = (._r‘𝑅)
38	1, 37	ringcl 18874	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σ_g (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑚𝑐))) ∈ 𝐾) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑚𝑐)))) ∈ 𝐾)
39	15, 22, 36, 38	syl3anc 1491	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑚𝑐)))) ∈ 𝐾)
40	39	ralrimiva 3145	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → ∀𝑝 ∈ (Base‘(SymGrp‘𝑁))((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑚𝑐)))) ∈ 𝐾)
41	1, 5, 14, 40	gsummptcl 18678	. 2 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → (𝑅 Σ_g (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑚𝑐)))))) ∈ 𝐾)
42		mdetf.d	. . 3 ⊢ 𝐷 = (𝑁 maDet 𝑅)
43		eqid 2797	. . 3 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
44		eqid 2797	. . 3 ⊢ (pmSgn‘𝑁) = (pmSgn‘𝑁)
45	42, 6, 7, 12, 43, 44, 37, 18	mdetfval 20715	. 2 ⊢ 𝐷 = (𝑚 ∈ 𝐵 ↦ (𝑅 Σ_g (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(._r‘𝑅)((mulGrp‘𝑅) Σ_g (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑚𝑐)))))))
46	41, 45	fmptd 6608	1 ⊢ (𝑅 ∈ CRing → 𝐷:𝐵⟶𝐾)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 Vcvv 3383 ↦ cmpt 4920 × cxp 5308 ∘ ccom 5314 ⟶wf 6095 ‘cfv 6099 (class class class)co 6876 ↑_𝑚 cmap 8093 Fincfn 8193 Basecbs 16181 ._rcmulr 16265 Σ_g cgsu 16413 MndHom cmhm 17645 SymGrpcsymg 18106 pmSgncpsgn 18218 CMndccmn 18505 mulGrpcmgp 18802 Ringcrg 18860 CRingccrg 18861 ℤRHomczrh 20167 Mat cmat 20535 maDet cmdat 20713

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 ax-rep 4962 ax-sep 4973 ax-nul 4981 ax-pow 5033 ax-pr 5095 ax-un 7181 ax-inf2 8786 ax-cnex 10278 ax-resscn 10279 ax-1cn 10280 ax-icn 10281 ax-addcl 10282 ax-addrcl 10283 ax-mulcl 10284 ax-mulrcl 10285 ax-mulcom 10286 ax-addass 10287 ax-mulass 10288 ax-distr 10289 ax-i2m1 10290 ax-1ne0 10291 ax-1rid 10292 ax-rnegex 10293 ax-rrecex 10294 ax-cnre 10295 ax-pre-lttri 10296 ax-pre-lttrn 10297 ax-pre-ltadd 10298 ax-pre-mulgt0 10299 ax-addf 10301 ax-mulf 10302

This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-xor 1635 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2590 df-eu 2607 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ne 2970 df-nel 3073 df-ral 3092 df-rex 3093 df-reu 3094 df-rmo 3095 df-rab 3096 df-v 3385 df-sbc 3632 df-csb 3727 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-pss 3783 df-nul 4114 df-if 4276 df-pw 4349 df-sn 4367 df-pr 4369 df-tp 4371 df-op 4373 df-ot 4375 df-uni 4627 df-int 4666 df-iun 4710 df-iin 4711 df-br 4842 df-opab 4904 df-mpt 4921 df-tr 4944 df-id 5218 df-eprel 5223 df-po 5231 df-so 5232 df-fr 5269 df-se 5270 df-we 5271 df-xp 5316 df-rel 5317 df-cnv 5318 df-co 5319 df-dm 5320 df-rn 5321 df-res 5322 df-ima 5323 df-pred 5896 df-ord 5942 df-on 5943 df-lim 5944 df-suc 5945 df-iota 6062 df-fun 6101 df-fn 6102 df-f 6103 df-f1 6104 df-fo 6105 df-f1o 6106 df-fv 6107 df-isom 6108 df-riota 6837 df-ov 6879 df-oprab 6880 df-mpt2 6881 df-om 7298 df-1st 7399 df-2nd 7400 df-supp 7531 df-tpos 7588 df-wrecs 7643 df-recs 7705 df-rdg 7743 df-1o 7797 df-2o 7798 df-oadd 7801 df-er 7980 df-map 8095 df-pm 8096 df-ixp 8147 df-en 8194 df-dom 8195 df-sdom 8196 df-fin 8197 df-fsupp 8516 df-sup 8588 df-oi 8655 df-card 9049 df-pnf 10363 df-mnf 10364 df-xr 10365 df-ltxr 10366 df-le 10367 df-sub 10556 df-neg 10557 df-div 10975 df-nn 11311 df-2 11372 df-3 11373 df-4 11374 df-5 11375 df-6 11376 df-7 11377 df-8 11378 df-9 11379 df-n0 11577 df-xnn0 11649 df-z 11663 df-dec 11780 df-uz 11927 df-rp 12071 df-fz 12577 df-fzo 12717 df-seq 13052 df-exp 13111 df-hash 13367 df-word 13531 df-lsw 13579 df-concat 13587 df-s1 13612 df-substr 13662 df-pfx 13711 df-splice 13818 df-reverse 13836 df-s2 13930 df-struct 16183 df-ndx 16184 df-slot 16185 df-base 16187 df-sets 16188 df-ress 16189 df-plusg 16277 df-mulr 16278 df-starv 16279 df-sca 16280 df-vsca 16281 df-ip 16282 df-tset 16283 df-ple 16284 df-ds 16286 df-unif 16287 df-hom 16288 df-cco 16289 df-0g 16414 df-gsum 16415 df-prds 16420 df-pws 16422 df-mre 16558 df-mrc 16559 df-acs 16561 df-mgm 17554 df-sgrp 17596 df-mnd 17607 df-mhm 17647 df-submnd 17648 df-grp 17738 df-minusg 17739 df-mulg 17854 df-subg 17901 df-ghm 17968 df-gim 18011 df-cntz 18059 df-oppg 18085 df-symg 18107 df-pmtr 18171 df-psgn 18220 df-cmn 18507 df-abl 18508 df-mgp 18803 df-ur 18815 df-ring 18862 df-cring 18863 df-oppr 18936 df-dvdsr 18954 df-unit 18955 df-invr 18985 df-dvr 18996 df-rnghom 19030 df-drng 19064 df-subrg 19093 df-sra 19492 df-rgmod 19493 df-cnfld 20066 df-zring 20138 df-zrh 20171 df-dsmm 20398 df-frlm 20413 df-mat 20536 df-mdet 20714

This theorem is referenced by: mdetcl 20725 mdetr0 20734 mdetero 20739 mdetuni0 20750 mdetmul 20752 maduf 20770 madurid 20773 madulid 20774 matunit 20808 cramerimp 20817

W3C validator