smadiadetlem1 - Metamath Proof Explorer

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

Theorem smadiadetlem1 22088

Description: Lemma 1 for smadiadet 22096: A summand of the determinant of a matrix belongs to the underlying ring. (Contributed by AV, 1-Jan-2019.)

**Hypotheses**
Ref	Expression
marep01ma.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
marep01ma.b	⊢ 𝐵 = (Base‘𝐴)
marep01ma.r	⊢ 𝑅 ∈ CRing
marep01ma.0	⊢ 0 = (0_g‘𝑅)
marep01ma.1	⊢ 1 = (1_r‘𝑅)
smadiadetlem.p	⊢ 𝑃 = (Base‘(SymGrp‘𝑁))
smadiadetlem.g	⊢ 𝐺 = (mulGrp‘𝑅)
madetminlem.y	⊢ 𝑌 = (ℤRHom‘𝑅)
madetminlem.s	⊢ 𝑆 = (pmSgn‘𝑁)
madetminlem.t	⊢ · = (._r‘𝑅)

**Assertion**
Ref	Expression
smadiadetlem1	⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) ∧ 𝑝 ∈ 𝑃) → (((𝑌 ∘ 𝑆)‘𝑝)(._r‘𝑅)(𝐺 Σ_g (𝑛 ∈ 𝑁 ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 1 , 0 ), (𝑖𝑀𝑗)))(𝑝‘𝑛))))) ∈ (Base‘𝑅))

Distinct variable groups: 𝑖,𝑗,𝑛,𝐵 𝑖,𝐾,𝑗,𝑛 𝑖,𝑀,𝑗,𝑛 𝑖,𝑁,𝑗,𝑛 𝑃,𝑖,𝑗,𝑛 𝑅,𝑖,𝑗,𝑛 1 ,𝑖,𝑗,𝑛 0 ,𝑖,𝑗,𝑛 𝑛,𝐺 𝑛,𝑝 Allowed substitution hints: 𝐴(𝑖,𝑗,𝑛,𝑝) 𝐵(𝑝) 𝑃(𝑝) 𝑅(𝑝) 𝑆(𝑖,𝑗,𝑛,𝑝) · (𝑖,𝑗,𝑛,𝑝) 1 (𝑝) 𝐺(𝑖,𝑗,𝑝) 𝐾(𝑝) 𝑀(𝑝) 𝑁(𝑝) 𝑌(𝑖,𝑗,𝑛,𝑝) 0 (𝑝)

