Metamath Proof Explorer

Theorem gsmsymgreqlem2

Description: Lemma 2 for gsmsymgreq . (Contributed by AV, 26-Jan-2019)

Ref Expression
Hypotheses gsmsymgrfix.s ⊢S=SymGrp⁡N
gsmsymgrfix.b ⊢B=BaseS
gsmsymgreq.z ⊢Z=SymGrp⁡M
gsmsymgreq.p ⊢P=BaseZ
gsmsymgreq.i ⊢I=N∩M
Assertion gsmsymgreqlem2 ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n→∀n∈I∑SX⁡n=∑ZY⁡n→∀i∈0..^X++⟨“C”⟩∀n∈IX++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n→∀n∈I∑SX++⟨“C”⟩⁡n=∑ZY++⟨“R”⟩⁡n

Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s ⊢S=SymGrp⁡N
2 gsmsymgrfix.b ⊢B=BaseS
3 gsmsymgreq.z ⊢Z=SymGrp⁡M
4 gsmsymgreq.p ⊢P=BaseZ
5 gsmsymgreq.i ⊢I=N∩M
6 ccatws1len ⊢X∈WordB→X++⟨“C”⟩=X+1
7 6 oveq2d ⊢X∈WordB→0..^X++⟨“C”⟩=0..^X+1
8 lencl ⊢X∈WordB→X∈ℕ0
9 elnn0uz ⊢X∈ℕ0↔X∈ℤ≥0
10 8 9 sylib ⊢X∈WordB→X∈ℤ≥0
11 fzosplitsn ⊢X∈ℤ≥0→0..^X+1=0..^X∪X
12 10 11 syl ⊢X∈WordB→0..^X+1=0..^X∪X
13 7 12 eqtrd ⊢X∈WordB→0..^X++⟨“C”⟩=0..^X∪X
14 13 adantr ⊢X∈WordB∧C∈B→0..^X++⟨“C”⟩=0..^X∪X
15 14 3ad2ant1 ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→0..^X++⟨“C”⟩=0..^X∪X
16 15 raleqdv ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→∀i∈0..^X++⟨“C”⟩∀n∈IX++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n↔∀i∈0..^X∪X∀n∈IX++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n
17 8 adantr ⊢X∈WordB∧C∈B→X∈ℕ0
18 17 3ad2ant1 ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→X∈ℕ0
19 fveq2 ⊢i=X→X++⟨“C”⟩⁡i=X++⟨“C”⟩⁡X
20 19 fveq1d ⊢i=X→X++⟨“C”⟩⁡i⁡n=X++⟨“C”⟩⁡X⁡n
21 fveq2 ⊢i=X→Y++⟨“R”⟩⁡i=Y++⟨“R”⟩⁡X
22 21 fveq1d ⊢i=X→Y++⟨“R”⟩⁡i⁡n=Y++⟨“R”⟩⁡X⁡n
23 20 22 eqeq12d ⊢i=X→X++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n↔X++⟨“C”⟩⁡X⁡n=Y++⟨“R”⟩⁡X⁡n
24 23 ralbidv ⊢i=X→∀n∈IX++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n↔∀n∈IX++⟨“C”⟩⁡X⁡n=Y++⟨“R”⟩⁡X⁡n
25 24 ralunsn ⊢X∈ℕ0→∀i∈0..^X∪X∀n∈IX++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n↔∀i∈0..^X∀n∈IX++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n∧∀n∈IX++⟨“C”⟩⁡X⁡n=Y++⟨“R”⟩⁡X⁡n
26 18 25 syl ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→∀i∈0..^X∪X∀n∈IX++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n↔∀i∈0..^X∀n∈IX++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n∧∀n∈IX++⟨“C”⟩⁡X⁡n=Y++⟨“R”⟩⁡X⁡n
27 simp1l ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→X∈WordB
28 ccats1val1 ⊢X∈WordB∧i∈0..^X→X++⟨“C”⟩⁡i=X⁡i
29 27 28 sylan ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧i∈0..^X→X++⟨“C”⟩⁡i=X⁡i
30 29 fveq1d ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧i∈0..^X→X++⟨“C”⟩⁡i⁡n=X⁡i⁡n
31 simp2l ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→Y∈WordP
32 oveq2 ⊢X=Y→0..^X=0..^Y
33 32 eleq2d ⊢X=Y→i∈0..^X↔i∈0..^Y
34 33 biimpd ⊢X=Y→i∈0..^X→i∈0..^Y
35 34 3ad2ant3 ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→i∈0..^X→i∈0..^Y
36 35 imp ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧i∈0..^X→i∈0..^Y
37 ccats1val1 ⊢Y∈WordP∧i∈0..^Y→Y++⟨“R”⟩⁡i=Y⁡i
38 31 36 37 syl2an2r ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧i∈0..^X→Y++⟨“R”⟩⁡i=Y⁡i
39 38 fveq1d ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧i∈0..^X→Y++⟨“R”⟩⁡i⁡n=Y⁡i⁡n
40 30 39 eqeq12d ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧i∈0..^X→X++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n↔X⁡i⁡n=Y⁡i⁡n
41 40 ralbidv ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧i∈0..^X→∀n∈IX++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n↔∀n∈IX⁡i⁡n=Y⁡i⁡n
42 41 ralbidva ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→∀i∈0..^X∀n∈IX++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n↔∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n
43 eqidd ⊢X∈WordB∧C∈B→X=X
44 ccats1val2 ⊢X∈WordB∧C∈B∧X=X→X++⟨“C”⟩⁡X=C
45 44 fveq1d ⊢X∈WordB∧C∈B∧X=X→X++⟨“C”⟩⁡X⁡n=C⁡n
46 43 45 mpd3an3 ⊢X∈WordB∧C∈B→X++⟨“C”⟩⁡X⁡n=C⁡n
47 46 3ad2ant1 ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→X++⟨“C”⟩⁡X⁡n=C⁡n
48 ccats1val2 ⊢Y∈WordP∧R∈P∧X=Y→Y++⟨“R”⟩⁡X=R
49 48 fveq1d ⊢Y∈WordP∧R∈P∧X=Y→Y++⟨“R”⟩⁡X⁡n=R⁡n
50 49 3expa ⊢Y∈WordP∧R∈P∧X=Y→Y++⟨“R”⟩⁡X⁡n=R⁡n
51 50 3adant1 ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→Y++⟨“R”⟩⁡X⁡n=R⁡n
52 47 51 eqeq12d ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→X++⟨“C”⟩⁡X⁡n=Y++⟨“R”⟩⁡X⁡n↔C⁡n=R⁡n
53 52 ralbidv ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→∀n∈IX++⟨“C”⟩⁡X⁡n=Y++⟨“R”⟩⁡X⁡n↔∀n∈IC⁡n=R⁡n
54 42 53 anbi12d ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→∀i∈0..^X∀n∈IX++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n∧∀n∈IX++⟨“C”⟩⁡X⁡n=Y++⟨“R”⟩⁡X⁡n↔∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n∧∀n∈IC⁡n=R⁡n
55 16 26 54 3bitrd ⊢X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→∀i∈0..^X++⟨“C”⟩∀n∈IX++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n↔∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n∧∀n∈IC⁡n=R⁡n
56 55 ad2antlr ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n→∀n∈I∑SX⁡n=∑ZY⁡n→∀i∈0..^X++⟨“C”⟩∀n∈IX++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n↔∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n∧∀n∈IC⁡n=R⁡n
57 pm3.35 ⊢∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n∧∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n→∀n∈I∑SX⁡n=∑ZY⁡n→∀n∈I∑SX⁡n=∑ZY⁡n
58 fveq2 ⊢n=j→∑SX⁡n=∑SX⁡j
59 fveq2 ⊢n=j→∑ZY⁡n=∑ZY⁡j
60 58 59 eqeq12d ⊢n=j→∑SX⁡n=∑ZY⁡n↔∑SX⁡j=∑ZY⁡j
61 60 cbvralvw ⊢∀n∈I∑SX⁡n=∑ZY⁡n↔∀j∈I∑SX⁡j=∑ZY⁡j
62 simp-4l ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧∀j∈I∑SX⁡j=∑ZY⁡j∧n∈I→N∈Fin
63 simp-4r ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧∀j∈I∑SX⁡j=∑ZY⁡j∧n∈I→M∈Fin
64 simpr ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧∀j∈I∑SX⁡j=∑ZY⁡j∧n∈I→n∈I
65 62 63 64 3jca ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧∀j∈I∑SX⁡j=∑ZY⁡j∧n∈I→N∈Fin∧M∈Fin∧n∈I
66 65 adantr ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧∀j∈I∑SX⁡j=∑ZY⁡j∧n∈I∧C⁡n=R⁡n→N∈Fin∧M∈Fin∧n∈I
67 simp-4r ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧∀j∈I∑SX⁡j=∑ZY⁡j∧n∈I∧C⁡n=R⁡n→X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y
68 simplr ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧∀j∈I∑SX⁡j=∑ZY⁡j∧n∈I→∀j∈I∑SX⁡j=∑ZY⁡j
69 68 anim1i ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧∀j∈I∑SX⁡j=∑ZY⁡j∧n∈I∧C⁡n=R⁡n→∀j∈I∑SX⁡j=∑ZY⁡j∧C⁡n=R⁡n
70 1 2 3 4 5 gsmsymgreqlem1 ⊢N∈Fin∧M∈Fin∧n∈I∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→∀j∈I∑SX⁡j=∑ZY⁡j∧C⁡n=R⁡n→∑SX++⟨“C”⟩⁡n=∑ZY++⟨“R”⟩⁡n
71 70 imp ⊢N∈Fin∧M∈Fin∧n∈I∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧∀j∈I∑SX⁡j=∑ZY⁡j∧C⁡n=R⁡n→∑SX++⟨“C”⟩⁡n=∑ZY++⟨“R”⟩⁡n
72 66 67 69 71 syl21anc ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧∀j∈I∑SX⁡j=∑ZY⁡j∧n∈I∧C⁡n=R⁡n→∑SX++⟨“C”⟩⁡n=∑ZY++⟨“R”⟩⁡n
73 72 ex ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧∀j∈I∑SX⁡j=∑ZY⁡j∧n∈I→C⁡n=R⁡n→∑SX++⟨“C”⟩⁡n=∑ZY++⟨“R”⟩⁡n
74 73 ralimdva ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧∀j∈I∑SX⁡j=∑ZY⁡j→∀n∈IC⁡n=R⁡n→∀n∈I∑SX++⟨“C”⟩⁡n=∑ZY++⟨“R”⟩⁡n
75 74 expcom ⊢∀j∈I∑SX⁡j=∑ZY⁡j→N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→∀n∈IC⁡n=R⁡n→∀n∈I∑SX++⟨“C”⟩⁡n=∑ZY++⟨“R”⟩⁡n
76 61 75 sylbi ⊢∀n∈I∑SX⁡n=∑ZY⁡n→N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→∀n∈IC⁡n=R⁡n→∀n∈I∑SX++⟨“C”⟩⁡n=∑ZY++⟨“R”⟩⁡n
77 76 com23 ⊢∀n∈I∑SX⁡n=∑ZY⁡n→∀n∈IC⁡n=R⁡n→N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→∀n∈I∑SX++⟨“C”⟩⁡n=∑ZY++⟨“R”⟩⁡n
78 57 77 syl ⊢∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n∧∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n→∀n∈I∑SX⁡n=∑ZY⁡n→∀n∈IC⁡n=R⁡n→N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→∀n∈I∑SX++⟨“C”⟩⁡n=∑ZY++⟨“R”⟩⁡n
79 78 impancom ⊢∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n∧∀n∈IC⁡n=R⁡n→∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n→∀n∈I∑SX⁡n=∑ZY⁡n→N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→∀n∈I∑SX++⟨“C”⟩⁡n=∑ZY++⟨“R”⟩⁡n
80 79 com13 ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n→∀n∈I∑SX⁡n=∑ZY⁡n→∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n∧∀n∈IC⁡n=R⁡n→∀n∈I∑SX++⟨“C”⟩⁡n=∑ZY++⟨“R”⟩⁡n
81 80 imp ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n→∀n∈I∑SX⁡n=∑ZY⁡n→∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n∧∀n∈IC⁡n=R⁡n→∀n∈I∑SX++⟨“C”⟩⁡n=∑ZY++⟨“R”⟩⁡n
82 56 81 sylbid ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y∧∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n→∀n∈I∑SX⁡n=∑ZY⁡n→∀i∈0..^X++⟨“C”⟩∀n∈IX++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n→∀n∈I∑SX++⟨“C”⟩⁡n=∑ZY++⟨“R”⟩⁡n
83 82 ex ⊢N∈Fin∧M∈Fin∧X∈WordB∧C∈B∧Y∈WordP∧R∈P∧X=Y→∀i∈0..^X∀n∈IX⁡i⁡n=Y⁡i⁡n→∀n∈I∑SX⁡n=∑ZY⁡n→∀i∈0..^X++⟨“C”⟩∀n∈IX++⟨“C”⟩⁡i⁡n=Y++⟨“R”⟩⁡i⁡n→∀n∈I∑SX++⟨“C”⟩⁡n=∑ZY++⟨“R”⟩⁡n