Metamath Proof Explorer


Theorem smadiadetlem3lem1

Description: Lemma 1 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 smadiadetlem3lem1 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 : W 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 smadiadetlem.w W = Base SymGrp N K
12 smadiadetlem.z Z = pmSgn N K
13 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
14 13 fmpttd 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 : W Base R