Theorem mdetf 22922

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 20484	. . . . 5 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
3	2	adantr 486	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → 𝑅 ∈ Ring)
4		ringcmn 20523	. . . 4 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
5	3, 4	syl 18	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → 𝑅 ∈ CMnd)
6		mdetf.a	. . . . . . 7 ⊢ 𝐴 = (𝑁 Mat 𝑅)
7		mdetf.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐴)
8	6, 7	matrcl 22739	. . . . . 6 ⊢ (𝑚 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
9	8	adantl 487	. . . . 5 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
10	9	simpld 500	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → 𝑁 ∈ Fin)
11		eqid 2763	. . . . 5 ⊢ (SymGrp‘𝑁) = (SymGrp‘𝑁)
12		eqid 2763	. . . . 5 ⊢ (Base‘(SymGrp‘𝑁)) = (Base‘(SymGrp‘𝑁))
13	11, 12	symgbasfi 19605	. . . 4 ⊢ (𝑁 ∈ Fin → (Base‘(SymGrp‘𝑁)) ∈ Fin)
14	10, 13	syl 18	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → (Base‘(SymGrp‘𝑁)) ∈ Fin)
15	2	ad2antrr 739	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑅 ∈ Ring)
16		zrhpsgnmhm 21902	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
17	3, 10, 16	syl2anc 596	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)))
18		eqid 2763	. . . . . . . . 9 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
19	18, 1	mgpbas 20377	. . . . . . . 8 ⊢ 𝐾 = (Base‘(mulGrp‘𝑅))
20	12, 19	mhmf 18996	. . . . . . 7 ⊢ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)) ∈ ((SymGrp‘𝑁) MndHom (mulGrp‘𝑅)) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾)
21	17, 20	syl 18	. . . . . 6 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁)):(Base‘(SymGrp‘𝑁))⟶𝐾)
22	21	ffvelcdmda 7092	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾)
23	18	crngmgp 20479	. . . . . . 7 ⊢ (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
24	23	ad2antrr 739	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → (mulGrp‘𝑅) ∈ CMnd)
25	10	adantr 486	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑁 ∈ Fin)
26	6, 1, 7	matbas2i 22749	. . . . . . . . . 10 ⊢ (𝑚 ∈ 𝐵 → 𝑚 ∈ (𝐾 ↑m (𝑁 × 𝑁)))
27	26	ad3antlr 744	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑚 ∈ (𝐾 ↑m (𝑁 × 𝑁)))
28		elmapi 8880	. . . . . . . . 9 ⊢ (𝑚 ∈ (𝐾 ↑m (𝑁 × 𝑁)) → 𝑚:(𝑁 × 𝑁)⟶𝐾)
29	27, 28	syl 18	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑚:(𝑁 × 𝑁)⟶𝐾)
30	11, 12	symgbasf 19602	. . . . . . . . . 10 ⊢ (𝑝 ∈ (Base‘(SymGrp‘𝑁)) → 𝑝:𝑁⟶𝑁)
31	30	adantl 487	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → 𝑝:𝑁⟶𝑁)
32	31	ffvelcdmda 7092	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → (𝑝‘𝑐) ∈ 𝑁)
33		simpr 490	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → 𝑐 ∈ 𝑁)
34	29, 32, 33	fovcdmd 7600	. . . . . . 7 ⊢ ((((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) ∧ 𝑐 ∈ 𝑁) → ((𝑝‘𝑐)𝑚𝑐) ∈ 𝐾)
35	34	ralrimiva 3157	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ∀𝑐 ∈ 𝑁 ((𝑝‘𝑐)𝑚𝑐) ∈ 𝐾)
36	19, 24, 25, 35	gsummptcl 20193	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑚𝑐))) ∈ 𝐾)
37		eqid 2763	. . . . . 6 ⊢ (.r‘𝑅) = (.r‘𝑅)
38	1, 37	ringcl 20489	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝) ∈ 𝐾 ∧ ((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑚𝑐))) ∈ 𝐾) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑚𝑐)))) ∈ 𝐾)
39	15, 22, 36, 38	syl3anc 1398	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) ∧ 𝑝 ∈ (Base‘(SymGrp‘𝑁))) → ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑚𝑐)))) ∈ 𝐾)
40	39	ralrimiva 3157	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → ∀𝑝 ∈ (Base‘(SymGrp‘𝑁))((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑚𝑐)))) ∈ 𝐾)
41	1, 5, 14, 40	gsummptcl 20193	. 2 ⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ 𝐵) → (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑚𝑐)))))) ∈ 𝐾)
42		mdetf.d	. . 3 ⊢ 𝐷 = (𝑁 maDet 𝑅)
43		eqid 2763	. . 3 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
44		eqid 2763	. . 3 ⊢ (pmSgn‘𝑁) = (pmSgn‘𝑁)
45	42, 6, 7, 12, 43, 44, 37, 18	mdetfval 22913	. 2 ⊢ 𝐷 = (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑁)) ↦ ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝑝)(.r‘𝑅)((mulGrp‘𝑅) Σg (𝑐 ∈ 𝑁 ↦ ((𝑝‘𝑐)𝑚𝑐)))))))
46	41, 45	fmptd 7122	1 ⊢ (𝑅 ∈ CRing → 𝐷:𝐵⟶𝐾)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2146  Vcvv 3453   ↦ cmpt 5188   × cxp 5652   ∘ ccom 5658  ⟶wf 6542  ‘cfv 6546  (class class class)co 7427   ↑_m cmap 8858  Fincfn 8984  Basecbs 17399  ._rcmulr 17441   Σ_g cgsu 17623   MndHom cmhm 18988  SymGrpcsymg 19595  pmSgncpsgn 19715  CMndccmn 20006  mulGrpcmgp 20372  Ringcrg 20471  CRingccrg 20472  ℤRHomczrh 21817   Mat cmat 22734   maDet cmdat 22911

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5234  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758  ax-cnex 11266  ax-resscn 11267  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-addrcl 11271  ax-mulcl 11272  ax-mulrcl 11273  ax-mulcom 11274  ax-addass 11275  ax-mulass 11276  ax-distr 11277  ax-i2m1 11278  ax-1ne0 11279  ax-1rid 11280  ax-rnegex 11281  ax-rrecex 11282  ax-cnre 11283  ax-pre-lttri 11284  ax-pre-lttrn 11285  ax-pre-ltadd 11286  ax-pre-mulgt0 11287  ax-addf 11289  ax-mulf 11290

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-xor 1541  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-pss 4016  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4838  df-ot 4861  df-uni 4870  df-int 4910  df-iun 4955  df-iin 4956  df-br 5106  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5549  df-eprel 5554  df-po 5562  df-so 5563  df-fr 5607  df-se 5608  df-we 5609  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6310  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-isom 6555  df-riota 7384  df-ov 7430  df-oprab 7431  df-mpo 7432  df-om 7885  df-1st 8008  df-2nd 8009  df-supp 8188  df-tpos 8254  df-frecs 8310  df-wrecs 8341  df-recs 8390  df-rdg 8429  df-1o 8487  df-2o 8488  df-er 8728  df-map 8860  df-pm 8861  df-ixp 8937  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fsupp 9365  df-sup 9444  df-oi 9514  df-card 10030  df-pnf 11355  df-mnf 11356  df-xr 11357  df-ltxr 11358  df-le 11359  df-sub 11553  df-neg 11554  df-div 11984  df-nn 12346  df-2 12415  df-3 12416  df-4 12417  df-5 12418  df-6 12419  df-7 12420  df-8 12421  df-9 12422  df-n0 12617  df-xnn0 12690  df-z 12704  df-dec 12825  df-uz 12976  df-rp 13131  df-fz 13650  df-fzo 13799  df-seq 14155  df-exp 14215  df-hash 14485  df-word 14669  df-lsw 14718  df-concat 14726  df-s1 14753  df-substr 14800  df-pfx 14832  df-splice 14910  df-reverse 14919  df-s2 15010  df-struct 17337  df-sets 17354  df-slot 17372  df-ndx 17384  df-base 17400  df-ress 17421  df-plusg 17453  df-mulr 17454  df-starv 17455  df-sca 17456  df-vsca 17457  df-ip 17458  df-tset 17459  df-ple 17460  df-ds 17462  df-unif 17463  df-hom 17464  df-cco 17465  df-0g 17624  df-gsum 17625  df-prds 17630  df-pws 17632  df-mre 17768  df-mrc 17769  df-acs 17771  df-mgm 18828  df-sgrp 18920  df-mnd 18936  df-mhm 18990  df-submnd 18991  df-efmnd 19077  df-grp 19159  df-minusg 19160  df-mulg 19290  df-subg 19345  df-ghm 19440  df-gim 19485  df-cntz 19543  df-oppg 19572  df-symg 19596  df-pmtr 19668  df-psgn 19717  df-cmn 20008  df-abl 20009  df-mgp 20373  df-rng 20387  df-ur 20420  df-ring 20473  df-cring 20474  df-oppr 20579  df-dvdsr 20599  df-unit 20600  df-invr 20630  df-dvr 20643  df-rhm 20714  df-subrng 20810  df-subrg 20834  df-drng 20994  df-sra 21460  df-rgmod 21461  df-cnfld 21691  df-zring 21765  df-zrh 21821  df-dsmm 22050  df-frlm 22065  df-mat 22735  df-mdet 22912

This theorem is used by:  mdetcl  22923  mdetr0  22932  mdetero  22937  mdetuni0  22948  mdetmul  22950  maduf  22968  madurid  22971  madulid  22972  matunit  23005  cramerimp  23016