Metamath Proof Explorer

Theorem smadiadetlem3

Description: Lemma 3 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 smadiadetlem3 ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) = ( 𝑅 Σ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 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14 eqid ⊢ ( Cntz ‘ 𝑅 ) = ( Cntz ‘ 𝑅 )
15 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
16 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
17 3 15 16 mp2b ⊢ 𝑅 ∈ Mnd
18 17 a1i ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → 𝑅 ∈ Mnd )
19 fvexd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∈ V )
20 11 19 eqeltrid ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → 𝑊 ∈ V )
21 1 2 3 4 5 6 7 8 9 10 11 12 smadiadetlem3lem1 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) : 𝑊 ⟶ ( Base ‘ 𝑅 ) )
22 1 2 3 4 5 6 7 8 9 10 11 12 smadiadetlem3lem2 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ran ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ⊆ ( ( Cntz ‘ 𝑅 ) ‘ ran ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) )
23 eqid ⊢ ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) = ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) )
24 1 2 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
25 24 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
26 25 adantr ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → 𝑁 ∈ Fin )
27 diffi ⊢ ( 𝑁 ∈ Fin → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
28 eqid ⊢ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) )
29 eqid ⊢ ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
30 28 29 symgbasfi ⊢ ( ( 𝑁 ∖ { 𝐾 } ) ∈ Fin → ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∈ Fin )
31 26 27 30 3syl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) ∈ Fin )
32 11 31 eqeltrid ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → 𝑊 ∈ Fin )
33 ovexd ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ 𝑊 ) → ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ∈ V )
34 4 fvexi ⊢ 0 ∈ V
35 34 a1i ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → 0 ∈ V )
36 23 32 33 35 fsuppmptdm ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) finSupp 0 )
37 fveq1 ⊢ ( 𝑞 = 𝑝 → ( 𝑞 ‘ 𝐾 ) = ( 𝑝 ‘ 𝐾 ) )
38 37 eqeq1d ⊢ ( 𝑞 = 𝑝 → ( ( 𝑞 ‘ 𝐾 ) = 𝐾 ↔ ( 𝑝 ‘ 𝐾 ) = 𝐾 ) )
39 38 cbvrabv ⊢ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } = { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ‘ 𝐾 ) = 𝐾 }
40 eqid ⊢ ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
41 6 39 11 40 symgfixf1o ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) : { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } –1-1-onto→ 𝑊 )
42 25 41 sylan ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) : { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } –1-1-onto→ 𝑊 )
43 13 4 14 18 20 21 22 36 42 gsumzf1o ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) = ( 𝑅 Σg ( ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ∘ ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) ) ) )
44 eqid ⊢ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
45 eqid ⊢ ( 𝑁 ∖ { 𝐾 } ) = ( 𝑁 ∖ { 𝐾 } )
46 6 44 11 45 symgfixelsi ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ∈ 𝑊 )
47 46 adantll ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ∈ 𝑊 )
48 eqidd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) )
49 fveq2 ⊢ ( 𝑝 = 𝑦 → ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) = ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑦 ) )
50 fveq1 ⊢ ( 𝑝 = 𝑦 → ( 𝑝 ‘ 𝑛 ) = ( 𝑦 ‘ 𝑛 ) )
51 50 oveq2d ⊢ ( 𝑝 = 𝑦 → ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) = ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑦 ‘ 𝑛 ) ) )
52 51 mpteq2dv ⊢ ( 𝑝 = 𝑦 → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑦 ‘ 𝑛 ) ) ) )
53 52 oveq2d ⊢ ( 𝑝 = 𝑦 → ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) = ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑦 ‘ 𝑛 ) ) ) ) )
54 49 53 oveq12d ⊢ ( 𝑝 = 𝑦 → ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) = ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑦 ‘ 𝑛 ) ) ) ) ) )
55 54 cbvmptv ⊢ ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) = ( 𝑦 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑦 ‘ 𝑛 ) ) ) ) ) )
56 55 a1i ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) = ( 𝑦 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) )
57 fveq2 ⊢ ( 𝑦 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) → ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑦 ) = ( ( 𝑌 ∘ 𝑍 ) ‘ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) )
58 fveq1 ⊢ ( 𝑦 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑦 ‘ 𝑛 ) = ( ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ‘ 𝑛 ) )
59 fvres ⊢ ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ‘ 𝑛 ) = ( 𝑝 ‘ 𝑛 ) )
60 58 59 sylan9eq ⊢ ( ( 𝑦 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑦 ‘ 𝑛 ) = ( 𝑝 ‘ 𝑛 ) )
61 60 oveq2d ⊢ ( ( 𝑦 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑦 ‘ 𝑛 ) ) = ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) )
62 61 mpteq2dva ⊢ ( 𝑦 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑦 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) )
63 62 oveq2d ⊢ ( 𝑦 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑦 ‘ 𝑛 ) ) ) ) = ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) )
64 57 63 oveq12d ⊢ ( 𝑦 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) → ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑦 ‘ 𝑛 ) ) ) ) ) = ( ( ( 𝑌 ∘ 𝑍 ) ‘ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) )
65 47 48 56 64 fmptco ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ∘ ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) ) = ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) )
66 6 9 12 copsgndif ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → ( ( 𝑌 ∘ 𝑍 ) ‘ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ) )
67 25 66 sylan ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } → ( ( 𝑌 ∘ 𝑍 ) ‘ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ) )
68 67 imp ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ( 𝑌 ∘ 𝑍 ) ‘ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) = ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) )
69 68 oveq1d ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ) → ( ( ( 𝑌 ∘ 𝑍 ) ‘ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) = ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) )
70 69 mpteq2dva ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) = ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) )
71 65 70 eqtrd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ∘ ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) ) = ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) )
72 71 oveq2d ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑅 Σg ( ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ∘ ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) )
73 43 72 eqtr2d ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑝 ∈ { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 } ↦ ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) = ( 𝑅 Σg ( 𝑝 ∈ 𝑊 ↦ ( ( ( 𝑌 ∘ 𝑍 ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) ( 𝑝 ‘ 𝑛 ) ) ) ) ) ) ) )