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 bilani ⊢ ( ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝐵 ∈ ( Base ‘ 𝐺 ) )
74 73 3ad2ant2 ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → 𝐵 ∈ ( Base ‘ 𝐺 ) )
75 71 74 ifcld ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → if ( ( 𝑄 ‘ 𝐾 ) = 𝐿 , 0 , 𝐵 ) ∈ ( Base ‘ 𝐺 ) )
76 66 75 eqeltrd ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( 𝐾 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝐾 ) ) ∈ ( Base ‘ 𝐺 ) )
77 id ⊢ ( 𝑛 = 𝐾 → 𝑛 = 𝐾 )
78 fveq2 ⊢ ( 𝑛 = 𝐾 → ( 𝑄 ‘ 𝑛 ) = ( 𝑄 ‘ 𝐾 ) )
79 77 78 oveq12d ⊢ ( 𝑛 = 𝐾 → ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) = ( 𝐾 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝐾 ) ) )
80 5 6 8 11 46 47 48 76 79 gsumunsn ⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin ) ∧ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝐴 𝑗 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅 ) ) → ( 𝐺 Σg ( 𝑛 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) = ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝐾 } ) ↦ ( 𝑛 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝑛 ) ) ) ) ( +g ‘ 𝐺 ) ( 𝐾 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 0 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝐾 ) ) ) )