Metamath Proof Explorer


Theorem smadiadetlem3lem1

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

Ref Expression
Hypotheses marep01ma.a 𝐴 = ( 𝑁 Mat 𝑅 )
marep01ma.b 𝐵 = ( Base ‘ 𝐴 )
marep01ma.r 𝑅 ∈ CRing
marep01ma.0 0 = ( 0g𝑅 )
marep01ma.1 1 = ( 1r𝑅 )
smadiadetlem.p 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
smadiadetlem.g 𝐺 = ( mulGrp ‘ 𝑅 )
madetminlem.y 𝑌 = ( ℤRHom ‘ 𝑅 )
madetminlem.s 𝑆 = ( pmSgn ‘ 𝑁 )
madetminlem.t · = ( .r𝑅 )
smadiadetlem.w 𝑊 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
smadiadetlem.z 𝑍 = ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) )
Assertion smadiadetlem3lem1 ( ( 𝑀𝐵𝐾𝑁 ) → ( 𝑝𝑊 ↦ ( ( ( 𝑌𝑍 ) ‘ 𝑝 ) ( .r𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝𝑛 ) ) ) ) ) ) : 𝑊 ⟶ ( Base ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 marep01ma.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 marep01ma.b 𝐵 = ( Base ‘ 𝐴 )
3 marep01ma.r 𝑅 ∈ CRing
4 marep01ma.0 0 = ( 0g𝑅 )
5 marep01ma.1 1 = ( 1r𝑅 )
6 smadiadetlem.p 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
7 smadiadetlem.g 𝐺 = ( mulGrp ‘ 𝑅 )
8 madetminlem.y 𝑌 = ( ℤRHom ‘ 𝑅 )
9 madetminlem.s 𝑆 = ( pmSgn ‘ 𝑁 )
10 madetminlem.t · = ( .r𝑅 )
11 smadiadetlem.w 𝑊 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
12 smadiadetlem.z 𝑍 = ( pmSgn ‘ ( 𝑁 ∖ { 𝐾 } ) )
13 1 2 3 4 5 6 7 8 9 10 11 12 smadiadetlem3lem0 ( ( ( 𝑀𝐵𝐾𝑁 ) ∧ 𝑝𝑊 ) → ( ( ( 𝑌𝑍 ) ‘ 𝑝 ) ( .r𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝𝑛 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
14 13 fmpttd ( ( 𝑀𝐵𝐾𝑁 ) → ( 𝑝𝑊 ↦ ( ( ( 𝑌𝑍 ) ‘ 𝑝 ) ( .r𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝𝑛 ) ) ) ) ) ) : 𝑊 ⟶ ( Base ‘ 𝑅 ) )