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 = Base S
Assertion gsmsymgrfix ⊢ N ∈ Fin ∧ K ∈ N ∧ W ∈ Word B → ∀ i ∈ 0 ..^ W W ⁡ i ⁡ K = K → ∑ S W ⁡ K = K

Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s ⊢ S = SymGrp ⁡ N
2 gsmsymgrfix.b ⊢ B = Base S
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 ..^ w w ⁡ i ⁡ K = K ↔ ∀ i ∈ ∅ ∅ ⁡ i ⁡ K = K
13 oveq2 ⊢ w = ∅ → ∑ S w = ∑ S ∅
14 13 fveq1d ⊢ w = ∅ → ∑ S w ⁡ K = ∑ S ∅ ⁡ K
15 14 eqeq1d ⊢ w = ∅ → ∑ S w ⁡ K = K ↔ ∑ S ∅ ⁡ K = K
16 12 15 imbi12d ⊢ w = ∅ → ∀ i ∈ 0 ..^ w w ⁡ i ⁡ K = K → ∑ S w ⁡ K = K ↔ ∀ i ∈ ∅ ∅ ⁡ i ⁡ K = K → ∑ S ∅ ⁡ K = K
17 16 imbi2d ⊢ w = ∅ → N ∈ Fin ∧ K ∈ N → ∀ i ∈ 0 ..^ w w ⁡ i ⁡ K = K → ∑ S w ⁡ 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 ..^ w w ⁡ i ⁡ K = K ↔ ∀ i ∈ 0 ..^ y y ⁡ i ⁡ K = K
24 oveq2 ⊢ w = y → ∑ S w = ∑ S y
25 24 fveq1d ⊢ w = y → ∑ S w ⁡ K = ∑ S y ⁡ K
26 25 eqeq1d ⊢ w = y → ∑ S w ⁡ K = K ↔ ∑ S y ⁡ K = K
27 23 26 imbi12d ⊢ w = y → ∀ i ∈ 0 ..^ w w ⁡ i ⁡ K = K → ∑ S w ⁡ K = K ↔ ∀ i ∈ 0 ..^ y y ⁡ i ⁡ K = K → ∑ S y ⁡ K = K
28 27 imbi2d ⊢ w = y → N ∈ Fin ∧ K ∈ N → ∀ i ∈ 0 ..^ w w ⁡ i ⁡ K = K → ∑ S w ⁡ K = K ↔ N ∈ Fin ∧ K ∈ N → ∀ i ∈ 0 ..^ y y ⁡ i ⁡ K = K → ∑ S y ⁡ 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 ..^ w w ⁡ i ⁡ K = K ↔ ∀ i ∈ 0 ..^ y ++ ⟨“ z ”⟩ y ++ ⟨“ z ”⟩ ⁡ i ⁡ K = K
35 oveq2 ⊢ w = y ++ ⟨“ z ”⟩ → ∑ S w = ∑ S y ++ ⟨“ z ”⟩
36 35 fveq1d ⊢ w = y ++ ⟨“ z ”⟩ → ∑ S w ⁡ K = ∑ S y ++ ⟨“ z ”⟩ ⁡ K
37 36 eqeq1d ⊢ w = y ++ ⟨“ z ”⟩ → ∑ S w ⁡ K = K ↔ ∑ S y ++ ⟨“ z ”⟩ ⁡ K = K
38 34 37 imbi12d ⊢ w = y ++ ⟨“ z ”⟩ → ∀ i ∈ 0 ..^ w w ⁡ i ⁡ K = K → ∑ S w ⁡ K = K ↔ ∀ i ∈ 0 ..^ y ++ ⟨“ z ”⟩ y ++ ⟨“ z ”⟩ ⁡ i ⁡ K = K → ∑ S y ++ ⟨“ z ”⟩ ⁡ K = K
39 38 imbi2d ⊢ w = y ++ ⟨“ z ”⟩ → N ∈ Fin ∧ K ∈ N → ∀ i ∈ 0 ..^ w w ⁡ i ⁡ K = K → ∑ S w ⁡ K = K ↔ N ∈ Fin ∧ K ∈ N → ∀ i ∈ 0 ..^ y ++ ⟨“ z ”⟩ y ++ ⟨“ z ”⟩ ⁡ i ⁡ K = K → ∑ S y ++ ⟨“ 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 ..^ w w ⁡ i ⁡ K = K ↔ ∀ i ∈ 0 ..^ W W ⁡ i ⁡ K = K
46 oveq2 ⊢ w = W → ∑ S w = ∑ S W
47 46 fveq1d ⊢ w = W → ∑ S w ⁡ K = ∑ S W ⁡ K
48 47 eqeq1d ⊢ w = W → ∑ S w ⁡ K = K ↔ ∑ S W ⁡ K = K
49 45 48 imbi12d ⊢ w = W → ∀ i ∈ 0 ..^ w w ⁡ i ⁡ K = K → ∑ S w ⁡ K = K ↔ ∀ i ∈ 0 ..^ W W ⁡ i ⁡ K = K → ∑ S W ⁡ K = K
50 49 imbi2d ⊢ w = W → N ∈ Fin ∧ K ∈ N → ∀ i ∈ 0 ..^ w w ⁡ i ⁡ K = K → ∑ S w ⁡ K = K ↔ N ∈ Fin ∧ K ∈ N → ∀ i ∈ 0 ..^ W W ⁡ i ⁡ K = K → ∑ S W ⁡ K = K
51 eqid ⊢ 0 S = 0 S
52 51 gsum0 ⊢ ∑ S ∅ = 0 S
53 1 symgid ⊢ N ∈ Fin → I ↾ N = 0 S
54 53 adantr ⊢ N ∈ Fin ∧ K ∈ N → I ↾ N = 0 S
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 ∈ Word B → y ++ ⟨“ z ”⟩ = y + 1
62 61 oveq2d ⊢ y ∈ Word B → 0 ..^ y ++ ⟨“ z ”⟩ = 0 ..^ y + 1
63 62 raleqdv ⊢ y ∈ Word B → ∀ i ∈ 0 ..^ y ++ ⟨“ z ”⟩ y ++ ⟨“ z ”⟩ ⁡ i ⁡ K = K ↔ ∀ i ∈ 0 ..^ y + 1 y ++ ⟨“ z ”⟩ ⁡ i ⁡ K = K
64 63 adantr ⊢ y ∈ Word B ∧ z ∈ B → ∀ i ∈ 0 ..^ y ++ ⟨“ z ”⟩ y ++ ⟨“ z ”⟩ ⁡ i ⁡ K = K ↔ ∀ i ∈ 0 ..^ y + 1 y ++ ⟨“ z ”⟩ ⁡ i ⁡ K = K
65 64 adantr ⊢ y ∈ Word B ∧ z ∈ B ∧ N ∈ Fin ∧ K ∈ N ∧ ∀ i ∈ 0 ..^ y y ⁡ i ⁡ K = K → ∑ S y ⁡ K = K → ∀ i ∈ 0 ..^ y ++ ⟨“ z ”⟩ y ++ ⟨“ z ”⟩ ⁡ i ⁡ K = K ↔ ∀ i ∈ 0 ..^ y + 1 y ++ ⟨“ z ”⟩ ⁡ i ⁡ K = K
66 1 2 gsmsymgrfixlem1 ⊢ y ∈ Word B ∧ z ∈ B ∧ N ∈ Fin ∧ K ∈ N ∧ ∀ i ∈ 0 ..^ y y ⁡ i ⁡ K = K → ∑ S y ⁡ K = K → ∀ i ∈ 0 ..^ y + 1 y ++ ⟨“ z ”⟩ ⁡ i ⁡ K = K → ∑ S y ++ ⟨“ z ”⟩ ⁡ K = K
67 66 3expb ⊢ y ∈ Word B ∧ z ∈ B ∧ N ∈ Fin ∧ K ∈ N ∧ ∀ i ∈ 0 ..^ y y ⁡ i ⁡ K = K → ∑ S y ⁡ K = K → ∀ i ∈ 0 ..^ y + 1 y ++ ⟨“ z ”⟩ ⁡ i ⁡ K = K → ∑ S y ++ ⟨“ z ”⟩ ⁡ K = K
68 65 67 sylbid ⊢ y ∈ Word B ∧ z ∈ B ∧ N ∈ Fin ∧ K ∈ N ∧ ∀ i ∈ 0 ..^ y y ⁡ i ⁡ K = K → ∑ S y ⁡ K = K → ∀ i ∈ 0 ..^ y ++ ⟨“ z ”⟩ y ++ ⟨“ z ”⟩ ⁡ i ⁡ K = K → ∑ S y ++ ⟨“ z ”⟩ ⁡ K = K
69 68 exp32 ⊢ y ∈ Word B ∧ z ∈ B → N ∈ Fin ∧ K ∈ N → ∀ i ∈ 0 ..^ y y ⁡ i ⁡ K = K → ∑ S y ⁡ K = K → ∀ i ∈ 0 ..^ y ++ ⟨“ z ”⟩ y ++ ⟨“ z ”⟩ ⁡ i ⁡ K = K → ∑ S y ++ ⟨“ z ”⟩ ⁡ K = K
70 69 a2d ⊢ y ∈ Word B ∧ z ∈ B → N ∈ Fin ∧ K ∈ N → ∀ i ∈ 0 ..^ y y ⁡ i ⁡ K = K → ∑ S y ⁡ K = K → N ∈ Fin ∧ K ∈ N → ∀ i ∈ 0 ..^ y ++ ⟨“ z ”⟩ y ++ ⟨“ z ”⟩ ⁡ i ⁡ K = K → ∑ S y ++ ⟨“ z ”⟩ ⁡ K = K
71 17 28 39 50 60 70 wrdind ⊢ W ∈ Word B → N ∈ Fin ∧ K ∈ N → ∀ i ∈ 0 ..^ W W ⁡ i ⁡ K = K → ∑ S W ⁡ K = K
72 71 com12 ⊢ N ∈ Fin ∧ K ∈ N → W ∈ Word B → ∀ i ∈ 0 ..^ W W ⁡ i ⁡ K = K → ∑ S W ⁡ K = K
73 72 3impia ⊢ N ∈ Fin ∧ K ∈ N ∧ W ∈ Word B → ∀ i ∈ 0 ..^ W W ⁡ i ⁡ K = K → ∑ S W ⁡ K = K