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

Metamath Proof Explorer

Theorem gsmsymgreqlem1

Description: Lemma 1 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 gsmsymgreqlem1 ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → ( ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ) → ( ( 𝑆 Σ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 simpr ⊢ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 )
7 simpr ⊢ ( ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) → 𝑅 ∈ 𝑃 )
8 6 7 anim12i ⊢ ( ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ) → ( 𝐶 ∈ 𝐵 ∧ 𝑅 ∈ 𝑃 ) )
9 8 3adant3 ⊢ ( ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) → ( 𝐶 ∈ 𝐵 ∧ 𝑅 ∈ 𝑃 ) )
10 9 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → ( 𝐶 ∈ 𝐵 ∧ 𝑅 ∈ 𝑃 ) )
11 10 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ) ) → ( 𝐶 ∈ 𝐵 ∧ 𝑅 ∈ 𝑃 ) )
12 simpll3 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ) ) → 𝐽 ∈ 𝐼 )
13 simpr ⊢ ( ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ) → ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) )
14 13 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ) ) → ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) )
15 simprl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ) ) → ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) )
16 12 14 15 3jca ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ) ) → ( 𝐽 ∈ 𝐼 ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ) )
17 1 2 3 4 5 fvcosymgeq ⊢ ( ( 𝐶 ∈ 𝐵 ∧ 𝑅 ∈ 𝑃 ) → ( ( 𝐽 ∈ 𝐼 ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ) → ( ( ( 𝑆 Σg 𝑋 ) ∘ 𝐶 ) ‘ 𝐽 ) = ( ( ( 𝑍 Σg 𝑌 ) ∘ 𝑅 ) ‘ 𝐽 ) ) )
18 11 16 17 sylc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ) ) → ( ( ( 𝑆 Σg 𝑋 ) ∘ 𝐶 ) ‘ 𝐽 ) = ( ( ( 𝑍 Σg 𝑌 ) ∘ 𝑅 ) ‘ 𝐽 ) )
19 simpl1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → 𝑁 ∈ Fin )
20 simpr1l ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → 𝑋 ∈ Word 𝐵 )
21 simpr1r ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → 𝐶 ∈ 𝐵 )
22 19 20 21 3jca ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) )
23 22 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) )
24 1 2 gsumccatsymgsn ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) = ( ( 𝑆 Σg 𝑋 ) ∘ 𝐶 ) )
25 23 24 syl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ) ) → ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) = ( ( 𝑆 Σg 𝑋 ) ∘ 𝐶 ) )
26 25 fveq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ) ) → ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝐽 ) = ( ( ( 𝑆 Σg 𝑋 ) ∘ 𝐶 ) ‘ 𝐽 ) )
27 simpl2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → 𝑀 ∈ Fin )
28 simpr2l ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → 𝑌 ∈ Word 𝑃 )
29 simpr2r ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → 𝑅 ∈ 𝑃 )
30 27 28 29 3jca ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → ( 𝑀 ∈ Fin ∧ 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) )
31 30 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ) ) → ( 𝑀 ∈ Fin ∧ 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) )
32 3 4 gsumccatsymgsn ⊢ ( ( 𝑀 ∈ Fin ∧ 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) → ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) = ( ( 𝑍 Σg 𝑌 ) ∘ 𝑅 ) )
33 31 32 syl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ) ) → ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) = ( ( 𝑍 Σg 𝑌 ) ∘ 𝑅 ) )
34 33 fveq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ) ) → ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝐽 ) = ( ( ( 𝑍 Σg 𝑌 ) ∘ 𝑅 ) ‘ 𝐽 ) )
35 18 26 34 3eqtr4d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) ∧ ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ) ) → ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝐽 ) = ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝐽 ) )
36 35 ex ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼 ) ∧ ( ( 𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ) ∧ ( ♯ ‘ 𝑋 ) = ( ♯ ‘ 𝑌 ) ) ) → ( ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑆 Σg 𝑋 ) ‘ 𝑛 ) = ( ( 𝑍 Σg 𝑌 ) ‘ 𝑛 ) ∧ ( 𝐶 ‘ 𝐽 ) = ( 𝑅 ‘ 𝐽 ) ) → ( ( 𝑆 Σg ( 𝑋 ++ ⟨“ 𝐶 ”⟩ ) ) ‘ 𝐽 ) = ( ( 𝑍 Σg ( 𝑌 ++ ⟨“ 𝑅 ”⟩ ) ) ‘ 𝐽 ) ) )