**Proof of Theorem smadiadetlem1**
Step	Hyp	Ref	Expression
1		marep01ma.r	. 2 ⊢ 𝑅 ∈ CRing
2		marep01ma.a	. . . 4 ⊢ 𝐴 = (𝑁 Mat 𝑅)
3		marep01ma.b	. . . 4 ⊢ 𝐵 = (Base‘𝐴)
4		marep01ma.0	. . . 4 ⊢ 0 = (0_g‘𝑅)
5		marep01ma.1	. . . 4 ⊢ 1 = (1_r‘𝑅)
6	2, 3, 1, 4, 5	marep01ma 22086	. . 3 ⊢ (𝑀 ∈ 𝐵 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 1 , 0 ), (𝑖𝑀𝑗))) ∈ 𝐵)
7	6	ad2antrr 724	. 2 ⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) ∧ 𝑝 ∈ 𝑃) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 1 , 0 ), (𝑖𝑀𝑗))) ∈ 𝐵)
8		simpr 485	. 2 ⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑃)
9		smadiadetlem.p	. . 3 ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))
10		madetminlem.s	. . 3 ⊢ 𝑆 = (pmSgn‘𝑁)
11		madetminlem.y	. . 3 ⊢ 𝑌 = (ℤRHom‘𝑅)
12		smadiadetlem.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
13	9, 10, 11, 2, 3, 12	madetsmelbas2 21891	. 2 ⊢ ((𝑅 ∈ CRing ∧ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 1 , 0 ), (𝑖𝑀𝑗))) ∈ 𝐵 ∧ 𝑝 ∈ 𝑃) → (((𝑌 ∘ 𝑆)‘𝑝)(._r‘𝑅)(𝐺 Σ_g (𝑛 ∈ 𝑁 ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 1 , 0 ), (𝑖𝑀𝑗)))(𝑝‘𝑛))))) ∈ (Base‘𝑅))
14	1, 7, 8, 13	mp3an2i 1466	1 ⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) ∧ 𝑝 ∈ 𝑃) → (((𝑌 ∘ 𝑆)‘𝑝)(._r‘𝑅)(𝐺 Σ_g (𝑛 ∈ 𝑁 ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 1 , 0 ), (𝑖𝑀𝑗)))(𝑝‘𝑛))))) ∈ (Base‘𝑅))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ifcif 4519 ↦ cmpt 5221 ∘ ccom 5670 ‘cfv 6529 (class class class)co 7390 ∈ cmpo 7392 Basecbs 17123 ._rcmulr 17177 0_gc0g 17364 Σ_g cgsu 17365 SymGrpcsymg 19195 pmSgncpsgn 19318 mulGrpcmgp 19943 1_rcur 19960 CRingccrg 20012 ℤRHomczrh 20977 Mat cmat 21831

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-rep 5275 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7705 ax-cnex 11145 ax-resscn 11146 ax-1cn 11147 ax-icn 11148 ax-addcl 11149 ax-addrcl 11150 ax-mulcl 11151 ax-mulrcl 11152 ax-mulcom 11153 ax-addass 11154 ax-mulass 11155 ax-distr 11156 ax-i2m1 11157 ax-1ne0 11158 ax-1rid 11159 ax-rnegex 11160 ax-rrecex 11161 ax-cnre 11162 ax-pre-lttri 11163 ax-pre-lttrn 11164 ax-pre-ltadd 11165 ax-pre-mulgt0 11166 ax-addf 11168 ax-mulf 11169

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-xor 1510 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3430 df-v 3472 df-sbc 3771 df-csb 3887 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-pss 3960 df-nul 4316 df-if 4520 df-pw 4595 df-sn 4620 df-pr 4622 df-tp 4624 df-op 4626 df-ot 4628 df-uni 4899 df-int 4941 df-iun 4989 df-iin 4990 df-br 5139 df-opab 5201 df-mpt 5222 df-tr 5256 df-id 5564 df-eprel 5570 df-po 5578 df-so 5579 df-fr 5621 df-se 5622 df-we 5623 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6286 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6531 df-fn 6532 df-f 6533 df-f1 6534 df-fo 6535 df-f1o 6536 df-fv 6537 df-isom 6538 df-riota 7346 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7836 df-1st 7954 df-2nd 7955 df-supp 8126 df-tpos 8190 df-frecs 8245 df-wrecs 8276 df-recs 8350 df-rdg 8389 df-1o 8445 df-2o 8446 df-er 8683 df-map 8802 df-ixp 8872 df-en 8920 df-dom 8921 df-sdom 8922 df-fin 8923 df-fsupp 9342 df-sup 9416 df-oi 9484 df-card 9913 df-pnf 11229 df-mnf 11230 df-xr 11231 df-ltxr 11232 df-le 11233 df-sub 11425 df-neg 11426 df-div 11851 df-nn 12192 df-2 12254 df-3 12255 df-4 12256 df-5 12257 df-6 12258 df-7 12259 df-8 12260 df-9 12261 df-n0 12452 df-xnn0 12524 df-z 12538 df-dec 12657 df-uz 12802 df-rp 12954 df-fz 13464 df-fzo 13607 df-seq 13946 df-exp 14007 df-hash 14270 df-word 14444 df-lsw 14492 df-concat 14500 df-s1 14525 df-substr 14570 df-pfx 14600 df-splice 14679 df-reverse 14688 df-s2 14778 df-struct 17059 df-sets 17076 df-slot 17094 df-ndx 17106 df-base 17124 df-ress 17153 df-plusg 17189 df-mulr 17190 df-starv 17191 df-sca 17192 df-vsca 17193 df-ip 17194 df-tset 17195 df-ple 17196 df-ds 17198 df-unif 17199 df-hom 17200 df-cco 17201 df-0g 17366 df-gsum 17367 df-prds 17372 df-pws 17374 df-mre 17509 df-mrc 17510 df-acs 17512 df-mgm 18540 df-sgrp 18589 df-mnd 18600 df-mhm 18644 df-submnd 18645 df-efmnd 18722 df-grp 18794 df-minusg 18795 df-mulg 18920 df-subg 18972 df-ghm 19053 df-gim 19096 df-cntz 19144 df-oppg 19171 df-symg 19196 df-pmtr 19271 df-psgn 19320 df-cmn 19611 df-mgp 19944 df-ur 19961 df-ring 20013 df-cring 20014 df-rnghom 20198 df-subrg 20305 df-sra 20729 df-rgmod 20730 df-cnfld 20874 df-zring 20947 df-zrh 20981 df-dsmm 21215 df-frlm 21230 df-mat 21832

This theorem is referenced by: smadiadet 22096

W3C validator