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.)
Hypotheses
Ref Expression
madetsmelbas.a 𝐴 = (𝑁 Mat 𝑅)
Assertion
Ref Expression
madetsmelbas2 ((𝑅 ∈ CRing ∧ 𝑀𝐵𝑄𝑃) → (((𝑌𝑆)‘𝑄)(.r𝑅)(𝐺 Σg (𝑛𝑁 ↦ (𝑛𝑀(𝑄𝑛))))) ∈ (Base‘𝑅))
Distinct variable groups:   𝐵,𝑛   𝑛,𝑀   𝑛,𝑁   𝑃,𝑛   𝑄,𝑛   𝑅,𝑛
Allowed substitution hints:   𝐴(𝑛)   𝑆(𝑛)   𝐺(𝑛)   𝑌(𝑛)

StepHypRef Expression
1 crngring 18381 . . 3 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
213ad2ant1 1075 . 2 ((𝑅 ∈ CRing ∧ 𝑀𝐵𝑄𝑃) → 𝑅 ∈ Ring)
3 madetsmelbas.a . . . . . 6 𝐴 = (𝑁 Mat 𝑅)
4 madetsmelbas.b . . . . . 6 𝐵 = (Base‘𝐴)
53, 4matrcl 20037 . . . . 5 (𝑀𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
65simpld 474 . . . 4 (𝑀𝐵𝑁 ∈ Fin)
763ad2ant2 1076 . . 3 ((𝑅 ∈ CRing ∧ 𝑀𝐵𝑄𝑃) → 𝑁 ∈ Fin)
8 simp3 1056 . . 3 ((𝑅 ∈ CRing ∧ 𝑀𝐵𝑄𝑃) → 𝑄𝑃)
9 madetsmelbas.p . . . 4 𝑃 = (Base‘(SymGrp‘𝑁))
10 madetsmelbas.s . . . 4 𝑆 = (pmSgn‘𝑁)
11 madetsmelbas.y . . . 4 𝑌 = (ℤRHom‘𝑅)
129, 10, 11zrhcopsgnelbas 19760 . . 3 ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄𝑃) → ((𝑌𝑆)‘𝑄) ∈ (Base‘𝑅))
132, 7, 8, 12syl3anc 1318 . 2 ((𝑅 ∈ CRing ∧ 𝑀𝐵𝑄𝑃) → ((𝑌𝑆)‘𝑄) ∈ (Base‘𝑅))
14 madetsmelbas.g . . . 4 𝐺 = (mulGrp‘𝑅)
15 eqid 2610 . . . 4 (Base‘𝑅) = (Base‘𝑅)
1614, 15mgpbas 18318 . . 3 (Base‘𝑅) = (Base‘𝐺)
1714crngmgp 18378 . . . 4 (𝑅 ∈ CRing → 𝐺 ∈ CMnd)
18173ad2ant1 1075 . . 3 ((𝑅 ∈ CRing ∧ 𝑀𝐵𝑄𝑃) → 𝐺 ∈ CMnd)
19 simp2 1055 . . . 4 ((𝑅 ∈ CRing ∧ 𝑀𝐵𝑄𝑃) → 𝑀𝐵)
203, 4, 9matepm2cl 20088 . . . 4 ((𝑅 ∈ Ring ∧ 𝑄𝑃𝑀𝐵) → ∀𝑛𝑁 (𝑛𝑀(𝑄𝑛)) ∈ (Base‘𝑅))
212, 8, 19, 20syl3anc 1318 . . 3 ((𝑅 ∈ CRing ∧ 𝑀𝐵𝑄𝑃) → ∀𝑛𝑁 (𝑛𝑀(𝑄𝑛)) ∈ (Base‘𝑅))
2216, 18, 7, 21gsummptcl 18189 . 2 ((𝑅 ∈ CRing ∧ 𝑀𝐵𝑄𝑃) → (𝐺 Σg (𝑛𝑁 ↦ (𝑛𝑀(𝑄𝑛)))) ∈ (Base‘𝑅))
23 eqid 2610 . . 3 (.r𝑅) = (.r𝑅)
2415, 23ringcl 18384 . 2 ((𝑅 ∈ Ring ∧ ((𝑌𝑆)‘𝑄) ∈ (Base‘𝑅) ∧ (𝐺 Σg (𝑛𝑁 ↦ (𝑛𝑀(𝑄𝑛)))) ∈ (Base‘𝑅)) → (((𝑌𝑆)‘𝑄)(.r𝑅)(𝐺 Σg (𝑛𝑁 ↦ (𝑛𝑀(𝑄𝑛))))) ∈ (Base‘𝑅))
252, 13, 22, 24syl3anc 1318 1 ((𝑅 ∈ CRing ∧ 𝑀𝐵𝑄𝑃) → (((𝑌𝑆)‘𝑄)(.r𝑅)(𝐺 Σg (𝑛𝑁 ↦ (𝑛𝑀(𝑄𝑛))))) ∈ (Base‘𝑅))