![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > madetsmelbas2 | Structured version Visualization version GIF version |
Description: A summand of the determinant of a matrix belongs to the underlying ring. (Contributed by AV, 1-Jan-2019.) |
Ref | Expression |
---|---|
madetsmelbas.p | ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) |
madetsmelbas.s | ⊢ 𝑆 = (pmSgn‘𝑁) |
madetsmelbas.y | ⊢ 𝑌 = (ℤRHom‘𝑅) |
madetsmelbas.a | ⊢ 𝐴 = (𝑁 Mat 𝑅) |
madetsmelbas.b | ⊢ 𝐵 = (Base‘𝐴) |
madetsmelbas.g | ⊢ 𝐺 = (mulGrp‘𝑅) |
Ref | Expression |
---|---|
madetsmelbas2 | ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃) → (((𝑌 ∘ 𝑆)‘𝑄)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛𝑀(𝑄‘𝑛))))) ∈ (Base‘𝑅)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crngring 19043 | . . 3 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | |
2 | 1 | 3ad2ant1 1114 | . 2 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃) → 𝑅 ∈ Ring) |
3 | madetsmelbas.a | . . . . . 6 ⊢ 𝐴 = (𝑁 Mat 𝑅) | |
4 | madetsmelbas.b | . . . . . 6 ⊢ 𝐵 = (Base‘𝐴) | |
5 | 3, 4 | matrcl 20740 | . . . . 5 ⊢ (𝑀 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
6 | 5 | simpld 487 | . . . 4 ⊢ (𝑀 ∈ 𝐵 → 𝑁 ∈ Fin) |
7 | 6 | 3ad2ant2 1115 | . . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃) → 𝑁 ∈ Fin) |
8 | simp3 1119 | . . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃) → 𝑄 ∈ 𝑃) | |
9 | madetsmelbas.p | . . . 4 ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) | |
10 | madetsmelbas.s | . . . 4 ⊢ 𝑆 = (pmSgn‘𝑁) | |
11 | madetsmelbas.y | . . . 4 ⊢ 𝑌 = (ℤRHom‘𝑅) | |
12 | 9, 10, 11 | zrhcopsgnelbas 20456 | . . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃) → ((𝑌 ∘ 𝑆)‘𝑄) ∈ (Base‘𝑅)) |
13 | 2, 7, 8, 12 | syl3anc 1352 | . 2 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃) → ((𝑌 ∘ 𝑆)‘𝑄) ∈ (Base‘𝑅)) |
14 | madetsmelbas.g | . . . 4 ⊢ 𝐺 = (mulGrp‘𝑅) | |
15 | eqid 2771 | . . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
16 | 14, 15 | mgpbas 18980 | . . 3 ⊢ (Base‘𝑅) = (Base‘𝐺) |
17 | 14 | crngmgp 19040 | . . . 4 ⊢ (𝑅 ∈ CRing → 𝐺 ∈ CMnd) |
18 | 17 | 3ad2ant1 1114 | . . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃) → 𝐺 ∈ CMnd) |
19 | simp2 1118 | . . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃) → 𝑀 ∈ 𝐵) | |
20 | 3, 4, 9 | matepm2cl 20791 | . . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵) → ∀𝑛 ∈ 𝑁 (𝑛𝑀(𝑄‘𝑛)) ∈ (Base‘𝑅)) |
21 | 2, 8, 19, 20 | syl3anc 1352 | . . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃) → ∀𝑛 ∈ 𝑁 (𝑛𝑀(𝑄‘𝑛)) ∈ (Base‘𝑅)) |
22 | 16, 18, 7, 21 | gsummptcl 18852 | . 2 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃) → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛𝑀(𝑄‘𝑛)))) ∈ (Base‘𝑅)) |
23 | eqid 2771 | . . 3 ⊢ (.r‘𝑅) = (.r‘𝑅) | |
24 | 15, 23 | ringcl 19046 | . 2 ⊢ ((𝑅 ∈ Ring ∧ ((𝑌 ∘ 𝑆)‘𝑄) ∈ (Base‘𝑅) ∧ (𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛𝑀(𝑄‘𝑛)))) ∈ (Base‘𝑅)) → (((𝑌 ∘ 𝑆)‘𝑄)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛𝑀(𝑄‘𝑛))))) ∈ (Base‘𝑅)) |
25 | 2, 13, 22, 24 | syl3anc 1352 | 1 ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃) → (((𝑌 ∘ 𝑆)‘𝑄)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛𝑀(𝑄‘𝑛))))) ∈ (Base‘𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1069 = wceq 1508 ∈ wcel 2051 ∀wral 3081 Vcvv 3408 ↦ cmpt 5004 ∘ ccom 5407 ‘cfv 6185 (class class class)co 6974 Fincfn 8304 Basecbs 16337 .rcmulr 16420 Σg cgsu 16568 SymGrpcsymg 18278 pmSgncpsgn 18390 CMndccmn 18678 mulGrpcmgp 18974 Ringcrg 19032 CRingccrg 19033 ℤRHomczrh 20364 Mat cmat 20735 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2743 ax-rep 5045 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 ax-cnex 10389 ax-resscn 10390 ax-1cn 10391 ax-icn 10392 ax-addcl 10393 ax-addrcl 10394 ax-mulcl 10395 ax-mulrcl 10396 ax-mulcom 10397 ax-addass 10398 ax-mulass 10399 ax-distr 10400 ax-i2m1 10401 ax-1ne0 10402 ax-1rid 10403 ax-rnegex 10404 ax-rrecex 10405 ax-cnre 10406 ax-pre-lttri 10407 ax-pre-lttrn 10408 ax-pre-ltadd 10409 ax-pre-mulgt0 10410 ax-addf 10412 ax-mulf 10413 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-xor 1490 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-ne 2961 df-nel 3067 df-ral 3086 df-rex 3087 df-reu 3088 df-rmo 3089 df-rab 3090 df-v 3410 df-sbc 3675 df-csb 3780 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-pss 3838 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-ot 4444 df-uni 4709 df-int 4746 df-iun 4790 df-iin 4791 df-br 4926 df-opab 4988 df-mpt 5005 df-tr 5027 df-id 5308 df-eprel 5313 df-po 5322 df-so 5323 df-fr 5362 df-se 5363 df-we 5364 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-pred 5983 df-ord 6029 df-on 6030 df-lim 6031 df-suc 6032 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-isom 6194 df-riota 6935 df-ov 6977 df-oprab 6978 df-mpo 6979 df-om 7395 df-1st 7499 df-2nd 7500 df-supp 7632 df-tpos 7693 df-wrecs 7748 df-recs 7810 df-rdg 7848 df-1o 7903 df-2o 7904 df-oadd 7907 df-er 8087 df-map 8206 df-ixp 8258 df-en 8305 df-dom 8306 df-sdom 8307 df-fin 8308 df-fsupp 8627 df-sup 8699 df-oi 8767 df-card 9160 df-pnf 10474 df-mnf 10475 df-xr 10476 df-ltxr 10477 df-le 10478 df-sub 10670 df-neg 10671 df-div 11097 df-nn 11438 df-2 11501 df-3 11502 df-4 11503 df-5 11504 df-6 11505 df-7 11506 df-8 11507 df-9 11508 df-n0 11706 df-xnn0 11778 df-z 11792 df-dec 11910 df-uz 12057 df-rp 12203 df-fz 12707 df-fzo 12848 df-seq 13183 df-exp 13243 df-hash 13504 df-word 13671 df-lsw 13724 df-concat 13732 df-s1 13757 df-substr 13802 df-pfx 13851 df-splice 13958 df-reverse 13976 df-s2 14070 df-struct 16339 df-ndx 16340 df-slot 16341 df-base 16343 df-sets 16344 df-ress 16345 df-plusg 16432 df-mulr 16433 df-starv 16434 df-sca 16435 df-vsca 16436 df-ip 16437 df-tset 16438 df-ple 16439 df-ds 16441 df-unif 16442 df-hom 16443 df-cco 16444 df-0g 16569 df-gsum 16570 df-prds 16575 df-pws 16577 df-mre 16727 df-mrc 16728 df-acs 16730 df-mgm 17722 df-sgrp 17764 df-mnd 17775 df-mhm 17815 df-submnd 17816 df-grp 17906 df-minusg 17907 df-mulg 18024 df-subg 18072 df-ghm 18139 df-gim 18182 df-cntz 18230 df-oppg 18257 df-symg 18279 df-pmtr 18343 df-psgn 18392 df-cmn 18680 df-mgp 18975 df-ur 18987 df-ring 19034 df-cring 19035 df-rnghom 19202 df-subrg 19268 df-sra 19678 df-rgmod 19679 df-cnfld 20263 df-zring 20335 df-zrh 20368 df-dsmm 20593 df-frlm 20608 df-mat 20736 |
This theorem is referenced by: smadiadetlem1 20990 smadiadetlem3lem0 20993 smadiadet 20998 |
Copyright terms: Public domain | W3C validator |