# Metamath Proof Explorer

## Theorem gsmsymgreqlem2

Description: Lemma 2 for gsmsymgreq . (Contributed by AV, 26-Jan-2019)

Ref Expression
Hypotheses gsmsymgrfix.s 𝑆 = ( SymGrp ‘ 𝑁 )
gsmsymgrfix.b 𝐵 = ( Base ‘ 𝑆 )
gsmsymgreq.z 𝑍 = ( SymGrp ‘ 𝑀 )
gsmsymgreq.p 𝑃 = ( Base ‘ 𝑍 )
gsmsymgreq.i 𝐼 = ( 𝑁𝑀 )
Assertion gsmsymgreqlem2 ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ) → ( ∀ 𝑖 ∈ ( 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 ccatws1len ( 𝑋 ∈ Word 𝐵 → ( ♯ ‘ ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) = ( ( ♯ ‘ 𝑋 ) + 1 ) )
7 6 oveq2d ( 𝑋 ∈ Word 𝐵 → ( 0 ..^ ( ♯ ‘ ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑋 ) + 1 ) ) )
8 lencl ( 𝑋 ∈ Word 𝐵 → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
9 elnn0uz ( ( ♯ ‘ 𝑋 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑋 ) ∈ ( ℤ ‘ 0 ) )
10 8 9 sylib ( 𝑋 ∈ Word 𝐵 → ( ♯ ‘ 𝑋 ) ∈ ( ℤ ‘ 0 ) )
11 fzosplitsn ( ( ♯ ‘ 𝑋 ) ∈ ( ℤ ‘ 0 ) → ( 0 ..^ ( ( ♯ ‘ 𝑋 ) + 1 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∪ { ( ♯ ‘ 𝑋 ) } ) )
12 10 11 syl ( 𝑋 ∈ Word 𝐵 → ( 0 ..^ ( ( ♯ ‘ 𝑋 ) + 1 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∪ { ( ♯ ‘ 𝑋 ) } ) )
13 7 12 eqtrd ( 𝑋 ∈ Word 𝐵 → ( 0 ..^ ( ♯ ‘ ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ) = ( ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∪ { ( ♯ ‘ 𝑋 ) } ) )
14 13 adantr ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) → ( 0 ..^ ( ♯ ‘ ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ) = ( ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∪ { ( ♯ ‘ 𝑋 ) } ) )
15 14 3ad2ant1 ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → ( 0 ..^ ( ♯ ‘ ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ) = ( ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∪ { ( ♯ ‘ 𝑋 ) } ) )
16 15 raleqdv ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ) ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ↔ ∀ 𝑖 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∪ { ( ♯ ‘ 𝑋 ) } ) ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ) )
17 8 adantr ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
18 17 3ad2ant1 ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
19 fveq2 ( 𝑖 = ( ♯ ‘ 𝑋 ) → ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) = ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) )
20 19 fveq1d ( 𝑖 = ( ♯ ‘ 𝑋 ) → ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) )
21 fveq2 ( 𝑖 = ( ♯ ‘ 𝑋 ) → ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) = ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) )
22 21 fveq1d ( 𝑖 = ( ♯ ‘ 𝑋 ) → ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) )
23 20 22 eqeq12d ( 𝑖 = ( ♯ ‘ 𝑋 ) → ( ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ↔ ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) ) )
24 23 ralbidv ( 𝑖 = ( ♯ ‘ 𝑋 ) → ( ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ↔ ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) ) )
25 24 ralunsn ( ( ♯ ‘ 𝑋 ) ∈ ℕ0 → ( ∀ 𝑖 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∪ { ( ♯ ‘ 𝑋 ) } ) ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ∧ ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) ) ) )
26 18 25 syl ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → ( ∀ 𝑖 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∪ { ( ♯ ‘ 𝑋 ) } ) ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ∧ ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) ) ) )
27 simp1l ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → 𝑋 ∈ Word 𝐵 )
28 ccats1val1 ( ( 𝑋 ∈ Word 𝐵𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ) → ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) = ( 𝑋𝑖 ) )
29 27 28 sylan ( ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ) → ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) = ( 𝑋𝑖 ) )
30 29 fveq1d ( ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ) → ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑋𝑖 ) ‘ 𝑛 ) )
31 simp2l ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → 𝑌 ∈ Word 𝑃 )
32 oveq2 ( ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) → ( 0 ..^ ( ♯ ‘ 𝑋 ) ) = ( 0 ..^ ( ♯ ‘ 𝑌 ) ) )
33 32 eleq2d ( ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑌 ) ) ) )
34 33 biimpd ( ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑌 ) ) ) )
35 34 3ad2ant3 ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑌 ) ) ) )
36 35 imp ( ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑌 ) ) )
37 ccats1val1 ( ( 𝑌 ∈ Word 𝑃𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑌 ) ) ) → ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) = ( 𝑌𝑖 ) )
38 31 36 37 syl2an2r ( ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ) → ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) = ( 𝑌𝑖 ) )
39 38 fveq1d ( ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ) → ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) )
40 30 39 eqeq12d ( ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ) → ( ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ↔ ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) ) )
41 40 ralbidv ( ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ) → ( ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ↔ ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) ) )
42 41 ralbidva ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) ) )
43 eqidd ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) → ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑋 ) )
44 ccats1val2 ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑋 ) ) → ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) = 𝐶 )
45 44 fveq1d ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑋 ) ) → ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) = ( 𝐶𝑛 ) )
46 43 45 mpd3an3 ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) → ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) = ( 𝐶𝑛 ) )
47 46 3ad2ant1 ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) = ( 𝐶𝑛 ) )
48 ccats1val2 ( ( 𝑌 ∈ Word 𝑃𝑅𝑃 ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) = 𝑅 )
49 48 fveq1d ( ( 𝑌 ∈ Word 𝑃𝑅𝑃 ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) = ( 𝑅𝑛 ) )
50 49 3expa ( ( ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) = ( 𝑅𝑛 ) )
51 50 3adant1 ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) = ( 𝑅𝑛 ) )
52 47 51 eqeq12d ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → ( ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) ↔ ( 𝐶𝑛 ) = ( 𝑅𝑛 ) ) )
53 52 ralbidv ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → ( ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) ↔ ∀ 𝑛𝐼 ( 𝐶𝑛 ) = ( 𝑅𝑛 ) ) )
54 42 53 anbi12d ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ∧ ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ ( ♯ ‘ 𝑋 ) ) ‘ 𝑛 ) ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) ∧ ∀ 𝑛𝐼 ( 𝐶𝑛 ) = ( 𝑅𝑛 ) ) ) )
55 16 26 54 3bitrd ( ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ) ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) ∧ ∀ 𝑛𝐼 ( 𝐶𝑛 ) = ( 𝑅𝑛 ) ) ) )
56 55 ad2antlr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ) ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) ∧ ∀ 𝑛𝐼 ( 𝐶𝑛 ) = ( 𝑅𝑛 ) ) ) )
57 pm3.35 ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ) ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) )
58 fveq2 ( 𝑛 = 𝑗 → ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) )
59 fveq2 ( 𝑛 = 𝑗 → ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) )
60 58 59 eqeq12d ( 𝑛 = 𝑗 → ( ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ↔ ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) ) )
61 60 cbvralvw ( ∀ 𝑛𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ↔ ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) )
62 simp-4l ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) ) ∧ 𝑛𝐼 ) → 𝑁 ∈ Fin )
63 simp-4r ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) ) ∧ 𝑛𝐼 ) → 𝑀 ∈ Fin )
64 simpr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) ) ∧ 𝑛𝐼 ) → 𝑛𝐼 )
65 62 63 64 3jca ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) ) ∧ 𝑛𝐼 ) → ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝑛𝐼 ) )
66 65 adantr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) ) ∧ 𝑛𝐼 ) ∧ ( 𝐶𝑛 ) = ( 𝑅𝑛 ) ) → ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝑛𝐼 ) )
67 simp-4r ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) ) ∧ 𝑛𝐼 ) ∧ ( 𝐶𝑛 ) = ( 𝑅𝑛 ) ) → ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) )
68 simplr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) ) ∧ 𝑛𝐼 ) → ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) )
69 68 anim1i ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) ) ∧ 𝑛𝐼 ) ∧ ( 𝐶𝑛 ) = ( 𝑅𝑛 ) ) → ( ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) ∧ ( 𝐶𝑛 ) = ( 𝑅𝑛 ) ) )
70 1 2 3 4 5 gsmsymgreqlem1 ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝑛𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → ( ( ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) ∧ ( 𝐶𝑛 ) = ( 𝑅𝑛 ) ) → ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝑛 ) ) )
71 70 imp ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝑛𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) ∧ ( 𝐶𝑛 ) = ( 𝑅𝑛 ) ) ) → ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝑛 ) )
72 66 67 69 71 syl21anc ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) ) ∧ 𝑛𝐼 ) ∧ ( 𝐶𝑛 ) = ( 𝑅𝑛 ) ) → ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝑛 ) )
73 72 ex ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) ) ∧ 𝑛𝐼 ) → ( ( 𝐶𝑛 ) = ( 𝑅𝑛 ) → ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝑛 ) ) )
74 73 ralimdva ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) ) → ( ∀ 𝑛𝐼 ( 𝐶𝑛 ) = ( 𝑅𝑛 ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝑛 ) ) )
75 74 expcom ( ∀ 𝑗𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑗 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑗 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → ( ∀ 𝑛𝐼 ( 𝐶𝑛 ) = ( 𝑅𝑛 ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝑛 ) ) ) )
76 61 75 sylbi ( ∀ 𝑛𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → ( ∀ 𝑛𝐼 ( 𝐶𝑛 ) = ( 𝑅𝑛 ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝑛 ) ) ) )
77 76 com23 ( ∀ 𝑛𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) → ( ∀ 𝑛𝐼 ( 𝐶𝑛 ) = ( 𝑅𝑛 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝑛 ) ) ) )
78 57 77 syl ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ) ) → ( ∀ 𝑛𝐼 ( 𝐶𝑛 ) = ( 𝑅𝑛 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝑛 ) ) ) )
79 78 impancom ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) ∧ ∀ 𝑛𝐼 ( 𝐶𝑛 ) = ( 𝑅𝑛 ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝑛 ) ) ) )
80 79 com13 ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) ∧ ∀ 𝑛𝐼 ( 𝐶𝑛 ) = ( 𝑅𝑛 ) ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝑛 ) ) ) )
81 80 imp ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) ∧ ∀ 𝑛𝐼 ( 𝐶𝑛 ) = ( 𝑅𝑛 ) ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝑛 ) ) )
82 56 81 sylbid ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ) ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝑛 ) ) )
83 82 ex ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ) ∧ ( ( 𝑋 ∈ Word 𝐵𝐶𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃𝑅𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → ( ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ∀ 𝑛𝐼 ( ( 𝑋𝑖 ) ‘ 𝑛 ) = ( ( 𝑌𝑖 ) ‘ 𝑛 ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ) ∀ 𝑛𝐼 ( ( ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) = ( ( ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ‘ 𝑖 ) ‘ 𝑛 ) → ∀ 𝑛𝐼 ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝑛 ) = ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝑛 ) ) ) )