Metamath Proof Explorer

Theorem gsummatr01

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

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

Proof

Step Hyp Ref Expression
1 gsummatr01.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2 gsummatr01.r ⊢ 𝑅 = { 𝑟 ∈ 𝑃 ∣ ( 𝑟 ‘ 𝐾 ) = 𝐿 }
3 gsummatr01.0 ⊢ 0 = ( 0g ‘ 𝐺 )
4 gsummatr01.s ⊢ 𝑆 = ( Base ‘ 𝐺 )
5 difsnid ⊢ ( 𝐾 ∈ 𝑁 → ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) = 𝑁 )
6 5 eqcomd ⊢ ( 𝐾 ∈ 𝑁 → 𝑁 = ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) )
7 6 3ad2ant1 ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) → 𝑁 = ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) )
8 7 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → 𝑁 = ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) )
9 8 mpteq1d ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) )
10 9 oveq2d ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) = ( 𝐺 Σg ( 𝑛 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) )
11 1 2 3 4 gsummatr01lem3 ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( 𝐺 Σg ( 𝑛 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) = ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) ( +g ‘ 𝐺 ) ( 𝐾 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝐾 ) ) ) )
12 eqidd ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) )
13 fveq1 ⊢ ( 𝑟 = 𝑄 → ( 𝑟 ‘ 𝐾 ) = ( 𝑄 ‘ 𝐾 ) )
14 13 eqeq1d ⊢ ( 𝑟 = 𝑄 → ( ( 𝑟 ‘ 𝐾 ) = 𝐿 ↔ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
15 14 2 elrab2 ⊢ ( 𝑄 ∈ 𝑅 ↔ ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) )
16 eqeq2 ⊢ ( ( 𝑄 ‘ 𝐾 ) = 𝐿 → ( 𝑗 = ( 𝑄 ‘ 𝐾 ) ↔ 𝑗 = 𝐿 ) )
17 16 adantl ⊢ ( ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) → ( 𝑗 = ( 𝑄 ‘ 𝐾 ) ↔ 𝑗 = 𝐿 ) )
18 17 anbi2d ⊢ ( ( 𝑄 ∈ 𝑃 ∧ ( 𝑄 ‘ 𝐾 ) = 𝐿 ) → ( ( 𝑖 = 𝐾 ∧ 𝑗 = ( 𝑄 ‘ 𝐾 ) ) ↔ ( 𝑖 = 𝐾 ∧ 𝑗 = 𝐿 ) ) )
19 15 18 sylbi ⊢ ( 𝑄 ∈ 𝑅 → ( ( 𝑖 = 𝐾 ∧ 𝑗 = ( 𝑄 ‘ 𝐾 ) ) ↔ ( 𝑖 = 𝐾 ∧ 𝑗 = 𝐿 ) ) )
20 19 3ad2ant3 ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) → ( ( 𝑖 = 𝐾 ∧ 𝑗 = ( 𝑄 ‘ 𝐾 ) ) ↔ ( 𝑖 = 𝐾 ∧ 𝑗 = 𝐿 ) ) )
21 iftrue ⊢ ( 𝑖 = 𝐾 → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) = if ( 𝑗 = 𝐿 , 0 , 𝐵 ) )
22 iftrue ⊢ ( 𝑗 = 𝐿 → if ( 𝑗 = 𝐿 , 0 , 𝐵 ) = 0 )
23 21 22 sylan9eq ⊢ ( ( 𝑖 = 𝐾 ∧ 𝑗 = 𝐿 ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) = 0 )
24 20 23 biimtrdi ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) → ( ( 𝑖 = 𝐾 ∧ 𝑗 = ( 𝑄 ‘ 𝐾 ) ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) = 0 ) )
25 24 imp ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ∧ ( 𝑖 = 𝐾 ∧ 𝑗 = ( 𝑄 ‘ 𝐾 ) ) ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) = 0 )
26 simp1 ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) → 𝐾 ∈ 𝑁 )
27 1 2 gsummatr01lem1 ⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝐾 ∈ 𝑁 ) → ( 𝑄 ‘ 𝐾 ) ∈ 𝑁 )
28 27 ancoms ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) → ( 𝑄 ‘ 𝐾 ) ∈ 𝑁 )
29 28 3adant2 ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) → ( 𝑄 ‘ 𝐾 ) ∈ 𝑁 )
30 3 fvexi ⊢ 0 ∈ V
31 30 a1i ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) → 0 ∈ V )
32 12 25 26 29 31 ovmpod ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) → ( 𝐾 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝐾 ) ) = 0 )
33 32 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( 𝐾 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝐾 ) ) = 0 )
34 33 oveq2d ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) ( +g ‘ 𝐺 ) ( 𝐾 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝐾 ) ) ) = ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) ( +g ‘ 𝐺 ) 0 ) )
35 cmnmnd ⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
36 35 adantr ⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) → 𝐺 ∈ Mnd )
37 36 3ad2ant1 ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → 𝐺 ∈ Mnd )
38 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
39 simp1l ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → 𝐺 ∈ CMnd )
40 diffi ⊢ ( 𝑁 ∈ Fin → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
41 40 adantl ⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
42 41 3ad2ant1 ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( 𝑁 ∖ { 𝐾 } ) ∈ Fin )
43 eqidd ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) )
44 eqeq1 ⊢ ( 𝑖 = 𝑛 → ( 𝑖 = 𝐾 ↔ 𝑛 = 𝐾 ) )
45 44 adantr ⊢ ( ( 𝑖 = 𝑛 ∧ 𝑗 = ( 𝑄 ‘ 𝑛 ) ) → ( 𝑖 = 𝐾 ↔ 𝑛 = 𝐾 ) )
46 eqeq1 ⊢ ( 𝑗 = ( 𝑄 ‘ 𝑛 ) → ( 𝑗 = 𝐿 ↔ ( 𝑄 ‘ 𝑛 ) = 𝐿 ) )
47 46 ifbid ⊢ ( 𝑗 = ( 𝑄 ‘ 𝑛 ) → if ( 𝑗 = 𝐿 , 0 , 𝐵 ) = if ( ( 𝑄 ‘ 𝑛 ) = 𝐿 , 0 , 𝐵 ) )
48 47 adantl ⊢ ( ( 𝑖 = 𝑛 ∧ 𝑗 = ( 𝑄 ‘ 𝑛 ) ) → if ( 𝑗 = 𝐿 , 0 , 𝐵 ) = if ( ( 𝑄 ‘ 𝑛 ) = 𝐿 , 0 , 𝐵 ) )
49 oveq12 ⊢ ( ( 𝑖 = 𝑛 ∧ 𝑗 = ( 𝑄 ‘ 𝑛 ) ) → ( 𝑖 𝐴 𝑗 ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) )
50 45 48 49 ifbieq12d ⊢ ( ( 𝑖 = 𝑛 ∧ 𝑗 = ( 𝑄 ‘ 𝑛 ) ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) = if ( 𝑛 = 𝐾 , if ( ( 𝑄 ‘ 𝑛 ) = 𝐿 , 0 , 𝐵 ) , ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ) )
51 eldifsni ⊢ ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → 𝑛 ≠ 𝐾 )
52 51 neneqd ⊢ ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ¬ 𝑛 = 𝐾 )
53 52 iffalsed ⊢ ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → if ( 𝑛 = 𝐾 , if ( ( 𝑄 ‘ 𝑛 ) = 𝐿 , 0 , 𝐵 ) , ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) )
54 53 adantl ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → if ( 𝑛 = 𝐾 , if ( ( 𝑄 ‘ 𝑛 ) = 𝐿 , 0 , 𝐵 ) , ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) )
55 50 54 sylan9eqr ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) ∧ ( 𝑖 = 𝑛 ∧ 𝑗 = ( 𝑄 ‘ 𝑛 ) ) ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) )
56 eldifi ⊢ ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → 𝑛 ∈ 𝑁 )
57 56 adantl ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → 𝑛 ∈ 𝑁 )
58 simp3 ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) → 𝑄 ∈ 𝑅 )
59 1 2 gsummatr01lem1 ⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝑛 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 )
60 58 56 59 syl2an ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 )
61 ovexd ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ∈ V )
62 43 55 57 60 61 ovmpod ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) )
63 62 3ad2antl3 ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) = ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) )
64 4 eleq2i ⊢ ( ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ↔ ( 𝑖 𝐴 𝑗 ) ∈ ( Base ‘ 𝐺 ) )
65 64 2ralbii ⊢ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ ( Base ‘ 𝐺 ) )
66 1 2 gsummatr01lem2 ⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝑛 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ ( Base ‘ 𝐺 ) → ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐺 ) ) )
67 65 66 biimtrid ⊢ ( ( 𝑄 ∈ 𝑅 ∧ 𝑛 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 → ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐺 ) ) )
68 58 56 67 syl2anr ⊢ ( ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 → ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐺 ) ) )
69 68 ex ⊢ ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 → ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐺 ) ) ) )
70 69 com13 ⊢ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 → ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐺 ) ) ) )
71 70 adantr ⊢ ( ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐺 ) ) ) )
72 71 imp ⊢ ( ( ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐺 ) ) )
73 72 3adant1 ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐺 ) ) )
74 73 imp ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 𝐴 ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐺 ) )
75 63 74 eqeltrd ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐺 ) )
76 75 ralrimiva ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐺 ) )
77 38 39 42 76 gsummptcl ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) ∈ ( Base ‘ 𝐺 ) )
78 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
79 38 78 3 mndrid ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) ( +g ‘ 𝐺 ) 0 ) = ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) )
80 37 77 79 syl2anc ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) ( +g ‘ 𝐺 ) 0 ) = ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) )
81 1 2 3 4 gsummatr01lem4 ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) = ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝐴 𝑗 ) ) ( 𝑄 ‘ 𝑛 ) ) )
82 81 mpteq2dva ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝐴 𝑗 ) ) ( 𝑄 ‘ 𝑛 ) ) ) )
83 82 oveq2d ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) = ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝐴 𝑗 ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) )
84 34 80 83 3eqtrd ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) ( +g ‘ 𝐺 ) ( 𝐾 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝐾 ) ) ) = ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝐴 𝑗 ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) )
85 10 11 84 3eqtrd ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) = ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ ( 𝑁 ∖ { 𝐿 } ) ↦ ( 𝑖 𝐴 𝑗 ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) )