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 ⊢ 𝑆 = ( SymGrp ‘ 𝑁 )
gsmsymgrfix.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
Assertion gsmsymgrfix ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ∧ 𝑊 ∈ Word 𝐵 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) )

Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s ⊢ 𝑆 = ( SymGrp ‘ 𝑁 )
2 gsmsymgrfix.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 hasheq0 ⊢ ( 𝑤 ∈ V → ( ( ♯ ‘ 𝑤 ) = 0 ↔ 𝑤 = ∅ ) )
4 3 elv ⊢ ( ( ♯ ‘ 𝑤 ) = 0 ↔ 𝑤 = ∅ )
5 4 biimpri ⊢ ( 𝑤 = ∅ → ( ♯ ‘ 𝑤 ) = 0 )
6 5 oveq2d ⊢ ( 𝑤 = ∅ → ( 0 ..^ ( ♯ ‘ 𝑤 ) ) = ( 0 ..^ 0 ) )
7 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
8 6 7 eqtrdi ⊢ ( 𝑤 = ∅ → ( 0 ..^ ( ♯ ‘ 𝑤 ) ) = ∅ )
9 fveq1 ⊢ ( 𝑤 = ∅ → ( 𝑤 ‘ 𝑖 ) = ( ∅ ‘ 𝑖 ) )
10 9 fveq1d ⊢ ( 𝑤 = ∅ → ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = ( ( ∅ ‘ 𝑖 ) ‘ 𝐾 ) )
11 10 eqeq1d ⊢ ( 𝑤 = ∅ → ( ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ( ( ∅ ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
12 8 11 raleqbidv ⊢ ( 𝑤 = ∅ → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ∀ 𝑖 ∈ ∅ ( ( ∅ ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
13 oveq2 ⊢ ( 𝑤 = ∅ → ( 𝑆 Σg 𝑤 ) = ( 𝑆 Σg ∅ ) )
14 13 fveq1d ⊢ ( 𝑤 = ∅ → ( ( 𝑆 Σg 𝑤 ) ‘ 𝐾 ) = ( ( 𝑆 Σg ∅ ) ‘ 𝐾 ) )
15 14 eqeq1d ⊢ ( 𝑤 = ∅ → ( ( ( 𝑆 Σg 𝑤 ) ‘ 𝐾 ) = 𝐾 ↔ ( ( 𝑆 Σg ∅ ) ‘ 𝐾 ) = 𝐾 ) )
16 12 15 imbi12d ⊢ ( 𝑤 = ∅ → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑤 ) ‘ 𝐾 ) = 𝐾 ) ↔ ( ∀ 𝑖 ∈ ∅ ( ( ∅ ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ∅ ) ‘ 𝐾 ) = 𝐾 ) ) )
17 16 imbi2d ⊢ ( 𝑤 = ∅ → ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑤 ) ‘ 𝐾 ) = 𝐾 ) ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ ∅ ( ( ∅ ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ∅ ) ‘ 𝐾 ) = 𝐾 ) ) ) )
18 fveq2 ⊢ ( 𝑤 = 𝑦 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑦 ) )
19 18 oveq2d ⊢ ( 𝑤 = 𝑦 → ( 0 ..^ ( ♯ ‘ 𝑤 ) ) = ( 0 ..^ ( ♯ ‘ 𝑦 ) ) )
20 fveq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) )
21 20 fveq1d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = ( ( 𝑦 ‘ 𝑖 ) ‘ 𝐾 ) )
22 21 eqeq1d ⊢ ( 𝑤 = 𝑦 → ( ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ( ( 𝑦 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
23 19 22 raleqbidv ⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑦 ) ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
24 oveq2 ⊢ ( 𝑤 = 𝑦 → ( 𝑆 Σg 𝑤 ) = ( 𝑆 Σg 𝑦 ) )
25 24 fveq1d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑆 Σg 𝑤 ) ‘ 𝐾 ) = ( ( 𝑆 Σg 𝑦 ) ‘ 𝐾 ) )
26 25 eqeq1d ⊢ ( 𝑤 = 𝑦 → ( ( ( 𝑆 Σg 𝑤 ) ‘ 𝐾 ) = 𝐾 ↔ ( ( 𝑆 Σg 𝑦 ) ‘ 𝐾 ) = 𝐾 ) )
27 23 26 imbi12d ⊢ ( 𝑤 = 𝑦 → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑤 ) ‘ 𝐾 ) = 𝐾 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑦 ) ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑦 ) ‘ 𝐾 ) = 𝐾 ) ) )
28 27 imbi2d ⊢ ( 𝑤 = 𝑦 → ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑤 ) ‘ 𝐾 ) = 𝐾 ) ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑦 ) ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑦 ) ‘ 𝐾 ) = 𝐾 ) ) ) )
29 fveq2 ⊢ ( 𝑤 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) )
30 29 oveq2d ⊢ ( 𝑤 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( 0 ..^ ( ♯ ‘ 𝑤 ) ) = ( 0 ..^ ( ♯ ‘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) )
31 fveq1 ⊢ ( 𝑤 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( 𝑤 ‘ 𝑖 ) = ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) )
32 31 fveq1d ⊢ ( 𝑤 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = ( ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) )
33 32 eqeq1d ⊢ ( 𝑤 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ( ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
34 30 33 raleqbidv ⊢ ( 𝑤 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) ( ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
35 oveq2 ⊢ ( 𝑤 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( 𝑆 Σg 𝑤 ) = ( 𝑆 Σg ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) )
36 35 fveq1d ⊢ ( 𝑤 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( ( 𝑆 Σg 𝑤 ) ‘ 𝐾 ) = ( ( 𝑆 Σg ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ‘ 𝐾 ) )
37 36 eqeq1d ⊢ ( 𝑤 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( ( ( 𝑆 Σg 𝑤 ) ‘ 𝐾 ) = 𝐾 ↔ ( ( 𝑆 Σg ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ‘ 𝐾 ) = 𝐾 ) )
38 34 37 imbi12d ⊢ ( 𝑤 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑤 ) ‘ 𝐾 ) = 𝐾 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) ( ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ‘ 𝐾 ) = 𝐾 ) ) )
39 38 imbi2d ⊢ ( 𝑤 = ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) → ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑤 ) ‘ 𝐾 ) = 𝐾 ) ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) ( ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ‘ 𝐾 ) = 𝐾 ) ) ) )
40 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑊 ) )
41 40 oveq2d ⊢ ( 𝑤 = 𝑊 → ( 0 ..^ ( ♯ ‘ 𝑤 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
42 fveq1 ⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) )
43 42 fveq1d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) )
44 43 eqeq1d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
45 41 44 raleqbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
46 oveq2 ⊢ ( 𝑤 = 𝑊 → ( 𝑆 Σg 𝑤 ) = ( 𝑆 Σg 𝑊 ) )
47 46 fveq1d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑆 Σg 𝑤 ) ‘ 𝐾 ) = ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) )
48 47 eqeq1d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑆 Σg 𝑤 ) ‘ 𝐾 ) = 𝐾 ↔ ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) )
49 45 48 imbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑤 ) ‘ 𝐾 ) = 𝐾 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) )
50 49 imbi2d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ( ( 𝑤 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑤 ) ‘ 𝐾 ) = 𝐾 ) ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) ) )
51 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
52 51 gsum0 ⊢ ( 𝑆 Σg ∅ ) = ( 0g ‘ 𝑆 )
53 1 symgid ⊢ ( 𝑁 ∈ Fin → ( I ↾ 𝑁 ) = ( 0g ‘ 𝑆 ) )
54 53 adantr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( I ↾ 𝑁 ) = ( 0g ‘ 𝑆 ) )
55 52 54 eqtr4id ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( 𝑆 Σg ∅ ) = ( I ↾ 𝑁 ) )
56 55 fveq1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ( 𝑆 Σg ∅ ) ‘ 𝐾 ) = ( ( I ↾ 𝑁 ) ‘ 𝐾 ) )
57 fvresi ⊢ ( 𝐾 ∈ 𝑁 → ( ( I ↾ 𝑁 ) ‘ 𝐾 ) = 𝐾 )
58 57 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ( I ↾ 𝑁 ) ‘ 𝐾 ) = 𝐾 )
59 56 58 eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ( 𝑆 Σg ∅ ) ‘ 𝐾 ) = 𝐾 )
60 59 a1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ ∅ ( ( ∅ ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ∅ ) ‘ 𝐾 ) = 𝐾 ) )
61 ccatws1len ⊢ ( 𝑦 ∈ Word 𝐵 → ( ♯ ‘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) = ( ( ♯ ‘ 𝑦 ) + 1 ) )
62 61 oveq2d ⊢ ( 𝑦 ∈ Word 𝐵 → ( 0 ..^ ( ♯ ‘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
63 62 raleqdv ⊢ ( 𝑦 ∈ Word 𝐵 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) ( ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ( ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
64 63 adantr ⊢ ( ( 𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) ( ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ( ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
65 64 adantr ⊢ ( ( ( 𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑦 ) ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑦 ) ‘ 𝐾 ) = 𝐾 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) ( ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ( ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 ) )
66 1 2 gsmsymgrfixlem1 ⊢ ( ( ( 𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑦 ) ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑦 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ( ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ‘ 𝐾 ) = 𝐾 ) )
67 66 3expb ⊢ ( ( ( 𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑦 ) ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑦 ) ‘ 𝐾 ) = 𝐾 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑦 ) + 1 ) ) ( ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ‘ 𝐾 ) = 𝐾 ) )
68 65 67 sylbid ⊢ ( ( ( 𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑦 ) ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑦 ) ‘ 𝐾 ) = 𝐾 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) ( ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ‘ 𝐾 ) = 𝐾 ) )
69 68 exp32 ⊢ ( ( 𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑦 ) ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑦 ) ‘ 𝐾 ) = 𝐾 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) ( ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ‘ 𝐾 ) = 𝐾 ) ) ) )
70 69 a2d ⊢ ( ( 𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑦 ) ) ( ( 𝑦 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑦 ) ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ) ( ( ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg ( 𝑦 ++ ⟨“ 𝑧 ”⟩ ) ) ‘ 𝐾 ) = 𝐾 ) ) ) )
71 17 28 39 50 60 70 wrdind ⊢ ( 𝑊 ∈ Word 𝐵 → ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) )
72 71 com12 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ) → ( 𝑊 ∈ Word 𝐵 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) ) )
73 72 3impia ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁 ∧ 𝑊 ∈ Word 𝐵 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( ( 𝑊 ‘ 𝑖 ) ‘ 𝐾 ) = 𝐾 → ( ( 𝑆 Σg 𝑊 ) ‘ 𝐾 ) = 𝐾 ) )