Metamath Proof Explorer

Theorem gsummatr01

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

Ref Expression
Hypotheses gsummatr01.p ⊢P=BaseSymGrp⁡N
gsummatr01.r ⊢R=r∈P|r⁡K=L
gsummatr01.0 ⊢0˙=0G
gsummatr01.s ⊢S=BaseG
Assertion gsummatr01 ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→∑Gn∈Nni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n=∑Gn∈N∖Kni∈N∖K,j∈N∖L⟼iAjQ⁡n

Proof

Step Hyp Ref Expression
1 gsummatr01.p ⊢P=BaseSymGrp⁡N
2 gsummatr01.r ⊢R=r∈P|r⁡K=L
3 gsummatr01.0 ⊢0˙=0G
4 gsummatr01.s ⊢S=BaseG
5 difsnid ⊢K∈N→N∖K∪K=N
6 5 eqcomd ⊢K∈N→N=N∖K∪K
7 6 3ad2ant1 ⊢K∈N∧L∈N∧Q∈R→N=N∖K∪K
8 7 3ad2ant3 ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→N=N∖K∪K
9 8 mpteq1d ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→n∈N⟼ni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n=n∈N∖K∪K⟼ni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n
10 9 oveq2d ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→∑Gn∈Nni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n=∑Gn∈N∖K∪Kni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n
11 1 2 3 4 gsummatr01lem3 ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→∑Gn∈N∖K∪Kni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n=∑Gn∈N∖Kni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n+GKi∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡K
12 eqidd ⊢K∈N∧L∈N∧Q∈R→i∈N,j∈N⟼ifi=Kifj=L0˙BiAj=i∈N,j∈N⟼ifi=Kifj=L0˙BiAj
13 fveq1 ⊢r=Q→r⁡K=Q⁡K
14 13 eqeq1d ⊢r=Q→r⁡K=L↔Q⁡K=L
15 14 2 elrab2 ⊢Q∈R↔Q∈P∧Q⁡K=L
16 eqeq2 ⊢Q⁡K=L→j=Q⁡K↔j=L
17 16 adantl ⊢Q∈P∧Q⁡K=L→j=Q⁡K↔j=L
18 17 anbi2d ⊢Q∈P∧Q⁡K=L→i=K∧j=Q⁡K↔i=K∧j=L
19 15 18 sylbi ⊢Q∈R→i=K∧j=Q⁡K↔i=K∧j=L
20 19 3ad2ant3 ⊢K∈N∧L∈N∧Q∈R→i=K∧j=Q⁡K↔i=K∧j=L
21 iftrue ⊢i=K→ifi=Kifj=L0˙BiAj=ifj=L0˙B
22 iftrue ⊢j=L→ifj=L0˙B=0˙
23 21 22 sylan9eq ⊢i=K∧j=L→ifi=Kifj=L0˙BiAj=0˙
24 20 23 syl6bi ⊢K∈N∧L∈N∧Q∈R→i=K∧j=Q⁡K→ifi=Kifj=L0˙BiAj=0˙
25 24 imp ⊢K∈N∧L∈N∧Q∈R∧i=K∧j=Q⁡K→ifi=Kifj=L0˙BiAj=0˙
26 simp1 ⊢K∈N∧L∈N∧Q∈R→K∈N
27 1 2 gsummatr01lem1 ⊢Q∈R∧K∈N→Q⁡K∈N
28 27 ancoms ⊢K∈N∧Q∈R→Q⁡K∈N
29 28 3adant2 ⊢K∈N∧L∈N∧Q∈R→Q⁡K∈N
30 3 fvexi ⊢0˙∈V
31 30 a1i ⊢K∈N∧L∈N∧Q∈R→0˙∈V
32 12 25 26 29 31 ovmpod ⊢K∈N∧L∈N∧Q∈R→Ki∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡K=0˙
33 32 3ad2ant3 ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→Ki∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡K=0˙
34 33 oveq2d ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→∑Gn∈N∖Kni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n+GKi∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡K=∑Gn∈N∖Kni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n+G0˙
35 cmnmnd ⊢G∈CMnd→G∈Mnd
36 35 adantr ⊢G∈CMnd∧N∈Fin→G∈Mnd
37 36 3ad2ant1 ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→G∈Mnd
38 eqid ⊢BaseG=BaseG
39 simp1l ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→G∈CMnd
40 diffi ⊢N∈Fin→N∖K∈Fin
41 40 adantl ⊢G∈CMnd∧N∈Fin→N∖K∈Fin
42 41 3ad2ant1 ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→N∖K∈Fin
43 eqidd ⊢K∈N∧L∈N∧Q∈R∧n∈N∖K→i∈N,j∈N⟼ifi=Kifj=L0˙BiAj=i∈N,j∈N⟼ifi=Kifj=L0˙BiAj
44 eqeq1 ⊢i=n→i=K↔n=K
45 44 adantr ⊢i=n∧j=Q⁡n→i=K↔n=K
46 eqeq1 ⊢j=Q⁡n→j=L↔Q⁡n=L
47 46 ifbid ⊢j=Q⁡n→ifj=L0˙B=ifQ⁡n=L0˙B
48 47 adantl ⊢i=n∧j=Q⁡n→ifj=L0˙B=ifQ⁡n=L0˙B
49 oveq12 ⊢i=n∧j=Q⁡n→iAj=nAQ⁡n
50 45 48 49 ifbieq12d ⊢i=n∧j=Q⁡n→ifi=Kifj=L0˙BiAj=ifn=KifQ⁡n=L0˙BnAQ⁡n
51 eldifsni ⊢n∈N∖K→n≠K
52 51 neneqd ⊢n∈N∖K→¬n=K
53 52 iffalsed ⊢n∈N∖K→ifn=KifQ⁡n=L0˙BnAQ⁡n=nAQ⁡n
54 53 adantl ⊢K∈N∧L∈N∧Q∈R∧n∈N∖K→ifn=KifQ⁡n=L0˙BnAQ⁡n=nAQ⁡n
55 50 54 sylan9eqr ⊢K∈N∧L∈N∧Q∈R∧n∈N∖K∧i=n∧j=Q⁡n→ifi=Kifj=L0˙BiAj=nAQ⁡n
56 eldifi ⊢n∈N∖K→n∈N
57 56 adantl ⊢K∈N∧L∈N∧Q∈R∧n∈N∖K→n∈N
58 simp3 ⊢K∈N∧L∈N∧Q∈R→Q∈R
59 1 2 gsummatr01lem1 ⊢Q∈R∧n∈N→Q⁡n∈N
60 58 56 59 syl2an ⊢K∈N∧L∈N∧Q∈R∧n∈N∖K→Q⁡n∈N
61 ovexd ⊢K∈N∧L∈N∧Q∈R∧n∈N∖K→nAQ⁡n∈V
62 43 55 57 60 61 ovmpod ⊢K∈N∧L∈N∧Q∈R∧n∈N∖K→ni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n=nAQ⁡n
63 62 3ad2antl3 ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R∧n∈N∖K→ni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n=nAQ⁡n
64 4 eleq2i ⊢iAj∈S↔iAj∈BaseG
65 64 2ralbii ⊢∀i∈N∀j∈NiAj∈S↔∀i∈N∀j∈NiAj∈BaseG
66 1 2 gsummatr01lem2 ⊢Q∈R∧n∈N→∀i∈N∀j∈NiAj∈BaseG→nAQ⁡n∈BaseG
67 65 66 biimtrid ⊢Q∈R∧n∈N→∀i∈N∀j∈NiAj∈S→nAQ⁡n∈BaseG
68 58 56 67 syl2anr ⊢n∈N∖K∧K∈N∧L∈N∧Q∈R→∀i∈N∀j∈NiAj∈S→nAQ⁡n∈BaseG
69 68 ex ⊢n∈N∖K→K∈N∧L∈N∧Q∈R→∀i∈N∀j∈NiAj∈S→nAQ⁡n∈BaseG
70 69 com13 ⊢∀i∈N∀j∈NiAj∈S→K∈N∧L∈N∧Q∈R→n∈N∖K→nAQ⁡n∈BaseG
71 70 adantr ⊢∀i∈N∀j∈NiAj∈S∧B∈S→K∈N∧L∈N∧Q∈R→n∈N∖K→nAQ⁡n∈BaseG
72 71 imp ⊢∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→n∈N∖K→nAQ⁡n∈BaseG
73 72 3adant1 ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→n∈N∖K→nAQ⁡n∈BaseG
74 73 imp ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R∧n∈N∖K→nAQ⁡n∈BaseG
75 63 74 eqeltrd ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R∧n∈N∖K→ni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n∈BaseG
76 75 ralrimiva ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→∀n∈N∖Kni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n∈BaseG
77 38 39 42 76 gsummptcl ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→∑Gn∈N∖Kni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n∈BaseG
78 eqid ⊢+G=+G
79 38 78 3 mndrid ⊢G∈Mnd∧∑Gn∈N∖Kni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n∈BaseG→∑Gn∈N∖Kni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n+G0˙=∑Gn∈N∖Kni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n
80 37 77 79 syl2anc ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→∑Gn∈N∖Kni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n+G0˙=∑Gn∈N∖Kni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n
81 1 2 3 4 gsummatr01lem4 ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R∧n∈N∖K→ni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n=ni∈N∖K,j∈N∖L⟼iAjQ⁡n
82 81 mpteq2dva ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→n∈N∖K⟼ni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n=n∈N∖K⟼ni∈N∖K,j∈N∖L⟼iAjQ⁡n
83 82 oveq2d ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→∑Gn∈N∖Kni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n=∑Gn∈N∖Kni∈N∖K,j∈N∖L⟼iAjQ⁡n
84 34 80 83 3eqtrd ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→∑Gn∈N∖Kni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n+GKi∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡K=∑Gn∈N∖Kni∈N∖K,j∈N∖L⟼iAjQ⁡n
85 10 11 84 3eqtrd ⊢G∈CMnd∧N∈Fin∧∀i∈N∀j∈NiAj∈S∧B∈S∧K∈N∧L∈N∧Q∈R→∑Gn∈Nni∈N,j∈N⟼ifi=Kifj=L0˙BiAjQ⁡n=∑Gn∈N∖Kni∈N∖K,j∈N∖L⟼iAjQ⁡n