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 , 𝐵 ) , ( 𝑖 𝐴 𝑗 ) ) ) ( 𝑄 ‘ 𝐾 ) ) ) ) |