Metamath Proof Explorer

Theorem smadiadetlem3lem2

Description: Lemma 2 for smadiadetlem3 . (Contributed by AV, 12-Jan-2019)

Ref Expression
Hypotheses marep01ma.a ⊢A=NMatR
marep01ma.b ⊢B=BaseA
marep01ma.r ⊢R∈CRing
marep01ma.0 ⊢0˙=0R
marep01ma.1 ⊢1˙=1R
smadiadetlem.p ⊢P=BaseSymGrp⁡N
smadiadetlem.g ⊢G=mulGrpR
madetminlem.y ⊢Y=ℤRHom⁡R
madetminlem.s ⊢S=pmSgn⁡N
madetminlem.t ⊢·˙=⋅R
smadiadetlem.w ⊢W=BaseSymGrp⁡N∖K
smadiadetlem.z ⊢Z=pmSgn⁡N∖K
Assertion smadiadetlem3lem2 ⊢M∈B∧K∈N→ran⁡p∈W⟼Y∘Z⁡p⋅R∑Gn∈N∖Kni∈N∖K,j∈N∖K⟼iMjp⁡n⊆Cntz⁡R⁡ran⁡p∈W⟼Y∘Z⁡p⋅R∑Gn∈N∖Kni∈N∖K,j∈N∖K⟼iMjp⁡n

Proof

Step Hyp Ref Expression
1 marep01ma.a ⊢A=NMatR
2 marep01ma.b ⊢B=BaseA
3 marep01ma.r ⊢R∈CRing
4 marep01ma.0 ⊢0˙=0R
5 marep01ma.1 ⊢1˙=1R
6 smadiadetlem.p ⊢P=BaseSymGrp⁡N
7 smadiadetlem.g ⊢G=mulGrpR
8 madetminlem.y ⊢Y=ℤRHom⁡R
9 madetminlem.s ⊢S=pmSgn⁡N
10 madetminlem.t ⊢·˙=⋅R
11 smadiadetlem.w ⊢W=BaseSymGrp⁡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∑Gn∈N∖Kni∈N∖K,j∈N∖K⟼iMjp⁡n∈BaseR
17 16 ralrimiva ⊢M∈B∧K∈N→∀p∈WY∘Z⁡p⋅R∑Gn∈N∖Kni∈N∖K,j∈N∖K⟼iMjp⁡n∈BaseR
18 eqid ⊢p∈W⟼Y∘Z⁡p⋅R∑Gn∈N∖Kni∈N∖K,j∈N∖K⟼iMjp⁡n=p∈W⟼Y∘Z⁡p⋅R∑Gn∈N∖Kni∈N∖K,j∈N∖K⟼iMjp⁡n
19 18 rnmptss ⊢∀p∈WY∘Z⁡p⋅R∑Gn∈N∖Kni∈N∖K,j∈N∖K⟼iMjp⁡n∈BaseR→ran⁡p∈W⟼Y∘Z⁡p⋅R∑Gn∈N∖Kni∈N∖K,j∈N∖K⟼iMjp⁡n⊆BaseR
20 17 19 syl ⊢M∈B∧K∈N→ran⁡p∈W⟼Y∘Z⁡p⋅R∑Gn∈N∖Kni∈N∖K,j∈N∖K⟼iMjp⁡n⊆BaseR
21 eqid ⊢BaseR=BaseR
22 eqid ⊢Cntz⁡R=Cntz⁡R
23 21 22 cntzcmnss ⊢R∈CMnd∧ran⁡p∈W⟼Y∘Z⁡p⋅R∑Gn∈N∖Kni∈N∖K,j∈N∖K⟼iMjp⁡n⊆BaseR→ran⁡p∈W⟼Y∘Z⁡p⋅R∑Gn∈N∖Kni∈N∖K,j∈N∖K⟼iMjp⁡n⊆Cntz⁡R⁡ran⁡p∈W⟼Y∘Z⁡p⋅R∑Gn∈N∖Kni∈N∖K,j∈N∖K⟼iMjp⁡n
24 15 20 23 sylancr ⊢M∈B∧K∈N→ran⁡p∈W⟼Y∘Z⁡p⋅R∑Gn∈N∖Kni∈N∖K,j∈N∖K⟼iMjp⁡n⊆Cntz⁡R⁡ran⁡p∈W⟼Y∘Z⁡p⋅R∑Gn∈N∖Kni∈N∖K,j∈N∖K⟼iMjp⁡n