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