Metamath Proof Explorer

Theorem gsmsymgrfixlem1

Description: Lemma 1 for gsmsymgrfix . (Contributed by AV, 20-Jan-2019)

Ref Expression
Hypotheses gsmsymgrfix.s ⊢S=SymGrp⁡N
gsmsymgrfix.b ⊢B=BaseS
Assertion gsmsymgrfixlem1 ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→∀i∈0..^W+1W++⟨“P”⟩⁡i⁡K=K→∑SW++⟨“P”⟩⁡K=K

Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s ⊢S=SymGrp⁡N
2 gsmsymgrfix.b ⊢B=BaseS
3 lencl ⊢W∈WordB→W∈ℕ0
4 elnn0uz ⊢W∈ℕ0↔W∈ℤ≥0
5 3 4 sylib ⊢W∈WordB→W∈ℤ≥0
6 5 adantr ⊢W∈WordB∧P∈B→W∈ℤ≥0
7 6 3ad2ant1 ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→W∈ℤ≥0
8 fzosplitsn ⊢W∈ℤ≥0→0..^W+1=0..^W∪W
9 7 8 syl ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→0..^W+1=0..^W∪W
10 9 raleqdv ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→∀i∈0..^W+1W++⟨“P”⟩⁡i⁡K=K↔∀i∈0..^W∪WW++⟨“P”⟩⁡i⁡K=K
11 3 adantr ⊢W∈WordB∧P∈B→W∈ℕ0
12 11 3ad2ant1 ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→W∈ℕ0
13 fveq2 ⊢i=W→W++⟨“P”⟩⁡i=W++⟨“P”⟩⁡W
14 13 fveq1d ⊢i=W→W++⟨“P”⟩⁡i⁡K=W++⟨“P”⟩⁡W⁡K
15 14 eqeq1d ⊢i=W→W++⟨“P”⟩⁡i⁡K=K↔W++⟨“P”⟩⁡W⁡K=K
16 15 ralunsn ⊢W∈ℕ0→∀i∈0..^W∪WW++⟨“P”⟩⁡i⁡K=K↔∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K∧W++⟨“P”⟩⁡W⁡K=K
17 12 16 syl ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→∀i∈0..^W∪WW++⟨“P”⟩⁡i⁡K=K↔∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K∧W++⟨“P”⟩⁡W⁡K=K
18 10 17 bitrd ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→∀i∈0..^W+1W++⟨“P”⟩⁡i⁡K=K↔∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K∧W++⟨“P”⟩⁡W⁡K=K
19 eqidd ⊢W∈WordB∧P∈B→W=W
20 ccats1val2 ⊢W∈WordB∧P∈B∧W=W→W++⟨“P”⟩⁡W=P
21 20 fveq1d ⊢W∈WordB∧P∈B∧W=W→W++⟨“P”⟩⁡W⁡K=P⁡K
22 21 eqeq1d ⊢W∈WordB∧P∈B∧W=W→W++⟨“P”⟩⁡W⁡K=K↔P⁡K=K
23 19 22 mpd3an3 ⊢W∈WordB∧P∈B→W++⟨“P”⟩⁡W⁡K=K↔P⁡K=K
24 23 3ad2ant1 ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→W++⟨“P”⟩⁡W⁡K=K↔P⁡K=K
25 simprl ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N→N∈Fin
26 simpll ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N→W∈WordB
27 simplr ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N→P∈B
28 1 2 gsumccatsymgsn ⊢N∈Fin∧W∈WordB∧P∈B→∑SW++⟨“P”⟩=∑SW∘P
29 28 fveq1d ⊢N∈Fin∧W∈WordB∧P∈B→∑SW++⟨“P”⟩⁡K=∑SW∘P⁡K
30 25 26 27 29 syl3anc ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N→∑SW++⟨“P”⟩⁡K=∑SW∘P⁡K
31 30 3adant3 ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→∑SW++⟨“P”⟩⁡K=∑SW∘P⁡K
32 31 adantr ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K∧P⁡K=K∧∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K→∑SW++⟨“P”⟩⁡K=∑SW∘P⁡K
33 1 2 symgbasf ⊢P∈B→P:N⟶N
34 33 ffnd ⊢P∈B→PFnN
35 34 adantl ⊢W∈WordB∧P∈B→PFnN
36 simpr ⊢N∈Fin∧K∈N→K∈N
37 fvco2 ⊢PFnN∧K∈N→∑SW∘P⁡K=∑SW⁡P⁡K
38 35 36 37 syl2an ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N→∑SW∘P⁡K=∑SW⁡P⁡K
39 38 3adant3 ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→∑SW∘P⁡K=∑SW⁡P⁡K
40 39 adantr ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K∧P⁡K=K∧∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K→∑SW∘P⁡K=∑SW⁡P⁡K
41 fveq2 ⊢P⁡K=K→∑SW⁡P⁡K=∑SW⁡K
42 41 ad2antrl ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K∧P⁡K=K∧∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K→∑SW⁡P⁡K=∑SW⁡K
43 ccats1val1 ⊢W∈WordB∧i∈0..^W→W++⟨“P”⟩⁡i=W⁡i
44 43 ad4ant14 ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧i∈0..^W→W++⟨“P”⟩⁡i=W⁡i
45 44 fveq1d ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧i∈0..^W→W++⟨“P”⟩⁡i⁡K=W⁡i⁡K
46 45 eqeq1d ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧i∈0..^W→W++⟨“P”⟩⁡i⁡K=K↔W⁡i⁡K=K
47 46 ralbidva ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N→∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K↔∀i∈0..^WW⁡i⁡K=K
48 47 biimpd ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N→∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K→∀i∈0..^WW⁡i⁡K=K
49 48 adantld ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N→P⁡K=K∧∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K→∀i∈0..^WW⁡i⁡K=K
50 49 3adant3 ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→P⁡K=K∧∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K→∀i∈0..^WW⁡i⁡K=K
51 simp3 ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K
52 50 51 syld ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→P⁡K=K∧∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K→∑SW⁡K=K
53 52 imp ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K∧P⁡K=K∧∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K→∑SW⁡K=K
54 42 53 eqtrd ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K∧P⁡K=K∧∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K→∑SW⁡P⁡K=K
55 32 40 54 3eqtrd ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K∧P⁡K=K∧∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K→∑SW++⟨“P”⟩⁡K=K
56 55 exp32 ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→P⁡K=K→∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K→∑SW++⟨“P”⟩⁡K=K
57 24 56 sylbid ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→W++⟨“P”⟩⁡W⁡K=K→∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K→∑SW++⟨“P”⟩⁡K=K
58 57 impcomd ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→∀i∈0..^WW++⟨“P”⟩⁡i⁡K=K∧W++⟨“P”⟩⁡W⁡K=K→∑SW++⟨“P”⟩⁡K=K
59 18 58 sylbid ⊢W∈WordB∧P∈B∧N∈Fin∧K∈N∧∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K→∀i∈0..^W+1W++⟨“P”⟩⁡i⁡K=K→∑SW++⟨“P”⟩⁡K=K