Metamath Proof Explorer


Theorem smadiadetlem3lem0

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

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
smadiadetlem.w W=BaseSymGrpNK
smadiadetlem.z Z=pmSgnNK
Assertion smadiadetlem3lem0 MBKNQWYZQRGnNKniNK,jNKiMjQnBaseR

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 smadiadetlem.w W=BaseSymGrpNK
12 smadiadetlem.z Z=pmSgnNK
13 difssd KNNKN
14 13 anim2i MBKNMBNKN
15 14 adantr MBKNQWMBNKN
16 1 2 submabas MBNKNiNK,jNKiMjBaseNKMatR
17 15 16 syl MBKNQWiNK,jNKiMjBaseNKMatR
18 simpr MBKNQWQW
19 eqid NKMatR=NKMatR
20 eqid BaseNKMatR=BaseNKMatR
21 11 12 8 19 20 7 madetsmelbas2 RCRingiNK,jNKiMjBaseNKMatRQWYZQRGnNKniNK,jNKiMjQnBaseR
22 3 17 18 21 mp3an2i MBKNQWYZQRGnNKniNK,jNKiMjQnBaseR