Metamath Proof Explorer

Theorem gsmsymgrfix

Description: The composition of permutations fixing one element also fixes this element. (Contributed by AV, 20-Jan-2019)

Ref Expression
Hypotheses gsmsymgrfix.s ⊢S=SymGrp⁡N
gsmsymgrfix.b ⊢B=BaseS
Assertion gsmsymgrfix ⊢N∈Fin∧K∈N∧W∈WordB→∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K

Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s ⊢S=SymGrp⁡N
2 gsmsymgrfix.b ⊢B=BaseS
3 hasheq0 ⊢w∈V→w=0↔w=∅
4 3 elv ⊢w=0↔w=∅
5 4 biimpri ⊢w=∅→w=0
6 5 oveq2d ⊢w=∅→0..^w=0..^0
7 fzo0 ⊢0..^0=∅
8 6 7 eqtrdi ⊢w=∅→0..^w=∅
9 fveq1 ⊢w=∅→w⁡i=∅⁡i
10 9 fveq1d ⊢w=∅→w⁡i⁡K=∅⁡i⁡K
11 10 eqeq1d ⊢w=∅→w⁡i⁡K=K↔∅⁡i⁡K=K
12 8 11 raleqbidv ⊢w=∅→∀i∈0..^ww⁡i⁡K=K↔∀i∈∅∅⁡i⁡K=K
13 oveq2 ⊢w=∅→∑Sw=∑S∅
14 13 fveq1d ⊢w=∅→∑Sw⁡K=∑S∅⁡K
15 14 eqeq1d ⊢w=∅→∑Sw⁡K=K↔∑S∅⁡K=K
16 12 15 imbi12d ⊢w=∅→∀i∈0..^ww⁡i⁡K=K→∑Sw⁡K=K↔∀i∈∅∅⁡i⁡K=K→∑S∅⁡K=K
17 16 imbi2d ⊢w=∅→N∈Fin∧K∈N→∀i∈0..^ww⁡i⁡K=K→∑Sw⁡K=K↔N∈Fin∧K∈N→∀i∈∅∅⁡i⁡K=K→∑S∅⁡K=K
18 fveq2 ⊢w=y→w=y
19 18 oveq2d ⊢w=y→0..^w=0..^y
20 fveq1 ⊢w=y→w⁡i=y⁡i
21 20 fveq1d ⊢w=y→w⁡i⁡K=y⁡i⁡K
22 21 eqeq1d ⊢w=y→w⁡i⁡K=K↔y⁡i⁡K=K
23 19 22 raleqbidv ⊢w=y→∀i∈0..^ww⁡i⁡K=K↔∀i∈0..^yy⁡i⁡K=K
24 oveq2 ⊢w=y→∑Sw=∑Sy
25 24 fveq1d ⊢w=y→∑Sw⁡K=∑Sy⁡K
26 25 eqeq1d ⊢w=y→∑Sw⁡K=K↔∑Sy⁡K=K
27 23 26 imbi12d ⊢w=y→∀i∈0..^ww⁡i⁡K=K→∑Sw⁡K=K↔∀i∈0..^yy⁡i⁡K=K→∑Sy⁡K=K
28 27 imbi2d ⊢w=y→N∈Fin∧K∈N→∀i∈0..^ww⁡i⁡K=K→∑Sw⁡K=K↔N∈Fin∧K∈N→∀i∈0..^yy⁡i⁡K=K→∑Sy⁡K=K
29 fveq2 ⊢w=y++⟨“z”⟩→w=y++⟨“z”⟩
30 29 oveq2d ⊢w=y++⟨“z”⟩→0..^w=0..^y++⟨“z”⟩
31 fveq1 ⊢w=y++⟨“z”⟩→w⁡i=y++⟨“z”⟩⁡i
32 31 fveq1d ⊢w=y++⟨“z”⟩→w⁡i⁡K=y++⟨“z”⟩⁡i⁡K
33 32 eqeq1d ⊢w=y++⟨“z”⟩→w⁡i⁡K=K↔y++⟨“z”⟩⁡i⁡K=K
34 30 33 raleqbidv ⊢w=y++⟨“z”⟩→∀i∈0..^ww⁡i⁡K=K↔∀i∈0..^y++⟨“z”⟩y++⟨“z”⟩⁡i⁡K=K
35 oveq2 ⊢w=y++⟨“z”⟩→∑Sw=∑Sy++⟨“z”⟩
36 35 fveq1d ⊢w=y++⟨“z”⟩→∑Sw⁡K=∑Sy++⟨“z”⟩⁡K
37 36 eqeq1d ⊢w=y++⟨“z”⟩→∑Sw⁡K=K↔∑Sy++⟨“z”⟩⁡K=K
38 34 37 imbi12d ⊢w=y++⟨“z”⟩→∀i∈0..^ww⁡i⁡K=K→∑Sw⁡K=K↔∀i∈0..^y++⟨“z”⟩y++⟨“z”⟩⁡i⁡K=K→∑Sy++⟨“z”⟩⁡K=K
39 38 imbi2d ⊢w=y++⟨“z”⟩→N∈Fin∧K∈N→∀i∈0..^ww⁡i⁡K=K→∑Sw⁡K=K↔N∈Fin∧K∈N→∀i∈0..^y++⟨“z”⟩y++⟨“z”⟩⁡i⁡K=K→∑Sy++⟨“z”⟩⁡K=K
40 fveq2 ⊢w=W→w=W
41 40 oveq2d ⊢w=W→0..^w=0..^W
42 fveq1 ⊢w=W→w⁡i=W⁡i
43 42 fveq1d ⊢w=W→w⁡i⁡K=W⁡i⁡K
44 43 eqeq1d ⊢w=W→w⁡i⁡K=K↔W⁡i⁡K=K
45 41 44 raleqbidv ⊢w=W→∀i∈0..^ww⁡i⁡K=K↔∀i∈0..^WW⁡i⁡K=K
46 oveq2 ⊢w=W→∑Sw=∑SW
47 46 fveq1d ⊢w=W→∑Sw⁡K=∑SW⁡K
48 47 eqeq1d ⊢w=W→∑Sw⁡K=K↔∑SW⁡K=K
49 45 48 imbi12d ⊢w=W→∀i∈0..^ww⁡i⁡K=K→∑Sw⁡K=K↔∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K
50 49 imbi2d ⊢w=W→N∈Fin∧K∈N→∀i∈0..^ww⁡i⁡K=K→∑Sw⁡K=K↔N∈Fin∧K∈N→∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K
51 eqid ⊢0S=0S
52 51 gsum0 ⊢∑S∅=0S
53 1 symgid ⊢N∈Fin→I↾N=0S
54 53 adantr ⊢N∈Fin∧K∈N→I↾N=0S
55 52 54 eqtr4id ⊢N∈Fin∧K∈N→∑S∅=I↾N
56 55 fveq1d ⊢N∈Fin∧K∈N→∑S∅⁡K=I↾N⁡K
57 fvresi ⊢K∈N→I↾N⁡K=K
58 57 adantl ⊢N∈Fin∧K∈N→I↾N⁡K=K
59 56 58 eqtrd ⊢N∈Fin∧K∈N→∑S∅⁡K=K
60 59 a1d ⊢N∈Fin∧K∈N→∀i∈∅∅⁡i⁡K=K→∑S∅⁡K=K
61 ccatws1len ⊢y∈WordB→y++⟨“z”⟩=y+1
62 61 oveq2d ⊢y∈WordB→0..^y++⟨“z”⟩=0..^y+1
63 62 raleqdv ⊢y∈WordB→∀i∈0..^y++⟨“z”⟩y++⟨“z”⟩⁡i⁡K=K↔∀i∈0..^y+1y++⟨“z”⟩⁡i⁡K=K
64 63 adantr ⊢y∈WordB∧z∈B→∀i∈0..^y++⟨“z”⟩y++⟨“z”⟩⁡i⁡K=K↔∀i∈0..^y+1y++⟨“z”⟩⁡i⁡K=K
65 64 adantr ⊢y∈WordB∧z∈B∧N∈Fin∧K∈N∧∀i∈0..^yy⁡i⁡K=K→∑Sy⁡K=K→∀i∈0..^y++⟨“z”⟩y++⟨“z”⟩⁡i⁡K=K↔∀i∈0..^y+1y++⟨“z”⟩⁡i⁡K=K
66 1 2 gsmsymgrfixlem1 ⊢y∈WordB∧z∈B∧N∈Fin∧K∈N∧∀i∈0..^yy⁡i⁡K=K→∑Sy⁡K=K→∀i∈0..^y+1y++⟨“z”⟩⁡i⁡K=K→∑Sy++⟨“z”⟩⁡K=K
67 66 3expb ⊢y∈WordB∧z∈B∧N∈Fin∧K∈N∧∀i∈0..^yy⁡i⁡K=K→∑Sy⁡K=K→∀i∈0..^y+1y++⟨“z”⟩⁡i⁡K=K→∑Sy++⟨“z”⟩⁡K=K
68 65 67 sylbid ⊢y∈WordB∧z∈B∧N∈Fin∧K∈N∧∀i∈0..^yy⁡i⁡K=K→∑Sy⁡K=K→∀i∈0..^y++⟨“z”⟩y++⟨“z”⟩⁡i⁡K=K→∑Sy++⟨“z”⟩⁡K=K
69 68 exp32 ⊢y∈WordB∧z∈B→N∈Fin∧K∈N→∀i∈0..^yy⁡i⁡K=K→∑Sy⁡K=K→∀i∈0..^y++⟨“z”⟩y++⟨“z”⟩⁡i⁡K=K→∑Sy++⟨“z”⟩⁡K=K
70 69 a2d ⊢y∈WordB∧z∈B→N∈Fin∧K∈N→∀i∈0..^yy⁡i⁡K=K→∑Sy⁡K=K→N∈Fin∧K∈N→∀i∈0..^y++⟨“z”⟩y++⟨“z”⟩⁡i⁡K=K→∑Sy++⟨“z”⟩⁡K=K
71 17 28 39 50 60 70 wrdind ⊢W∈WordB→N∈Fin∧K∈N→∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K
72 71 com12 ⊢N∈Fin∧K∈N→W∈WordB→∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K
73 72 3impia ⊢N∈Fin∧K∈N∧W∈WordB→∀i∈0..^WW⁡i⁡K=K→∑SW⁡K=K