Metamath Proof Explorer

Theorem gsmsymgreq

Description: Two combination of permutations moves an element of the intersection of the base sets of the permutations to the same element if each pair of corresponding permutations moves such an element to the same element. (Contributed by AV, 20-Jan-2019)

Ref Expression
Hypotheses gsmsymgrfix.s ⊢ 𝑆 = ( SymGrp ‘ 𝑁 )
gsmsymgrfix.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
gsmsymgreq.z ⊢ 𝑍 = ( SymGrp ‘ 𝑀 )
gsmsymgreq.p ⊢ 𝑃 = ( Base ‘ 𝑍 )
gsmsymgreq.i ⊢ 𝐼 = ( 𝑁 ∩ 𝑀 )
Assertion gsmsymgreq ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝑊 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝑃 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑊 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s ⊢ 𝑆 = ( SymGrp ‘ 𝑁 )
2 gsmsymgrfix.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 gsmsymgreq.z ⊢ 𝑍 = ( SymGrp ‘ 𝑀 )
4 gsmsymgreq.p ⊢ 𝑃 = ( Base ‘ 𝑍 )
5 gsmsymgreq.i ⊢ 𝐼 = ( 𝑁 ∩ 𝑀 )
6 fveq2 ⊢ ( 𝑤 = ∅ → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ∅ ) )
7 6 oveq2d ⊢ ( 𝑤 = ∅ → ( 0 ..^ ( ♯ ‘ 𝑤 ) ) = ( 0 ..^ ( ♯ ‘ ∅ ) ) )
8 7 adantr ⊢ ( ( 𝑤 = ∅ ∧ 𝑢 = ∅ ) → ( 0 ..^ ( ♯ ‘ 𝑤 ) ) = ( 0 ..^ ( ♯ ‘ ∅ ) ) )
9 fveq1 ⊢ ( 𝑤 = ∅ → ( 𝑤 ‘ 𝑖 ) = ( ∅ ‘ 𝑖 ) )
10 9 fveq1d ⊢ ( 𝑤 = ∅ → ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ∅ ‘ 𝑖 ) ‘ 𝑛 ) )
11 fveq1 ⊢ ( 𝑢 = ∅ → ( 𝑢 ‘ 𝑖 ) = ( ∅ ‘ 𝑖 ) )
12 11 fveq1d ⊢ ( 𝑢 = ∅ → ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ∅ ‘ 𝑖 ) ‘ 𝑛 ) )
13 10 12 eqeqan12d ⊢ ( ( 𝑤 = ∅ ∧ 𝑢 = ∅ ) → ( ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ( ( ∅ ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ∅ ‘ 𝑖 ) ‘ 𝑛 ) ) )
14 13 ralbidv ⊢ ( ( 𝑤 = ∅ ∧ 𝑢 = ∅ ) → ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐼 ( ( ∅ ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ∅ ‘ 𝑖 ) ‘ 𝑛 ) ) )
15 8 14 raleqbidv ⊢ ( ( 𝑤 = ∅ ∧ 𝑢 = ∅ ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) ∀ 𝑛 ∈ 𝐼 ( ( ∅ ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ∅ ‘ 𝑖 ) ‘ 𝑛 ) ) )
16 oveq2 ⊢ ( 𝑤 = ∅ → ( 𝑆 Σg 𝑤 ) = ( 𝑆 Σg ∅ ) )
17 16 fveq1d ⊢ ( 𝑤 = ∅ → ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑆 Σg ∅ ) ‘ 𝑛 ) )
18 oveq2 ⊢ ( 𝑢 = ∅ → ( 𝑍 Σg 𝑢 ) = ( 𝑍 Σg ∅ ) )
19 18 fveq1d ⊢ ( 𝑢 = ∅ → ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) = ( ( 𝑍 Σg ∅ ) ‘ 𝑛 ) )
20 17 19 eqeqan12d ⊢ ( ( 𝑤 = ∅ ∧ 𝑢 = ∅ ) → ( ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) ↔ ( ( 𝑆 Σg ∅ ) ‘ 𝑛 ) = ( ( 𝑍 Σg ∅ ) ‘ 𝑛 ) ) )
21 20 ralbidv ⊢ ( ( 𝑤 = ∅ ∧ 𝑢 = ∅ ) → ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg ∅ ) ‘ 𝑛 ) = ( ( 𝑍 Σg ∅ ) ‘ 𝑛 ) ) )
22 15 21 imbi12d ⊢ ( ( 𝑤 = ∅ ∧ 𝑢 = ∅ ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) ∀ 𝑛 ∈ 𝐼 ( ( ∅ ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ∅ ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg ∅ ) ‘ 𝑛 ) = ( ( 𝑍 Σg ∅ ) ‘ 𝑛 ) ) ) )
23 22 imbi2d ⊢ ( ( 𝑤 = ∅ ∧ 𝑢 = ∅ ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) ) ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) ∀ 𝑛 ∈ 𝐼 ( ( ∅ ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ∅ ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg ∅ ) ‘ 𝑛 ) = ( ( 𝑍 Σg ∅ ) ‘ 𝑛 ) ) ) ) )
24 fveq2 ⊢ ( 𝑤 = 𝑥 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑥 ) )
25 24 oveq2d ⊢ ( 𝑤 = 𝑥 → ( 0 ..^ ( ♯ ‘ 𝑤 ) ) = ( 0 ..^ ( ♯ ‘ 𝑥 ) ) )
26 25 adantr ⊢ ( ( 𝑤 = 𝑥 ∧ 𝑢 = 𝑦 ) → ( 0 ..^ ( ♯ ‘ 𝑤 ) ) = ( 0 ..^ ( ♯ ‘ 𝑥 ) ) )
27 fveq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ‘ 𝑖 ) = ( 𝑥 ‘ 𝑖 ) )
28 27 fveq1d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑛 ) )
29 fveq1 ⊢ ( 𝑢 = 𝑦 → ( 𝑢 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) )
30 29 fveq1d ⊢ ( 𝑢 = 𝑦 → ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑛 ) )
31 28 30 eqeqan12d ⊢ ( ( 𝑤 = 𝑥 ∧ 𝑢 = 𝑦 ) → ( ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑛 ) ) )
32 31 ralbidv ⊢ ( ( 𝑤 = 𝑥 ∧ 𝑢 = 𝑦 ) → ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐼 ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑛 ) ) )
33 26 32 raleqbidv ⊢ ( ( 𝑤 = 𝑥 ∧ 𝑢 = 𝑦 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑛 ) ) )
34 oveq2 ⊢ ( 𝑤 = 𝑥 → ( 𝑆 Σg 𝑤 ) = ( 𝑆 Σg 𝑥 ) )
35 34 fveq1d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑆 Σg 𝑥 ) ‘ 𝑛 ) )
36 oveq2 ⊢ ( 𝑢 = 𝑦 → ( 𝑍 Σg 𝑢 ) = ( 𝑍 Σg 𝑦 ) )
37 36 fveq1d ⊢ ( 𝑢 = 𝑦 → ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑦 ) ‘ 𝑛 ) )
38 35 37 eqeqan12d ⊢ ( ( 𝑤 = 𝑥 ∧ 𝑢 = 𝑦 ) → ( ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) ↔ ( ( 𝑆 Σg 𝑥 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑦 ) ‘ 𝑛 ) ) )
39 38 ralbidv ⊢ ( ( 𝑤 = 𝑥 ∧ 𝑢 = 𝑦 ) → ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑥 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑦 ) ‘ 𝑛 ) ) )
40 33 39 imbi12d ⊢ ( ( 𝑤 = 𝑥 ∧ 𝑢 = 𝑦 ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑥 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑦 ) ‘ 𝑛 ) ) ) )
41 40 imbi2d ⊢ ( ( 𝑤 = 𝑥 ∧ 𝑢 = 𝑦 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) ) ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑥 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑦 ) ‘ 𝑛 ) ) ) ) )
42 fveq2 ⊢ ( 𝑤 = ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) )
43 42 oveq2d ⊢ ( 𝑤 = ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) → ( 0 ..^ ( ♯ ‘ 𝑤 ) ) = ( 0 ..^ ( ♯ ‘ ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) ) )
44 43 adantr ⊢ ( ( 𝑤 = ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ∧ 𝑢 = ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) → ( 0 ..^ ( ♯ ‘ 𝑤 ) ) = ( 0 ..^ ( ♯ ‘ ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) ) )
45 fveq1 ⊢ ( 𝑤 = ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) → ( 𝑤 ‘ 𝑖 ) = ( ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ‘ 𝑖 ) )
46 45 fveq1d ⊢ ( 𝑤 = ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) → ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) )
47 fveq1 ⊢ ( 𝑢 = ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) → ( 𝑢 ‘ 𝑖 ) = ( ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) )
48 47 fveq1d ⊢ ( 𝑢 = ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) → ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) )
49 46 48 eqeqan12d ⊢ ( ( 𝑤 = ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ∧ 𝑢 = ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) → ( ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ( ( ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ) )
50 49 ralbidv ⊢ ( ( 𝑤 = ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ∧ 𝑢 = ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) → ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐼 ( ( ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ) )
51 44 50 raleqbidv ⊢ ( ( 𝑤 = ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ∧ 𝑢 = ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) ) ∀ 𝑛 ∈ 𝐼 ( ( ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ) )
52 oveq2 ⊢ ( 𝑤 = ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) → ( 𝑆 Σg 𝑤 ) = ( 𝑆 Σg ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) )
53 52 fveq1d ⊢ ( 𝑤 = ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) → ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑆 Σg ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) ‘ 𝑛 ) )
54 oveq2 ⊢ ( 𝑢 = ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) → ( 𝑍 Σg 𝑢 ) = ( 𝑍 Σg ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) )
55 54 fveq1d ⊢ ( 𝑢 = ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) → ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) ‘ 𝑛 ) )
56 53 55 eqeqan12d ⊢ ( ( 𝑤 = ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ∧ 𝑢 = ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) → ( ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) ↔ ( ( 𝑆 Σg ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) ‘ 𝑛 ) ) )
57 56 ralbidv ⊢ ( ( 𝑤 = ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ∧ 𝑢 = ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) → ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) ‘ 𝑛 ) ) )
58 51 57 imbi12d ⊢ ( ( 𝑤 = ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ∧ 𝑢 = ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) ) ∀ 𝑛 ∈ 𝐼 ( ( ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) ‘ 𝑛 ) ) ) )
59 58 imbi2d ⊢ ( ( 𝑤 = ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ∧ 𝑢 = ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) ) ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) ) ∀ 𝑛 ∈ 𝐼 ( ( ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) ‘ 𝑛 ) ) ) ) )
60 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑊 ) )
61 60 oveq2d ⊢ ( 𝑤 = 𝑊 → ( 0 ..^ ( ♯ ‘ 𝑤 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
62 fveq1 ⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ 𝑖 ) = ( 𝑊 ‘ 𝑖 ) )
63 62 fveq1d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) )
64 63 eqeq1d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) )
65 64 ralbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐼 ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) )
66 61 65 raleqbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) )
67 oveq2 ⊢ ( 𝑤 = 𝑊 → ( 𝑆 Σg 𝑤 ) = ( 𝑆 Σg 𝑊 ) )
68 67 fveq1d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑆 Σg 𝑊 ) ‘ 𝑛 ) )
69 68 eqeq1d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ↔ ( ( 𝑆 Σg 𝑊 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ) )
70 69 ralbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑊 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ) )
71 66 70 imbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑊 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ) ) )
72 71 imbi2d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ) ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑊 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ) ) ) )
73 fveq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) )
74 73 fveq1d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) )
75 74 eqeq2d ⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) )
76 75 ralbidv ⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) )
77 76 ralbidv ⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) ) )
78 oveq2 ⊢ ( 𝑢 = 𝑈 → ( 𝑍 Σg 𝑢 ) = ( 𝑍 Σg 𝑈 ) )
79 78 fveq1d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) )
80 79 eqeq2d ⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) ↔ ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ) )
81 80 ralbidv ⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ) )
82 77 81 imbi12d ⊢ ( 𝑢 = 𝑈 → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ) ) )
83 82 imbi2d ⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑢 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑢 ) ‘ 𝑛 ) ) ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑤 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑤 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ) ) ) )
84 eleq2 ⊢ ( 𝐼 = ( 𝑁 ∩ 𝑀 ) → ( 𝑛 ∈ 𝐼 ↔ 𝑛 ∈ ( 𝑁 ∩ 𝑀 ) ) )
85 elin ⊢ ( 𝑛 ∈ ( 𝑁 ∩ 𝑀 ) ↔ ( 𝑛 ∈ 𝑁 ∧ 𝑛 ∈ 𝑀 ) )
86 84 85 bitrdi ⊢ ( 𝐼 = ( 𝑁 ∩ 𝑀 ) → ( 𝑛 ∈ 𝐼 ↔ ( 𝑛 ∈ 𝑁 ∧ 𝑛 ∈ 𝑀 ) ) )
87 simpl ⊢ ( ( 𝑛 ∈ 𝑁 ∧ 𝑛 ∈ 𝑀 ) → 𝑛 ∈ 𝑁 )
88 86 87 biimtrdi ⊢ ( 𝐼 = ( 𝑁 ∩ 𝑀 ) → ( 𝑛 ∈ 𝐼 → 𝑛 ∈ 𝑁 ) )
89 5 88 ax-mp ⊢ ( 𝑛 ∈ 𝐼 → 𝑛 ∈ 𝑁 )
90 89 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ 𝑛 ∈ 𝐼 ) → 𝑛 ∈ 𝑁 )
91 fvresi ⊢ ( 𝑛 ∈ 𝑁 → ( ( I ↾ 𝑁 ) ‘ 𝑛 ) = 𝑛 )
92 90 91 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ 𝑛 ∈ 𝐼 ) → ( ( I ↾ 𝑁 ) ‘ 𝑛 ) = 𝑛 )
93 simpr ⊢ ( ( 𝑛 ∈ 𝑁 ∧ 𝑛 ∈ 𝑀 ) → 𝑛 ∈ 𝑀 )
94 86 93 biimtrdi ⊢ ( 𝐼 = ( 𝑁 ∩ 𝑀 ) → ( 𝑛 ∈ 𝐼 → 𝑛 ∈ 𝑀 ) )
95 5 94 ax-mp ⊢ ( 𝑛 ∈ 𝐼 → 𝑛 ∈ 𝑀 )
96 95 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ 𝑛 ∈ 𝐼 ) → 𝑛 ∈ 𝑀 )
97 fvresi ⊢ ( 𝑛 ∈ 𝑀 → ( ( I ↾ 𝑀 ) ‘ 𝑛 ) = 𝑛 )
98 96 97 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ 𝑛 ∈ 𝐼 ) → ( ( I ↾ 𝑀 ) ‘ 𝑛 ) = 𝑛 )
99 92 98 eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ 𝑛 ∈ 𝐼 ) → ( ( I ↾ 𝑁 ) ‘ 𝑛 ) = ( ( I ↾ 𝑀 ) ‘ 𝑛 ) )
100 99 ralrimiva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ∀ 𝑛 ∈ 𝐼 ( ( I ↾ 𝑁 ) ‘ 𝑛 ) = ( ( I ↾ 𝑀 ) ‘ 𝑛 ) )
101 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
102 101 gsum0 ⊢ ( 𝑆 Σg ∅ ) = ( 0g ‘ 𝑆 )
103 1 symgid ⊢ ( 𝑁 ∈ Fin → ( I ↾ 𝑁 ) = ( 0g ‘ 𝑆 ) )
104 103 adantr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( I ↾ 𝑁 ) = ( 0g ‘ 𝑆 ) )
105 102 104 eqtr4id ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( 𝑆 Σg ∅ ) = ( I ↾ 𝑁 ) )
106 105 fveq1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ( 𝑆 Σg ∅ ) ‘ 𝑛 ) = ( ( I ↾ 𝑁 ) ‘ 𝑛 ) )
107 eqid ⊢ ( 0g ‘ 𝑍 ) = ( 0g ‘ 𝑍 )
108 107 gsum0 ⊢ ( 𝑍 Σg ∅ ) = ( 0g ‘ 𝑍 )
109 3 symgid ⊢ ( 𝑀 ∈ Fin → ( I ↾ 𝑀 ) = ( 0g ‘ 𝑍 ) )
110 109 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( I ↾ 𝑀 ) = ( 0g ‘ 𝑍 ) )
111 108 110 eqtr4id ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( 𝑍 Σg ∅ ) = ( I ↾ 𝑀 ) )
112 111 fveq1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ( 𝑍 Σg ∅ ) ‘ 𝑛 ) = ( ( I ↾ 𝑀 ) ‘ 𝑛 ) )
113 106 112 eqeq12d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ( ( 𝑆 Σg ∅ ) ‘ 𝑛 ) = ( ( 𝑍 Σg ∅ ) ‘ 𝑛 ) ↔ ( ( I ↾ 𝑁 ) ‘ 𝑛 ) = ( ( I ↾ 𝑀 ) ‘ 𝑛 ) ) )
114 113 ralbidv ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg ∅ ) ‘ 𝑛 ) = ( ( 𝑍 Σg ∅ ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐼 ( ( I ↾ 𝑁 ) ‘ 𝑛 ) = ( ( I ↾ 𝑀 ) ‘ 𝑛 ) ) )
115 100 114 mpbird ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg ∅ ) ‘ 𝑛 ) = ( ( 𝑍 Σg ∅ ) ‘ 𝑛 ) )
116 115 a1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) ∀ 𝑛 ∈ 𝐼 ( ( ∅ ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ∅ ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg ∅ ) ‘ 𝑛 ) = ( ( 𝑍 Σg ∅ ) ‘ 𝑛 ) ) )
117 1 2 3 4 5 gsmsymgreqlem2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑥 ∈ Word 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑦 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑥 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑦 ) ‘ 𝑛 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) ) ∀ 𝑛 ∈ 𝐼 ( ( ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) ‘ 𝑛 ) ) ) )
118 117 expcom ⊢ ( ( ( 𝑥 ∈ Word 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑦 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑥 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑦 ) ‘ 𝑛 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) ) ∀ 𝑛 ∈ 𝐼 ( ( ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) ‘ 𝑛 ) ) ) ) )
119 118 a2d ⊢ ( ( ( 𝑥 ∈ Word 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑦 ∈ Word 𝑃 ∧ 𝑝 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑦 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑥 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑦 ) ‘ 𝑛 ) ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) ) ∀ 𝑛 ∈ 𝐼 ( ( ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg ( 𝑥 ++ ⟨“ 𝑏 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑦 ++ ⟨“ 𝑝 ”⟩ ) ) ‘ 𝑛 ) ) ) ) )
120 23 41 59 72 83 116 119 wrd2ind ⊢ ( ( 𝑊 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝑃 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑊 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ) ) )
121 120 impcom ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( 𝑊 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝑃 ∧ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∀ 𝑛 ∈ 𝐼 ( ( 𝑊 ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑊 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑈 ) ‘ 𝑛 ) ) )