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 ‘ 𝑅 ) ) |