Metamath Proof Explorer

Theorem smadiadetlem1

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

Ref Expression
Hypotheses marep01ma.a ⊢ A = N Mat R
marep01ma.b ⊢ B = Base A
marep01ma.r ⊢ R ∈ CRing
marep01ma.0 ⊢ 0 ˙ = 0 R
marep01ma.1 ⊢ 1 ˙ = 1 R
smadiadetlem.p ⊢ P = Base SymGrp ⁡ N
smadiadetlem.g ⊢ G = mulGrp R
madetminlem.y ⊢ Y = ℤRHom ⁡ R
madetminlem.s ⊢ S = pmSgn ⁡ N
madetminlem.t ⊢ · ˙ = ⋅ R
Assertion smadiadetlem1 ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ P → Y ∘ S ⁡ p ⋅ R ∑ G n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 ˙ 0 ˙ i M j p ⁡ n ∈ Base R

Proof

Step Hyp Ref Expression
1 marep01ma.a ⊢ A = N Mat R
2 marep01ma.b ⊢ B = Base A
3 marep01ma.r ⊢ R ∈ CRing
4 marep01ma.0 ⊢ 0 ˙ = 0 R
5 marep01ma.1 ⊢ 1 ˙ = 1 R
6 smadiadetlem.p ⊢ P = Base SymGrp ⁡ N
7 smadiadetlem.g ⊢ G = mulGrp R
8 madetminlem.y ⊢ Y = ℤRHom ⁡ R
9 madetminlem.s ⊢ S = pmSgn ⁡ N
10 madetminlem.t ⊢ · ˙ = ⋅ R
11 1 2 3 4 5 marep01ma ⊢ M ∈ B → i ∈ N , j ∈ N ⟼ if i = K if j = K 1 ˙ 0 ˙ i M j ∈ B
12 11 ad2antrr ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ P → i ∈ N , j ∈ N ⟼ if i = K if j = K 1 ˙ 0 ˙ i M j ∈ B
13 simpr ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ P → p ∈ P
14 6 9 8 1 2 7 madetsmelbas2 ⊢ R ∈ CRing ∧ i ∈ N , j ∈ N ⟼ if i = K if j = K 1 ˙ 0 ˙ i M j ∈ B ∧ p ∈ P → Y ∘ S ⁡ p ⋅ R ∑ G n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 ˙ 0 ˙ i M j p ⁡ n ∈ Base R
15 3 12 13 14 mp3an2i ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ P → Y ∘ S ⁡ p ⋅ R ∑ G n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 ˙ 0 ˙ i M j p ⁡ n ∈ Base R