This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝑛 ) ) ) )