Metamath Proof Explorer

Theorem smadiadetlem3lem2

Description: Lemma 2 for smadiadetlem3 . (Contributed by AV, 12-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
smadiadetlem.w ⊢ W = Base SymGrp ⁡ N ∖ K
smadiadetlem.z ⊢ Z = pmSgn ⁡ N ∖ K
Assertion smadiadetlem3lem2 ⊢ M ∈ B ∧ K ∈ N → ran ⁡ p ∈ W ⟼ Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n ⊆ Cntz ⁡ R ⁡ ran ⁡ p ∈ W ⟼ Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n

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 smadiadetlem.w ⊢ W = Base SymGrp ⁡ N ∖ K
12 smadiadetlem.z ⊢ Z = pmSgn ⁡ N ∖ K
13 crngring ⊢ R ∈ CRing → R ∈ Ring
14 ringcmn ⊢ R ∈ Ring → R ∈ CMnd
15 3 13 14 mp2b ⊢ R ∈ CMnd
16 1 2 3 4 5 6 7 8 9 10 11 12 smadiadetlem3lem0 ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ W → Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n ∈ Base R
17 16 ralrimiva ⊢ M ∈ B ∧ K ∈ N → ∀ p ∈ W Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n ∈ Base R
18 eqid ⊢ p ∈ W ⟼ Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n = p ∈ W ⟼ Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n
19 18 rnmptss ⊢ ∀ p ∈ W Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n ∈ Base R → ran ⁡ p ∈ W ⟼ Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n ⊆ Base R
20 17 19 syl ⊢ M ∈ B ∧ K ∈ N → ran ⁡ p ∈ W ⟼ Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n ⊆ Base R
21 eqid ⊢ Base R = Base R
22 eqid ⊢ Cntz ⁡ R = Cntz ⁡ R
23 21 22 cntzcmnss ⊢ R ∈ CMnd ∧ ran ⁡ p ∈ W ⟼ Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n ⊆ Base R → ran ⁡ p ∈ W ⟼ Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n ⊆ Cntz ⁡ R ⁡ ran ⁡ p ∈ W ⟼ Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n
24 15 20 23 sylancr ⊢ M ∈ B ∧ K ∈ N → ran ⁡ p ∈ W ⟼ Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n ⊆ Cntz ⁡ R ⁡ ran ⁡ p ∈ W ⟼ Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n