Metamath Proof Explorer

Theorem smadiadetlem4

Description: Lemma 4 for smadiadet . (Contributed by AV, 31-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 smadiadetlem4 ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) )

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 7 crngmgp ⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ CMnd )
14 3 13 mp1i ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → 𝐺 ∈ CMnd )
15 1 2 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
16 15 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
17 16 adantr ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → 𝑁 ∈ Fin )
18 14 17 jca ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) )
19 18 adantr ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) )
20 simprl ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
21 simprr ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
22 2 eleq2i ⊢ ( 𝑀 ∈ 𝐵 ↔ 𝑀 ∈ ( Base ‘ 𝐴 ) )
23 22 biimpi ⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( Base ‘ 𝐴 ) )
24 23 adantr ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
25 24 adantr ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
26 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
27 1 26 matecl ⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
28 20 21 25 27 syl3anc ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
29 7 26 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝐺 )
30 28 29 eleqtrdi ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝐺 ) )
31 30 ralrimivva ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝐺 ) )
32 31 adantr ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝐺 ) )
33 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
34 26 4 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
35 3 33 34 mp2b ⊢ 0 ∈ ( Base ‘ 𝑅 )
36 35 29 eleqtri ⊢ 0 ∈ ( Base ‘ 𝐺 )
37 32 36 jctir ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝐺 ) ∧ 0 ∈ ( Base ‘ 𝐺 ) ) )
38 simpr ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → 𝐾 ∈ 𝑁 )
39 38 adantr ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → 𝐾 ∈ 𝑁 )
40 simpr ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } )
41 eqid ⊢ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
42 7 5 ringidval ⊢ 1 = ( 0g ‘ 𝐺 )
43 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
44 6 41 42 43 gsummatr01 ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝐺 ) ∧ 0 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ∧ 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) ) → ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) = ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) )
45 19 37 39 39 40 44 syl113anc ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) = ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) )
46 45 oveq2d ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) = ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) )
47 46 mpteq2dva ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) = ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) )
48 47 oveq2d ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) )
49 1 2 3 4 5 6 7 8 9 10 11 12 smadiadetlem3 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) )
50 48 49 eqtrd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) )