Metamath Proof Explorer


Theorem smadiadetlem2

Description: Lemma 2 for smadiadet : The summands of the Leibniz' formula vanish for all permutations fixing the index of the row containing the 0's and the 1 to itself. (Contributed by AV, 31-Dec-2018)

Ref Expression
Hypotheses marep01ma.a A=NMatR
marep01ma.b B=BaseA
marep01ma.r RCRing
marep01ma.0 0˙=0R
marep01ma.1 1˙=1R
smadiadetlem.p P=BaseSymGrpN
smadiadetlem.g G=mulGrpR
madetminlem.y Y=ℤRHomR
madetminlem.s S=pmSgnN
madetminlem.t ·˙=R
Assertion smadiadetlem2 MBKNRpPqP|qK=KYSp·˙GnNniN,jNifi=Kifj=K1˙0˙iMjpn=0˙

Proof

Step Hyp Ref Expression
1 marep01ma.a A=NMatR
2 marep01ma.b B=BaseA
3 marep01ma.r RCRing
4 marep01ma.0 0˙=0R
5 marep01ma.1 1˙=1R
6 smadiadetlem.p P=BaseSymGrpN
7 smadiadetlem.g G=mulGrpR
8 madetminlem.y Y=ℤRHomR
9 madetminlem.s S=pmSgnN
10 madetminlem.t ·˙=R
11 1 2 3 4 5 6 7 8 9 10 smadiadetlem1a MBKNKNRpPqP|qK=KYSp·˙GnNniN,jNifi=Kifj=K1˙0˙iMjpn=0˙
12 11 3anidm23 MBKNRpPqP|qK=KYSp·˙GnNniN,jNifi=Kifj=K1˙0˙iMjpn=0˙