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

 Description: Lemma 1 for smadiadet 20295: 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 = (0g𝑅)
marep01ma.1 1 = (1r𝑅)
Assertion
Ref Expression
smadiadetlem1 (((𝑀𝐵𝐾𝑁) ∧ 𝑝𝑃) → (((𝑌𝑆)‘𝑝)(.r𝑅)(𝐺 Σg (𝑛𝑁 ↦ (𝑛(𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 1 , 0 ), (𝑖𝑀𝑗)))(𝑝𝑛))))) ∈ (Base‘𝑅))
Distinct variable groups:   𝑖,𝑗,𝑛,𝐵   𝑖,𝐾,𝑗,𝑛   𝑖,𝑀,𝑗,𝑛   𝑖,𝑁,𝑗,𝑛   𝑃,𝑖,𝑗,𝑛   𝑅,𝑖,𝑗,𝑛   1 ,𝑖,𝑗,𝑛   0 ,𝑖,𝑗,𝑛   𝑛,𝐺   𝑛,𝑝
Allowed substitution hints:   𝐴(𝑖,𝑗,𝑛,𝑝)   𝐵(𝑝)   𝑃(𝑝)   𝑅(𝑝)   𝑆(𝑖,𝑗,𝑛,𝑝)   · (𝑖,𝑗,𝑛,𝑝)   1 (𝑝)   𝐺(𝑖,𝑗,𝑝)   𝐾(𝑝)   𝑀(𝑝)   𝑁(𝑝)   𝑌(𝑖,𝑗,𝑛,𝑝)   0 (𝑝)

StepHypRef Expression
1 marep01ma.r . . 3 𝑅 ∈ CRing
21a1i 11 . 2 (((𝑀𝐵𝐾𝑁) ∧ 𝑝𝑃) → 𝑅 ∈ CRing)
3 marep01ma.a . . . 4 𝐴 = (𝑁 Mat 𝑅)
4 marep01ma.b . . . 4 𝐵 = (Base‘𝐴)
5 marep01ma.0 . . . 4 0 = (0g𝑅)
6 marep01ma.1 . . . 4 1 = (1r𝑅)
73, 4, 1, 5, 6marep01ma 20285 . . 3 (𝑀𝐵 → (𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 1 , 0 ), (𝑖𝑀𝑗))) ∈ 𝐵)
87ad2antrr 758 . 2 (((𝑀𝐵𝐾𝑁) ∧ 𝑝𝑃) → (𝑖𝑁, 𝑗𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 1 , 0 ), (𝑖𝑀𝑗))) ∈ 𝐵)
9 simpr 476 . 2 (((𝑀𝐵𝐾𝑁) ∧ 𝑝𝑃) → 𝑝𝑃)