Metamath Proof Explorer

Theorem madetsmelbas2

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

Ref Expression
Hypotheses madetsmelbas.p ⊢ P = Base SymGrp ⁡ N
madetsmelbas.s ⊢ S = pmSgn ⁡ N
madetsmelbas.y ⊢ Y = ℤRHom ⁡ R
madetsmelbas.a ⊢ A = N Mat R
madetsmelbas.b ⊢ B = Base A
madetsmelbas.g ⊢ G = mulGrp R
Assertion madetsmelbas2 ⊢ R ∈ CRing ∧ M ∈ B ∧ Q ∈ P → Y ∘ S ⁡ Q ⋅ R ∑ G n ∈ N n M Q ⁡ n ∈ Base R

Proof

Step Hyp Ref Expression
1 madetsmelbas.p ⊢ P = Base SymGrp ⁡ N
2 madetsmelbas.s ⊢ S = pmSgn ⁡ N
3 madetsmelbas.y ⊢ Y = ℤRHom ⁡ R
4 madetsmelbas.a ⊢ A = N Mat R
5 madetsmelbas.b ⊢ B = Base A
6 madetsmelbas.g ⊢ G = mulGrp R
7 crngring ⊢ R ∈ CRing → R ∈ Ring
8 7 3ad2ant1 ⊢ R ∈ CRing ∧ M ∈ B ∧ Q ∈ P → R ∈ Ring
9 4 5 matrcl ⊢ M ∈ B → N ∈ Fin ∧ R ∈ V
10 9 simpld ⊢ M ∈ B → N ∈ Fin
11 10 3ad2ant2 ⊢ R ∈ CRing ∧ M ∈ B ∧ Q ∈ P → N ∈ Fin
12 simp3 ⊢ R ∈ CRing ∧ M ∈ B ∧ Q ∈ P → Q ∈ P
13 1 2 3 zrhcopsgnelbas ⊢ R ∈ Ring ∧ N ∈ Fin ∧ Q ∈ P → Y ∘ S ⁡ Q ∈ Base R
14 8 11 12 13 syl3anc ⊢ R ∈ CRing ∧ M ∈ B ∧ Q ∈ P → Y ∘ S ⁡ Q ∈ Base R
15 eqid ⊢ Base R = Base R
16 6 15 mgpbas ⊢ Base R = Base G
17 6 crngmgp ⊢ R ∈ CRing → G ∈ CMnd
18 17 3ad2ant1 ⊢ R ∈ CRing ∧ M ∈ B ∧ Q ∈ P → G ∈ CMnd
19 simp2 ⊢ R ∈ CRing ∧ M ∈ B ∧ Q ∈ P → M ∈ B
20 4 5 1 matepm2cl ⊢ R ∈ Ring ∧ Q ∈ P ∧ M ∈ B → ∀ n ∈ N n M Q ⁡ n ∈ Base R
21 8 12 19 20 syl3anc ⊢ R ∈ CRing ∧ M ∈ B ∧ Q ∈ P → ∀ n ∈ N n M Q ⁡ n ∈ Base R
22 16 18 11 21 gsummptcl ⊢ R ∈ CRing ∧ M ∈ B ∧ Q ∈ P → ∑ G n ∈ N n M Q ⁡ n ∈ Base R
23 eqid ⊢ ⋅ R = ⋅ R
24 15 23 ringcl ⊢ R ∈ Ring ∧ Y ∘ S ⁡ Q ∈ Base R ∧ ∑ G n ∈ N n M Q ⁡ n ∈ Base R → Y ∘ S ⁡ Q ⋅ R ∑ G n ∈ N n M Q ⁡ n ∈ Base R
25 8 14 22 24 syl3anc ⊢ R ∈ CRing ∧ M ∈ B ∧ Q ∈ P → Y ∘ S ⁡ Q ⋅ R ∑ G n ∈ N n M Q ⁡ n ∈ Base R