Metamath Proof Explorer


Theorem gsummatr01lem3

Description: Lemma 1 for gsummatr01 . (Contributed by AV, 8-Jan-2019)

Ref Expression
Hypotheses gsummatr01.p 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
gsummatr01.r 𝑅 = { 𝑟𝑃 ∣ ( 𝑟𝐾 ) = 𝐿 }
gsummatr01.0 0 = ( 0g𝐺 )
gsummatr01.s 𝑆 = ( Base ‘ 𝐺 )
Assertion gsummatr01lem3 ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → ( 𝐺 Σg ( 𝑛 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄𝑛 ) ) ) ) = ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄𝑛 ) ) ) ) ( +g𝐺 ) ( 𝐾 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄𝐾 ) ) ) )

Proof

Step Hyp Ref Expression
1 gsummatr01.p 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2 gsummatr01.r 𝑅 = { 𝑟𝑃 ∣ ( 𝑟𝐾 ) = 𝐿 }
3 gsummatr01.0 0 = ( 0g𝐺 )
4 gsummatr01.s 𝑆 = ( Base ‘ 𝐺 )
5 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6 eqid ( +g𝐺 ) = ( +g𝐺 )
7 simpl ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) → 𝐺 ∈ CMnd )
8 7 3ad2ant1 ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → 𝐺 ∈ CMnd )
9 diffi ( 𝑁 ∈ Fin → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
10 9 adantl ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
11 10 3ad2ant1 ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
12 eqidd ( ( ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) )
13 eqeq1 ( 𝑖 = 𝑛 → ( 𝑖 = 𝐾𝑛 = 𝐾 ) )
14 13 adantr ( ( 𝑖 = 𝑛𝑗 = ( 𝑄𝑛 ) ) → ( 𝑖 = 𝐾𝑛 = 𝐾 ) )
15 eqeq1 ( 𝑗 = ( 𝑄𝑛 ) → ( 𝑗 = 𝐿 ↔ ( 𝑄𝑛 ) = 𝐿 ) )
16 15 ifbid ( 𝑗 = ( 𝑄𝑛 ) → if ( 𝑗 = 𝐿 , 0 , 𝐵 ) = if ( ( 𝑄𝑛 ) = 𝐿 , 0 , 𝐵 ) )
17 16 adantl ( ( 𝑖 = 𝑛𝑗 = ( 𝑄𝑛 ) ) → if ( 𝑗 = 𝐿 , 0 , 𝐵 ) = if ( ( 𝑄𝑛 ) = 𝐿 , 0 , 𝐵 ) )
18 oveq12 ( ( 𝑖 = 𝑛𝑗 = ( 𝑄𝑛 ) ) → ( 𝑖 𝐴 𝑗 ) = ( 𝑛 𝐴 ( 𝑄𝑛 ) ) )
19 14 17 18 ifbieq12d ( ( 𝑖 = 𝑛𝑗 = ( 𝑄𝑛 ) ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) = if ( 𝑛 = 𝐾 , if ( ( 𝑄𝑛 ) = 𝐿 , 0 , 𝐵 ) , ( 𝑛 𝐴 ( 𝑄𝑛 ) ) ) )
20 eldifsni ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → 𝑛𝐾 )
21 20 neneqd ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ¬ 𝑛 = 𝐾 )
22 21 iffalsed ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → if ( 𝑛 = 𝐾 , if ( ( 𝑄𝑛 ) = 𝐿 , 0 , 𝐵 ) , ( 𝑛 𝐴 ( 𝑄𝑛 ) ) ) = ( 𝑛 𝐴 ( 𝑄𝑛 ) ) )
23 22 adantl ( ( ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → if ( 𝑛 = 𝐾 , if ( ( 𝑄𝑛 ) = 𝐿 , 0 , 𝐵 ) , ( 𝑛 𝐴 ( 𝑄𝑛 ) ) ) = ( 𝑛 𝐴 ( 𝑄𝑛 ) ) )
24 19 23 sylan9eqr ( ( ( ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) ∧ ( 𝑖 = 𝑛𝑗 = ( 𝑄𝑛 ) ) ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) = ( 𝑛 𝐴 ( 𝑄𝑛 ) ) )
25 eldifi ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → 𝑛𝑁 )
26 25 adantl ( ( ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → 𝑛𝑁 )
27 1 2 gsummatr01lem1 ( ( 𝑄𝑅𝑛𝑁 ) → ( 𝑄𝑛 ) ∈ 𝑁 )
28 27 expcom ( 𝑛𝑁 → ( 𝑄𝑅 → ( 𝑄𝑛 ) ∈ 𝑁 ) )
29 28 25 syl11 ( 𝑄𝑅 → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝑄𝑛 ) ∈ 𝑁 ) )
30 29 3ad2ant3 ( ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝑄𝑛 ) ∈ 𝑁 ) )
31 30 imp ( ( ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑄𝑛 ) ∈ 𝑁 )
32 ovexd ( ( ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 𝐴 ( 𝑄𝑛 ) ) ∈ V )
33 12 24 26 31 32 ovmpod ( ( ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄𝑛 ) ) = ( 𝑛 𝐴 ( 𝑄𝑛 ) ) )
34 33 3ad2antl3 ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄𝑛 ) ) = ( 𝑛 𝐴 ( 𝑄𝑛 ) ) )
35 4 eleq2i ( ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ↔ ( 𝑖 𝐴 𝑗 ) ∈ ( Base ‘ 𝐺 ) )
36 35 2ralbii ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ↔ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ ( Base ‘ 𝐺 ) )
37 1 2 gsummatr01lem2 ( ( 𝑄𝑅𝑛𝑁 ) → ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ ( Base ‘ 𝐺 ) → ( 𝑛 𝐴 ( 𝑄𝑛 ) ) ∈ ( Base ‘ 𝐺 ) ) )
38 25 37 sylan2 ( ( 𝑄𝑅𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ ( Base ‘ 𝐺 ) → ( 𝑛 𝐴 ( 𝑄𝑛 ) ) ∈ ( Base ‘ 𝐺 ) ) )
39 38 ex ( 𝑄𝑅 → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ ( Base ‘ 𝐺 ) → ( 𝑛 𝐴 ( 𝑄𝑛 ) ) ∈ ( Base ‘ 𝐺 ) ) ) )
40 39 3ad2ant3 ( ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ ( Base ‘ 𝐺 ) → ( 𝑛 𝐴 ( 𝑄𝑛 ) ) ∈ ( Base ‘ 𝐺 ) ) ) )
41 40 com3r ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ ( Base ‘ 𝐺 ) → ( ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝑛 𝐴 ( 𝑄𝑛 ) ) ∈ ( Base ‘ 𝐺 ) ) ) )
42 36 41 sylbi ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 → ( ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝑛 𝐴 ( 𝑄𝑛 ) ) ∈ ( Base ‘ 𝐺 ) ) ) )
43 42 adantr ( ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) → ( ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝑛 𝐴 ( 𝑄𝑛 ) ) ∈ ( Base ‘ 𝐺 ) ) ) )
44 43 imp31 ( ( ( ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 𝐴 ( 𝑄𝑛 ) ) ∈ ( Base ‘ 𝐺 ) )
45 44 3adantl1 ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 𝐴 ( 𝑄𝑛 ) ) ∈ ( Base ‘ 𝐺 ) )
46 34 45 eqeltrd ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄𝑛 ) ) ∈ ( Base ‘ 𝐺 ) )
47 simp31 ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → 𝐾𝑁 )
48 neldifsnd ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → ¬ 𝐾 ∈ ( 𝑁 ∖ { 𝐾 } ) )
49 eqidd ( ( 𝐵𝑆 ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) )
50 iftrue ( 𝑖 = 𝐾 → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) = if ( 𝑗 = 𝐿 , 0 , 𝐵 ) )
51 eqeq1 ( 𝑗 = ( 𝑄𝐾 ) → ( 𝑗 = 𝐿 ↔ ( 𝑄𝐾 ) = 𝐿 ) )
52 51 ifbid ( 𝑗 = ( 𝑄𝐾 ) → if ( 𝑗 = 𝐿 , 0 , 𝐵 ) = if ( ( 𝑄𝐾 ) = 𝐿 , 0 , 𝐵 ) )
53 50 52 sylan9eq ( ( 𝑖 = 𝐾𝑗 = ( 𝑄𝐾 ) ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) = if ( ( 𝑄𝐾 ) = 𝐿 , 0 , 𝐵 ) )
54 53 adantl ( ( ( 𝐵𝑆 ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) ∧ ( 𝑖 = 𝐾𝑗 = ( 𝑄𝐾 ) ) ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) = if ( ( 𝑄𝐾 ) = 𝐿 , 0 , 𝐵 ) )
55 simpr1 ( ( 𝐵𝑆 ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → 𝐾𝑁 )
56 1 2 gsummatr01lem1 ( ( 𝑄𝑅𝐾𝑁 ) → ( 𝑄𝐾 ) ∈ 𝑁 )
57 56 ancoms ( ( 𝐾𝑁𝑄𝑅 ) → ( 𝑄𝐾 ) ∈ 𝑁 )
58 57 3adant2 ( ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) → ( 𝑄𝐾 ) ∈ 𝑁 )
59 58 adantl ( ( 𝐵𝑆 ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → ( 𝑄𝐾 ) ∈ 𝑁 )
60 3 fvexi 0 ∈ V
61 simpl ( ( 𝐵𝑆 ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → 𝐵𝑆 )
62 ifexg ( ( 0 ∈ V ∧ 𝐵𝑆 ) → if ( ( 𝑄𝐾 ) = 𝐿 , 0 , 𝐵 ) ∈ V )
63 60 61 62 sylancr ( ( 𝐵𝑆 ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → if ( ( 𝑄𝐾 ) = 𝐿 , 0 , 𝐵 ) ∈ V )
64 49 54 55 59 63 ovmpod ( ( 𝐵𝑆 ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → ( 𝐾 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄𝐾 ) ) = if ( ( 𝑄𝐾 ) = 𝐿 , 0 , 𝐵 ) )
65 64 adantll ( ( ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → ( 𝐾 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄𝐾 ) ) = if ( ( 𝑄𝐾 ) = 𝐿 , 0 , 𝐵 ) )
66 65 3adant1 ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → ( 𝐾 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄𝐾 ) ) = if ( ( 𝑄𝐾 ) = 𝐿 , 0 , 𝐵 ) )
67 cmnmnd ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
68 5 3 mndidcl ( 𝐺 ∈ Mnd → 0 ∈ ( Base ‘ 𝐺 ) )
69 67 68 syl ( 𝐺 ∈ CMnd → 0 ∈ ( Base ‘ 𝐺 ) )
70 69 adantr ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) → 0 ∈ ( Base ‘ 𝐺 ) )
71 70 3ad2ant1 ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → 0 ∈ ( Base ‘ 𝐺 ) )
72 4 eleq2i ( 𝐵𝑆𝐵 ∈ ( Base ‘ 𝐺 ) )
73 72 biimpi ( 𝐵𝑆𝐵 ∈ ( Base ‘ 𝐺 ) )
74 73 adantl ( ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) → 𝐵 ∈ ( Base ‘ 𝐺 ) )
75 74 3ad2ant2 ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → 𝐵 ∈ ( Base ‘ 𝐺 ) )
76 71 75 ifcld ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → if ( ( 𝑄𝐾 ) = 𝐿 , 0 , 𝐵 ) ∈ ( Base ‘ 𝐺 ) )
77 66 76 eqeltrd ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → ( 𝐾 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄𝐾 ) ) ∈ ( Base ‘ 𝐺 ) )
78 id ( 𝑛 = 𝐾𝑛 = 𝐾 )
79 fveq2 ( 𝑛 = 𝐾 → ( 𝑄𝑛 ) = ( 𝑄𝐾 ) )
80 78 79 oveq12d ( 𝑛 = 𝐾 → ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄𝑛 ) ) = ( 𝐾 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄𝐾 ) ) )
81 5 6 8 11 46 47 48 77 80 gsumunsn ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆𝐵𝑆 ) ∧ ( 𝐾𝑁𝐿𝑁𝑄𝑅 ) ) → ( 𝐺 Σg ( 𝑛 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄𝑛 ) ) ) ) = ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄𝑛 ) ) ) ) ( +g𝐺 ) ( 𝐾 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄𝐾 ) ) ) )